(*  Title:      Tools/Compute_Oracle/am_compiler.ML

    ID:         $Id$

    Author:     Steven Obua

*)

signature COMPILING_AM = 

sig

  include ABSTRACT_MACHINE

  val set_compiled_rewriter : (term -> term) -> unit

  val list_nth : 'a list * int -> 'a

  val list_map : ('a -> 'b) -> 'a list -> 'b list

end

structure AM_Compiler : COMPILING_AM = struct

val list_nth = List.nth;

val list_map = map;

open AbstractMachine;

val compiled_rewriter = ref (NONE:(term -> term)Option.option)

fun set_compiled_rewriter r = (compiled_rewriter := SOME r)

type program = (term -> term)

(*Returns true iff at most 0 .. (free-1) occur unbound. therefore

  check_freevars 0 t iff t is closed*)

fun check_freevars free (Var x) = x < free

  | check_freevars free (Const c) = true

  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v

  | check_freevars free (Abs m) = check_freevars (free+1) m

fun count_patternvars PVar = 1

  | count_patternvars (PConst (_, ps)) =

      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps

fun print_rule (p, t) = 

    let	

	fun str x = Int.toString x		    

	fun print_pattern n PVar = (n+1, "x"^(str n))

	  | print_pattern n (PConst (c, [])) = (n, "c"^(str c))

	  | print_pattern n (PConst (c, args)) = 

	    let

		val h = print_pattern n (PConst (c,[]))

	    in

		print_pattern_list h args

	    end

	and print_pattern_list r [] = r

	  | print_pattern_list (n, p) (t::ts) = 

	    let

		val (n, t) = print_pattern n t

	    in

		print_pattern_list (n, "App ("^p^", "^t^")") ts

	    end

	val (n, pattern) = print_pattern 0 p

	val pattern =

            if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")"

            else pattern

	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)

              "Var " ^ str x

	  | print_term d (Const c) = "c" ^ str c

	  | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"

	  | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"

	fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))

	val term = print_term 0 t

	val term =

            if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"

            else "Closure ([], "^term^")"

    in

	"  | weak_reduce (false, stack, "^pattern^") = Continue (false, stack, "^term^")"

    end

fun constants_of PVar = []

  | constants_of (PConst (c, ps)) = c :: maps constants_of ps

fun constants_of_term (Var _) = []

  | constants_of_term (Abs m) = constants_of_term m

  | constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b)

  | constants_of_term (Const c) = [c]

fun load_rules sname name prog = 

    let

	val buffer = ref ""

	fun write s = (buffer := (!buffer)^s)

	fun writeln s = (write s; write "\n")

	fun writelist [] = ()

	  | writelist (s::ss) = (writeln s; writelist ss)

	fun str i = Int.toString i

	val _ = writelist [

		"structure "^name^" = struct",

		"",

		"datatype term = Dummy | App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]

	val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)

	val _ = map (fn x => write (" | c"^(str x))) constants

	val _ = writelist [

		"",

		"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",

		"",

		"type state = bool * stack * term",

		"",

		"datatype loopstate = Continue of state | Stop of stack * term",

		"",

		"fun proj_C (Continue s) = s",

		"  | proj_C _ = raise Match",

		"",

		"fun proj_S (Stop s) = s",

		"  | proj_S _ = raise Match",

		"",

		"fun cont (Continue _) = true",

		"  | cont _ = false",

		"",

		"fun do_reduction reduce p =",

		"    let",

		"       val s = ref (Continue p)",

		"       val _ = while cont (!s) do (s := reduce (proj_C (!s)))",

		"   in",

		"       proj_S (!s)",

		"   end",

		""]

	val _ = writelist [

		"fun weak_reduce (false, stack, Closure (e, App (a, b))) = Continue (false, SAppL (Closure (e, b), stack), Closure (e, a))",

		"  | weak_reduce (false, SAppL (b, stack), Closure (e, Abs m)) = Continue (false, stack, Closure (b::e, m))",

		"  | weak_reduce (false, stack, c as Closure (e, Abs m)) = Continue (true, stack, c)",

		"  | weak_reduce (false, stack, Closure (e, Var n)) = Continue (false, stack, case "^sname^".list_nth (e, n) of Dummy => Var n | r => r)",

		"  | weak_reduce (false, stack, Closure (e, c)) = Continue (false, stack, c)"]

	val _ = writelist (map print_rule prog)

        val _ = writelist [

		"  | weak_reduce (false, stack, clos) = Continue (true, stack, clos)",

		"  | weak_reduce (true, SAppR (a, stack), b) = Continue (false, stack, App (a,b))",

		"  | weak_reduce (true, s as (SAppL (b, stack)), a) = Continue (false, SAppR (a, stack), b)",

		"  | weak_reduce (true, stack, c) = Stop (stack, c)",

		"",

		"fun strong_reduce (false, stack, Closure (e, Abs m)) =",

		"    let",

		"        val (stack', wnf) = do_reduction weak_reduce (false, SEmpty, Closure (Dummy::e, m))",

		"    in",

		"        case stack' of",

		"            SEmpty => Continue (false, SAbs stack, wnf)",

		"          | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",

		"    end",		

		"  | strong_reduce (false, stack, clos as (App (u, v))) = Continue (false, SAppL (v, stack), u)",

		"  | strong_reduce (false, stack, clos) = Continue (true, stack, clos)",

		"  | strong_reduce (true, SAbs stack, m) = Continue (false, stack, Abs m)",

		"  | strong_reduce (true, SAppL (b, stack), a) = Continue (false, SAppR (a, stack), b)",

		"  | strong_reduce (true, SAppR (a, stack), b) = Continue (true, stack, App (a, b))",

		"  | strong_reduce (true, stack, clos) = Stop (stack, clos)",

		""]

	val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"						  	

	val _ = writelist [

		"fun importTerm ("^sname^".Var x) = Var x",

		"  | importTerm ("^sname^".Const c) =  "^ic,

		"  | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)",

		"  | importTerm ("^sname^".Abs m) = Abs (importTerm m)",

		""]

	fun ec c = "  | exportTerm c"^(str c)^" = "^sname^".Const "^(str c)

	val _ = writelist [

		"fun exportTerm (Var x) = "^sname^".Var x",

		"  | exportTerm (Const c) = "^sname^".Const c",

		"  | exportTerm (App (a,b)) = "^sname^".App (exportTerm a, exportTerm b)",

		"  | exportTerm (Abs m) = "^sname^".Abs (exportTerm m)",

		"  | exportTerm (Closure (closlist, clos)) = raise ("^sname^".Run \"internal error, cannot export Closure\")",

		"  | exportTerm Dummy = raise ("^sname^".Run \"internal error, cannot export Dummy\")"]

	val _ = writelist (map ec constants)

	val _ = writelist [

		"",

		"fun rewrite t = ",

		"    let",

		"      val (stack, wnf) = do_reduction weak_reduce (false, SEmpty, Closure ([], importTerm t))",

		"    in",

		"      case stack of ",

		"           SEmpty => (case do_reduction strong_reduce (false, SEmpty, wnf) of",

		"                          (SEmpty, snf) => exportTerm snf",

		"                        | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",

		"         | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",

		"    end",

		"",

		"val _ = "^sname^".set_compiled_rewriter rewrite",

		"",

		"end;"]

    in

	compiled_rewriter := NONE;	

	use_text "" Output.ml_output false (!buffer);

	case !compiled_rewriter of 

	    NONE => raise (Compile "cannot communicate with compiled function")

	  | SOME r => (compiled_rewriter := NONE; r)

    end	

fun compile eqs = 

    let

	val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()

	val eqs = map (fn (a,b,c) => (b,c)) eqs

	fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule") 

	val _ = map (fn (p, r) => 

                  (check (p, r); 

                   case p of PVar => raise (Compile "pattern is just a variable") | _ => ())) eqs

    in

	load_rules "AM_Compiler" "AM_compiled_code" eqs

    end	

fun run prog t = (prog t)

fun discard p = ()

end