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
print.sig
print.sml
+env.sig
+env.sml
+
tycheck.sig
tycheck.sml
+reduce.sig
+reduce.sml
+
main.sig
main.sml
--- /dev/null
+(* 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
--- /dev/null
+(* 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
structure Main :> MAIN = struct
-open Ast
+open Ast Print
val dmy = ErrorMsg.dummyLoc
()
else
let
- val G' = Tycheck.checkFile Tycheck.empty tInit prog
+ val G' = Tycheck.checkFile Env.empty tInit prog
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
--- /dev/null
+(* 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
--- /dev/null
+(* 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
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. *)
- 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
structure Tycheck :> TYCHECK = struct
-open Ast Print
+open Ast Print Env
-structure SS = StringSet
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
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)
| 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
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
--- /dev/null
+One = (\x -> 1) 42;
+Fred = \x -> ((\f -> \x -> [f, \y : (int) -> x]) x)