Mercurial > urweb

comparison src/explify.sml @ 88:7bab29834cd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Constraints in modules
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 15:58:02 -0400
parents 275aaeb73f1f
children f0f59e918cac
comparison
equal deleted inserted replaced
87:275aaeb73f1f 88:7bab29834cd6
89 89
90 | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc) 90 | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)
91 91
92 fun explifySgi (sgi, loc) = 92 fun explifySgi (sgi, loc) =
93 case sgi of 93 case sgi of
94 L.SgiConAbs (x, n, k) => (L'.SgiConAbs (x, n, explifyKind k), loc) 94 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
95 | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) 95 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
96 | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc) 96 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
97 | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc) 97 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
98 | L.SgiSgn (x, n, sgn) => (L'.SgiSgn (x, n, explifySgn sgn), loc) 98 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
99 | L.SgiConstraint _ => NONE
99 100
100 and explifySgn (sgn, loc) = 101 and explifySgn (sgn, loc) =
101 case sgn of 102 case sgn of
102 L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc) 103 L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
103 | L.SgnVar n => (L'.SgnVar n, loc) 104 | L.SgnVar n => (L'.SgnVar n, loc)
104 | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc) 105 | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
105 | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc) 106 | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc)
106 | L.SgnProj x => (L'.SgnProj x, loc) 107 | L.SgnProj x => (L'.SgnProj x, loc)
107 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) 108 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
108 109
109 fun explifyDecl (d, loc : EM.span) = 110 fun explifyDecl (d, loc : EM.span) =
110 case d of 111 case d of
111 L.DCon (x, n, k, c) => (L'.DCon (x, n, explifyKind k, explifyCon c), loc) 112 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
112 | L.DVal (x, n, t, e) => (L'.DVal (x, n, explifyCon t, explifyExp e), loc) 113 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
113 114
114 | L.DSgn (x, n, sgn) => (L'.DSgn (x, n, explifySgn sgn), loc) 115 | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc)
115 | L.DStr (x, n, sgn, str) => (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) 116 | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
116 | L.DFfiStr (x, n, sgn) => (L'.DFfiStr (x, n, explifySgn sgn), loc) 117 | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
118 | L.DConstraint (c1, c2) => NONE
117 119
118 and explifyStr (str, loc) = 120 and explifyStr (str, loc) =
119 case str of 121 case str of
120 L.StrConst ds => (L'.StrConst (map explifyDecl ds), loc) 122 L.StrConst ds => (L'.StrConst (List.mapPartial explifyDecl ds), loc)
121 | L.StrVar n => (L'.StrVar n, loc) 123 | L.StrVar n => (L'.StrVar n, loc)
122 | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc) 124 | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc)
123 | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc) 125 | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc)
124 | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc) 126 | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc)
125 | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc) 127 | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
126 128
127 val explify = map explifyDecl 129 val explify = List.mapPartial explifyDecl
128 130
129 end 131 end