Reduction

[hcoop/domtool2.git] / src / reduce.sml

diff --git a/src/reduce.sml b/src/reduce.sml
new file mode 100644 (file)
index 0000000..17a8507
--- /dev/null
+++ b/src/reduce.sml
@@ -0,0 +1,132 @@
+(* HCoop Domtool (http://hcoop.sourceforge.net/)
+ * Copyright (c) 2006, Adam Chlipala
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+*)
+
+(* Evaluation of expressions until only externs are around *)
+
+structure Reduce :> REDUCE = struct
+
+open Ast Print Env
+
+fun freeIn x (b, _) =
+    case b of
+       EInt _ => false
+      | EString _ => false
+      | EList es => List.exists (freeIn x) es
+
+      | ELam (x', _, b') => x <> x' andalso freeIn x b'
+      | EVar x' => x = x'
+      | EApp (e1, e2) => freeIn x e1 orelse freeIn x e2
+
+      | ESkip => false
+      | ESet (_, e) => freeIn x e
+      | EGet (x', _, b') => x <> x' andalso freeIn x b'
+      | ESeq es => List.exists (freeIn x) es
+      | ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2
+      | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
+
+local
+    val freshCount = ref 0
+in
+fun freshVar () =
+    let
+       val v = !freshCount
+    in
+       freshCount := v + 1;
+       Int.toString v ^ "v"
+    end
+end
+
+fun subst x e (bAll as (b, loc)) =
+    case b of
+       EInt _ => bAll
+      | EString _ => bAll
+      | EList es => (EList (map (subst x e) es), loc)
+
+      | ELam (x', to, b') =>
+       if x = x' then
+           bAll
+       else if freeIn x' e then
+           let
+               val x'' = freshVar ()
+           in
+               (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc)
+           end
+       else
+           (ELam (x', to, subst x e b'), loc)
+      | EVar x' =>
+       if x = x' then
+           e
+       else
+           bAll
+      | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc)
+
+      | ESkip => bAll
+      | ESet (v, b) => (ESet (v, subst x e b), loc)
+      | EGet (x', v, b') =>
+       if x = x' then
+           bAll
+       else if freeIn x' e then
+           let
+               val x'' = freshVar ()
+           in
+               (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc)
+           end
+       else
+           (EGet (x', v, subst x e b'), loc)
+      | ESeq es => (ESeq (map (subst x e) es), loc)
+      | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
+      | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
+
+fun reduceExp G (eAll as (e, loc)) =
+    case e of
+       EInt _ => eAll
+      | EString _ => eAll
+      | EList es => (EList (map (reduceExp G) es), loc)
+
+      | ELam (x, to, e) =>
+       let
+           val to' = case to of
+                         NONE => (Tycheck.newUnif (), loc)
+                       | SOME to => to
+
+           val G' = bindVal G (x, to', NONE)
+       in
+           (ELam (x, to, reduceExp G' e), loc)
+       end
+      | EVar x =>
+       (case lookupEquation G x of
+            NONE => eAll
+          | SOME e => reduceExp G e)
+      | EApp (e1, e2) =>
+       let
+           val e1' = reduceExp G e1
+           val e2' = reduceExp G e2
+       in
+           case e1' of
+               (ELam (x, _, b), _) => reduceExp G (subst x e2' b)
+             | _ => (EApp (e1', e2'), loc)
+       end
+
+      | ESkip => eAll
+      | ESet (v, b) => (ESet (v, reduceExp G b), loc)
+      | EGet (x, v, b) => (EGet (x, v, reduceExp G b), loc)
+      | ESeq es => (ESeq (map (reduceExp G) es), loc)
+      | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
+      | EWith (e1, e2) => (EWith (reduceExp G e1, reduceExp G e2), loc)
+
+end