Mercurial > urweb

comparison src/explify.sml @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children dd82457fda82
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
79 fun explifyPat (p, loc) = 79 fun explifyPat (p, loc) =
80 case p of 80 case p of
81 L.PWild => (L'.PWild, loc) 81 L.PWild => (L'.PWild, loc)
82 | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc) 82 | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc)
83 | L.PPrim p => (L'.PPrim p, loc) 83 | L.PPrim p => (L'.PPrim p, loc)
84 | L.PCon (dk, pc, po) => (L'.PCon (dk, explifyPatCon pc, Option.map explifyPat po), loc) 84 | L.PCon (dk, pc, cs, po) => (L'.PCon (dk, explifyPatCon pc, map explifyCon cs, Option.map explifyPat po), loc)
85 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc) 85 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc)
86 86
87 fun explifyExp (e, loc) = 87 fun explifyExp (e, loc) =
88 case e of 88 case e of
89 L.EPrim p => (L'.EPrim p, loc) 89 L.EPrim p => (L'.EPrim p, loc)
111 111
112 fun explifySgi (sgi, loc) = 112 fun explifySgi (sgi, loc) =
113 case sgi of 113 case sgi of
114 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) 114 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
115 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) 115 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
116 | L.SgiDatatype (x, n, xncs) => SOME (L'.SgiDatatype (x, n, map (fn (x, n, co) => 116 | L.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs,
117 (x, n, Option.map explifyCon co)) xncs), loc) 117 map (fn (x, n, co) =>
118 | L.SgiDatatypeImp (x, n, m1, ms, s, xncs) => 118 (x, n, Option.map explifyCon co)) xncs), loc)
119 SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) => 119 | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
120 (x, n, Option.map explifyCon co)) xncs), loc) 120 SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
121 (x, n, Option.map explifyCon co)) xncs), loc)
121 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) 122 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
122 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) 123 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
123 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) 124 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
124 | L.SgiConstraint _ => NONE 125 | L.SgiConstraint _ => NONE
125 126
133 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) 134 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
134 135
135 fun explifyDecl (d, loc : EM.span) = 136 fun explifyDecl (d, loc : EM.span) =
136 case d of 137 case d of
137 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) 138 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
138 | L.DDatatype (x, n, xncs) => SOME (L'.DDatatype (x, n, map (fn (x, n, co) => 139 | L.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs,
139 (x, n, Option.map explifyCon co)) xncs), loc) 140 map (fn (x, n, co) =>
140 | L.DDatatypeImp (x, n, m1, ms, s, xncs) => 141 (x, n, Option.map explifyCon co)) xncs), loc)
141 SOME (L'.DDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) => 142 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
142 (x, n, Option.map explifyCon co)) xncs), loc) 143 SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
144 map (fn (x, n, co) =>
145 (x, n, Option.map explifyCon co)) xncs), loc)
143 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) 146 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
144 | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc) 147 | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc)
145 148
146 | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc) 149 | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc)
147 | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) 150 | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)