Evaluate `val' and `var' bindings in the environment in which they were defined
[hcoop/domtool2.git] / src / reduce.sml
CommitLineData
492c1cff
AC
1(* HCoop Domtool (http://hcoop.sourceforge.net/)
2 * Copyright (c) 2006, Adam Chlipala
3 *
4 * This program is free software; you can redistribute it and/or
5 * modify it under the terms of the GNU General Public License
6 * as published by the Free Software Foundation; either version 2
7 * of the License, or (at your option) any later version.
8 *
9 * This program is distributed in the hope that it will be useful,
10 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 * GNU General Public License for more details.
13 *
14 * You should have received a copy of the GNU General Public License
15 * along with this program; if not, write to the Free Software
16 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.
dac62e84 17 *)
492c1cff
AC
18
19(* Evaluation of expressions until only externs are around *)
20
21structure Reduce :> REDUCE = struct
22
23open Ast Print Env
24
6bb366c5
AC
25structure SM = StringMap
26
492c1cff
AC
27fun freeIn x (b, _) =
28 case b of
29 EInt _ => false
30 | EString _ => false
31 | EList es => List.exists (freeIn x) es
32
33 | ELam (x', _, b') => x <> x' andalso freeIn x b'
34 | EVar x' => x = x'
35 | EApp (e1, e2) => freeIn x e1 orelse freeIn x e2
36
37 | ESkip => false
38 | ESet (_, e) => freeIn x e
8cbb9632 39 | EGet (x', _, _, b') => x <> x' andalso freeIn x b'
492c1cff
AC
40 | ESeq es => List.exists (freeIn x) es
41 | ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2
42 | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
6bb366c5 43 | EALam (x', _, b') => x <> x' andalso freeIn x b'
492c1cff 44
75d4c2d6
AC
45 | EIf (e1, e2, e3) => freeIn x e1 orelse freeIn x e2 orelse freeIn x e3
46
492c1cff
AC
47local
48 val freshCount = ref 0
49in
50fun freshVar () =
51 let
52 val v = !freshCount
53 in
54 freshCount := v + 1;
55 Int.toString v ^ "v"
56 end
57end
58
59fun subst x e (bAll as (b, loc)) =
60 case b of
61 EInt _ => bAll
62 | EString _ => bAll
63 | EList es => (EList (map (subst x e) es), loc)
64
65 | ELam (x', to, b') =>
66 if x = x' then
67 bAll
68 else if freeIn x' e then
69 let
70 val x'' = freshVar ()
71 in
72 (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc)
73 end
74 else
75 (ELam (x', to, subst x e b'), loc)
76 | EVar x' =>
77 if x = x' then
78 e
79 else
80 bAll
81 | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc)
82
83 | ESkip => bAll
84 | ESet (v, b) => (ESet (v, subst x e b), loc)
8cbb9632 85 | EGet (x', topt, v, b') =>
492c1cff
AC
86 if x = x' then
87 bAll
88 else if freeIn x' e then
89 let
90 val x'' = freshVar ()
91 in
8cbb9632 92 (EGet (x'', topt, v, subst x e (subst x' (EVar x'', loc) b')), loc)
492c1cff
AC
93 end
94 else
8cbb9632 95 (EGet (x', topt, v, subst x e b'), loc)
492c1cff
AC
96 | ESeq es => (ESeq (map (subst x e) es), loc)
97 | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
98 | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
6bb366c5
AC
99 | EALam (x', p, b') =>
100 if x = x' then
101 bAll
102 else if freeIn x' e then
103 let
104 val x'' = freshVar ()
105 in
106 (EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc)
107 end
108 else
109 (EALam (x', p, subst x e b'), loc)
492c1cff 110
75d4c2d6
AC
111 | EIf (b1, b2, b3) => (EIf (subst x e b1, subst x e b2, subst x e b3), loc)
112
cf879b4f
AC
113fun findPrim (e, _) =
114 case e of
115 EApp (f, x) =>
116 (case findPrim f of
117 NONE => NONE
118 | SOME (f, xs) => SOME (f, xs @ [x]))
119 | EVar x => SOME (x, [])
120 | _ => NONE
121
492c1cff
AC
122fun reduceExp G (eAll as (e, loc)) =
123 case e of
124 EInt _ => eAll
125 | EString _ => eAll
126 | EList es => (EList (map (reduceExp G) es), loc)
127
128 | ELam (x, to, e) =>
129 let
130 val to' = case to of
131 NONE => (Tycheck.newUnif (), loc)
132 | SOME to => to
133
134 val G' = bindVal G (x, to', NONE)
135 in
136 (ELam (x, to, reduceExp G' e), loc)
137 end
138 | EVar x =>
139 (case lookupEquation G x of
e9f528ab
AC
140 NONE =>
141 (case function x of
142 NONE => eAll
143 | SOME f => case f [] of
144 NONE => eAll
145 | SOME e' => reduceExp G e')
8061fadf 146 | SOME (e, G') => reduceExp G' e)
492c1cff
AC
147 | EApp (e1, e2) =>
148 let
149 val e1' = reduceExp G e1
150 val e2' = reduceExp G e2
151 in
152 case e1' of
153 (ELam (x, _, b), _) => reduceExp G (subst x e2' b)
cf879b4f
AC
154 | _ =>
155 case findPrim eAll of
156 NONE => (EApp (e1', e2'), loc)
157 | SOME (f, args) =>
158 case function f of
159 NONE => (EApp (e1', e2'), loc)
160 | SOME f => case f (map (reduceExp G) args) of
161 NONE => (EApp (e1', e2'), loc)
162 | SOME e' => reduceExp G e'
492c1cff
AC
163 end
164
165 | ESkip => eAll
166 | ESet (v, b) => (ESet (v, reduceExp G b), loc)
8cbb9632 167 | EGet (x, topt, v, b) => (EGet (x, topt, v, reduceExp G b), loc)
492c1cff
AC
168 | ESeq es => (ESeq (map (reduceExp G) es), loc)
169 | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
6bb366c5
AC
170 | EWith (e1, e2) =>
171 let
172 val e1' = reduceExp G e1
173 val e2' = reduceExp G e2
174 in
175 case e1' of
176 (EALam (x, _, b), _) => reduceExp G (subst x e2' b)
177 | _ => (EWith (e1', e2'), loc)
178 end
179 | EALam (x, p, e) =>
180 let
181 val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
182 in
183 (EALam (x, p, reduceExp G' e), loc)
184 end
492c1cff 185
75d4c2d6
AC
186 | EIf (e1, e2, e3) =>
187 let
188 val e1' = reduceExp G e1
189 fun e2' () = reduceExp G e2
190 fun e3' () = reduceExp G e3
191 in
192 case e1' of
193 (EVar "true", _) => e2' ()
194 | (EVar "false", _) => e3' ()
195 | _ => (EIf (e1', e2' (), e3' ()), loc)
196 end
197
492c1cff 198end