src/reduce.sml

   1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
   2  * Copyright (c) 2006, Adam Chlipala
   3  *
   4  * This program is free software; you can redistribute it and/or
   5  * modify it under the terms of the GNU General Public License
   6  * as published by the Free Software Foundation; either version 2
   7  * of the License, or (at your option) any later version.
   8  *
   9  * This program is distributed in the hope that it will be useful,
  10  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  11  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12  * GNU General Public License for more details.
  13  *
  14  * You should have received a copy of the GNU General Public License
  15  * along with this program; if not, write to the Free Software
  16  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
  17  *)
  18
  19 (* Evaluation of expressions until only externs are around *)
  20
  21 structure Reduce :> REDUCE = struct
  22
  23 open Ast Print Env
  24
  25 structure SM = StringMap
  26
  27 fun freeIn x (b, _) =
  28     case b of
  29         EInt _ => false
  30       | EString _ => false
  31       | EList es => List.exists (freeIn x) es
  32
  33       | ELam (x', _, b') => x <> x' andalso freeIn x b'
  34       | EVar x' => x = x'
  35       | EApp (e1, e2) => freeIn x e1 orelse freeIn x e2
  36
  37       | ESkip => false
  38       | ESet (_, e) => freeIn x e
  39       | EGet (x', _, b') => x <> x' andalso freeIn x b'
  40       | ESeq es => List.exists (freeIn x) es
  41       | ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2
  42       | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
  43       | EALam (x', _, b') => x <> x' andalso freeIn x b'
  44
  45 local
  46     val freshCount = ref 0
  47 in
  48 fun freshVar () =
  49     let
  50         val v = !freshCount
  51     in
  52         freshCount := v + 1;
  53         Int.toString v ^ "v"
  54     end
  55 end
  56
  57 fun subst x e (bAll as (b, loc)) =
  58     case b of
  59         EInt _ => bAll
  60       | EString _ => bAll
  61       | EList es => (EList (map (subst x e) es), loc)
  62
  63       | ELam (x', to, b') =>
  64         if x = x' then
  65             bAll
  66         else if freeIn x' e then
  67             let
  68                 val x'' = freshVar ()
  69             in
  70                 (ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc)
  71             end
  72         else
  73             (ELam (x', to, subst x e b'), loc)
  74       | EVar x' =>
  75         if x = x' then
  76             e
  77         else
  78             bAll
  79       | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc)
  80
  81       | ESkip => bAll
  82       | ESet (v, b) => (ESet (v, subst x e b), loc)
  83       | EGet (x', v, b') =>
  84         if x = x' then
  85             bAll
  86         else if freeIn x' e then
  87             let
  88                 val x'' = freshVar ()
  89             in
  90                 (EGet (x'', v, subst x e (subst x' (EVar x'', loc) b')), loc)
  91             end
  92         else
  93             (EGet (x', v, subst x e b'), loc)
  94       | ESeq es => (ESeq (map (subst x e) es), loc)
  95       | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
  96       | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
  97       | EALam (x', p, b') =>
  98         if x = x' then
  99             bAll
 100         else if freeIn x' e then
 101             let
 102                 val x'' = freshVar ()
 103             in
 104                 (EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc)
 105             end
 106         else
 107             (EALam (x', p, subst x e b'), loc)
 108
 109 fun reduceExp G (eAll as (e, loc)) =
 110     case e of
 111         EInt _ => eAll
 112       | EString _ => eAll
 113       | EList es => (EList (map (reduceExp G) es), loc)
 114
 115       | ELam (x, to, e) =>
 116         let
 117             val to' = case to of
 118                           NONE => (Tycheck.newUnif (), loc)
 119                         | SOME to => to
 120
 121             val G' = bindVal G (x, to', NONE)
 122         in
 123             (ELam (x, to, reduceExp G' e), loc)
 124         end
 125       | EVar x =>
 126         (case lookupEquation G x of
 127              NONE => eAll
 128            | SOME e => reduceExp G e)
 129       | EApp (e1, e2) =>
 130         let
 131             val e1' = reduceExp G e1
 132             val e2' = reduceExp G e2
 133         in
 134             case e1' of
 135                 (ELam (x, _, b), _) => reduceExp G (subst x e2' b)
 136               | _ => (EApp (e1', e2'), loc)
 137         end
 138
 139       | ESkip => eAll
 140       | ESet (v, b) => (ESet (v, reduceExp G b), loc)
 141       | EGet (x, v, b) => (EGet (x, v, reduceExp G b), loc)
 142       | ESeq es => (ESeq (map (reduceExp G) es), loc)
 143       | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
 144       | EWith (e1, e2) =>
 145         let
 146             val e1' = reduceExp G e1
 147             val e2' = reduceExp G e2
 148         in
 149             case e1' of
 150                 (EALam (x, _, b), _) => reduceExp G (subst x e2' b)
 151               | _ => (EWith (e1', e2'), loc)
 152         end
 153       | EALam (x, p, e) =>
 154         let
 155             val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
 156         in
 157             (EALam (x, p, reduceExp G' e), loc)
 158         end
 159
 160 end