code/untyped_evaluator.ml

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