Mercurial > urweb

comparison src/specialize.sml @ 1276:5b5c0b552f59

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Another run of Specialize, using ReduceLocal on datatype parameters
author Adam Chlipala <adamc@hcoop.net>
date Sat, 05 Jun 2010 09:42:37 -0400
parents 20a364c4a6dc
children
comparison
equal deleted inserted replaced
1275:74150edf1134 1276:5b5c0b552f59
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
71 case c of 71 case c of
72 CRel _ => true 72 CRel _ => true
73 | _ => false} 73 | _ => false}
74 74
75 fun considerSpecialization (st : state, n, args, dt : datatyp) = 75 fun considerSpecialization (st : state, n, args, dt : datatyp) =
76 case CM.find (#specializations dt, args) of 76 let
77 SOME dt' => (#name dt', #constructors dt', st) 77 val args = map ReduceLocal.reduceCon args
78 | NONE => 78 in
79 let 79 case CM.find (#specializations dt, args) of
80 (*val () = Print.prefaces "Args" [("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*) 80 SOME dt' => (#name dt', #constructors dt', st)
81 81 | NONE =>
82 val n' = #count st 82 let
83 83 (*val () = Print.prefaces "Args" [("n", Print.PD.string (Int.toString n)),
84 val nxs = length args - 1 84 ("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*)
85 fun sub t = ListUtil.foldli (fn (i, arg, t) => 85
86 subConInCon (nxs - i, arg) t) t args 86 val n' = #count st
87 87
88 val (cons, (count, cmap)) = 88 val nxs = length args - 1
89 ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) => 89 fun sub t = ListUtil.foldli (fn (i, arg, t) =>
90 let 90 subConInCon (nxs - i, arg) t) t args
91 val to = Option.map sub to 91
92 in 92 val (cons, (count, cmap)) =
93 ((x, count, to), 93 ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) =>
94 (count + 1, 94 let
95 IM.insert (cmap, n, count))) 95 val to = Option.map sub to
96 end) (n' + 1, IM.empty) (#constructors dt) 96 in
97 97 ((x, count, to),
98 val st = {count = count, 98 (count + 1,
99 datatypes = IM.insert (#datatypes st, n, 99 IM.insert (cmap, n, count)))
100 {name = #name dt, 100 end) (n' + 1, IM.empty) (#constructors dt)
101 params = #params dt, 101
102 constructors = #constructors dt, 102 val st = {count = count,
103 specializations = CM.insert (#specializations dt, 103 datatypes = IM.insert (#datatypes st, n,
104 args, 104 {name = #name dt,
105 {name = n', 105 params = #params dt,
106 constructors = cmap})}), 106 constructors = #constructors dt,
107 constructors = #constructors st, 107 specializations = CM.insert (#specializations dt,
108 decls = #decls st} 108 args,
109 109 {name = n',
110 val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st) 110 constructors = cmap})}),
111 | ((x, n, SOME t), st) => 111 constructors = #constructors st,
112 let 112 decls = #decls st}
113 val (t, st) = specCon st t 113
114 in 114 val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st)
115 ((x, n, SOME t), st) 115 | ((x, n, SOME t), st) =>
116 end) st cons 116 let
117 117 val (t, st) = specCon st t
118 val dt = (#name dt ^ "_s", 118 in
119 n', 119 ((x, n, SOME t), st)
120 [], 120 end) st cons
121 cons) 121
122 in 122 val dt = (#name dt ^ "_s",
123 (n', cmap, {count = #count st, 123 n',
124 datatypes = #datatypes st, 124 [],
125 constructors = #constructors st, 125 cons)
126 decls = dt :: #decls st}) 126 in
127 end 127 (n', cmap, {count = #count st,
128 datatypes = #datatypes st,
129 constructors = #constructors st,
130 decls = dt :: #decls st})
131 end
132 end
128 133
129 and con (c, st : state) = 134 and con (c, st : state) =
130 let 135 let
131 fun findApp (c, args) = 136 fun findApp (c, args) =
132 case c of 137 case c of