Mercurial > urweb
comparison src/unpoly.sml @ 316:04ebfe929a98
Unpolyed a polymorphic function of two arguments
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 11 Sep 2008 10:14:59 -0400 |
parents | e21d0dddda09 |
children | e457d8972ff1 |
comparison
equal
deleted
inserted
replaced
315:e21d0dddda09 | 316:04ebfe929a98 |
---|---|
44 val subConInCon = E.subConInCon | 44 val subConInCon = E.subConInCon |
45 | 45 |
46 val liftConInExp = E.liftConInExp | 46 val liftConInExp = E.liftConInExp |
47 val subConInExp = E.subConInExp | 47 val subConInExp = E.subConInExp |
48 | 48 |
49 fun unpolyNamed (xn, rep) = | |
50 U.Exp.map {kind = fn k => k, | |
51 con = fn c => c, | |
52 exp = fn e => | |
53 case e of | |
54 ENamed xn' => | |
55 if xn' = xn then | |
56 rep | |
57 else | |
58 e | |
59 | ECApp (e, _) => #1 e | |
60 | _ => e} | |
61 | |
49 type state = { | 62 type state = { |
50 funcs : (kind list * (string * int * con * exp * string) list) IM.map, | 63 funcs : (kind list * (string * int * con * exp * string) list) IM.map, |
51 decls : decl list, | 64 decls : decl list, |
52 nextName : int | 65 nextName : int |
53 } | 66 } |
91 val t = subConInCon (length cargs, carg) t | 104 val t = subConInCon (length cargs, carg) t |
92 val e = subConInExp (length cargs, carg) e | 105 val e = subConInExp (length cargs, carg) e |
93 in | 106 in |
94 trim (t, e, cargs) | 107 trim (t, e, cargs) |
95 end | 108 end |
96 | (_, _, []) => SOME (t, e) | 109 | (_, _, []) => |
110 let | |
111 val e = foldl (fn ((_, n, n_old, _, _, _), e) => | |
112 unpolyNamed (n_old, ENamed n) e) | |
113 e vis | |
114 in | |
115 SOME (t, e) | |
116 end | |
97 | _ => NONE | 117 | _ => NONE |
98 in | 118 in |
99 (*Print.prefaces "specialize" | 119 (*Print.prefaces "specialize" |
100 [("t", CorePrint.p_con CoreEnv.empty t), | 120 [("t", CorePrint.p_con CoreEnv.empty t), |
101 ("e", CorePrint.p_exp CoreEnv.empty e), | 121 ("e", CorePrint.p_exp CoreEnv.empty e), |
104 (trim (t, e, cargs)) | 124 (trim (t, e, cargs)) |
105 end | 125 end |
106 | 126 |
107 val vis = List.map specialize vis | 127 val vis = List.map specialize vis |
108 in | 128 in |
109 if List.exists (not o Option.isSome) vis then | 129 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then |
110 (e, st) | 130 (e, st) |
111 else | 131 else |
112 let | 132 let |
113 val vis = List.mapPartial (fn x => x) vis | 133 val vis = List.mapPartial (fn x => x) vis |
134 val vis = map (fn (x, n, n_old, t, e, s) => | |
135 (x ^ "_unpoly", n, n_old, t, e, s)) vis | |
114 val vis' = map (fn (x, n, _, t, e, s) => | 136 val vis' = map (fn (x, n, _, t, e, s) => |
115 (x ^ "_unpoly", n, t, e, s)) vis | 137 (x, n, t, e, s)) vis |
138 | |
139 val ks' = List.drop (ks, length cargs) | |
116 in | 140 in |
117 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of | 141 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of |
118 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" | 142 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" |
119 | SOME (_, n, _, _, _, _) => | 143 | SOME (_, n, _, _, _, _) => |
120 (ENamed n, | 144 (ENamed n, |
121 {funcs = #funcs st, | 145 {funcs = foldl (fn (vi, funcs) => |
146 IM.insert (funcs, #2 vi, (ks', vis'))) | |
147 (#funcs st) vis', | |
122 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, | 148 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, |
123 nextName = nextName}) | 149 nextName = nextName}) |
124 end | 150 end |
125 end | 151 end |
126 end | 152 end |