Catch-all aliases working again
[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
AC
44
45local
46 val freshCount = ref 0
47in
48fun freshVar () =
49 let
50 val v = !freshCount
51 in
52 freshCount := v + 1;
53 Int.toString v ^ "v"
54 end
55end
56
57fun subst x e (bAll as (b, loc)) =
58 case b of
59 EInt _ => bAll
60 | EString _ => bAll
61 | EList es => (EList (map (subst x e) es), loc)
62
63 | ELam (x', to, b') =>
64 if x = x' then
65 bAll
66 else if freeIn x' e then
67 let
68 val x'' = freshVar ()
69 in
70 (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc)
71 end
72 else
73 (ELam (x', to, subst x e b'), loc)
74 | EVar x' =>
75 if x = x' then
76 e
77 else
78 bAll
79 | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc)
80
81 | ESkip => bAll
82 | ESet (v, b) => (ESet (v, subst x e b), loc)
8cbb9632 83 | EGet (x', topt, v, b') =>
492c1cff
AC
84 if x = x' then
85 bAll
86 else if freeIn x' e then
87 let
88 val x'' = freshVar ()
89 in
8cbb9632 90 (EGet (x'', topt, v, subst x e (subst x' (EVar x'', loc) b')), loc)
492c1cff
AC
91 end
92 else
8cbb9632 93 (EGet (x', topt, v, subst x e b'), loc)
492c1cff
AC
94 | ESeq es => (ESeq (map (subst x e) es), loc)
95 | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
96 | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
6bb366c5
AC
97 | EALam (x', p, b') =>
98 if x = x' then
99 bAll
100 else if freeIn x' e then
101 let
102 val x'' = freshVar ()
103 in
104 (EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc)
105 end
106 else
107 (EALam (x', p, subst x e b'), loc)
492c1cff 108
cf879b4f
AC
109fun findPrim (e, _) =
110 case e of
111 EApp (f, x) =>
112 (case findPrim f of
113 NONE => NONE
114 | SOME (f, xs) => SOME (f, xs @ [x]))
115 | EVar x => SOME (x, [])
116 | _ => NONE
117
492c1cff
AC
118fun reduceExp G (eAll as (e, loc)) =
119 case e of
120 EInt _ => eAll
121 | EString _ => eAll
122 | EList es => (EList (map (reduceExp G) es), loc)
123
124 | ELam (x, to, e) =>
125 let
126 val to' = case to of
127 NONE => (Tycheck.newUnif (), loc)
128 | SOME to => to
129
130 val G' = bindVal G (x, to', NONE)
131 in
132 (ELam (x, to, reduceExp G' e), loc)
133 end
134 | EVar x =>
135 (case lookupEquation G x of
e9f528ab
AC
136 NONE =>
137 (case function x of
138 NONE => eAll
139 | SOME f => case f [] of
140 NONE => eAll
141 | SOME e' => reduceExp G e')
492c1cff
AC
142 | SOME e => reduceExp G e)
143 | EApp (e1, e2) =>
144 let
145 val e1' = reduceExp G e1
146 val e2' = reduceExp G e2
147 in
148 case e1' of
149 (ELam (x, _, b), _) => reduceExp G (subst x e2' b)
cf879b4f
AC
150 | _ =>
151 case findPrim eAll of
152 NONE => (EApp (e1', e2'), loc)
153 | SOME (f, args) =>
154 case function f of
155 NONE => (EApp (e1', e2'), loc)
156 | SOME f => case f (map (reduceExp G) args) of
157 NONE => (EApp (e1', e2'), loc)
158 | SOME e' => reduceExp G e'
492c1cff
AC
159 end
160
161 | ESkip => eAll
162 | ESet (v, b) => (ESet (v, reduceExp G b), loc)
8cbb9632 163 | EGet (x, topt, v, b) => (EGet (x, topt, v, reduceExp G b), loc)
492c1cff
AC
164 | ESeq es => (ESeq (map (reduceExp G) es), loc)
165 | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
6bb366c5
AC
166 | EWith (e1, e2) =>
167 let
168 val e1' = reduceExp G e1
169 val e2' = reduceExp G e2
170 in
171 case e1' of
172 (EALam (x, _, b), _) => reduceExp G (subst x e2' b)
173 | _ => (EWith (e1', e2'), loc)
174 end
175 | EALam (x, p, e) =>
176 let
177 val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
178 in
179 (EALam (x, p, reduceExp G' e), loc)
180 end
492c1cff
AC
181
182end