Mercurial > urweb

comparison src/unpoly.sml @ 399:2d64457eedb1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
listFun uses length
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 13:41:03 -0400
parents e457d8972ff1
children dc3fc3f3b834
comparison
equal deleted inserted replaced
398:ab3177746c78 399:2d64457eedb1
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 val isOpen = U.Con.exists {kind = fn _ => false,
50 con = fn c =>
51 case c of
52 CRel _ => true
53 | _ => false}
54
49 fun unpolyNamed (xn, rep) = 55 fun unpolyNamed (xn, rep) =
50 U.Exp.map {kind = fn k => k, 56 U.Exp.map {kind = fn k => k,
51 con = fn c => c, 57 con = fn c => c,
52 exp = fn e => 58 exp = fn e =>
53 case e of 59 case e of
54 ENamed xn' => 60 ECApp (e', _) =>
55 if xn' = xn then
56 rep
57 else
58 e
59 | ECApp (e', _) =>
60 let 61 let
61 fun isTheOne (e, _) = 62 fun isTheOne (e, _) =
62 case e of 63 case e of
63 ENamed xn' => xn' = xn 64 ENamed xn' => xn' = xn
64 | ECApp (e, _) => isTheOne e 65 | ECApp (e, _) => isTheOne e
65 | _ => false 66 | _ => false
66 in 67 in
67 if isTheOne e' then 68 if isTheOne e' then
68 #1 e' 69 rep
69 else 70 else
70 e 71 e
71 end 72 end
72 | _ => e} 73 | _ => e}
73 74
94 | _ => NONE 95 | _ => NONE
95 in 96 in
96 case unravel (e, []) of 97 case unravel (e, []) of
97 NONE => (e, st) 98 NONE => (e, st)
98 | SOME (n, cargs) => 99 | SOME (n, cargs) =>
99 case IM.find (#funcs st, n) of 100 if List.exists isOpen cargs then
100 NONE => (e, st) 101 (e, st)
101 | SOME (ks, vis) => 102 else
102 let 103 case IM.find (#funcs st, n) of
103 val (vis, nextName) = ListUtil.foldlMap 104 NONE => (e, st)
104 (fn ((x, n, t, e, s), nextName) => 105 | SOME (ks, vis) =>
105 ((x, nextName, n, t, e, s), nextName + 1)) 106 let
106 (#nextName st) vis 107 val (vis, nextName) = ListUtil.foldlMap
107 108 (fn ((x, n, t, e, s), nextName) =>
108 fun specialize (x, n, n_old, t, e, s) = 109 ((x, nextName, n, t, e, s), nextName + 1))
109 let 110 (#nextName st) vis
110 fun trim (t, e, cargs) = 111
111 case (t, e, cargs) of 112 fun specialize (x, n, n_old, t, e, s) =
112 ((TCFun (_, _, t), _), 113 let
113 (ECAbs (_, _, e), _), 114 fun trim (t, e, cargs) =
114 carg :: cargs) => 115 case (t, e, cargs) of
115 let 116 ((TCFun (_, _, t), _),
116 val t = subConInCon (length cargs, carg) t 117 (ECAbs (_, _, e), _),
117 val e = subConInExp (length cargs, carg) e 118 carg :: cargs) =>
118 in 119 let
119 trim (t, e, cargs) 120 val t = subConInCon (length cargs, carg) t
120 end 121 val e = subConInExp (length cargs, carg) e
121 | (_, _, []) => 122 in
122 let 123 trim (t, e, cargs)
123 val e = foldl (fn ((_, n, n_old, _, _, _), e) => 124 end
124 unpolyNamed (n_old, ENamed n) e) 125 | (_, _, []) =>
125 e vis 126 let
126 in 127 val e = foldl (fn ((_, n, n_old, _, _, _), e) =>
127 SOME (t, e) 128 unpolyNamed (n_old, ENamed n) e)
128 end 129 e vis
129 | _ => NONE 130 in
130 in 131 SOME (t, e)
131 (*Print.prefaces "specialize" 132 end
132 [("t", CorePrint.p_con CoreEnv.empty t), 133 | _ => NONE
133 ("e", CorePrint.p_exp CoreEnv.empty e), 134 in
134 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) 135 (*Print.prefaces "specialize"
135 Option.map (fn (t, e) => (x, n, n_old, t, e, s)) 136 [("t", CorePrint.p_con CoreEnv.empty t),
136 (trim (t, e, cargs)) 137 ("e", CorePrint.p_exp CoreEnv.empty e),
137 end 138 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
138 139 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
139 val vis = List.map specialize vis 140 (trim (t, e, cargs))
140 in 141 end
141 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then 142
142 (e, st) 143 val vis = List.map specialize vis
143 else 144 in
144 let 145 if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
145 val vis = List.mapPartial (fn x => x) vis 146 (e, st)
146 val vis = map (fn (x, n, n_old, t, e, s) => 147 else
147 (x ^ "_unpoly", n, n_old, t, e, s)) vis 148 let
148 val vis' = map (fn (x, n, _, t, e, s) => 149 val vis = List.mapPartial (fn x => x) vis
149 (x, n, t, e, s)) vis 150 val vis = map (fn (x, n, n_old, t, e, s) =>
150 151 (x ^ "_unpoly", n, n_old, t, e, s)) vis
151 val ks' = List.drop (ks, length cargs) 152 val vis' = map (fn (x, n, _, t, e, s) =>
152 in 153 (x, n, t, e, s)) vis
153 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of 154
154 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record" 155 val ks' = List.drop (ks, length cargs)
155 | SOME (_, n, _, _, _, _) => 156 in
156 (ENamed n, 157 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of
157 {funcs = foldl (fn (vi, funcs) => 158 NONE => raise Fail "Unpoly: Inconsistent 'val rec' record"
158 IM.insert (funcs, #2 vi, (ks', vis'))) 159 | SOME (_, n, _, _, _, _) =>
159 (#funcs st) vis', 160 (ENamed n,
160 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st, 161 {funcs = foldl (fn (vi, funcs) =>
161 nextName = nextName}) 162 IM.insert (funcs, #2 vi, (ks', vis')))
162 end 163 (#funcs st) vis',
163 end 164 decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
165 nextName = nextName})
166 end
167 end
164 end 168 end
165 | _ => (e, st) 169 | _ => (e, st)
166 170
167 fun decl (d, st : state) = 171 fun decl (d, st : state) =
168 case d of 172 case d of