src/Tools/Compute_Oracle/am_sml.ML

 (*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
 
 val compiled_rewriter = ref (NONE:(term -> term)Option.option)
 
 fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
-
-fun importable (Var _) = false
-  | importable (Const _) = true			   
-  | importable (App (a, b)) = importable a andalso importable b
-  | importable (Abs _) = false
-
-(*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
 

   | beta (App (a, b)) = 
     (case beta a of
 	 Abs m => beta (App (Abs m, b))
        | a => App (a, beta b))
   | beta (Abs m) = Abs (beta m)
+  | beta (Computed t) = Computed t
 and subst x (Const c) t = Const c
   | subst x (Var i) t = if i = x then t else Var i
   | subst x (App (a,b)) t = App (subst x a t, subst x b t)
   | subst x (Abs m) t = Abs (subst (x+1) m (lift 0 t))
 and lift level (Const c) = Const c

 		    in
 			"  | eval bounds ("^left^") = "^right
 		    end
 	    in
 		map eval_rule (rev (section (arity + 1)))
+	    end
+
+	fun (convert_computed_rules : int -> string list) c = 
+	    let
+		val arity = the (arity_of c)
+		fun eval_rule () = 
+		    let
+			val sc = string_of_int c
+			val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section arity) ("AbstractMachine.Const "^sc)
+                        fun arg i = "(convert_computed "^(indexed "x" i)^")" 
+			val right = "C"^sc^" "^(string_of_tuple (map arg (section arity)))		
+			val right = if arity > 0 then right else "C"^sc
+		    in
+			"  | convert_computed ("^left^") = "^right
+		    end
+	    in
+		[eval_rule ()]
 	    end
         
 	fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else ""
 	val _ = writelist [                   
 		"structure "^name^" = struct",

 		val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
 	    in
 		"  | convert (C"^(str c)^" "^leftargs^") = "^right
 	    end 		
 	val _ = writelist (map make_convert constants)
+        val _ = writelist [
+                "",
+                "fun convert_computed (AbstractMachine.Abs b) = raise AM_SML.Run \"no abstraction in convert_computed allowed\"",
+                "  | convert_computed (AbstractMachine.Var i) = raise AM_SML.Run \"no bound variables in convert_computed allowed\""]
+        val _ = map (writelist o convert_computed_rules) constants
+        val _ = writelist [
+                "  | convert_computed (AbstractMachine.Const c) = Const c",
+                "  | convert_computed (AbstractMachine.App (a, b)) = App (convert_computed a, convert_computed b)",
+                "  | convert_computed (AbstractMachine.Computed a) = raise AM_SML.Run \"no nesting in convert_computed allowed\""] 
 	val _ = writelist [
 		"",
 		"fun eval bounds (AbstractMachine.Abs m) = Abs (fn b => eval (b::bounds) m)",
 		"  | eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"]
 	val _ = map (writelist o eval_rules) constants
 	val _ = writelist [
                 "  | eval bounds (AbstractMachine.App (a, b)) = app (eval bounds a) (eval bounds b)",
-                "  | eval bounds (AbstractMachine.Const c) = Const c"]                
+                "  | eval bounds (AbstractMachine.Const c) = Const c",
+                "  | eval bounds (AbstractMachine.Computed t) = convert_computed t"]                
 	val _ = writelist [		
 		"",
 		"fun export term = AM_SML.save_result (\""^code^"\", convert term)",
 		"",
                 "val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))",

     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 _ = writeTextFile "Gencode.ML" source
 	val _ = compiled_rewriter := NONE
 	val _ = use_source source
     in
 	case !compiled_rewriter of 
 	    NONE => raise Compile "broken link to compiled function"

 	val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
 	fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
 	  | inline (Var i) = Var i
 	  | inline (App (a, b)) = App (inline a, inline b)
 	  | inline (Abs m) = Abs (inline m)
+	  | inline (Computed t) = Computed t
     in
 	compiled_fun (beta (inline t))
     end	
 
 fun discard p = ()