| 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. |
| 17 | *) |
| 18 | |
| 19 | (* Evaluation of expressions until only externs are around *) |
| 20 | |
| 21 | structure Reduce :> REDUCE = struct |
| 22 | |
| 23 | open Ast Print Env |
| 24 | |
| 25 | structure SM = StringMap |
| 26 | |
| 27 | fun 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 |
| 39 | | EGet (x', _, b') => x <> x' andalso freeIn x b' |
| 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 |
| 43 | | EALam (x', _, b') => x <> x' andalso freeIn x b' |
| 44 | |
| 45 | local |
| 46 | val freshCount = ref 0 |
| 47 | in |
| 48 | fun freshVar () = |
| 49 | let |
| 50 | val v = !freshCount |
| 51 | in |
| 52 | freshCount := v + 1; |
| 53 | Int.toString v ^ "v" |
| 54 | end |
| 55 | end |
| 56 | |
| 57 | fun 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) |
| 83 | | EGet (x', v, b') => |
| 84 | if x = x' then |
| 85 | bAll |
| 86 | else if freeIn x' e then |
| 87 | let |
| 88 | val x'' = freshVar () |
| 89 | in |
| 90 | (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc) |
| 91 | end |
| 92 | else |
| 93 | (EGet (x', v, subst x e b'), loc) |
| 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) |
| 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) |
| 108 | |
| 109 | fun 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 | |
| 118 | fun 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 |
| 136 | NONE => eAll |
| 137 | | SOME e => reduceExp G e) |
| 138 | | EApp (e1, e2) => |
| 139 | let |
| 140 | val e1' = reduceExp G e1 |
| 141 | val e2' = reduceExp G e2 |
| 142 | in |
| 143 | case e1' of |
| 144 | (ELam (x, _, b), _) => reduceExp G (subst x e2' b) |
| 145 | | _ => |
| 146 | case findPrim eAll of |
| 147 | NONE => (EApp (e1', e2'), loc) |
| 148 | | SOME (f, args) => |
| 149 | case function f of |
| 150 | NONE => (EApp (e1', e2'), loc) |
| 151 | | SOME f => case f (map (reduceExp G) args) of |
| 152 | NONE => (EApp (e1', e2'), loc) |
| 153 | | SOME e' => reduceExp G e' |
| 154 | end |
| 155 | |
| 156 | | ESkip => eAll |
| 157 | | ESet (v, b) => (ESet (v, reduceExp G b), loc) |
| 158 | | EGet (x, v, b) => (EGet (x, v, reduceExp G b), loc) |
| 159 | | ESeq es => (ESeq (map (reduceExp G) es), loc) |
| 160 | | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc) |
| 161 | | EWith (e1, e2) => |
| 162 | let |
| 163 | val e1' = reduceExp G e1 |
| 164 | val e2' = reduceExp G e2 |
| 165 | in |
| 166 | case e1' of |
| 167 | (EALam (x, _, b), _) => reduceExp G (subst x e2' b) |
| 168 | | _ => (EWith (e1', e2'), loc) |
| 169 | end |
| 170 | | EALam (x, p, e) => |
| 171 | let |
| 172 | val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE) |
| 173 | in |
| 174 | (EALam (x, p, reduceExp G' e), loc) |
| 175 | end |
| 176 | |
| 177 | end |