Reduction

diff --git a/src/ast.sml b/src/ast.sml
index 0c6ddd1..bd87121 100644 (file)
--- a/src/ast.sml
+++ b/src/ast.sml
@@ -94,6 +94,7 @@ withtype exp = exp' * position
 datatype decl' =
         DExternType of string
        | DExternVal of string * typ
 datatype decl' =
         DExternType of string
        | DExternVal of string * typ

+       | DVal of string * typ option * exp

 type decl = decl' * string option * position
 
 type file = decl list * exp option
 type decl = decl' * string option * position
 
 type file = decl list * exp option

diff --git a/src/domtool.cm b/src/domtool.cm
index 790625c..fb9f9e1 100644 (file)
--- a/src/domtool.cm
+++ b/src/domtool.cm
@@ -21,8 +21,14 @@ parse.sml
 print.sig
 print.sml
 
 print.sig
 print.sml
 

+env.sig
+env.sml
+

 tycheck.sig
 tycheck.sml
 
 tycheck.sig
 tycheck.sml
 

+reduce.sig
+reduce.sml
+

 main.sig
 main.sml
 main.sig
 main.sml

diff --git a/src/env.sig b/src/env.sig
new file mode 100644 (file)
index 0000000..cc68b53
--- /dev/null
+++ b/src/env.sig
@@ -0,0 +1,33 @@
+(* 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.
+*)
+
+(* Domtool type-checking and reduction environments *)
+
+signature ENV = sig
+
+    type env
+    val empty : env
+
+    val bindType : env -> string -> env
+    val bindVal : env -> string * Ast.typ * Ast.exp option -> env
+
+    val lookupType : env -> string -> bool
+    val lookupVal : env -> string -> Ast.typ option
+    val lookupEquation : env -> string -> Ast.exp option
+
+end

diff --git a/src/env.sml b/src/env.sml
new file mode 100644 (file)
index 0000000..b52ead1
--- /dev/null
+++ b/src/env.sml
@@ -0,0 +1,45 @@
+(* 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.
+*)
+
+(* Domtool type-checking and reduction environments *)
+
+structure Env :> ENV = struct
+
+open Ast
+
+structure SS = StringSet
+structure SM = StringMap
+
+type env = SS.set * (typ * exp option) SM.map
+val empty : env = (SS.add (SS.singleton "int", "string"),
+                  SM.empty)
+
+fun lookupType (ts, _) name = SS.member (ts, name)
+fun lookupVal (_, vs) name =
+    case SM.find (vs, name) of
+       NONE => NONE
+      | SOME (t, _) => SOME t
+fun lookupEquation (_, vs) name =
+    case SM.find (vs, name) of
+       NONE => NONE
+      | SOME (_, eqo) => eqo
+
+fun bindType (ts, vs) name = (SS.add (ts, name), vs)
+fun bindVal (ts, vs) (name, t, eqo) = (ts, SM.insert (vs, name, (t, eqo)))
+
+end

diff --git a/src/main.sml b/src/main.sml
index 8cf8e67..7f7d2c0 100644 (file)
--- a/src/main.sml
+++ b/src/main.sml
@@ -20,7 +20,7 @@
 
 structure Main :> MAIN = struct
 
 
 structure Main :> MAIN = struct
 

-open Ast
+open Ast Print

 
 val dmy = ErrorMsg.dummyLoc
 
 
 val dmy = ErrorMsg.dummyLoc
 


@@ -37,9 +37,22 @@ fun check fname =
            ()
        else
            let
            ()
        else
            let

-               val G' = Tycheck.checkFile Tycheck.empty tInit prog
+               val G' = Tycheck.checkFile Env.empty tInit prog

            in
            in

-               ()
+               if !ErrorMsg.anyErrors then
+                   ()
+               else
+                   case prog of
+                       (_, SOME body) =>
+                       let
+                           val body' = Reduce.reduceExp G' body
+                       in
+                           printd (PD.hovBox (PD.PPS.Rel 0,
+                                              [PD.string "Result:",
+                                               PD.space 1,
+                                               p_exp body']))
+                       end
+                     | _ => ()

            end
     end
 
            end
     end
 

diff --git a/src/reduce.sig b/src/reduce.sig
new file mode 100644 (file)
index 0000000..a874362
--- /dev/null
+++ b/src/reduce.sig
@@ -0,0 +1,28 @@
+(* 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 *)
+
+signature REDUCE = sig
+
+    val reduceExp : Env.env -> Ast.exp -> Ast.exp
+
+    val freeIn : string -> Ast.exp -> bool
+    val subst : string -> Ast.exp -> Ast.exp -> Ast.exp
+
+end

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

diff --git a/src/tycheck.sig b/src/tycheck.sig
index a86ae37..50a816f 100644 (file)
--- a/src/tycheck.sig
+++ b/src/tycheck.sig
@@ -20,17 +20,17 @@
 
 signature TYCHECK = sig
 
 
 signature TYCHECK = sig
 

-    type env
-    val empty : env
+    val checkTyp : Env.env -> Ast.typ -> Ast.typ

 
 

-    val checkTyp : env -> Ast.typ -> Ast.typ
-
-    val checkExp : env -> Ast.exp -> Ast.typ
-    val checkUnit : env -> Ast.exp -> Ast.typ
+    val checkExp : Env.env -> Ast.exp -> Ast.typ
+    val checkUnit : Env.env -> Ast.exp -> Ast.typ

     (* [checkUnit] checks that all unification variables have been resolved. *)
 
     (* [checkUnit] checks that all unification variables have been resolved. *)
 

-    val checkDecl : env -> Ast.decl -> env
+    val checkDecl : Env.env -> Ast.decl -> Env.env
+
+    val checkFile : Env.env -> Ast.typ -> Ast.file -> Env.env

 
 

-    val checkFile : env -> Ast.typ -> Ast.file -> env
+    val resetUnif : unit -> unit
+    val newUnif : unit -> Ast.typ'

 
 end
 
 end

diff --git a/src/tycheck.sml b/src/tycheck.sml
index 5ce94c8..fa006df 100644 (file)
--- a/src/tycheck.sml
+++ b/src/tycheck.sml
@@ -20,21 +20,10 @@
 
 structure Tycheck :> TYCHECK = struct
 
 
 structure Tycheck :> TYCHECK = struct
 

-open Ast Print
+open Ast Print Env

 
 

-structure SS = StringSet

 structure SM = StringMap
 
 structure SM = StringMap
 

-type env = SS.set * typ SM.map
-val empty : env = (SS.add (SS.singleton "int", "string"),
-                  SM.empty)
-
-fun lookupType (ts, _) name = SS.member (ts, name)
-fun lookupVal (_, vs) name = SM.find (vs, name)
-
-fun bindType (ts, vs) name = (SS.add (ts, name), vs)
-fun bindVal (ts, vs) (name, t) = (ts, SM.insert (vs, name, t))
-

 local
     val unifCount = ref 0
 in
 local
     val unifCount = ref 0
 in


@@ -349,7 +338,7 @@ fun checkExp G (eAll as (e, loc)) =
                        NONE => (newUnif (), loc)
                      | SOME t => checkTyp G t
 
                        NONE => (newUnif (), loc)
                      | SOME t => checkTyp G t
 

-               val G' = bindVal G (x, t)
+               val G' = bindVal G (x, t, NONE)

                val t' = checkExp G' e
            in
                (TArrow (t, t'), loc)
                val t' = checkExp G' e
            in
                (TArrow (t, t'), loc)


@@ -397,7 +386,7 @@ fun checkExp G (eAll as (e, loc)) =
          | EGet (x, evar, rest) =>
            let
                val xt = (newUnif (), loc)
          | EGet (x, evar, rest) =>
            let
                val xt = (newUnif (), loc)

-               val G' = bindVal G (x, xt)
+               val G' = bindVal G (x, xt, NONE)

 
                val rt = whnorm (checkExp G' rest)
            in
 
                val rt = whnorm (checkExp G' rest)
            in


@@ -638,7 +627,26 @@ fun checkUnit G (eAll as (_, loc)) =
 fun checkDecl G (d, _, loc) =
     case d of
        DExternType name => bindType G name
 fun checkDecl G (d, _, loc) =
     case d of
        DExternType name => bindType G name

-      | DExternVal (name, t) => bindVal G (name, checkTyp G t)
+      | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
+      | DVal (name, to, e) =>
+       let
+           val to =
+               case to of
+                   NONE => (newUnif (), loc)
+                 | SOME to => checkTyp G to
+
+           val t = checkExp G e
+       in
+           subTyp (t, to)
+           handle Unify ue =>
+                  describe_type_error loc
+                                      (WrongType ("Bound value",
+                                                  e,
+                                                  t,
+                                                  to,
+                                                  SOME ue));
+           bindVal G (name, to, SOME e)
+       end

 
 fun checkFile G tInit (ds, eo) =
     let
 
 fun checkFile G tInit (ds, eo) =
     let

diff --git a/tests/reduce.dtl b/tests/reduce.dtl
new file mode 100644 (file)
index 0000000..36a78b9
--- /dev/null
+++ b/tests/reduce.dtl
@@ -0,0 +1,2 @@
+One = (\x -> 1) 42;
+Fred = \x -> ((\f -> \x -> [f, \y : (int) -> x]) x)