src/Tools/Compute_Oracle/am_sml.ML
changeset 25520 e123c81257a5
parent 25279 5ff6fc338db1
child 25548 121705bba349
--- a/src/Tools/Compute_Oracle/am_sml.ML	Mon Dec 03 16:04:17 2007 +0100
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Dec 03 17:47:35 2007 +0100
@@ -13,12 +13,15 @@
   val save_result : (string * term) -> unit
   val set_compiled_rewriter : (term -> term) -> unit				       
   val list_nth : 'a list * int -> 'a
+  val dump_output : (string option) ref 
 end
 
 structure AM_SML : AM_SML = struct
 
 open AbstractMachine;
 
+val dump_output = ref NONE
+
 type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
 
 val saved_result = ref (NONE:(string*term)option)
@@ -155,8 +158,8 @@
 	val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
 	fun arity_of c = the (Inttab.lookup arity c)
 	fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c)
-	fun adjust_pattern PVar = PVar
-	  | adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C
+	fun test_pattern PVar = ()
+	  | test_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ())
 	fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable")
 	  | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters")
 	  | adjust_rule (rule as (prems, p as PConst (c, args),t)) = 
@@ -165,13 +168,13 @@
 		fun check_fv t = check_freevars patternvars_counted t
 		val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else () 
 		val _ = if not (forall (fn (Guard (a,b)) => check_fv a andalso check_fv b) prems) then raise Compile ("unbound variables in guards") else () 
-		val args = map adjust_pattern args	        
+		val _ = map test_pattern args	        
 		val len = length args
 		val arity = arity_of c
 		val lift = nlift 0
-		fun adjust_tm n t = if n=0 then t else adjust_tm (n-1) (App (t, Var (n-1)))
-		fun adjust_term n t = adjust_tm n (lift n t)
-		fun adjust_guard n (Guard (a,b)) = Guard (adjust_term n a, adjust_term n b)
+		fun addapps_tm n t = if n=0 then t else addapps_tm (n-1) (App (t, Var (n-1)))
+		fun adjust_term n t = addapps_tm n (lift n t)
+		fun adjust_guard n (Guard (a,b)) = Guard (lift n a, lift n b)
 	    in
 		if len = arity then
 		    rule
@@ -179,8 +182,7 @@
 		    (map (adjust_guard (arity-len)) prems, PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) t)
 		else (raise Compile "internal error in adjust_rule")
 	    end
-	fun beta_guard (Guard (a,b)) = Guard (beta a, beta b)
-	fun beta_rule (prems, p, t) = ((map beta_guard prems, p, beta t) handle Match => raise Compile "beta_rule")
+	fun beta_rule (prems, p, t) = ((prems, p, beta t) handle Match => raise Compile "beta_rule")
     in
 	(arity, toplevel_arity, map (beta_rule o adjust_rule) rules)
     end		    
@@ -493,13 +495,13 @@
 
 fun use_source src = use_text "" Output.ml_output false src
     
-fun compile eqs = 
+fun compile cache_patterns const_arity eqs = 
     let
 	val guid = get_guid ()
 	val code = Real.toString (random ())
 	val module = "AMSML_"^guid
 	val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs
-	(*val _ = writeTextFile "Gencode.ML" source*)
+	val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source
 	val _ = compiled_rewriter := NONE
 	val _ = use_source source
     in