Fix indentation in GPL headers
[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
25fun freeIn x (b, _) =
26 case b of
27 EInt _ => false
28 | EString _ => false
29 | EList es => List.exists (freeIn x) es
30
31 | ELam (x', _, b') => x <> x' andalso freeIn x b'
32 | EVar x' => x = x'
33 | EApp (e1, e2) => freeIn x e1 orelse freeIn x e2
34
35 | ESkip => false
36 | ESet (_, e) => freeIn x e
37 | EGet (x', _, b') => x <> x' andalso freeIn x b'
38 | ESeq es => List.exists (freeIn x) es
39 | ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2
40 | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
41
42local
43 val freshCount = ref 0
44in
45fun freshVar () =
46 let
47 val v = !freshCount
48 in
49 freshCount := v + 1;
50 Int.toString v ^ "v"
51 end
52end
53
54fun subst x e (bAll as (b, loc)) =
55 case b of
56 EInt _ => bAll
57 | EString _ => bAll
58 | EList es => (EList (map (subst x e) es), loc)
59
60 | ELam (x', to, b') =>
61 if x = x' then
62 bAll
63 else if freeIn x' e then
64 let
65 val x'' = freshVar ()
66 in
67 (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc)
68 end
69 else
70 (ELam (x', to, subst x e b'), loc)
71 | EVar x' =>
72 if x = x' then
73 e
74 else
75 bAll
76 | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc)
77
78 | ESkip => bAll
79 | ESet (v, b) => (ESet (v, subst x e b), loc)
80 | EGet (x', v, b') =>
81 if x = x' then
82 bAll
83 else if freeIn x' e then
84 let
85 val x'' = freshVar ()
86 in
87 (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc)
88 end
89 else
90 (EGet (x', v, subst x e b'), loc)
91 | ESeq es => (ESeq (map (subst x e) es), loc)
92 | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
93 | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
94
95fun reduceExp G (eAll as (e, loc)) =
96 case e of
97 EInt _ => eAll
98 | EString _ => eAll
99 | EList es => (EList (map (reduceExp G) es), loc)
100
101 | ELam (x, to, e) =>
102 let
103 val to' = case to of
104 NONE => (Tycheck.newUnif (), loc)
105 | SOME to => to
106
107 val G' = bindVal G (x, to', NONE)
108 in
109 (ELam (x, to, reduceExp G' e), loc)
110 end
111 | EVar x =>
112 (case lookupEquation G x of
113 NONE => eAll
114 | SOME e => reduceExp G e)
115 | EApp (e1, e2) =>
116 let
117 val e1' = reduceExp G e1
118 val e2' = reduceExp G e2
119 in
120 case e1' of
121 (ELam (x, _, b), _) => reduceExp G (subst x e2' b)
122 | _ => (EApp (e1', e2'), loc)
123 end
124
125 | ESkip => eAll
126 | ESet (v, b) => (ESet (v, reduceExp G b), loc)
127 | EGet (x, v, b) => (EGet (x, v, reduceExp G b), loc)
128 | ESeq es => (ESeq (map (reduceExp G) es), loc)
129 | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
130 | EWith (e1, e2) => (EWith (reduceExp G e1, reduceExp G e2), loc)
131
132end