code/untyped_evaluator.ml

   1 (*
   2    This is a simplified version of the code at ...
   3    You can use this code as follows:
   4
   5    1. First, use a text editor to fill in the uncompleted portions.
   6    2. Then see if OCaml will compile it, by typing `ocamlc -c simple.ml` in a Terminal.
   7    3. If it doesn't work, go back to step 1.
   8    4. If it does work, then you can start up the OCaml toplevel using `ocaml -I DIRECTORY`,
   9       where DIRECTORY is the name of the folder that contains your `simple.ml` file.
  10       (Alternatively, if OCaml is already started, you can type `#directory "DIRECTORY";;`
  11    5. Then once OCaml is started, you can either: (a) type `#load "simple.cmo";;`, then type
  12       `open Simple;;` (this has to be on a separate line from step (a), it seems);
  13       or (b) instead you can type `#use "simple.ml";;`
  14    6. Now you can try commands like `interpret (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty`
  15       Or V1.reduce (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty`
  16       Or V1.evaluate (App(Lambda("x",Var "x"),Lambda("y",Var "y"))) empty`
  17
  18    The environments play absolutely no role in this simplified V1 interpreter. In the
  19    fuller code, they have a limited role in the V1 interpreter. In the V2 interpreter,
  20    the environments are essential. This simplified code just provides a single
  21    implementation of environments; but the fuller code provides more.
  22 *)
  23
  24 type identifier = string
  25
  26 type term =
  27   | Var of identifier
  28   | App of term * term
  29   | Lambda of identifier * term
  30   | Let of identifier * term * term
  31   | If of term * term * term
  32   | Closure of identifier * term * env
  33
  34 and result = term
  35
  36 and env = identifier -> term option
  37
  38 let empty = fun _ -> None
  39 let push (ident : identifier) binding env =
  40   fun (sought_ident : identifier) ->
  41     if ident = sought_ident
  42     then Some binding
  43     else env sought_ident
  44 let lookup sought_ident env = env sought_ident
  45
  46
  47 (*
  48    eval raises this exception when it fails to reduce/evaluate
  49    a term, because it has components for which no
  50    reduction/evaluation is defined, such as `succ false`. The
  51    reduction-based interpreter just signaled this with a normal
  52    return value; but the environment- based interpreter uses an
  53    exception to abort prematurely.
  54
  55   In this simplified version of the code, we also use this
  56   exception to report a failed term in V1, since we lack
  57   the resources to print the term instead, as the full code does.
  58 *)
  59 exception Stuck of term
  60
  61 module V1 = struct
  62   (* ---------------------------------------------------------------
  63      Interpreter that reduces by substituting, using:
  64          val reduce_head_once : term -> env -> reduceOutcome
  65          val reduce : term -> env -> result
  66
  67      reduce_head_once is similiar to reduce_if_redex in the
  68      combinatory logic interpreter, except that the latter only
  69      performed a reduction if its argument was exactly a redex.
  70      It had to rely on its caller to detect cases where the term
  71      was instead a longer sequence of applications that had a
  72      redex at its head.  In the present code, on the other hand,
  73      we have reduce_head_once take care of this itself, by
  74      calling itself recursively where appropriate. Still, it will
  75      only perform at most one reduction per invocation.
  76   *)
  77
  78
  79   (* Search term and find a variable that isn't used in it,
  80      either free or bound.  We do this by appending primes to base
  81      until we find an unused or "fresh" variable. *)
  82   let fresh_var (base : identifier) (term : term) : identifier =
  83     let rec aux term vars =
  84     match term with
  85     | Var(var_ident) ->
  86         var_ident :: vars
  87     | App(head, arg) ->
  88         let vars' = aux head vars in
  89         aux arg vars'
  90     | Lambda(bound_ident, body) ->
  91         aux body (bound_ident :: vars)
  92     | Let(bound_ident, arg, body) ->
  93         let vars' = aux arg vars in
  94         aux body (bound_ident :: vars')
  95     | If(test, yes, no) ->
  96         let vars' = aux test vars in
  97         let vars'' = aux yes vars' in
  98         aux no vars''
  99     | Closure _ -> assert false in
 100     let used_vars = aux term [] in
 101     let rec check ident =
 102       if List.mem ident used_vars
 103       then check (ident ^ "'")
 104       else ident in
 105     check (base ^ "'")
 106
 107   let rec free_in (ident : identifier) (term : term) : bool =
 108     match term with
 109     | Var(var_ident) ->
 110         var_ident = ident
 111     | App(head, arg) ->
 112         free_in ident head || free_in ident arg
 113     | Lambda(bound_ident, body) ->
 114         bound_ident <> ident && free_in ident body
 115     | Let(bound_ident, arg, body) ->
 116         free_in ident arg || (bound_ident <> ident && free_in ident body)
 117     | If(test, yes, no) ->
 118         free_in ident test || free_in ident yes || free_in ident no
 119     | Closure _ -> assert false
 120
 121   let rec substitute (ident:identifier) (replacement : term) (original : term) =
 122     match original with
 123     | Var(var_ident) when var_ident = ident -> replacement
 124     | Var _ as orig -> orig
 125     | App(head, arg) ->
 126         let head' = substitute ident replacement head in
 127         let arg' = substitute ident replacement arg in
 128         App(head', arg')
 129     | Lambda(bound_ident, body) as orig
 130       when bound_ident = ident || not (free_in ident body) ->
 131         (* vacuous substitution *)
 132         orig
 133     | Lambda(bound_ident, body)
 134       when not (free_in bound_ident replacement) ->
 135         (* can substitute without renaming bound_ident *)
 136         let body' = substitute ident replacement body in
 137         Lambda(bound_ident, body')
 138     | Lambda(bound_ident, body) ->
 139         (* find a fresh variable unused in either body or
 140            replacement (which we hack by specifying their App) *)
 141         let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
 142         let body' = substitute bound_ident (Var bound_ident') body in
 143         let body'' = substitute ident replacement body' in
 144         Lambda(bound_ident', body'')
 145     | Let(bound_ident, arg, body)
 146       when bound_ident = ident || not (free_in ident body) ->
 147         let arg' = substitute ident replacement arg in
 148         Let(bound_ident, arg', body)
 149     | Let(bound_ident, arg, body)
 150       when not (free_in bound_ident replacement) ->
 151         (* can substitute without renaming bound_ident *)
 152         let body' = substitute ident replacement body in
 153         let arg' = substitute ident replacement arg in
 154         Let(bound_ident, arg', body')
 155     | Let(bound_ident, arg, body) ->
 156         (* find a fresh variable unused in either body or
 157            replacement (which we hack by specifying their App) *)
 158         let bound_ident' = fresh_var bound_ident (App(body,replacement)) in
 159         let body' = substitute bound_ident (Var bound_ident') body in
 160         let body'' = substitute ident replacement body' in
 161         let arg' = substitute ident replacement arg in
 162         Let(bound_ident', arg', body'')
 163     | If(test, yes, no) ->
 164         let test' = substitute ident replacement test in
 165         let yes' = substitute ident replacement yes in
 166         let no' = substitute ident replacement no in
 167         If(test', yes', no')
 168     | Closure _ -> assert false
 169
 170   type reduceOutcome = AlreadyResult of result | StuckAt of term | ReducedTo of term
 171
 172   let rec reduce_head_once (term : term) (env : env) : reduceOutcome =
 173     match term with
 174     | Lambda _ -> AlreadyResult term
 175
 176     | Var var -> failwith ("Unbound variable `" ^ var ^ "`")
 177     | Closure _ -> assert false (* no Closures in V1 *)
 178
 179 (* In this simplified version there are no Bool Literals, so If terms are always stuck
 180     | If(Literal(Bool true),yes,no) -> ReducedTo yes
 181     | If(Literal(Bool false),yes,no) -> ReducedTo no
 182 *)
 183     | If(test,yes,no) ->
 184         (match reduce_head_once test env with
 185         | AlreadyResult _ -> StuckAt term (* if test was not reducible to a bool, the if-term is not reducible at all *)
 186         | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
 187         | ReducedTo test' -> ReducedTo(If(test',yes,no)))
 188
 189     (* notice we never evaluate the body except after substituting
 190        and that happens only after arg is reduced to a result *)
 191     | Let(bound_var,arg,body) ->
 192         (match reduce_head_once arg env with
 193         | AlreadyResult _ ->
 194             (* if arg was not reducible, we can substitute *)
 195             ReducedTo (substitute bound_var arg body)
 196         | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
 197         | ReducedTo arg' -> ReducedTo (Let(bound_var,arg',body)))
 198
 199     (* notice we only substitute after arg is reduced to a result *)
 200     | App(Lambda(bound_var, body) as head, arg) ->
 201         (match reduce_head_once arg env with
 202         | AlreadyResult _ ->
 203             (* if arg was not reducible, we can substitute *)
 204             ReducedTo (substitute bound_var arg body)
 205         | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
 206         | ReducedTo arg' -> ReducedTo (App(head, arg')))
 207
 208     (* first the head should be reduced, next the arg *)
 209     | App(head, arg) ->
 210         (match reduce_head_once head env with
 211         | AlreadyResult _ -> (* head was not reducible, was arg? *)
 212             (match reduce_head_once arg env with
 213             | ReducedTo arg' -> ReducedTo (App(head, arg'))
 214             (* reducible cases of App(result, result) were caught above; so here we're stuck *)
 215             | AlreadyResult _ -> StuckAt term
 216             | StuckAt _ as outcome -> outcome) (* propagate Stuck subterm *)
 217         | StuckAt _ as outcome -> outcome (* propagate Stuck subterm *)
 218         | ReducedTo head' -> ReducedTo (App(head', arg)))
 219
 220
 221
 222
 223   let rec reduce (term : term) (env : env) =
 224     match reduce_head_once term env with
 225     | AlreadyResult res -> res
 226     | StuckAt subterm -> raise (Stuck subterm)
 227     | ReducedTo term' -> reduce term' env (* keep trying *)
 228
 229 end (* module V1 *)
 230
 231 module V2 = struct
 232   (* ---------------------------------------------------------------
 233      Interpreter that employs an "environment" or assignment
 234      function of results, using:
 235          val eval term -> env -> result, or may raise (Stuck term)
 236          val evaluate term -> env -> result
 237      Now `env` contains local as well as toplevel bindings.
 238   *)
 239
 240   let rec eval (term : term) (env : env) : result =
 241     match term with
 242     | Closure _ -> term
 243
 244     | Lambda(bound_var, body) -> Closure(bound_var, body, env)
 245
 246     | Var var ->
 247         (match lookup var env with
 248         (* the first case is different from V1.reduce_head_once *)
 249         | Some res -> res
 250         | None -> failwith ("Unbound variable `" ^ var ^ "`"))
 251
 252     | If(test, yes, no) ->
 253         (match eval test env with
 254 (* In this simplified version there are no Bool Literals, so If terms are always stuck
 255         | Literal(Bool true) -> eval yes env
 256         | Literal(Bool false) -> eval no env
 257 *)
 258         | res -> raise (Stuck(If(res,yes,no))))
 259
 260     | Let(bound_var, arg, body) ->
 261         (* evaluate body under a new env where bound_var has been
 262            bound to the result of evaluating arg under the
 263            current env *)
 264         let arg' = eval arg env in
 265         let env' = push bound_var arg' env in
 266         eval body env'
 267
 268     | App(head, arg) ->
 269         (match eval head env with
 270         | Closure(bound_var, body, saved_env) ->
 271             (* argument gets evaluated in current env *)
 272             let arg' = eval arg env in
 273             (* evaluate body under saved_env to govern its free
 274                variables, except that we add a binding of
 275                bound_var to arg' *)
 276             let saved_env' = push bound_var arg' saved_env in
 277             eval body saved_env'
 278         | head' -> raise (Stuck(App(head',arg))))
 279
 280
 281
 282   let evaluate (term : term) (env : env) : result =
 283     eval term env (* in the fuller code, this function catches the Stuck errors and prints them more nicely *)
 284
 285 end (* module V2 *)
 286
 287
 288 (* Put comment (* *)s around exactly one of the following two pairs of lines. *)
 289
 290 let version = "version 1 (reduce by substituting)"
 291 let interpret = V1.reduce
 292
 293 (*
 294 let version = "version 2 (use environment for local bindings)"
 295 let interpret = V2.evaluate
 296 *)