| 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 | fun 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 | |
| 42 | local |
| 43 | val freshCount = ref 0 |
| 44 | in |
| 45 | fun freshVar () = |
| 46 | let |
| 47 | val v = !freshCount |
| 48 | in |
| 49 | freshCount := v + 1; |
| 50 | Int.toString v ^ "v" |
| 51 | end |
| 52 | end |
| 53 | |
| 54 | fun 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 | |
| 95 | fun 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 | |
| 132 | end |