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