comparison src/explify.sml @ 563:44958d74c43f

Initial conversion to arbitrary-kind classes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 19 Dec 2008 10:03:31 -0500
parents ae03d09043c1
children 8998114760c1
comparison
equal deleted inserted replaced
562:6daa59a55c43 563:44958d74c43f
137 (x, n, Option.map explifyCon co)) xncs), loc) 137 (x, n, Option.map explifyCon co)) xncs), loc)
138 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) 138 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
139 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) 139 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
140 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) 140 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
141 | L.SgiConstraint _ => NONE 141 | L.SgiConstraint _ => NONE
142 | L.SgiClassAbs (x, n) => SOME (L'.SgiConAbs (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)), loc) 142 | L.SgiClassAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc)), loc)
143 | L.SgiClass (x, n, c) => SOME (L'.SgiCon (x, n, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), 143 | L.SgiClass (x, n, k, c) => SOME (L'.SgiCon (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc),
144 explifyCon c), loc) 144 explifyCon c), loc)
145 145
146 and explifySgn (sgn, loc) = 146 and explifySgn (sgn, loc) =
147 case sgn of 147 case sgn of
148 L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc) 148 L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
149 | L.SgnVar n => (L'.SgnVar n, loc) 149 | L.SgnVar n => (L'.SgnVar n, loc)
170 | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc) 170 | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
171 | L.DConstraint (c1, c2) => NONE 171 | L.DConstraint (c1, c2) => NONE
172 | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc) 172 | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc)
173 | L.DTable (nt, x, n, c) => SOME (L'.DTable (nt, x, n, explifyCon c), loc) 173 | L.DTable (nt, x, n, c) => SOME (L'.DTable (nt, x, n, explifyCon c), loc)
174 | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc) 174 | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc)
175 | L.DClass (x, n, c) => SOME (L'.DCon (x, n, 175 | L.DClass (x, n, k, c) => SOME (L'.DCon (x, n,
176 (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), explifyCon c), loc) 176 (L'.KArrow (explifyKind k, (L'.KType, loc)), loc), explifyCon c), loc)
177 | L.DDatabase s => SOME (L'.DDatabase s, loc) 177 | L.DDatabase s => SOME (L'.DDatabase s, loc)
178 | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc) 178 | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc)
179 179
180 and explifyStr (str, loc) = 180 and explifyStr (str, loc) =
181 case str of 181 case str of