(* Substitution model interpreter for BINDEX *)

module HoflSubstInterp = struct
  

  open Hofl
  open List

  exception EvalError of string

  let print = StringUtils.print 
  let println = StringUtils.println

  (* val run : Hofl.pgm -> int list -> int *)
  let rec run (Pgm(fmls,body)) ints = 
    let flen = length fmls
    and ilen = length ints 
    in 
      if flen = ilen then 
        eval (subst body (Env.make fmls (map (fun i -> Lit i) ints)))
      else 
        raise (EvalError ("Program expected " ^ (string_of_int flen)
                          ^ " arguments but got " ^ (string_of_int ilen)))

  (* val eval : Hofl.exp -> valu *)
  and eval exp = 
    match exp with 
      Lit v -> v
    | Var name -> raise (EvalError("Unbound variable: " ^ name))
    | PrimApp(op, rands) -> HoflEnvInterp.primApply op (map eval rands)
    | If(tst,thn,els) -> 
       (match eval tst with 
         Bool true -> eval thn
       | Bool false -> eval els
       | v -> raise (EvalError ("Non-boolean test value " 
				^ (valuToString v)
				^ " in if expression:\n"
				^ (expToString exp)))
       )
    | Abs(fml,body) -> Fun(fml,body,Env.empty) (* make a closure *)
    | App(rator,rand) -> apply (eval rator) (eval rand)
    | Bindrec(names,defns,body) -> 
        let recenv = Env.make names 
                              (map (fun name -> Bindrec(names,defns, Var name))
                                   names)
	in eval (subst body (Env.make names
			              (map (fun defn -> subst defn recenv) defns)))

  and apply fcn arg = 
    match fcn with 
      Fun(fml,body,_) -> eval (subst1 fml (Lit arg) body)
                         (* Converts any argument valu (including functions, pairs, lists) 
                            into a literal for purposes of substitution *)
    | _ -> raise (EvalError ("Non-function rator in application: "
			     ^ (valuToString fcn)))

  (* A function for running programs expressed as strings *)
  let runString pgmString args = 
    run (sexpToPgm (Sexp.stringToSexp pgmString)) args	  

  (* A function for running a programs in a files *)
  let runFile pgmFile args = 
    run (sexpToPgm (Sexp.stringToSexp (File.fileToString pgmFile))) args	  

  (* An interactive read-eval-print loop (REPL) for Hofl expressions.
     By default, assumes zero arguments, but this can be changed
     with the #args directive (see below). The following directives
     are supported:

     + (#desugar <exp>) prints out the desugared form of <exp>

     + (def <name> <exp>) introduces a top-level binding of <name> to <exp>. 
       This binding is mutually recursive with all other top-level bindings.

     + (def (<name> <fml1> ... <fmln>) <exp>) is sugar for
       (def <name> (fun (<fml1> ... <fmln>) <exp>))

     + (#load "<filename>") loads definitions and other recursive loads
       from file named <filename>.

     + (#quit): Exit the interpreter
   *)

  (* val repl : unit -> unit *)
  let rec repl () =
    let sexpToSymIntPair sexp =   (* sexpToStringIntPair : sexp -> (string * int) *)
      match sexp with 
        Sexp.Seq [Sexp.Sym s; Sexp.Int i] -> (s, i)
      | _ -> raise (Failure "Not an symbol/int pair!") in 
    (* Repl loop carries with it a list of name/exp bindings introduced by DEFs. 
       These are used as the bindings of a BINDREC every time an expression is 
       evaluated. Thus, all the bindings are mutually recursive. *)
    let rec loop bindings = 
      let _ = print "\n\nhofl> " in 
      let sexp = Sexp.readSexp() in 
        try 
          match sexp with 
            Sexp.Seq [Sexp.Sym "#quit"] -> print "\ndone\n"
          | Sexp.Seq [Sexp.Sym "#desugar"; sexp] -> 
	      ((match sexp with 
		Sexp.Seq (Sexp.Sym "def" :: _) -> 
		  print (Sexp.sexpToString (desugarDef sexp))
 	        | _ -> print (Sexp.sexpToString (desugar sexp))); 
	       loop bindings)
          | Sexp.Seq ((Sexp.Sym "#load" | Sexp.Sym "def") :: _) -> 
	      (* add new bindings to end of binding list *)
	      loop (bindings @ (declToBindings sexp))
          | _ -> 
           (* Bindrec-based interpretation of top-level definitions. *)
	      let (names,defns) = ListUtils.unzip (List.rev bindings)
                (* although bindings are mutually recursive, pay attention
                   to more recent bindings when the same name is defined twice. *)
	      in (print (valuToString (eval (Bindrec(names,defns, sexpToExp sexp))));
		  loop bindings)
        with 
          EvalError s -> (print ("EvalError: " ^ s); loop bindings)
        | SyntaxError s -> (print ("SyntaxError: " ^ s); loop bindings)
        | Sexp.IllFormedSexp s -> (print ("SexpError: " ^ s); loop bindings)
        | Sys_error s -> (print ("Sys_error: " ^ s); loop bindings)
    in loop [] 

  and declToBindings decl = 
    match decl with 
      (* "def" is effectively a top-level directive, but doesn't begin with a sharp sign. *)
      Sexp.Seq ((Sexp.Sym "def") :: _) -> 
        let ((name,defn) as binding) = defToBinding decl in (* defined in Hofl.ml *)
	let _ = println name in 
	[binding]
    | Sexp.Seq [Sexp.Sym "#load"; Sexp.Str filename] -> 
      (* filename is required to be a string literal *)
        let _ = println ("Loading " ^ filename) in 
        let bindings = fileToBindings filename in 
        let _ = println ("Done loading " ^ filename)in 
	bindings
    | _ -> raise (EvalError ("unrecognized declaration" ^ (Sexp.sexpToString decl)))

  (* val fileToBindings: string -> (string * Hofl.exp) list *)
  and fileToBindings filename = 
    let decls = Sexp.fileToSexps filename in 
      flatten (map declToBindings decls)


end