(* 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 structure SM = StringMap 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 | EALam (x', _, b') => x <> x' andalso freeIn x b' 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) | EALam (x', p, b') => if x = x' then bAll else if freeIn x' e then let val x'' = freshVar () in (EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc) end else (EALam (x', p, subst x e b'), loc) fun findPrim (e, _) = case e of EApp (f, x) => (case findPrim f of NONE => NONE | SOME (f, xs) => SOME (f, xs @ [x])) | EVar x => SOME (x, []) | _ => NONE 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) | _ => case findPrim eAll of NONE => (EApp (e1', e2'), loc) | SOME (f, args) => case function f of NONE => (EApp (e1', e2'), loc) | SOME f => case f (map (reduceExp G) args) of NONE => (EApp (e1', e2'), loc) | SOME e' => reduceExp G e' 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) => let val e1' = reduceExp G e1 val e2' = reduceExp G e2 in case e1' of (EALam (x, _, b), _) => reduceExp G (subst x e2' b) | _ => (EWith (e1', e2'), loc) end | EALam (x, p, e) => let val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE) in (EALam (x, p, reduceExp G' e), loc) end end