comparison src/explify.sml @ 156:34ccd7d2bea8

Start of datatype support
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:02:03 -0400
parents 7420fa18d657
children 06a98129b23f
comparison
equal deleted inserted replaced
155:4334bb734187 156:34ccd7d2bea8
93 93
94 fun explifySgi (sgi, loc) = 94 fun explifySgi (sgi, loc) =
95 case sgi of 95 case sgi of
96 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) 96 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
97 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) 97 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
98 | L.SgiDatatype _ => raise Fail "Explify SgiDatatype"
99 | L.SgiDatatypeImp _ => raise Fail "Explify SgiDatatypeImp"
98 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) 100 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
99 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) 101 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
100 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) 102 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
101 | L.SgiConstraint _ => NONE 103 | L.SgiConstraint _ => NONE
102 104
110 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) 112 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
111 113
112 fun explifyDecl (d, loc : EM.span) = 114 fun explifyDecl (d, loc : EM.span) =
113 case d of 115 case d of
114 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) 116 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
117 | L.DDatatype _ => raise Fail "Explify DDatatype"
118 | L.DDatatypeImp _ => raise Fail "Explify DDatatypeImp"
115 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) 119 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
116 | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc) 120 | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc)
117 121
118 | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc) 122 | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc)
119 | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) 123 | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)