(*============================================================================*)
(*== UE Conception de Langages -- Octobre 2006                              ==*)
(*============================================================================*)
(*== Fichier: lb_eval.ml                                                    ==*)
(*== ---------------------------------------------------------------------- ==*)
(*== Evaluateur d'un lambda calcul étendu.                                  ==*)
(*==                                                                        ==*)
(*==                                                                        ==*)
(*============================================================================*)
open Lb_type ;;

(*== Environnement                                                            *)
type env =
    Nil
  | Cons of string * (lterm * env) * env

exception Undefined of string

let rec get_env x e =
  match e with
    Nil -> raise (Undefined x)
  | Cons(x',c,e)
    -> if x=x' then c
       else get_env x e

let rec string_of_env e =
  match e with
    Nil -> ""
  | Cons(x,(t,_),e)
    -> Printf.sprintf"%s = %s\n%s" x (Lb_type.to_string t) (string_of_env e)

(*== Operateurs predefinis (appel)                                            *)
exception Op_call of string 

let op_call_fail op vs =
  raise (Op_call 
	   (Printf.sprintf"%s: %s" 
	      op 
	      (Lb_type.to_strings vs)))

let op_call op vs =
  try
    (Hashtbl.find op_tab op) vs
  with
    _ -> op_call_fail op vs

(*== Evaluateur                                                               *)

(*-- Auxiliaire: projection 1/3                                               *)
let fst3 (x,y,z) = x

(*-- Auxiliaire pour le traitement de l'abstraction multiple:                 *)
(*              itération de dépilement dans l'encvironnement                 *)
(*  Arguments:                                                                *)
(*    'xs' liste de (noms de) variables                                       *)
(*    'e' environnement 'e'                                                   *)
(*    's' pile                                                                *)
(*  Résultat: un tiplet ('xs','e','s') avec                                   *)
(*    'xs' variables restantes (non empilées)                                 *)
(*    'e'  nouvel environnement obtenu                                        *)
(*    's'  pile restante                                                      *)
let rec pops xs e s =
  match xs, s with
    x::xs, c::s -> pops xs (Cons(x,c,e)) s
  | _ -> xs, e, s

(*-- Fonction d'évaluation                                                    *)
(*  Arguments:                                                                *)
(*    't' lambda terme                                                        *)
(*    'e' environnement                                                       *)
(*    's' pile                                                                *)
(*  Résultat: un triplet ('t','e','s')                                        *)
(*    't' lambda terme (forme normale de tête)                                *)
(*    'e' environnement résultant                                             *)
(*    's'  pile restante                                                      *)
let rec eval t e s =
 match t, e, s with
   (VAR x), _, _
   -> let t,e = get_env x e in
	eval t e s

 | (LBD(xs,t)), _, _
   -> (match pops xs e s with
         [], e, s -> eval t e s
       | xs, e, [] -> (LBD(xs,t), e, [])
       | _ -> failwith "eval pops")

 | (APP((OP o)::ts)), _, _ 
    -> (op_call o (List.map (fun t -> fst3(eval t e [])) ts), Nil, s)
 | (APP(t::ts)), _, _
   -> eval t e (push_evals ts e s)

 | NIL, _, _
   -> (NIL, Nil, s)
 | FST, _, ((PAIR(t1,_),e)::s)
   -> eval t1 e s
 | SND, _, ((PAIR(_,t2),e)::s)
   -> eval t2 e s
 | (PAIR _), _, _
   -> (t, e, s)

 | ALT,_,((BOOL true,_)::(PAIR(t1,_),e')::s)
     -> eval t1 e' s
 | ALT,_,((BOOL false,_)::(PAIR(_,t2),e')::s)
     -> eval t2 e' s

 | REC(f,t'),_,_
     -> eval t' (Cons(f,(t,e),e)) s

 | (QUOTE t), _, _
   -> (t, e, s)

 | (SYM _), _, _
   -> (t, Nil, s)
 | (NUM _), _, _
   -> (t, Nil, s)
 | (STR _), _, _
   -> (t, Nil, s)
 | (BOOL _), _, _
   -> (t, Nil, s)
 | _, _, [] -> failwith ("eval: "^(Lb_type.to_string t))
 | _ -> failwith ("eval fatal: "^(Lb_type.to_string t)^" "^(Lb_type.to_string (fst(List.hd s))))

(*-- Auxiliaire pour le traitement de l'application multiple                  *)
(*              itération d'empilements                                       *)
(*  Arguments:                                                                *)
(*    'ts' liste de termes (argument de l'application)                        *)
(*    'e' environnement 'e'                                                   *)
(*    's' pile                                                                *)
(*  Résultat:                                                                 *)
(*    une pile contenant les clotures ('t','e') pour tout 't' dans 'ts'       *)
and push_evals ts e s =
  let clos (t,e,s) = (t,e) in
  match ts with
    [] -> s
  | t::ts -> (clos (eval t e []))::(push_evals ts e s)