%{
  CH 3:  Untyped arithmetic expressions
  Author: Brigitte Pientka

  IMPLEMENTING AN INTERPRETER

  We interpret the big-step evaluation rules
  as a specification for an interpreter.
}%

final_value:  type.
no_result: final_value.
result: term -> final_value.

rec eval : [ |- term] -> [ |- final_value] =
/ total m (eval m)/
fn m => case m of
| [ |- true]  => [ |- result true]
| [ |- false] => [ |- result false]
| [ |- if_then_else T1 T2 T3] =>
  (case eval [ |- T1] of
    | [ |- result true]  => eval [ |- T2]
    | [ |- result false] => eval [ |- T3]
    | [ |- _]            => [ |- no_result]
  )
;



let r = eval [ |- (if_then_else (if_then_else (if_then_else true false false)
                               true
                               true)
                       false
                       false) ] ;
