From 492c1cff68a2da969a559627725369c211470c92 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 30 Jul 2006 01:12:01 +0000 Subject: [PATCH] Reduction --- src/ast.sml | 1 + src/domtool.cm | 6 +++ src/env.sig | 33 ++++++++++++ src/env.sml | 45 ++++++++++++++++ src/main.sml | 19 +++++-- src/reduce.sig | 28 ++++++++++ src/reduce.sml | 132 +++++++++++++++++++++++++++++++++++++++++++++++ src/tycheck.sig | 16 +++--- src/tycheck.sml | 38 ++++++++------ tests/reduce.dtl | 2 + 10 files changed, 294 insertions(+), 26 deletions(-) create mode 100644 src/env.sig create mode 100644 src/env.sml create mode 100644 src/reduce.sig create mode 100644 src/reduce.sml create mode 100644 tests/reduce.dtl diff --git a/src/ast.sml b/src/ast.sml index 0c6ddd1..bd87121 100644 --- 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 + | DVal of string * typ option * exp 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 --- a/src/domtool.cm +++ b/src/domtool.cm @@ -21,8 +21,14 @@ parse.sml print.sig print.sml +env.sig +env.sml + tycheck.sig tycheck.sml +reduce.sig +reduce.sml + main.sig main.sml diff --git a/src/env.sig b/src/env.sig new file mode 100644 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 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 --- a/src/main.sml +++ b/src/main.sml @@ -20,7 +20,7 @@ structure Main :> MAIN = struct -open Ast +open Ast Print val dmy = ErrorMsg.dummyLoc @@ -37,9 +37,22 @@ fun check fname = () 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 diff --git a/src/reduce.sig b/src/reduce.sig new file mode 100644 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 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 --- a/src/tycheck.sig +++ b/src/tycheck.sig @@ -20,17 +20,17 @@ 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 diff --git a/src/tycheck.sml b/src/tycheck.sml index 5ce94c8..fa006df 100644 --- a/src/tycheck.sml +++ b/src/tycheck.sml @@ -20,21 +20,10 @@ 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 @@ -349,7 +338,7 @@ fun checkExp G (eAll as (e, loc)) = 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) @@ -397,7 +386,7 @@ fun checkExp G (eAll as (e, 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 @@ -638,7 +627,26 @@ fun checkUnit G (eAll as (_, loc)) = 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 diff --git a/tests/reduce.dtl b/tests/reduce.dtl new file mode 100644 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) -- 2.20.1