new version of computing oracle
authorobua
Mon Jul 09 17:36:25 2007 +0200 (2007-07-09)
changeset 2366384b5c89b8b49
parent 23662 91d06b04951f
child 23664 9c486517354a
new version of computing oracle
src/Tools/Compute_Oracle/Compute_Oracle.thy
src/Tools/Compute_Oracle/am.ML
src/Tools/Compute_Oracle/am_compiler.ML
src/Tools/Compute_Oracle/am_ghc.ML
src/Tools/Compute_Oracle/am_interpreter.ML
src/Tools/Compute_Oracle/am_sml.ML
src/Tools/Compute_Oracle/am_util.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/Compute_Oracle/linker.ML
     1.1 --- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Mon Jul 09 11:44:23 2007 +0200
     1.2 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Mon Jul 09 17:36:25 2007 +0200
     1.3 @@ -5,28 +5,10 @@
     1.4  Steven Obua's evaluator.
     1.5  *)
     1.6  
     1.7 -theory Compute_Oracle
     1.8 -imports CPure
     1.9 -uses
    1.10 -  "am_interpreter.ML"
    1.11 -  "am_compiler.ML"
    1.12 -  "am_util.ML"
    1.13 -  "compute.ML"
    1.14 +theory Compute_Oracle imports CPure
    1.15 +uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML"
    1.16  begin
    1.17  
    1.18 -oracle compute_oracle ("Compute.computer * (int -> string) * cterm") =
    1.19 -  {* Compute.oracle_fn *}
    1.20 -
    1.21 -ML {*
    1.22 -structure Compute =
    1.23 -struct
    1.24 -  open Compute
    1.25 +setup {* Compute.setup; *}
    1.26  
    1.27 -  fun rewrite_param r n ct =
    1.28 -    compute_oracle (Thm.theory_of_cterm ct) (r, n, ct)
    1.29 -
    1.30 -  fun rewrite r ct = rewrite_param r default_naming ct
    1.31 -end
    1.32 -*}
    1.33 -
    1.34 -end
    1.35 +end
    1.36 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/Compute_Oracle/am.ML	Mon Jul 09 17:36:25 2007 +0200
     2.3 @@ -0,0 +1,46 @@
     2.4 +signature ABSTRACT_MACHINE =
     2.5 +sig
     2.6 +
     2.7 +datatype term = Var of int | Const of int | App of term * term | Abs of term
     2.8 +
     2.9 +datatype pattern = PVar | PConst of int * (pattern list)
    2.10 +
    2.11 +datatype guard = Guard of term * term
    2.12 +
    2.13 +type program
    2.14 +
    2.15 +exception Compile of string;
    2.16 +
    2.17 +(* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right,
    2.18 +   1 to the second last, and so on. *)
    2.19 +val compile : (guard list * pattern * term) list -> program
    2.20 +
    2.21 +val discard : program -> unit
    2.22 +
    2.23 +exception Run of string;
    2.24 +val run : program -> term -> term
    2.25 +
    2.26 +end
    2.27 +
    2.28 +structure AbstractMachine : ABSTRACT_MACHINE = 
    2.29 +struct
    2.30 +
    2.31 +datatype term = Var of int | Const of int | App of term * term | Abs of term
    2.32 +
    2.33 +datatype pattern = PVar | PConst of int * (pattern list)
    2.34 +
    2.35 +datatype guard = Guard of term * term
    2.36 +
    2.37 +type program = unit
    2.38 +
    2.39 +exception Compile of string;
    2.40 +
    2.41 +fun compile _ = raise Compile "abstract machine stub"
    2.42 +
    2.43 +fun discard _ = raise Compile "abstract machine stub"
    2.44 +
    2.45 +exception Run of string;
    2.46 +
    2.47 +fun run p t = raise Run "abstract machine stub"
    2.48 +
    2.49 +end
     3.1 --- a/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jul 09 11:44:23 2007 +0200
     3.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Mon Jul 09 17:36:25 2007 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      Tools/Compute_Oracle/am_compiler.ML
     3.5 +(*  Title:      Pure/Tools/am_compiler.ML
     3.6      ID:         $Id$
     3.7      Author:     Steven Obua
     3.8  *)
     3.9 @@ -7,10 +7,7 @@
    3.10  sig
    3.11    include ABSTRACT_MACHINE
    3.12  
    3.13 -  datatype closure = CVar of int | CConst of int
    3.14 -    | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
    3.15 -
    3.16 -  val set_compiled_rewriter : (term -> closure) -> unit
    3.17 +  val set_compiled_rewriter : (term -> term) -> unit
    3.18    val list_nth : 'a list * int -> 'a
    3.19    val list_map : ('a -> 'b) -> 'a list -> 'b list
    3.20  end
    3.21 @@ -20,39 +17,14 @@
    3.22  val list_nth = List.nth;
    3.23  val list_map = map;
    3.24  
    3.25 -datatype term = Var of int | Const of int | App of term * term | Abs of term
    3.26 -
    3.27 -datatype pattern = PVar | PConst of int * (pattern list)
    3.28 +open AbstractMachine;
    3.29  
    3.30 -datatype closure = CVar of int | CConst of int
    3.31 -	         | CApp of closure * closure | CAbs of closure
    3.32 -                 | Closure of (closure list) * closure
    3.33 -
    3.34 -val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
    3.35 +val compiled_rewriter = ref (NONE:(term -> term)Option.option)
    3.36  
    3.37  fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
    3.38  
    3.39  type program = (term -> term)
    3.40  
    3.41 -datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
    3.42 -
    3.43 -exception Compile of string;
    3.44 -exception Run of string;
    3.45 -
    3.46 -fun clos_of_term (Var x) = CVar x
    3.47 -  | clos_of_term (Const c) = CConst c
    3.48 -  | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
    3.49 -  | clos_of_term (Abs u) = CAbs (clos_of_term u)
    3.50 -
    3.51 -fun term_of_clos (CVar x) = Var x
    3.52 -  | term_of_clos (CConst c) = Const c
    3.53 -  | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
    3.54 -  | term_of_clos (CAbs u) = Abs (term_of_clos u)
    3.55 -  | term_of_clos (Closure (e, u)) =
    3.56 -      raise (Run "internal error: closure in normalized term found")
    3.57 -
    3.58 -fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
    3.59 -  | strip_closure args x = (x, args)
    3.60  
    3.61  (*Returns true iff at most 0 .. (free-1) occur unbound. therefore
    3.62    check_freevars 0 t iff t is closed*)
    3.63 @@ -103,7 +75,7 @@
    3.64              else "Closure ([], "^term^")"
    3.65  			   
    3.66      in
    3.67 -	"lookup stack "^pattern^" = weak stack ("^term^")"
    3.68 +	"  | weak_reduce (false, stack, "^pattern^") = Continue (false, stack, "^term^")"
    3.69      end
    3.70  
    3.71  fun constants_of PVar = []
    3.72 @@ -116,7 +88,6 @@
    3.73      
    3.74  fun load_rules sname name prog = 
    3.75      let
    3.76 -        (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
    3.77  	val buffer = ref ""
    3.78  	fun write s = (buffer := (!buffer)^s)
    3.79  	fun writeln s = (write s; write "\n")
    3.80 @@ -126,50 +97,62 @@
    3.81  	val _ = writelist [
    3.82  		"structure "^name^" = struct",
    3.83  		"",
    3.84 -		"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
    3.85 +		"datatype term = Dummy | App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
    3.86  	val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
    3.87  	val _ = map (fn x => write (" | c"^(str x))) constants
    3.88  	val _ = writelist [
    3.89  		"",
    3.90  		"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",
    3.91 -		""]
    3.92 -	val _ = (case prog of
    3.93 -		    r::rs => (writeln ("fun "^(print_rule r)); 
    3.94 -			      map (fn r => writeln("  | "^(print_rule r))) rs; 
    3.95 -			      writeln ("  | lookup stack clos = weak_last stack clos"); ())								
    3.96 -		  | [] => (writeln "fun lookup stack clos = weak_last stack clos"))
    3.97 -	val _ = writelist [
    3.98 -		"and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))",
    3.99 -		"  | weak (SAppL (b, stack)) (Closure (e, Abs m)) =  weak stack (Closure (b::e, m))",
   3.100 -		"  | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos",
   3.101 -		"  | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))",
   3.102 -		"  | weak stack (Closure (e, c)) = weak stack c",
   3.103 -		"  | weak stack clos = lookup stack clos",
   3.104 -		"and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))",
   3.105 -		"  | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b",
   3.106 -		"  | weak_last stack c = (stack, c)",
   3.107 +		"",
   3.108 +		"type state = bool * stack * term",
   3.109 +		"",
   3.110 +		"datatype loopstate = Continue of state | Stop of stack * term",
   3.111 +		"",
   3.112 +		"fun proj_C (Continue s) = s",
   3.113 +		"  | proj_C _ = raise Match",
   3.114 +		"",
   3.115 +		"fun proj_S (Stop s) = s",
   3.116 +		"  | proj_S _ = raise Match",
   3.117 +		"",
   3.118 +		"fun cont (Continue _) = true",
   3.119 +		"  | cont _ = false",
   3.120  		"",
   3.121 -		"fun lift n (v as Var m) = if m < n then v else Var (m+1)",
   3.122 -		"  | lift n (Abs t) = Abs (lift (n+1) t)",
   3.123 -		"  | lift n (App (a,b)) = App (lift n a, lift n b)",
   3.124 -		"  | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)",
   3.125 -		"  | lift n c = c",
   3.126 -		"and lift_env n e = map (lift n) e",
   3.127 +		"fun do_reduction reduce p =",
   3.128 +		"    let",
   3.129 +		"       val s = ref (Continue p)",
   3.130 +		"       val _ = while cont (!s) do (s := reduce (proj_C (!s)))",
   3.131 +		"   in",
   3.132 +		"       proj_S (!s)",
   3.133 +		"   end",
   3.134 +		""]
   3.135 +
   3.136 +	val _ = writelist [
   3.137 +		"fun weak_reduce (false, stack, Closure (e, App (a, b))) = Continue (false, SAppL (Closure (e, b), stack), Closure (e, a))",
   3.138 +		"  | weak_reduce (false, SAppL (b, stack), Closure (e, Abs m)) = Continue (false, stack, Closure (b::e, m))",
   3.139 +		"  | weak_reduce (false, stack, c as Closure (e, Abs m)) = Continue (true, stack, c)",
   3.140 +		"  | weak_reduce (false, stack, Closure (e, Var n)) = Continue (false, stack, case "^sname^".list_nth (e, n) of Dummy => Var n | r => r)",
   3.141 +		"  | weak_reduce (false, stack, Closure (e, c)) = Continue (false, stack, c)"]
   3.142 +	val _ = writelist (map print_rule prog)
   3.143 +        val _ = writelist [
   3.144 +		"  | weak_reduce (false, stack, clos) = Continue (true, stack, clos)",
   3.145 +		"  | weak_reduce (true, SAppR (a, stack), b) = Continue (false, stack, App (a,b))",
   3.146 +		"  | weak_reduce (true, s as (SAppL (b, stack)), a) = Continue (false, SAppR (a, stack), b)",
   3.147 +		"  | weak_reduce (true, stack, c) = Stop (stack, c)",
   3.148  		"",
   3.149 -		"fun strong stack (Closure (e, Abs m)) = ",
   3.150 +		"fun strong_reduce (false, stack, Closure (e, Abs m)) =",
   3.151  		"    let",
   3.152 -		"      val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))",
   3.153 +		"        val (stack', wnf) = do_reduction weak_reduce (false, SEmpty, Closure (Dummy::e, m))",
   3.154  		"    in",
   3.155 -		"      case stack' of",
   3.156 -		"           SEmpty => strong (SAbs stack) wnf",
   3.157 -		"         | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
   3.158 -		"    end",
   3.159 -		"  | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u",
   3.160 -		"  | strong stack clos = strong_last stack clos",
   3.161 -		"and strong_last (SAbs stack) m = strong stack (Abs m)",
   3.162 -		"  | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b",
   3.163 -		"  | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))",
   3.164 -		"  | strong_last stack clos = (stack, clos)",
   3.165 +		"        case stack' of",
   3.166 +		"            SEmpty => Continue (false, SAbs stack, wnf)",
   3.167 +		"          | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
   3.168 +		"    end",		
   3.169 +		"  | strong_reduce (false, stack, clos as (App (u, v))) = Continue (false, SAppL (v, stack), u)",
   3.170 +		"  | strong_reduce (false, stack, clos) = Continue (true, stack, clos)",
   3.171 +		"  | strong_reduce (true, SAbs stack, m) = Continue (false, stack, Abs m)",
   3.172 +		"  | strong_reduce (true, SAppL (b, stack), a) = Continue (false, SAppR (a, stack), b)",
   3.173 +		"  | strong_reduce (true, SAppR (a, stack), b) = Continue (true, stack, App (a, b))",
   3.174 +		"  | strong_reduce (true, stack, clos) = Stop (stack, clos)",
   3.175  		""]
   3.176  	
   3.177  	val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"						  	
   3.178 @@ -180,23 +163,24 @@
   3.179  		"  | importTerm ("^sname^".Abs m) = Abs (importTerm m)",
   3.180  		""]
   3.181  
   3.182 -	fun ec c = "  | exportTerm c"^(str c)^" = "^sname^".CConst "^(str c)
   3.183 +	fun ec c = "  | exportTerm c"^(str c)^" = "^sname^".Const "^(str c)
   3.184  	val _ = writelist [
   3.185 -		"fun exportTerm (Var x) = "^sname^".CVar x",
   3.186 -		"  | exportTerm (Const c) = "^sname^".CConst c",
   3.187 -		"  | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)",
   3.188 -		"  | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)",
   3.189 -		"  | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"]
   3.190 +		"fun exportTerm (Var x) = "^sname^".Var x",
   3.191 +		"  | exportTerm (Const c) = "^sname^".Const c",
   3.192 +		"  | exportTerm (App (a,b)) = "^sname^".App (exportTerm a, exportTerm b)",
   3.193 +		"  | exportTerm (Abs m) = "^sname^".Abs (exportTerm m)",
   3.194 +		"  | exportTerm (Closure (closlist, clos)) = raise ("^sname^".Run \"internal error, cannot export Closure\")",
   3.195 +		"  | exportTerm Dummy = raise ("^sname^".Run \"internal error, cannot export Dummy\")"]
   3.196  	val _ = writelist (map ec constants)
   3.197  		
   3.198  	val _ = writelist [
   3.199  		"",
   3.200  		"fun rewrite t = ",
   3.201  		"    let",
   3.202 -		"      val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))",
   3.203 +		"      val (stack, wnf) = do_reduction weak_reduce (false, SEmpty, Closure ([], importTerm t))",
   3.204  		"    in",
   3.205  		"      case stack of ",
   3.206 -		"           SEmpty => (case strong SEmpty wnf of",
   3.207 +		"           SEmpty => (case do_reduction strong_reduce (false, SEmpty, wnf) of",
   3.208  		"                          (SEmpty, snf) => exportTerm snf",
   3.209  		"                        | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",
   3.210  		"         | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",
   3.211 @@ -206,33 +190,29 @@
   3.212  		"",
   3.213  		"end;"]
   3.214  
   3.215 -	val _ = 
   3.216 -	    let
   3.217 -		(*val fout = TextIO.openOut "gen_code.ML"
   3.218 -		val _ = TextIO.output (fout, !buffer)
   3.219 -		val _  = TextIO.closeOut fout*)
   3.220 -	    in
   3.221 -		()
   3.222 -	    end
   3.223      in
   3.224  	compiled_rewriter := NONE;	
   3.225  	use_text "" Output.ml_output false (!buffer);
   3.226  	case !compiled_rewriter of 
   3.227  	    NONE => raise (Compile "cannot communicate with compiled function")
   3.228 -	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
   3.229 +	  | SOME r => (compiled_rewriter := NONE; r)
   3.230      end	
   3.231  
   3.232  fun compile eqs = 
   3.233      let
   3.234 +	val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
   3.235 +	val eqs = map (fn (a,b,c) => (b,c)) eqs
   3.236 +	fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule") 
   3.237  	val _ = map (fn (p, r) => 
   3.238 -                  (check_freevars (count_patternvars p) r; 
   3.239 -                   case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs
   3.240 +                  (check (p, r); 
   3.241 +                   case p of PVar => raise (Compile "pattern is just a variable") | _ => ())) eqs
   3.242      in
   3.243  	load_rules "AM_Compiler" "AM_compiled_code" eqs
   3.244      end	
   3.245  
   3.246  fun run prog t = (prog t)
   3.247 +
   3.248 +fun discard p = ()
   3.249  			 	  
   3.250  end
   3.251  
   3.252 -structure AbstractMachine = AM_Compiler
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/Compute_Oracle/am_ghc.ML	Mon Jul 09 17:36:25 2007 +0200
     4.3 @@ -0,0 +1,334 @@
     4.4 +(*  Title:      Pure/Tools/am_ghc.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Steven Obua
     4.7 +*)
     4.8 +
     4.9 +structure AM_GHC : ABSTRACT_MACHINE = struct
    4.10 +
    4.11 +open AbstractMachine;
    4.12 +
    4.13 +type program = string * string * (int Inttab.table)
    4.14 +
    4.15 +
    4.16 +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
    4.17 +  check_freevars 0 t iff t is closed*)
    4.18 +fun check_freevars free (Var x) = x < free
    4.19 +  | check_freevars free (Const c) = true
    4.20 +  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    4.21 +  | check_freevars free (Abs m) = check_freevars (free+1) m
    4.22 +
    4.23 +fun count_patternvars PVar = 1
    4.24 +  | count_patternvars (PConst (_, ps)) =
    4.25 +      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    4.26 +
    4.27 +fun update_arity arity code a = 
    4.28 +    (case Inttab.lookup arity code of
    4.29 +	 NONE => Inttab.update_new (code, a) arity
    4.30 +       | SOME a' => if a > a' then Inttab.update (code, a) arity else arity)
    4.31 +
    4.32 +(* We have to find out the maximal arity of each constant *)
    4.33 +fun collect_pattern_arity PVar arity = arity
    4.34 +  | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
    4.35 + 
    4.36 +local
    4.37 +fun collect applevel (Var _) arity = arity
    4.38 +  | collect applevel (Const c) arity = update_arity arity c applevel
    4.39 +  | collect applevel (Abs m) arity = collect 0 m arity
    4.40 +  | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
    4.41 +in
    4.42 +fun collect_term_arity t arity = collect 0 t arity
    4.43 +end
    4.44 +
    4.45 +fun nlift level n (Var m) = if m < level then Var m else Var (m+n) 
    4.46 +  | nlift level n (Const c) = Const c
    4.47 +  | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
    4.48 +  | nlift level n (Abs b) = Abs (nlift (level+1) n b)
    4.49 +
    4.50 +fun rep n x = if n = 0 then [] else x::(rep (n-1) x)
    4.51 +
    4.52 +fun adjust_rules rules =
    4.53 +    let
    4.54 +	val arity = fold (fn (p, t) => fn arity => collect_term_arity t (collect_pattern_arity p arity)) rules Inttab.empty
    4.55 +	fun arity_of c = the (Inttab.lookup arity c)
    4.56 +	fun adjust_pattern PVar = PVar
    4.57 +	  | 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
    4.58 +	fun adjust_rule (PVar, t) = raise Compile ("pattern may not be a variable")
    4.59 +	  | adjust_rule (rule as (p as PConst (c, args),t)) = 
    4.60 +	    let
    4.61 +		val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else () 
    4.62 +		val args = map adjust_pattern args	        
    4.63 +		val len = length args
    4.64 +		val arity = arity_of c
    4.65 +		fun lift level n (Var m) = if m < level then Var m else Var (m+n) 
    4.66 +		  | lift level n (Const c) = Const c
    4.67 +		  | lift level n (App (a,b)) = App (lift level n a, lift level n b)
    4.68 +		  | lift level n (Abs b) = Abs (lift (level+1) n b)
    4.69 +		val lift = lift 0
    4.70 +		fun adjust_term n t = if n=0 then t else adjust_term (n-1) (App (t, Var (n-1))) 
    4.71 +	    in
    4.72 +		if len = arity then
    4.73 +		    rule
    4.74 +		else if arity >= len then  
    4.75 +		    (PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) (lift (arity-len) t))
    4.76 +		else (raise Compile "internal error in adjust_rule")
    4.77 +	    end
    4.78 +    in
    4.79 +	(arity, map adjust_rule rules)
    4.80 +    end		    
    4.81 +
    4.82 +fun print_term arity_of n =
    4.83 +let
    4.84 +    fun str x = string_of_int x
    4.85 +    fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
    4.86 +											  
    4.87 +    fun print_apps d f [] = f
    4.88 +      | print_apps d f (a::args) = print_apps d ("app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
    4.89 +    and print_call d (App (a, b)) args = print_call d a (b::args) 
    4.90 +      | print_call d (Const c) args = 
    4.91 +	(case arity_of c of 
    4.92 +	     NONE => print_apps d ("Const "^(str c)) args 
    4.93 +	   | SOME a =>
    4.94 +	     let
    4.95 +		 val len = length args
    4.96 +	     in
    4.97 +		 if a <= len then 
    4.98 +		     let
    4.99 +			 val s = "c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
   4.100 +		     in
   4.101 +			 print_apps d s (List.drop (args, a))
   4.102 +		     end
   4.103 +		 else 
   4.104 +		     let
   4.105 +			 fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n-1)))
   4.106 +			 fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
   4.107 +			 fun append_args [] t = t
   4.108 +			   | append_args (c::cs) t = append_args cs (App (t, c))
   4.109 +		     in
   4.110 +			 print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
   4.111 +		     end
   4.112 +	     end)
   4.113 +      | print_call d t args = print_apps d (print_term d t) args
   4.114 +    and print_term d (Var x) = if x < d then "b"^(str (d-x-1)) else "x"^(str (n-(x-d)-1))
   4.115 +      | print_term d (Abs c) = "Abs (\\b"^(str d)^" -> "^(print_term (d + 1) c)^")"
   4.116 +      | print_term d t = print_call d t []
   4.117 +in
   4.118 +    print_term 0 
   4.119 +end
   4.120 +			 			
   4.121 +fun print_rule arity_of (p, t) = 
   4.122 +    let	
   4.123 +	fun str x = Int.toString x		    
   4.124 +	fun print_pattern top n PVar = (n+1, "x"^(str n))
   4.125 +	  | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c))
   4.126 +	  | print_pattern top n (PConst (c, args)) = 
   4.127 +	    let
   4.128 +		val (n,s) = print_pattern_list (n, (if top then "c" else "C")^(str c)) args
   4.129 +	    in
   4.130 +		(n, if top then s else "("^s^")")
   4.131 +	    end
   4.132 +	and print_pattern_list r [] = r
   4.133 +	  | print_pattern_list (n, p) (t::ts) = 
   4.134 +	    let
   4.135 +		val (n, t) = print_pattern false n t
   4.136 +	    in
   4.137 +		print_pattern_list (n, p^" "^t) ts
   4.138 +	    end
   4.139 +	val (n, pattern) = print_pattern true 0 p
   4.140 +    in
   4.141 +	pattern^" = "^(print_term arity_of n t)	
   4.142 +    end
   4.143 +
   4.144 +fun group_rules rules =
   4.145 +    let
   4.146 +	fun add_rule (r as (PConst (c,_), _)) groups =
   4.147 +	    let
   4.148 +		val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
   4.149 +	    in
   4.150 +		Inttab.update (c, r::rs) groups
   4.151 +	    end
   4.152 +	  | add_rule _ _ = raise Compile "internal error group_rules"
   4.153 +    in
   4.154 +	fold_rev add_rule rules Inttab.empty
   4.155 +    end
   4.156 +
   4.157 +fun haskell_prog name rules = 
   4.158 +    let
   4.159 +	val buffer = ref ""
   4.160 +	fun write s = (buffer := (!buffer)^s)
   4.161 +	fun writeln s = (write s; write "\n")
   4.162 +	fun writelist [] = ()
   4.163 +	  | writelist (s::ss) = (writeln s; writelist ss)
   4.164 +	fun str i = Int.toString i
   4.165 +	val (arity, rules) = adjust_rules rules
   4.166 +	val rules = group_rules rules
   4.167 +	val constants = Inttab.keys arity
   4.168 +	fun arity_of c = Inttab.lookup arity c
   4.169 +	fun rep_str s n = concat (rep n s)
   4.170 +	fun indexed s n = s^(str n)
   4.171 +	fun section n = if n = 0 then [] else (section (n-1))@[n-1]
   4.172 +	fun make_show c = 
   4.173 +	    let
   4.174 +		val args = section (the (arity_of c))
   4.175 +	    in
   4.176 +		"  show ("^(indexed "C" c)^(concat (map (indexed " a") args))^") = "
   4.177 +		^"\""^(indexed "C" c)^"\""^(concat (map (fn a => "++(show "^(indexed "a" a)^")") args))
   4.178 +	    end
   4.179 +	fun default_case c = 
   4.180 +	    let
   4.181 +		val args = concat (map (indexed " x") (section (the (arity_of c))))
   4.182 +	    in
   4.183 +		(indexed "c" c)^args^" = "^(indexed "C" c)^args
   4.184 +	    end
   4.185 +	val _ = writelist [        
   4.186 +		"module "^name^" where",
   4.187 +		"",
   4.188 +		"data Term = Const Integer | App Term Term | Abs (Term -> Term)",
   4.189 +		"         "^(concat (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
   4.190 +		"",
   4.191 +		"instance Show Term where"]
   4.192 +	val _ = writelist (map make_show constants)
   4.193 +	val _ = writelist [
   4.194 +		"  show (Const c) = \"c\"++(show c)",
   4.195 +		"  show (App a b) = \"A\"++(show a)++(show b)",
   4.196 +		"  show (Abs _) = \"L\"",
   4.197 +		""]
   4.198 +	val _ = writelist [
   4.199 +		"app (Abs a) b = a b",
   4.200 +		"app a b = App a b",
   4.201 +		"",
   4.202 +		"calc s c = writeFile s (show c)",
   4.203 +		""]
   4.204 +	fun list_group c = (writelist (case Inttab.lookup rules c of 
   4.205 +					   NONE => [default_case c, ""] 
   4.206 +					 | SOME (rs as ((PConst (_, []), _)::rs')) => 
   4.207 +					   if not (null rs') then raise Compile "multiple declaration of constant"
   4.208 +					   else (map (print_rule arity_of) rs) @ [""]
   4.209 +					 | SOME rs => (map (print_rule arity_of) rs) @ [default_case c, ""]))
   4.210 +	val _ = map list_group constants
   4.211 +    in
   4.212 +	(arity, !buffer)
   4.213 +    end
   4.214 +
   4.215 +val guid_counter = ref 0
   4.216 +fun get_guid () = 
   4.217 +    let
   4.218 +	val c = !guid_counter
   4.219 +	val _ = guid_counter := !guid_counter + 1
   4.220 +    in
   4.221 +	(LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
   4.222 +    end
   4.223 +
   4.224 +fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
   4.225 +fun wrap s = "\""^s^"\""
   4.226 +
   4.227 +fun writeTextFile name s = File.write (Path.explode name) s
   4.228 +    
   4.229 +val ghc = ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
   4.230 +
   4.231 +fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
   4.232 +
   4.233 +fun compile eqs = 
   4.234 +    let
   4.235 +	val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
   4.236 +	val eqs = map (fn (a,b,c) => (b,c)) eqs
   4.237 +	val guid = get_guid ()
   4.238 +	val module = "AMGHC_Prog_"^guid
   4.239 +	val (arity, source) = haskell_prog module eqs
   4.240 +	val module_file = tmp_file (module^".hs")
   4.241 +	val object_file = tmp_file (module^".o")
   4.242 +	val _ = writeTextFile module_file source
   4.243 +	val _ = system ((!ghc)^" -c "^module_file)
   4.244 +	val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
   4.245 +    in
   4.246 +	(guid, module_file, arity)	
   4.247 +    end
   4.248 +
   4.249 +fun readResultFile name = File.read (Path.explode name) 
   4.250 +			  			  			      			    
   4.251 +fun parse_result arity_of result =
   4.252 +    let
   4.253 +	val result = String.explode result
   4.254 +	fun shift NONE x = SOME x
   4.255 +	  | shift (SOME y) x = SOME (y*10 + x)
   4.256 +	fun parse_int' x (#"0"::rest) = parse_int' (shift x 0) rest
   4.257 +	  | parse_int' x (#"1"::rest) = parse_int' (shift x 1) rest
   4.258 +	  | parse_int' x (#"2"::rest) = parse_int' (shift x 2) rest
   4.259 +	  | parse_int' x (#"3"::rest) = parse_int' (shift x 3) rest
   4.260 +	  | parse_int' x (#"4"::rest) = parse_int' (shift x 4) rest
   4.261 +	  | parse_int' x (#"5"::rest) = parse_int' (shift x 5) rest
   4.262 +	  | parse_int' x (#"6"::rest) = parse_int' (shift x 6) rest
   4.263 +	  | parse_int' x (#"7"::rest) = parse_int' (shift x 7) rest
   4.264 +	  | parse_int' x (#"8"::rest) = parse_int' (shift x 8) rest
   4.265 +	  | parse_int' x (#"9"::rest) = parse_int' (shift x 9) rest
   4.266 +	  | parse_int' x rest = (x, rest)
   4.267 +	fun parse_int rest = parse_int' NONE rest
   4.268 +
   4.269 +	fun parse (#"C"::rest) = 
   4.270 +	    (case parse_int rest of 
   4.271 +		 (SOME c, rest) => 
   4.272 +		 let
   4.273 +		     val (args, rest) = parse_list (the (arity_of c)) rest
   4.274 +		     fun app_args [] t = t
   4.275 +		       | app_args (x::xs) t = app_args xs (App (t, x))
   4.276 +		 in
   4.277 +		     (app_args args (Const c), rest)
   4.278 +		 end		     
   4.279 +	       | (NONE, rest) => raise Run "parse C")
   4.280 +	  | parse (#"c"::rest) = 
   4.281 +	    (case parse_int rest of
   4.282 +		 (SOME c, rest) => (Const c, rest)
   4.283 +	       | _ => raise Run "parse c")
   4.284 +	  | parse (#"A"::rest) = 
   4.285 +	    let
   4.286 +		val (a, rest) = parse rest
   4.287 +		val (b, rest) = parse rest
   4.288 +	    in
   4.289 +		(App (a,b), rest)
   4.290 +	    end
   4.291 +	  | parse (#"L"::rest) = raise Run "there may be no abstraction in the result"
   4.292 +	  | parse _ = raise Run "invalid result"
   4.293 +	and parse_list n rest = 
   4.294 +	    if n = 0 then 
   4.295 +		([], rest) 
   4.296 +	    else 
   4.297 +		let 
   4.298 +		    val (x, rest) = parse rest
   4.299 +		    val (xs, rest) = parse_list (n-1) rest
   4.300 +		in
   4.301 +		    (x::xs, rest)
   4.302 +		end
   4.303 +	val (parsed, rest) = parse result
   4.304 +	fun is_blank (#" "::rest) = is_blank rest
   4.305 +	  | is_blank (#"\n"::rest) = is_blank rest
   4.306 +	  | is_blank [] = true
   4.307 +	  | is_blank _ = false
   4.308 +    in
   4.309 +	if is_blank rest then parsed else raise Run "non-blank suffix in result file"	
   4.310 +    end
   4.311 +
   4.312 +fun run (guid, module_file, arity) t = 
   4.313 +    let
   4.314 +	val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
   4.315 +	fun arity_of c = Inttab.lookup arity c			 
   4.316 +	val callguid = get_guid()
   4.317 +	val module = "AMGHC_Prog_"^guid
   4.318 +	val call = module^"_Call_"^callguid
   4.319 +	val result_file = tmp_file (module^"_Result_"^callguid^".txt")
   4.320 +	val call_file = tmp_file (call^".hs")
   4.321 +	val term = print_term arity_of 0 t
   4.322 +	val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
   4.323 +	val _ = writeTextFile call_file call_source
   4.324 +	val _ = system ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
   4.325 +	val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
   4.326 +	val t' = parse_result arity_of result
   4.327 +	val _ = OS.FileSys.remove call_file
   4.328 +	val _ = OS.FileSys.remove result_file
   4.329 +    in
   4.330 +	t'
   4.331 +    end
   4.332 +
   4.333 +	
   4.334 +fun discard _ = ()
   4.335 +		 	  
   4.336 +end
   4.337 +
     5.1 --- a/src/Tools/Compute_Oracle/am_interpreter.ML	Mon Jul 09 11:44:23 2007 +0200
     5.2 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Mon Jul 09 17:36:25 2007 +0200
     5.3 @@ -1,32 +1,13 @@
     5.4 -(*  Title:      Tools/Compute_Oracle/am_interpreter.ML
     5.5 +(*  Title:      Pure/Tools/am_interpreter.ML
     5.6      ID:         $Id$
     5.7      Author:     Steven Obua
     5.8  *)
     5.9  
    5.10 -signature ABSTRACT_MACHINE =
    5.11 -sig
    5.12 -
    5.13 -datatype term = Var of int | Const of int | App of term * term | Abs of term
    5.14 -
    5.15 -datatype pattern = PVar | PConst of int * (pattern list)
    5.16 -
    5.17 -type program
    5.18 -
    5.19 -exception Compile of string;
    5.20 -val compile : (pattern * term) list -> program
    5.21 -
    5.22 -exception Run of string;
    5.23 -val run : program -> term -> term
    5.24 -
    5.25 -end
    5.26 -
    5.27  structure AM_Interpreter : ABSTRACT_MACHINE = struct
    5.28  
    5.29 -datatype term = Var of int | Const of int | App of term * term | Abs of term
    5.30 +open AbstractMachine;
    5.31  
    5.32 -datatype pattern = PVar | PConst of int * (pattern list)
    5.33 -
    5.34 -datatype closure = CVar of int | CConst of int
    5.35 +datatype closure = CDummy | CVar of int | CConst of int
    5.36                   | CApp of closure * closure | CAbs of closure
    5.37                   | Closure of (closure list) * closure
    5.38  
    5.39 @@ -36,9 +17,6 @@
    5.40  
    5.41  datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
    5.42  
    5.43 -exception Compile of string;
    5.44 -exception Run of string;
    5.45 -
    5.46  fun clos_of_term (Var x) = CVar x
    5.47    | clos_of_term (Const c) = CConst c
    5.48    | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
    5.49 @@ -49,6 +27,7 @@
    5.50    | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
    5.51    | term_of_clos (CAbs u) = Abs (term_of_clos u)
    5.52    | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found")
    5.53 +  | term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found")
    5.54  
    5.55  fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
    5.56    | strip_closure args x = (x, args)
    5.57 @@ -78,24 +57,29 @@
    5.58        | SOME args => pattern_match_list args ps cs)
    5.59    | pattern_match_list _ _ _ = NONE
    5.60  
    5.61 -(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
    5.62 -fun check_freevars free (Var x) = x < free
    5.63 -  | check_freevars free (Const c) = true
    5.64 -  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    5.65 -  | check_freevars free (Abs m) = check_freevars (free+1) m
    5.66 -
    5.67  fun count_patternvars PVar = 1
    5.68    | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    5.69  
    5.70  fun pattern_key (PConst (c, ps)) = (c, length ps)
    5.71    | pattern_key _ = raise (Compile "pattern reduces to variable")
    5.72  
    5.73 +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
    5.74 +  check_freevars 0 t iff t is closed*)
    5.75 +fun check_freevars free (Var x) = x < free
    5.76 +  | check_freevars free (Const c) = true
    5.77 +  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    5.78 +  | check_freevars free (Abs m) = check_freevars (free+1) m
    5.79 +
    5.80  fun compile eqs =
    5.81      let
    5.82 -        val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
    5.83 -                                     (pattern_key p, (p, clos_of_term r)))) eqs
    5.84 +	val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
    5.85 +	val eqs = map (fn (a,b,c) => (b,c)) eqs
    5.86 +	fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule") 
    5.87 +        val eqs = map (fn (p, r) => (check (p,r); (pattern_key p, (p, clos_of_term r)))) eqs
    5.88 +	fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a] | SOME l => a::l) table
    5.89 +	val p = fold merge eqs prog_struct.empty 
    5.90      in
    5.91 -        Program (prog_struct.make (map (fn (k, a) => (k, [a])) eqs))
    5.92 +        Program p
    5.93      end
    5.94  
    5.95  fun match_rules n [] clos = NONE
    5.96 @@ -112,51 +96,66 @@
    5.97            | SOME rules => match_rules 0 rules clos)
    5.98        | _ => NONE
    5.99  
   5.100 -fun lift n (c as (CConst _)) = c
   5.101 -  | lift n (v as CVar m) = if m < n then v else CVar (m+1)
   5.102 -  | lift n (CAbs t) = CAbs (lift (n+1) t)
   5.103 -  | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
   5.104 -  | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
   5.105 -and lift_env n e = map (lift n) e
   5.106 +
   5.107 +type state = bool * program * stack * closure
   5.108 +
   5.109 +datatype loopstate = Continue of state | Stop of stack * closure
   5.110 +
   5.111 +fun proj_C (Continue s) = s
   5.112 +  | proj_C _ = raise Match
   5.113 +
   5.114 +fun proj_S (Stop s) = s
   5.115 +  | proj_S _ = raise Match
   5.116 +
   5.117 +fun cont (Continue _) = true
   5.118 +  | cont _ = false
   5.119  
   5.120 -fun weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
   5.121 -  | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
   5.122 -  | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
   5.123 -  | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
   5.124 -  | weak prog stack clos =
   5.125 -    case match_closure prog clos of
   5.126 -        NONE => weak_last prog stack clos
   5.127 -      | SOME r => weak prog stack r
   5.128 -and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
   5.129 -  | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
   5.130 -  | weak_last prog stack c = (stack, c)
   5.131 +fun do_reduction reduce p =
   5.132 +    let
   5.133 +	val s = ref (Continue p)
   5.134 +	val _ = while cont (!s) do (s := reduce (proj_C (!s)))
   5.135 +    in
   5.136 +	proj_S (!s)
   5.137 +    end
   5.138  
   5.139 -fun strong prog stack (Closure (e, CAbs m)) =
   5.140 +fun weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
   5.141 +  | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
   5.142 +  | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
   5.143 +  | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
   5.144 +  | weak_reduce (false, prog, stack, clos) =
   5.145 +    (case match_closure prog clos of
   5.146 +         NONE => Continue (true, prog, stack, clos)
   5.147 +       | SOME r => Continue (false, prog, stack, r))
   5.148 +  | weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
   5.149 +  | weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
   5.150 +  | weak_reduce (true, prog, stack, c) = Stop (stack, c)
   5.151 +
   5.152 +fun strong_reduce (false, prog, stack, Closure (e, CAbs m)) =
   5.153      let
   5.154 -        val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
   5.155 +        val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m))
   5.156      in
   5.157          case stack' of
   5.158 -            SEmpty => strong prog (SAbs stack) wnf
   5.159 +            SEmpty => Continue (false, prog, SAbs stack, wnf)
   5.160            | _ => raise (Run "internal error in strong: weak failed")
   5.161      end
   5.162 -  | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
   5.163 -  | strong prog stack clos = strong_last prog stack clos
   5.164 -and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
   5.165 -  | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
   5.166 -  | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
   5.167 -  | strong_last prog stack clos = (stack, clos)
   5.168 +  | strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u)
   5.169 +  | strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos)
   5.170 +  | strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m)
   5.171 +  | strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
   5.172 +  | strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b))
   5.173 +  | strong_reduce (true, prog, stack, clos) = Stop (stack, clos)
   5.174  
   5.175  fun run prog t =
   5.176      let
   5.177 -        val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
   5.178 +        val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t))
   5.179      in
   5.180          case stack of
   5.181 -            SEmpty => (case strong prog SEmpty wnf of
   5.182 +            SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of
   5.183                             (SEmpty, snf) => term_of_clos snf
   5.184                           | _ => raise (Run "internal error in run: strong failed"))
   5.185            | _ => raise (Run "internal error in run: weak failed")
   5.186      end
   5.187  
   5.188 -end
   5.189 +fun discard p = ()
   5.190  
   5.191 -structure AbstractMachine = AM_Interpreter
   5.192 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Mon Jul 09 17:36:25 2007 +0200
     6.3 @@ -0,0 +1,530 @@
     6.4 +(*  Title:      Pure/Tools/am_sml.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Steven Obua
     6.7 +
     6.8 +    ToDO: "parameterless rewrite cannot be used in pattern": In a lot of cases it CAN be used, and these cases should be handled properly; 
     6.9 +          right now, all cases throw an exception.
    6.10 + 
    6.11 +*)
    6.12 +
    6.13 +signature AM_SML = 
    6.14 +sig
    6.15 +  include ABSTRACT_MACHINE
    6.16 +  val save_result : (string * term) -> unit
    6.17 +  val set_compiled_rewriter : (term -> term) -> unit				       
    6.18 +  val list_nth : 'a list * int -> 'a
    6.19 +end
    6.20 +
    6.21 +structure AM_SML : AM_SML = struct
    6.22 +
    6.23 +open AbstractMachine;
    6.24 +
    6.25 +type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
    6.26 +
    6.27 +val saved_result = ref (NONE:(string*term)option)
    6.28 +
    6.29 +fun save_result r = (saved_result := SOME r)
    6.30 +fun clear_result () = (saved_result := NONE)
    6.31 +
    6.32 +val list_nth = List.nth
    6.33 +
    6.34 +(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
    6.35 +
    6.36 +val compiled_rewriter = ref (NONE:(term -> term)Option.option)
    6.37 +
    6.38 +fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
    6.39 +
    6.40 +fun importable (Var _) = false
    6.41 +  | importable (Const _) = true			   
    6.42 +  | importable (App (a, b)) = importable a andalso importable b
    6.43 +  | importable (Abs _) = false
    6.44 +
    6.45 +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
    6.46 +  check_freevars 0 t iff t is closed*)
    6.47 +fun check_freevars free (Var x) = x < free
    6.48 +  | check_freevars free (Const c) = true
    6.49 +  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    6.50 +  | check_freevars free (Abs m) = check_freevars (free+1) m
    6.51 +
    6.52 +fun count_patternvars PVar = 1
    6.53 +  | count_patternvars (PConst (_, ps)) =
    6.54 +      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    6.55 +
    6.56 +fun update_arity arity code a = 
    6.57 +    (case Inttab.lookup arity code of
    6.58 +	 NONE => Inttab.update_new (code, a) arity
    6.59 +       | SOME a' => if a > a' then Inttab.update (code, a) arity else arity)
    6.60 +
    6.61 +(* We have to find out the maximal arity of each constant *)
    6.62 +fun collect_pattern_arity PVar arity = arity
    6.63 +  | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
    6.64 +
    6.65 +(* We also need to find out the maximal toplevel arity of each function constant *)
    6.66 +fun collect_pattern_toplevel_arity PVar arity = raise Compile "internal error: collect_pattern_toplevel_arity"
    6.67 +  | collect_pattern_toplevel_arity (PConst (c, args)) arity = update_arity arity c (length args)
    6.68 +
    6.69 +local
    6.70 +fun collect applevel (Var _) arity = arity
    6.71 +  | collect applevel (Const c) arity = update_arity arity c applevel
    6.72 +  | collect applevel (Abs m) arity = collect 0 m arity
    6.73 +  | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
    6.74 +in
    6.75 +fun collect_term_arity t arity = collect 0 t arity
    6.76 +end
    6.77 +
    6.78 +fun collect_guard_arity (Guard (a,b)) arity  = collect_term_arity b (collect_term_arity a arity)
    6.79 +
    6.80 +
    6.81 +fun rep n x = if n < 0 then raise Compile "internal error: rep" else if n = 0 then [] else x::(rep (n-1) x)
    6.82 +
    6.83 +fun beta (Const c) = Const c
    6.84 +  | beta (Var i) = Var i
    6.85 +  | beta (App (Abs m, b)) = beta (unlift 0 (subst 0 m (lift 0 b)))
    6.86 +  | beta (App (a, b)) = 
    6.87 +    (case beta a of
    6.88 +	 Abs m => beta (App (Abs m, b))
    6.89 +       | a => App (a, beta b))
    6.90 +  | beta (Abs m) = Abs (beta m)
    6.91 +and subst x (Const c) t = Const c
    6.92 +  | subst x (Var i) t = if i = x then t else Var i
    6.93 +  | subst x (App (a,b)) t = App (subst x a t, subst x b t)
    6.94 +  | subst x (Abs m) t = Abs (subst (x+1) m (lift 0 t))
    6.95 +and lift level (Const c) = Const c
    6.96 +  | lift level (App (a,b)) = App (lift level a, lift level b)
    6.97 +  | lift level (Var i) = if i < level then Var i else Var (i+1)
    6.98 +  | lift level (Abs m) = Abs (lift (level + 1) m)
    6.99 +and unlift level (Const c) = Const c
   6.100 +  | unlift level (App (a, b)) = App (unlift level a, unlift level b)
   6.101 +  | unlift level (Abs m) = Abs (unlift (level+1) m)
   6.102 +  | unlift level (Var i) = if i < level then Var i else Var (i-1)
   6.103 +
   6.104 +fun nlift level n (Var m) = if m < level then Var m else Var (m+n) 
   6.105 +  | nlift level n (Const c) = Const c
   6.106 +  | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
   6.107 +  | nlift level n (Abs b) = Abs (nlift (level+1) n b)
   6.108 +
   6.109 +fun subst_const (c, t) (Const c') = if c = c' then t else Const c'
   6.110 +  | subst_const _ (Var i) = Var i
   6.111 +  | subst_const ct (App (a, b)) = App (subst_const ct a, subst_const ct b)
   6.112 +  | subst_const ct (Abs m) = Abs (subst_const ct m)
   6.113 +
   6.114 +(* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *)
   6.115 +fun inline_rules rules =
   6.116 +    let
   6.117 +	fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
   6.118 +	  | term_contains_const c (Abs m) = term_contains_const c m
   6.119 +	  | term_contains_const c (Var i) = false
   6.120 +	  | term_contains_const c (Const c') = (c = c')
   6.121 +	fun find_rewrite [] = NONE
   6.122 +	  | find_rewrite ((prems, PConst (c, []), r) :: _) = 
   6.123 +	    if check_freevars 0 r then 
   6.124 +		if term_contains_const c r then 
   6.125 +		    raise Compile "parameterless rewrite is caught in cycle"
   6.126 +		else if not (null prems) then
   6.127 +		    raise Compile "parameterless rewrite may not be guarded"
   6.128 +		else
   6.129 +		    SOME (c, r) 
   6.130 +	    else raise Compile "unbound variable on right hand side or guards of rule"
   6.131 +	  | find_rewrite (_ :: rules) = find_rewrite rules
   6.132 +	fun remove_rewrite (c,r) [] = []
   6.133 +	  | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = 
   6.134 +	    (if c = c' then 
   6.135 +		 if null args andalso r = r' andalso null (prems') then 
   6.136 +		     remove_rewrite cr rules 
   6.137 +		 else raise Compile "incompatible parameterless rewrites found"
   6.138 +	     else
   6.139 +		 rule :: (remove_rewrite cr rules))
   6.140 +	  | remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs)
   6.141 +	fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args)
   6.142 +	  | pattern_contains_const c (PVar) = false
   6.143 +	fun inline_rewrite (ct as (c, _)) (prems, p, r) = 
   6.144 +	    if pattern_contains_const c p then 
   6.145 +		raise Compile "parameterless rewrite cannot be used in pattern"
   6.146 +	    else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r)
   6.147 +	fun inline inlined rules =
   6.148 +	    (case find_rewrite rules of 
   6.149 +		 NONE => (Inttab.make inlined, rules)
   6.150 +	       | SOME ct => 
   6.151 +		 let
   6.152 +		     val rules = map (inline_rewrite ct) (remove_rewrite ct rules)
   6.153 +		     val inlined =  ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined)
   6.154 +		 in
   6.155 +		     inline inlined rules
   6.156 +		 end)		
   6.157 +    in
   6.158 +	inline [] rules		
   6.159 +    end
   6.160 +
   6.161 +
   6.162 +(*
   6.163 +   Calculate the arity, the toplevel_arity, and adjust rules so that all toplevel pattern constants have maximal arity.
   6.164 +   Also beta reduce the adjusted right hand side of a rule.   
   6.165 +*)
   6.166 +fun adjust_rules rules = 
   6.167 +    let
   6.168 +	val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty
   6.169 +	val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
   6.170 +	fun arity_of c = the (Inttab.lookup arity c)
   6.171 +	fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c)
   6.172 +	fun adjust_pattern PVar = PVar
   6.173 +	  | 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
   6.174 +	fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable")
   6.175 +	  | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters")
   6.176 +	  | adjust_rule (rule as (prems, p as PConst (c, args),t)) = 
   6.177 +	    let
   6.178 +		val patternvars_counted = count_patternvars p
   6.179 +		fun check_fv t = check_freevars patternvars_counted t
   6.180 +		val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else () 
   6.181 +		val _ = if not (forall (fn (Guard (a,b)) => check_fv a andalso check_fv b) prems) then raise Compile ("unbound variables in guards") else () 
   6.182 +		val args = map adjust_pattern args	        
   6.183 +		val len = length args
   6.184 +		val arity = arity_of c
   6.185 +		val lift = nlift 0
   6.186 +		fun adjust_tm n t = if n=0 then t else adjust_tm (n-1) (App (t, Var (n-1)))
   6.187 +		fun adjust_term n t = adjust_tm n (lift n t)
   6.188 +		fun adjust_guard n (Guard (a,b)) = Guard (adjust_term n a, adjust_term n b)
   6.189 +	    in
   6.190 +		if len = arity then
   6.191 +		    rule
   6.192 +		else if arity >= len then  
   6.193 +		    (map (adjust_guard (arity-len)) prems, PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) t)
   6.194 +		else (raise Compile "internal error in adjust_rule")
   6.195 +	    end
   6.196 +	fun beta_guard (Guard (a,b)) = Guard (beta a, beta b)
   6.197 +	fun beta_rule (prems, p, t) = ((map beta_guard prems, p, beta t) handle Match => raise Compile "beta_rule")
   6.198 +    in
   6.199 +	(arity, toplevel_arity, map (beta_rule o adjust_rule) rules)
   6.200 +    end		    
   6.201 +
   6.202 +fun print_term module arity_of toplevel_arity_of pattern_var_count pattern_lazy_var_count =
   6.203 +let
   6.204 +    fun str x = string_of_int x
   6.205 +    fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
   6.206 +    val module_prefix = (case module of NONE => "" | SOME s => s^".")											  
   6.207 +    fun print_apps d f [] = f
   6.208 +      | print_apps d f (a::args) = print_apps d (module_prefix^"app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
   6.209 +    and print_call d (App (a, b)) args = print_call d a (b::args) 
   6.210 +      | print_call d (Const c) args = 
   6.211 +	(case arity_of c of 
   6.212 +	     NONE => print_apps d (module_prefix^"Const "^(str c)) args 
   6.213 +	   | SOME 0 => module_prefix^"C"^(str c)
   6.214 +	   | SOME a =>
   6.215 +	     let
   6.216 +		 val len = length args
   6.217 +	     in
   6.218 +		 if a <= len then 
   6.219 +		     let
   6.220 +			 val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
   6.221 +			 val _ = if strict_a > a then raise Compile "strict" else ()
   6.222 +			 val s = module_prefix^"c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
   6.223 +			 val s = s^(concat (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
   6.224 +		     in
   6.225 +			 print_apps d s (List.drop (args, a))
   6.226 +		     end
   6.227 +		 else 
   6.228 +		     let
   6.229 +			 fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n - 1)))
   6.230 +			 fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
   6.231 +			 fun append_args [] t = t
   6.232 +			   | append_args (c::cs) t = append_args cs (App (t, c))
   6.233 +		     in
   6.234 +			 print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
   6.235 +		     end
   6.236 +	     end)
   6.237 +      | print_call d t args = print_apps d (print_term d t) args
   6.238 +    and print_term d (Var x) = 
   6.239 +	if x < d then 
   6.240 +	    "b"^(str (d-x-1)) 
   6.241 +	else 
   6.242 +	    let
   6.243 +		val n = pattern_var_count - (x-d) - 1
   6.244 +		val x = "x"^(str n)
   6.245 +	    in
   6.246 +		if n < pattern_var_count - pattern_lazy_var_count then 
   6.247 +		    x
   6.248 +		else 
   6.249 +		    "("^x^" ())"
   6.250 +	    end								
   6.251 +      | print_term d (Abs c) = module_prefix^"Abs (fn b"^(str d)^" => "^(print_term (d + 1) c)^")"
   6.252 +      | print_term d t = print_call d t []
   6.253 +in
   6.254 +    print_term 0 
   6.255 +end
   6.256 +
   6.257 +fun section n = if n = 0 then [] else (section (n-1))@[n-1]
   6.258 +			 			
   6.259 +fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) = 
   6.260 +    let	
   6.261 +	fun str x = Int.toString x		    
   6.262 +	fun print_pattern top n PVar = (n+1, "x"^(str n))
   6.263 +	  | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else ""))
   6.264 +	  | print_pattern top n (PConst (c, args)) = 
   6.265 +	    let
   6.266 +		val f = (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "")
   6.267 +		val (n, s) = print_pattern_list 0 top (n, f) args
   6.268 +	    in
   6.269 +		(n, s)
   6.270 +	    end
   6.271 +	and print_pattern_list' counter top (n,p) [] = if top then (n,p) else (n,p^")")
   6.272 +	  | print_pattern_list' counter top (n, p) (t::ts) = 
   6.273 +	    let
   6.274 +		val (n, t) = print_pattern false n t
   6.275 +	    in
   6.276 +		print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^", "^t) ts
   6.277 +	    end	
   6.278 +	and print_pattern_list counter top (n, p) (t::ts) = 
   6.279 +	    let
   6.280 +		val (n, t) = print_pattern false n t
   6.281 +	    in
   6.282 +		print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^" ("^t) ts
   6.283 +	    end
   6.284 +	val c = (case p of PConst (c, _) => c | _ => raise Match)
   6.285 +	val (n, pattern) = print_pattern true 0 p
   6.286 +	val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
   6.287 +	fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
   6.288 +        fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
   6.289 +	val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(concat (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
   6.290 +	fun print_guards t [] = print_tm t
   6.291 +	  | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(concat (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
   6.292 +    in
   6.293 +	(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
   6.294 +    end
   6.295 +
   6.296 +fun group_rules rules =
   6.297 +    let
   6.298 +	fun add_rule (r as (_, PConst (c,_), _)) groups =
   6.299 +	    let
   6.300 +		val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
   6.301 +	    in
   6.302 +		Inttab.update (c, r::rs) groups
   6.303 +	    end
   6.304 +	  | add_rule _ _ = raise Compile "internal error group_rules"
   6.305 +    in
   6.306 +	fold_rev add_rule rules Inttab.empty
   6.307 +    end
   6.308 +
   6.309 +fun sml_prog name code rules = 
   6.310 +    let
   6.311 +	val buffer = ref ""
   6.312 +	fun write s = (buffer := (!buffer)^s)
   6.313 +	fun writeln s = (write s; write "\n")
   6.314 +	fun writelist [] = ()
   6.315 +	  | writelist (s::ss) = (writeln s; writelist ss)
   6.316 +	fun str i = Int.toString i
   6.317 +	val (inlinetab, rules) = inline_rules rules
   6.318 +	val (arity, toplevel_arity, rules) = adjust_rules rules
   6.319 +	val rules = group_rules rules
   6.320 +	val constants = Inttab.keys arity
   6.321 +	fun arity_of c = Inttab.lookup arity c
   6.322 +	fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
   6.323 +	fun rep_str s n = concat (rep n s)
   6.324 +	fun indexed s n = s^(str n)
   6.325 +        fun string_of_tuple [] = ""
   6.326 +	  | string_of_tuple (x::xs) = "("^x^(concat (map (fn s => ", "^s) xs))^")"
   6.327 +        fun string_of_args [] = ""
   6.328 +	  | string_of_args (x::xs) = x^(concat (map (fn s => " "^s) xs))
   6.329 +	fun default_case gnum c = 
   6.330 +	    let
   6.331 +		val leftargs = concat (map (indexed " x") (section (the (arity_of c))))
   6.332 +		val rightargs = section (the (arity_of c))
   6.333 +		val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa)
   6.334 +		val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs
   6.335 +		val right = (indexed "C" c)^" "^(string_of_tuple xs)
   6.336 +		val debug_lazy = "(print x"^(string_of_int (strict_args - 1))^";"
   6.337 +		val right = if strict_args < the (arity_of c) then debug_lazy^"raise AM_SML.Run \"unresolved lazy call: "^(string_of_int c)^"\")" else right		
   6.338 +	    in
   6.339 +		(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right
   6.340 +	    end
   6.341 +
   6.342 +	fun eval_rules c = 
   6.343 +	    let
   6.344 +		val arity = the (arity_of c)
   6.345 +		val strict_arity = (case toplevel_arity_of c of NONE => arity | SOME sa => sa)
   6.346 +		fun eval_rule n = 
   6.347 +		    let
   6.348 +			val sc = string_of_int c
   6.349 +			val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section n) ("AbstractMachine.Const "^sc)
   6.350 +                        fun arg i = 
   6.351 +			    let
   6.352 +				val x = indexed "x" i
   6.353 +				val x = if i < n then "(eval bounds "^x^")" else x
   6.354 +				val x = if i < strict_arity then x else "(fn () => "^x^")"
   6.355 +			    in
   6.356 +				x
   6.357 +			    end
   6.358 +			val right = "c"^sc^" "^(string_of_args (map arg (section arity)))
   6.359 +			val right = fold_rev (fn i => fn s => "Abs (fn "^(indexed "x" i)^" => "^s^")") (List.drop (section arity, n)) right		
   6.360 +			val right = if arity > 0 then right else "C"^sc
   6.361 +		    in
   6.362 +			"  | eval bounds ("^left^") = "^right
   6.363 +		    end
   6.364 +	    in
   6.365 +		map eval_rule (rev (section (arity + 1)))
   6.366 +	    end
   6.367 +        
   6.368 +	fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else ""
   6.369 +	val _ = writelist [        
   6.370 +		"structure "^name^" = struct",
   6.371 +		"",
   6.372 +		"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
   6.373 +		"         "^(concat (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
   6.374 +		""]
   6.375 +	fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
   6.376 +	fun make_term_eq c = "  | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
   6.377 +                             (case the (arity_of c) of 
   6.378 +				  0 => "true"
   6.379 +				| n => 
   6.380 +				  let 
   6.381 +				      val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
   6.382 +				      val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
   6.383 +				  in
   6.384 +				      eq^(concat eqs)
   6.385 +				  end)
   6.386 +	val _ = writelist [
   6.387 +		"fun term_eq (Const c1) (Const c2) = (c1 = c2)",
   6.388 +		"  | term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"]
   6.389 +	val _ = writelist (map make_term_eq constants)		
   6.390 +	val _ = writelist [
   6.391 +		"  | term_eq _ _ = false",
   6.392 +                "" 
   6.393 +		] 
   6.394 +	val _ = writelist [
   6.395 +		"fun app (Abs a) b = a b",
   6.396 +		"  | app a b = App (a, b)",
   6.397 +		""]	
   6.398 +	fun defcase gnum c = (case arity_of c of NONE => [] | SOME a => if a > 0 then [default_case gnum c] else [])
   6.399 +	fun writefundecl [] = () 
   6.400 +	  | writefundecl (x::xs) = writelist ((("and "^x)::(map (fn s => "  | "^s) xs)))
   6.401 +	fun list_group c = (case Inttab.lookup rules c of 
   6.402 +				NONE => [defcase 0 c]
   6.403 +			      | SOME rs => 
   6.404 +				let
   6.405 +				    val rs = 
   6.406 +					fold
   6.407 +					    (fn r => 
   6.408 +					     fn rs =>
   6.409 +						let 
   6.410 +						    val (gnum, l, rs) = 
   6.411 +							(case rs of 
   6.412 +							     [] => (0, [], []) 
   6.413 +							   | (gnum, l)::rs => (gnum, l, rs))
   6.414 +						    val (gnum', r) = print_rule gnum arity_of toplevel_arity_of r 
   6.415 +						in 
   6.416 +						    if gnum' = gnum then 
   6.417 +							(gnum, r::l)::rs
   6.418 +						    else
   6.419 +							let
   6.420 +							    val args = concat (map (fn i => " a"^(str i)) (section (the (arity_of c))))
   6.421 +							    fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
   6.422 +							    val s = gnumc (gnum) ^ " = " ^ gnumc (gnum') 
   6.423 +							in
   6.424 +							    (gnum', [])::(gnum, s::r::l)::rs
   6.425 +							end
   6.426 +						end)
   6.427 +					rs []
   6.428 +				    val rs = (case rs of [] => [(0,defcase 0 c)] | (gnum,l)::rs => (gnum, (defcase gnum c)@l)::rs)
   6.429 +				in
   6.430 +				    rev (map (fn z => rev (snd z)) rs)
   6.431 +				end)
   6.432 +	val _ = map (fn z => (map writefundecl z; writeln "")) (map list_group constants)
   6.433 +	val _ = writelist [
   6.434 +		"fun convert (Const i) = AM_SML.Const i",
   6.435 +		"  | convert (App (a, b)) = AM_SML.App (convert a, convert b)",
   6.436 +                "  | convert (Abs _) = raise AM_SML.Run \"no abstraction in result allowed\""]	
   6.437 +	fun make_convert c = 
   6.438 +	    let
   6.439 +		val args = map (indexed "a") (section (the (arity_of c)))
   6.440 +		val leftargs = 
   6.441 +		    case args of
   6.442 +			[] => ""
   6.443 +		      | (x::xs) => "("^x^(concat (map (fn s => ", "^s) xs))^")"
   6.444 +		val args = map (indexed "convert a") (section (the (arity_of c)))
   6.445 +		val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
   6.446 +	    in
   6.447 +		"  | convert (C"^(str c)^" "^leftargs^") = "^right
   6.448 +	    end 		
   6.449 +	val _ = writelist (map make_convert constants)
   6.450 +	val _ = writelist [
   6.451 +		"",
   6.452 +		"fun eval bounds (AbstractMachine.Abs m) = Abs (fn b => eval (b::bounds) m)",
   6.453 +		"  | eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"]
   6.454 +	val _ = map (writelist o eval_rules) constants
   6.455 +	val _ = writelist [
   6.456 +                "  | eval bounds (AbstractMachine.App (a, b)) = app (eval bounds a) (eval bounds b)",
   6.457 +                "  | eval bounds (AbstractMachine.Const c) = Const c"]                
   6.458 +	val _ = writelist [		
   6.459 +		"",
   6.460 +		"fun export term = AM_SML.save_result (\""^code^"\", convert term)",
   6.461 +		"",
   6.462 +                "val _ = AM_SML.set_compiled_rewriter (fn t => convert (eval [] t))",
   6.463 +                "",
   6.464 +		"end"]
   6.465 +    in
   6.466 +	(arity, toplevel_arity, inlinetab, !buffer)
   6.467 +    end
   6.468 +
   6.469 +val guid_counter = ref 0
   6.470 +fun get_guid () = 
   6.471 +    let
   6.472 +	val c = !guid_counter
   6.473 +	val _ = guid_counter := !guid_counter + 1
   6.474 +    in
   6.475 +	(LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
   6.476 +    end
   6.477 +
   6.478 +
   6.479 +fun writeTextFile name s = File.write (Path.explode name) s
   6.480 +
   6.481 +fun use_source src = use_text "" Output.ml_output false src
   6.482 +    
   6.483 +fun compile eqs = 
   6.484 +    let
   6.485 +	val guid = get_guid ()
   6.486 +	val code = Real.toString (random ())
   6.487 +	val module = "AMSML_"^guid
   6.488 +	val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs
   6.489 +(*	val _ = writeTextFile "Gencode.ML" source*)
   6.490 +	val _ = compiled_rewriter := NONE
   6.491 +	val _ = use_source source
   6.492 +    in
   6.493 +	case !compiled_rewriter of 
   6.494 +	    NONE => raise Compile "broken link to compiled function"
   6.495 +	  | SOME f => (module, code, arity, toplevel_arity, inlinetab, f)
   6.496 +    end
   6.497 +
   6.498 +
   6.499 +fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = 
   6.500 +    let	
   6.501 +	val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
   6.502 +	fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
   6.503 +	  | inline (Var i) = Var i
   6.504 +	  | inline (App (a, b)) = App (inline a, inline b)
   6.505 +	  | inline (Abs m) = Abs (inline m)
   6.506 +	val t = beta (inline t)
   6.507 +	fun arity_of c = Inttab.lookup arity c		 	 
   6.508 +	fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
   6.509 +	val term = print_term NONE arity_of toplevel_arity_of 0 0 t 
   6.510 +        val source = "local open "^module^" in val _ = export ("^term^") end"
   6.511 +	val _ = writeTextFile "Gencode_call.ML" source
   6.512 +	val _ = clear_result ()
   6.513 +	val _ = use_source source
   6.514 +    in
   6.515 +	case !saved_result of 
   6.516 +	    NONE => raise Run "broken link to compiled code"
   6.517 +	  | SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked")
   6.518 +    end		
   6.519 +
   6.520 +fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = 
   6.521 +    let	
   6.522 +	val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
   6.523 +	fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
   6.524 +	  | inline (Var i) = Var i
   6.525 +	  | inline (App (a, b)) = App (inline a, inline b)
   6.526 +	  | inline (Abs m) = Abs (inline m)
   6.527 +    in
   6.528 +	compiled_fun (beta (inline t))
   6.529 +    end	
   6.530 +
   6.531 +fun discard p = ()
   6.532 +			 	  
   6.533 +end
     7.1 --- a/src/Tools/Compute_Oracle/am_util.ML	Mon Jul 09 11:44:23 2007 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,172 +0,0 @@
     7.4 -(*  Title:      Tools/Compute_Oracle/am_util.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Steven Obua
     7.7 -*)
     7.8 -
     7.9 -signature AM_UTIL = sig
    7.10 -
    7.11 -    type naming (* = string -> int *)
    7.12 -
    7.13 -    exception Parse of string
    7.14 -    exception Tokenize
    7.15 -
    7.16 -    (* takes a naming for the constants *)
    7.17 -    val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
    7.18 -
    7.19 -    (* takes a naming for the constants and one for the free variables *)
    7.20 -    val read_term : naming -> naming -> string -> AbstractMachine.term
    7.21 -
    7.22 -    val term_ord : AbstractMachine.term * AbstractMachine.term -> order
    7.23 -
    7.24 -end
    7.25 -
    7.26 -structure AM_Util : AM_UTIL =
    7.27 -struct
    7.28 -
    7.29 -fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
    7.30 -  | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
    7.31 -  | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
    7.32 -      prod_ord term_ord term_ord (a1, a2)
    7.33 -  | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
    7.34 -  | term_ord (AbstractMachine.Const _, _) = LESS
    7.35 -  | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
    7.36 -  | term_ord (AbstractMachine.Var _, _) = LESS
    7.37 -  | term_ord (AbstractMachine.App _, AbstractMachine.Abs _) = LESS
    7.38 -  | term_ord (AbstractMachine.App _, _) = GREATER
    7.39 -  | term_ord (AbstractMachine.Abs _, _) = LESS
    7.40 -
    7.41 -type naming = string -> int
    7.42 -
    7.43 -datatype token =
    7.44 -  TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
    7.45 -  TokenLambda | TokenDot | TokenNone | TokenEq
    7.46 -
    7.47 -exception Tokenize;
    7.48 -
    7.49 -fun tokenize s =
    7.50 -    let
    7.51 -      fun is_lower c = "a" <= c andalso c <= "z";
    7.52 -      val is_alphanum = Symbol.is_ascii_letter orf Symbol.is_ascii_digit;
    7.53 -      fun tz TokenNone [] = []
    7.54 -        | tz x [] = [x]
    7.55 -        | tz TokenNone (c::cs) =
    7.56 -          if Symbol.is_ascii_blank c then tz TokenNone cs
    7.57 -          else if is_lower c then (tz (TokenVar c) cs)
    7.58 -          else if is_alphanum c then (tz (TokenConst c) cs)
    7.59 -          else if c = "%" then (TokenLambda :: (tz TokenNone cs))
    7.60 -          else if c = "." then (TokenDot :: (tz TokenNone cs))
    7.61 -          else if c = "(" then (TokenLeft :: (tz TokenNone cs))
    7.62 -          else if c = ")" then (TokenRight :: (tz TokenNone cs))
    7.63 -          else if c = "=" then (TokenEq :: (tz TokenNone cs))
    7.64 -          else raise Tokenize
    7.65 -        | tz (TokenConst s) (c::cs) =
    7.66 -          if is_alphanum c then (tz (TokenConst (s ^ c)) cs)
    7.67 -          else (TokenConst s)::(tz TokenNone (c::cs))
    7.68 -        | tz (TokenVar s) (c::cs) =
    7.69 -          if is_alphanum c then (tz (TokenVar (s ^ c)) cs)
    7.70 -          else (TokenVar s)::(tz TokenNone (c::cs))
    7.71 -        | tz _ _ = raise Tokenize
    7.72 -    in tz TokenNone (explode s) end
    7.73 -    
    7.74 -exception Parse of string;
    7.75 -
    7.76 -fun cons x xs =
    7.77 -  if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
    7.78 -  else (x::xs)
    7.79 -
    7.80 -fun parse_pattern f pvars ((TokenConst c)::ts) =
    7.81 -    let
    7.82 -        val (pvars, ts, plist) = parse_pattern_list f pvars ts
    7.83 -    in
    7.84 -        (pvars, ts, AbstractMachine.PConst (f c, plist))
    7.85 -    end
    7.86 -  | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
    7.87 -and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
    7.88 -  | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
    7.89 -  | parse_pattern_single f pvars (TokenLeft::ts) =
    7.90 -    let
    7.91 -        val (pvars, ts, p) = parse_pattern f pvars ts
    7.92 -    in
    7.93 -        case ts of
    7.94 -            TokenRight::ts => (pvars, ts, p)
    7.95 -          | _ => raise (Parse "parse_pattern_single: closing bracket expected")
    7.96 -    end
    7.97 -  | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
    7.98 -and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
    7.99 -  | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
   7.100 -  | parse_pattern_list f pvars ts =
   7.101 -    let
   7.102 -        val (pvars, ts, p) = parse_pattern_single f pvars ts
   7.103 -        val (pvars, ts, ps) = parse_pattern_list f pvars ts
   7.104 -    in
   7.105 -        (pvars, ts, p::ps)
   7.106 -    end
   7.107 -
   7.108 -fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
   7.109 -  | app_terms x [] = x
   7.110 -
   7.111 -fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
   7.112 -  | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
   7.113 -  | parse_term_single f vars (TokenLeft::ts) =
   7.114 -    let
   7.115 -        val (ts, term) = parse_term f vars ts
   7.116 -    in
   7.117 -        case ts of
   7.118 -            TokenRight::ts => (ts, term)
   7.119 -          | _ => raise Parse ("parse_term_single: closing bracket expected")
   7.120 -    end
   7.121 -  | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
   7.122 -    let
   7.123 -        val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
   7.124 -    in
   7.125 -        (ts, AbstractMachine.Abs term)
   7.126 -    end
   7.127 -  | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
   7.128 -and parse_term_list f vars [] = ([], [])
   7.129 -  | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
   7.130 -  | parse_term_list f vars ts =
   7.131 -    let
   7.132 -        val (ts, term) = parse_term_single f vars ts
   7.133 -        val (ts, terms) = parse_term_list f vars ts
   7.134 -    in
   7.135 -        (ts, term::terms)
   7.136 -    end
   7.137 -and parse_term f vars ts =
   7.138 -    let
   7.139 -        val (ts, terms) = parse_term_list f vars ts
   7.140 -    in
   7.141 -        case terms of
   7.142 -            [] => raise (Parse "parse_term: no term found")
   7.143 -          | (t::terms) => (ts, app_terms t terms)
   7.144 -    end
   7.145 -
   7.146 -fun read_rule f s =
   7.147 -    let
   7.148 -        val t = tokenize s
   7.149 -        val (v, ts, pattern) = parse_pattern f [] t
   7.150 -        fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
   7.151 -          | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
   7.152 -    in
   7.153 -        case ts of
   7.154 -            TokenEq::ts =>
   7.155 -            let
   7.156 -                val (ts, term) = parse_term f (vars v) ts
   7.157 -            in
   7.158 -                case ts of
   7.159 -                    [] => (pattern, term)
   7.160 -                  | _ => raise (Parse "read_rule: still tokens left, end expected")
   7.161 -            end
   7.162 -          | _ => raise (Parse ("read_rule: = expected"))
   7.163 -    end
   7.164 -
   7.165 -fun read_term f g s =
   7.166 -    let
   7.167 -        val t = tokenize s
   7.168 -        val (ts, term) = parse_term f g t
   7.169 -    in
   7.170 -        case ts of
   7.171 -            [] => term
   7.172 -          | _ => raise (Parse ("read_term: still tokens left, end expected"))
   7.173 -    end
   7.174 -
   7.175 -end
     8.1 --- a/src/Tools/Compute_Oracle/compute.ML	Mon Jul 09 11:44:23 2007 +0200
     8.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Mon Jul 09 17:36:25 2007 +0200
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      Tools/Compute_Oracle/compute.ML
     8.5 +(*  Title:      Pure/Tools/compute.ML
     8.6      ID:         $Id$
     8.7      Author:     Steven Obua
     8.8  *)
     8.9 @@ -7,272 +7,356 @@
    8.10  
    8.11      type computer
    8.12  
    8.13 -    exception Make of string
    8.14 +    datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
    8.15  
    8.16 -    val basic_make : theory -> thm list -> computer
    8.17 -    val make : theory -> thm list -> computer
    8.18 +    exception Make of string
    8.19 +    val make : machine -> theory -> thm list -> computer
    8.20  
    8.21 +    exception Compute of string
    8.22      val compute : computer -> (int -> string) -> cterm -> term
    8.23      val theory_of : computer -> theory
    8.24 +    val hyps_of : computer -> term list
    8.25 +    val shyps_of : computer -> sort list
    8.26  
    8.27 -    val default_naming: int -> string
    8.28 -    val oracle_fn: theory -> computer * (int -> string) * cterm -> term
    8.29 +    val rewrite_param : computer -> (int -> string) -> cterm -> thm
    8.30 +    val rewrite : computer -> cterm -> thm
    8.31 +
    8.32 +    val discard : computer -> unit
    8.33 +
    8.34 +    val setup : theory -> theory
    8.35 +
    8.36  end
    8.37  
    8.38 -structure Compute: COMPUTE = struct
    8.39 +structure Compute :> COMPUTE = struct
    8.40 +
    8.41 +datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML	 
    8.42 +
    8.43 +(* Terms are mapped to integer codes *)
    8.44 +structure Encode :> 
    8.45 +sig
    8.46 +    type encoding
    8.47 +    val empty : encoding
    8.48 +    val insert : term -> encoding -> int * encoding
    8.49 +    val lookup_code : term -> encoding -> int option
    8.50 +    val lookup_term : int -> encoding -> term option					
    8.51 +    val remove_code : int -> encoding -> encoding
    8.52 +    val remove_term : term -> encoding -> encoding
    8.53 +    val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a    
    8.54 +end 
    8.55 += 
    8.56 +struct
    8.57 +
    8.58 +type encoding = int * (int Termtab.table) * (term Inttab.table)
    8.59 +
    8.60 +val empty = (0, Termtab.empty, Inttab.empty)
    8.61 +
    8.62 +fun insert t (e as (count, term2int, int2term)) = 
    8.63 +    (case Termtab.lookup term2int t of
    8.64 +	 NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
    8.65 +       | SOME code => (code, e))
    8.66 +
    8.67 +fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
    8.68 +
    8.69 +fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c
    8.70 +
    8.71 +fun remove_code c (e as (count, term2int, int2term)) = 
    8.72 +    (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term))
    8.73 +
    8.74 +fun remove_term t (e as (count, term2int, int2term)) = 
    8.75 +    (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term))
    8.76 +
    8.77 +fun fold f (_, term2int, _) = Termtab.fold f term2int 
    8.78 +
    8.79 +end
    8.80 +
    8.81  
    8.82  exception Make of string;
    8.83 -
    8.84 -fun is_mono_typ (Type (_, list)) = forall is_mono_typ list
    8.85 -  | is_mono_typ _ = false
    8.86 -
    8.87 -fun is_mono_term (Const (_, t)) = is_mono_typ t
    8.88 -  | is_mono_term (Var (_, t)) = is_mono_typ t
    8.89 -  | is_mono_term (Free (_, t)) = is_mono_typ t
    8.90 -  | is_mono_term (Bound _) = true
    8.91 -  | is_mono_term (a $ b) = is_mono_term a andalso is_mono_term b
    8.92 -  | is_mono_term (Abs (_, ty, t)) = is_mono_typ ty andalso is_mono_term t
    8.93 -
    8.94 -structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)
    8.95 -
    8.96 -fun add x y = x + y : int;
    8.97 -fun inc x = x + 1;
    8.98 -
    8.99 -exception Mono of term;
   8.100 +exception Compute of string;
   8.101  
   8.102 -val remove_types =
   8.103 -    let
   8.104 -        fun remove_types_var table invtable ccount vcount ldepth t =
   8.105 -            (case Termtab.lookup table t of
   8.106 -                 NONE =>
   8.107 -                 let
   8.108 -                     val a = AbstractMachine.Var vcount
   8.109 -                 in
   8.110 -                     (Termtab.update (t, a) table,
   8.111 -                      AMTermTab.update (a, t) invtable,
   8.112 -                      ccount,
   8.113 -                      inc vcount,
   8.114 -                      AbstractMachine.Var (add vcount ldepth))
   8.115 -                 end
   8.116 -               | SOME (AbstractMachine.Var v) =>
   8.117 -                 (table, invtable, ccount, vcount, AbstractMachine.Var (add v ldepth))
   8.118 -               | SOME _ => sys_error "remove_types_var: lookup should be a var")
   8.119 -
   8.120 -        fun remove_types_const table invtable ccount vcount ldepth t =
   8.121 -            (case Termtab.lookup table t of
   8.122 -                 NONE =>
   8.123 -                 let
   8.124 -                     val a = AbstractMachine.Const ccount
   8.125 -                 in
   8.126 -                     (Termtab.update (t, a) table,
   8.127 -                      AMTermTab.update (a, t) invtable,
   8.128 -                      inc ccount,
   8.129 -                      vcount,
   8.130 -                      a)
   8.131 -                 end
   8.132 -               | SOME (c as AbstractMachine.Const _) =>
   8.133 -                 (table, invtable, ccount, vcount, c)
   8.134 -               | SOME _ => sys_error "remove_types_const: lookup should be a const")
   8.135 +local
   8.136 +    fun make_constant t ty encoding = 
   8.137 +	let 
   8.138 +	    val (code, encoding) = Encode.insert t encoding 
   8.139 +	in 
   8.140 +	    (encoding, AbstractMachine.Const code)
   8.141 +	end
   8.142 +in
   8.143  
   8.144 -        fun remove_types table invtable ccount vcount ldepth t =
   8.145 -            case t of
   8.146 -                Var (_, ty) =>
   8.147 -                  if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
   8.148 -                  else raise (Mono t)
   8.149 -              | Free (_, ty) =>
   8.150 -                  if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
   8.151 -                  else raise (Mono t)
   8.152 -              | Const (_, ty) =>
   8.153 -                  if is_mono_typ ty then remove_types_const table invtable ccount vcount ldepth t
   8.154 -                  else raise (Mono t)
   8.155 -              | Abs (_, ty, t') =>
   8.156 -                if is_mono_typ ty then
   8.157 -                    let
   8.158 -                        val (table, invtable, ccount, vcount, t') =
   8.159 -                            remove_types table invtable ccount vcount (inc ldepth) t'
   8.160 -                    in
   8.161 -                        (table, invtable, ccount, vcount, AbstractMachine.Abs t')
   8.162 -                    end
   8.163 -                else
   8.164 -                    raise (Mono t)
   8.165 -              | a $ b =>
   8.166 -                let
   8.167 -                    val (table, invtable, ccount, vcount, a) =
   8.168 -                        remove_types table invtable ccount vcount ldepth a
   8.169 -                    val (table, invtable, ccount, vcount, b) =
   8.170 -                        remove_types table invtable ccount vcount ldepth b
   8.171 -                in
   8.172 -                    (table, invtable, ccount, vcount, AbstractMachine.App (a,b))
   8.173 -                end
   8.174 -              | Bound b => (table, invtable, ccount, vcount, AbstractMachine.Var b)
   8.175 -    in
   8.176 -     fn (table, invtable, ccount, vcount) => remove_types table invtable ccount vcount 0
   8.177 -    end
   8.178 -
   8.179 -fun infer_types naming =
   8.180 +fun remove_types encoding t =
   8.181 +    case t of 
   8.182 +	Var (_, ty) => make_constant t ty encoding
   8.183 +      | Free (_, ty) => make_constant t ty encoding
   8.184 +      | Const (_, ty) => make_constant t ty encoding
   8.185 +      | Abs (_, ty, t') => 
   8.186 +	let val (encoding, t'') = remove_types encoding t' in
   8.187 +	    (encoding, AbstractMachine.Abs t'')
   8.188 +	end
   8.189 +      | a $ b => 
   8.190 +	let
   8.191 +	    val (encoding, a) = remove_types encoding a
   8.192 +	    val (encoding, b) = remove_types encoding b
   8.193 +	in
   8.194 +	    (encoding, AbstractMachine.App (a,b))
   8.195 +	end
   8.196 +      | Bound b => (encoding, AbstractMachine.Var b)
   8.197 +end
   8.198 +    
   8.199 +local
   8.200 +    fun type_of (Free (_, ty)) = ty
   8.201 +      | type_of (Const (_, ty)) = ty
   8.202 +      | type_of (Var (_, ty)) = ty
   8.203 +      | type_of _ = sys_error "infer_types: type_of error"
   8.204 +in
   8.205 +fun infer_types naming encoding =
   8.206      let
   8.207 -        fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
   8.208 -            if v < ldepth then (Bound v, List.nth (bounds, v)) else
   8.209 -            (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of
   8.210 -                 SOME (t as Var (_, ty)) => (t, ty)
   8.211 -               | SOME (t as Free (_, ty)) => (t, ty)
   8.212 -               | _ => sys_error "infer_types: lookup should deliver Var or Free")
   8.213 -          | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
   8.214 -            (case AMTermTab.lookup invtable c of
   8.215 -                 SOME (c as Const (_, ty)) => (c, ty)
   8.216 -               | _ => sys_error "infer_types: lookup should deliver Const")
   8.217 -          | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
   8.218 -            let
   8.219 -                val (a, aty) = infer_types invtable ldepth bounds (n+1, ty) a
   8.220 -                val (adom, arange) =
   8.221 +        fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
   8.222 +	  | infer_types _ bounds _ (AbstractMachine.Const code) = 
   8.223 +	    let
   8.224 +		val c = the (Encode.lookup_term code encoding)
   8.225 +	    in
   8.226 +		(c, type_of c)
   8.227 +	    end
   8.228 +	  | infer_types level bounds _ (AbstractMachine.App (a, b)) = 
   8.229 +	    let
   8.230 +		val (a, aty) = infer_types level bounds NONE a
   8.231 +		val (adom, arange) =
   8.232                      case aty of
   8.233                          Type ("fun", [dom, range]) => (dom, range)
   8.234                        | _ => sys_error "infer_types: function type expected"
   8.235 -                val (b, bty) = infer_types invtable ldepth bounds (0, adom) b
   8.236 -            in
   8.237 -                (a $ b, arange)
   8.238 -            end
   8.239 -          | infer_types invtable ldepth bounds (0, ty as Type ("fun", [dom, range]))
   8.240 -              (AbstractMachine.Abs m) =
   8.241 +                val (b, bty) = infer_types level bounds (SOME adom) b
   8.242 +	    in
   8.243 +		(a $ b, arange)
   8.244 +	    end
   8.245 +          | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
   8.246              let
   8.247 -                val (m, _) = infer_types invtable (ldepth+1) (dom::bounds) (0, range) m
   8.248 +                val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
   8.249              in
   8.250 -                (Abs (naming ldepth, dom, m), ty)
   8.251 +                (Abs (naming level, dom, m), ty)
   8.252              end
   8.253 -          | infer_types invtable ldepth bounds ty (AbstractMachine.Abs m) =
   8.254 -            sys_error "infer_types: cannot infer type of abstraction"
   8.255 +          | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
   8.256  
   8.257 -        fun infer invtable ty term =
   8.258 +        fun infer ty term =
   8.259              let
   8.260 -                val (term', _) = infer_types invtable 0 [] (0, ty) term
   8.261 +                val (term', _) = infer_types 0 [] (SOME ty) term
   8.262              in
   8.263                  term'
   8.264              end
   8.265      in
   8.266          infer
   8.267      end
   8.268 +end
   8.269  
   8.270 -datatype computer =
   8.271 -  Computer of theory_ref *
   8.272 -    (AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program)
   8.273 +datatype prog = 
   8.274 +	 ProgBarras of AM_Interpreter.program 
   8.275 +       | ProgBarrasC of AM_Compiler.program
   8.276 +       | ProgHaskell of AM_GHC.program
   8.277 +       | ProgSML of AM_SML.program
   8.278  
   8.279 -fun basic_make thy raw_ths =
   8.280 +structure Sorttab = TableFun(type key = sort val ord = Term.sort_ord)
   8.281 +
   8.282 +datatype computer = Computer of theory_ref * Encode.encoding * term list * unit Sorttab.table * prog
   8.283 +
   8.284 +datatype cthm = ComputeThm of term list * sort list * term
   8.285 +
   8.286 +fun thm2cthm th = 
   8.287      let
   8.288 -        val ths = map (Thm.transfer thy) raw_ths;
   8.289 +	val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
   8.290 +	val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
   8.291 +    in
   8.292 +	ComputeThm (hyps, shyps, prop)
   8.293 +    end
   8.294  
   8.295 -        fun thm2rule table invtable ccount th =
   8.296 -            let
   8.297 -                val prop = Thm.plain_prop_of th
   8.298 -                  handle THM _ => raise (Make "theorems must be plain propositions")
   8.299 -                val (a, b) = Logic.dest_equals prop
   8.300 -                  handle TERM _ => raise (Make "theorems must be meta-level equations")
   8.301 +fun make machine thy raw_ths =
   8.302 +    let
   8.303 +	fun transfer (x:thm) = Thm.transfer thy x
   8.304 +	val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
   8.305  
   8.306 -                val (table, invtable, ccount, vcount, prop) =
   8.307 -                    remove_types (table, invtable, ccount, 0) (a$b)
   8.308 -                    handle Mono _ => raise (Make "no type variables allowed")
   8.309 -                val (left, right) =
   8.310 -                    (case prop of AbstractMachine.App x => x | _ =>
   8.311 -                      sys_error "make: remove_types should deliver application")
   8.312 +        fun thm2rule (encoding, hyptable, shyptable) th =
   8.313 +            let
   8.314 +		val (ComputeThm (hyps, shyps, prop)) = th
   8.315 +		val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
   8.316 +		val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
   8.317 +		val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
   8.318 +                val (a, b) = Logic.dest_equals prop
   8.319 +                  handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
   8.320 +		val a = Envir.eta_contract a
   8.321 +		val b = Envir.eta_contract b
   8.322 +		val prems = map Envir.eta_contract prems
   8.323  
   8.324 -                fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
   8.325 +                val (encoding, left) = remove_types encoding a     
   8.326 +		val (encoding, right) = remove_types encoding b  
   8.327 +                fun remove_types_of_guard encoding g = 
   8.328 +		    (let
   8.329 +			 val (t1, t2) = Logic.dest_equals g 
   8.330 +			 val (encoding, t1) = remove_types encoding t1
   8.331 +			 val (encoding, t2) = remove_types encoding t2
   8.332 +		     in
   8.333 +			 (encoding, AbstractMachine.Guard (t1, t2))
   8.334 +		     end handle TERM _ => raise (Make "guards must be meta-level equations"))
   8.335 +                val (encoding, prems) = fold_rev (fn p => fn (encoding, ps) => let val (e, p) = remove_types_of_guard encoding p in (e, p::ps) end) prems (encoding, [])
   8.336 +                
   8.337 +                fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
   8.338 +		    raise (Make "no lambda abstractions allowed in pattern")
   8.339 +		  | make_pattern encoding n vars (var as AbstractMachine.Var _) =
   8.340 +		    raise (Make "no bound variables allowed in pattern")
   8.341 +		  | make_pattern encoding n vars (AbstractMachine.Const code) =
   8.342 +		    (case the (Encode.lookup_term code encoding) of
   8.343 +			 Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
   8.344 +				   handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
   8.345 +		       | _ => (n, vars, AbstractMachine.PConst (code, [])))
   8.346 +                  | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
   8.347                      let
   8.348 -                        val var' = the (AMTermTab.lookup invtable var)
   8.349 -                        val table = Termtab.delete var' table
   8.350 -                        val invtable = AMTermTab.delete var invtable
   8.351 -                        val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>
   8.352 -                          raise (Make "no duplicate variable in pattern allowed")
   8.353 -                    in
   8.354 -                        (table, invtable, n+1, vars, AbstractMachine.PVar)
   8.355 -                    end
   8.356 -                  | make_pattern table invtable n vars (AbstractMachine.Abs _) =
   8.357 -                      raise (Make "no lambda abstractions allowed in pattern")
   8.358 -                  | make_pattern table invtable n vars (AbstractMachine.Const c) =
   8.359 -                    (table, invtable, n, vars, AbstractMachine.PConst (c, []))
   8.360 -                  | make_pattern table invtable n vars (AbstractMachine.App (a, b)) =
   8.361 -                    let
   8.362 -                        val (table, invtable, n, vars, pa) =
   8.363 -                            make_pattern table invtable n vars a
   8.364 -                        val (table, invtable, n, vars, pb) =
   8.365 -                            make_pattern table invtable n vars b
   8.366 +                        val (n, vars, pa) = make_pattern encoding n vars a
   8.367 +                        val (n, vars, pb) = make_pattern encoding n vars b
   8.368                      in
   8.369                          case pa of
   8.370                              AbstractMachine.PVar =>
   8.371                                raise (Make "patterns may not start with a variable")
   8.372                            | AbstractMachine.PConst (c, args) =>
   8.373 -                              (table, invtable, n, vars, AbstractMachine.PConst (c, args@[pb]))
   8.374 +                              (n, vars, AbstractMachine.PConst (c, args@[pb]))
   8.375                      end
   8.376  
   8.377 -                val (table, invtable, vcount, vars, pattern) =
   8.378 -                    make_pattern table invtable 0 Inttab.empty left
   8.379 +                (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
   8.380 +                   As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore
   8.381 +                   this check can be left out. *)
   8.382 +
   8.383 +                val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left
   8.384                  val _ = (case pattern of
   8.385 -                           AbstractMachine.PVar =>
   8.386 +                             AbstractMachine.PVar =>
   8.387                               raise (Make "patterns may not start with a variable")
   8.388 -                         | _ => ())
   8.389 -
   8.390 -                (* at this point, there shouldn't be any variables
   8.391 -                  left in table or invtable, only constants *)
   8.392 +                         (*  | AbstractMachine.PConst (_, []) => 
   8.393 +			     (print th; raise (Make "no parameter rewrite found"))*)
   8.394 +			   | _ => ())
   8.395  
   8.396                  (* finally, provide a function for renaming the
   8.397 -                  pattern bound variables on the right hand side *)
   8.398 +                   pattern bound variables on the right hand side *)
   8.399  
   8.400 -                fun rename ldepth vars (var as AbstractMachine.Var v) =
   8.401 -                    if v < ldepth then var
   8.402 -                    else (case Inttab.lookup vars (v - ldepth) of
   8.403 -                              NONE => raise (Make "new variable on right hand side")
   8.404 -                            | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
   8.405 -                  | rename ldepth vars (c as AbstractMachine.Const _) = c
   8.406 -                  | rename ldepth vars (AbstractMachine.App (a, b)) =
   8.407 -                    AbstractMachine.App (rename ldepth vars a, rename ldepth vars b)
   8.408 -                  | rename ldepth vars (AbstractMachine.Abs m) =
   8.409 -                    AbstractMachine.Abs (rename (ldepth+1) vars m)
   8.410 -
   8.411 +                fun rename level vars (var as AbstractMachine.Var _) = var
   8.412 +		  | rename level vars (c as AbstractMachine.Const code) =
   8.413 +		    (case Inttab.lookup vars code of 
   8.414 +			 NONE => c 
   8.415 +		       | SOME n => AbstractMachine.Var (vcount-n-1+level))
   8.416 +                  | rename level vars (AbstractMachine.App (a, b)) =
   8.417 +                    AbstractMachine.App (rename level vars a, rename level vars b)
   8.418 +                  | rename level vars (AbstractMachine.Abs m) =
   8.419 +                    AbstractMachine.Abs (rename (level+1) vars m)
   8.420 +		    
   8.421 +		fun rename_guard (AbstractMachine.Guard (a,b)) = 
   8.422 +		    AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
   8.423              in
   8.424 -                (table, invtable, ccount, (pattern, rename 0 vars right))
   8.425 +                ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
   8.426              end
   8.427  
   8.428 -        val (table, invtable, ccount, rules) =
   8.429 -          fold_rev (fn th => fn (table, invtable, ccount, rules) =>
   8.430 +        val ((encoding, hyptable, shyptable), rules) =
   8.431 +          fold_rev (fn th => fn (encoding_hyptable, rules) =>
   8.432              let
   8.433 -              val (table, invtable, ccount, rule) =
   8.434 -                  thm2rule table invtable ccount th
   8.435 -            in (table, invtable, ccount, rule::rules) end)
   8.436 -          ths (Termtab.empty, AMTermTab.empty, 0, [])
   8.437 +              val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
   8.438 +            in (encoding_hyptable, rule::rules) end)
   8.439 +          ths ((Encode.empty, Termtab.empty, Sorttab.empty), [])
   8.440  
   8.441 -        val prog = AbstractMachine.compile rules
   8.442 +        val prog = 
   8.443 +	    case machine of 
   8.444 +		BARRAS => ProgBarras (AM_Interpreter.compile rules)
   8.445 +	      | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile rules)
   8.446 +	      | HASKELL => ProgHaskell (AM_GHC.compile rules)
   8.447 +	      | SML => ProgSML (AM_SML.compile rules)
   8.448  
   8.449 -    in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end
   8.450 +(*	val _ = print (Encode.fold (fn x => fn s => x::s) encoding [])*)
   8.451 +
   8.452 +        fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
   8.453  
   8.454 -fun make thy ths =
   8.455 +	val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
   8.456 +
   8.457 +    in Computer (Theory.self_ref thy, encoding, Termtab.keys hyptable, shyptable, prog) end
   8.458 +
   8.459 +(*fun timeit f =
   8.460      let
   8.461 -      val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)
   8.462 -      fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th'])
   8.463 +	val t1 = Time.toMicroseconds (Time.now ())
   8.464 +	val x = f ()
   8.465 +	val t2 = Time.toMicroseconds (Time.now ())
   8.466 +	val _ = writeln ("### time = "^(Real.toString ((Real.fromLargeInt t2 - Real.fromLargeInt t1)/(1000000.0)))^"s")
   8.467      in
   8.468 -      basic_make thy (maps mk (maps mk_eq_True ths))
   8.469 -    end
   8.470 +	x
   8.471 +    end*)
   8.472 +
   8.473 +fun report s f = f () (*writeln s; timeit f*)
   8.474  
   8.475 -fun compute (Computer r) naming ct =
   8.476 +fun compute (Computer (rthy, encoding, hyps, shyptable, prog)) naming ct =
   8.477      let
   8.478 +	fun run (ProgBarras p) = AM_Interpreter.run p
   8.479 +	  | run (ProgBarrasC p) = AM_Compiler.run p
   8.480 +	  | run (ProgHaskell p) = AM_GHC.run p
   8.481 +	  | run (ProgSML p) = AM_SML.run p	    
   8.482          val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct
   8.483 -        val (rthy, (table, invtable, ccount, prog)) = r
   8.484          val thy = Theory.merge (Theory.deref rthy, ctthy)
   8.485 -        val (table, invtable, ccount, vcount, t) = remove_types (table, invtable, ccount, 0) t
   8.486 -        val t = AbstractMachine.run prog t
   8.487 -        val t = infer_types naming invtable ty t
   8.488 +        val (encoding, t) = report "remove_types" (fn () => remove_types encoding t)
   8.489 +        val t = report "run" (fn () => run prog t)
   8.490 +        val t = report "infer_types" (fn () => infer_types naming encoding ty t)
   8.491      in
   8.492          t
   8.493      end
   8.494  
   8.495 -fun theory_of (Computer (rthy, _)) = Theory.deref rthy
   8.496 +fun discard (Computer (rthy, encoding, hyps, shyptable, prog)) = 
   8.497 +    (case prog of
   8.498 +	 ProgBarras p => AM_Interpreter.discard p
   8.499 +       | ProgBarrasC p => AM_Compiler.discard p
   8.500 +       | ProgHaskell p => AM_GHC.discard p
   8.501 +       | ProgSML p => AM_SML.discard p)
   8.502 +
   8.503 +fun theory_of (Computer (rthy, _, _,_,_)) = Theory.deref rthy
   8.504 +fun hyps_of (Computer (_, _, hyps, _, _)) = hyps
   8.505 +fun shyps_of (Computer (_, _, _, shyptable, _)) = Sorttab.keys (shyptable)
   8.506 +fun shyptab_of (Computer (_, _, _, shyptable, _)) = shyptable
   8.507  
   8.508  fun default_naming i = "v_" ^ Int.toString i
   8.509  
   8.510 +exception Param of computer * (int -> string) * cterm;
   8.511  
   8.512 -fun oracle_fn thy (r, naming, ct) =
   8.513 +fun rewrite_param r n ct =
   8.514 +    let 
   8.515 +	val thy = theory_of_cterm ct 
   8.516 +	val th = timeit (fn () => invoke_oracle_i thy "Compute_Oracle.compute" (thy, Param (r, n, ct)))
   8.517 +	val hyps = map (fn h => assume (cterm_of thy h)) (hyps_of r)
   8.518 +    in
   8.519 +	fold (fn h => fn p => implies_elim p h) hyps th 
   8.520 +    end
   8.521 +
   8.522 +(*fun rewrite_param r n ct =
   8.523 +    let	
   8.524 +	val hyps = hyps_of r
   8.525 +	val shyps = shyps_of r
   8.526 +	val thy = theory_of_cterm ct
   8.527 +	val _ = Theory.assert_super (theory_of r) thy
   8.528 +	val t' = timeit (fn () => compute r n ct)
   8.529 +	val eq = Logic.mk_equals (term_of ct, t')
   8.530 +    in
   8.531 +	Thm.unchecked_oracle thy "Compute.compute" (eq, hyps, shyps)
   8.532 +    end*)
   8.533 +
   8.534 +fun rewrite r ct = rewrite_param r default_naming ct
   8.535 +
   8.536 +(* theory setup *)
   8.537 +
   8.538 +fun compute_oracle (thy, Param (r, naming, ct)) =
   8.539      let
   8.540          val _ = Theory.assert_super (theory_of r) thy
   8.541          val t' = compute r naming ct
   8.542 +	val eq = Logic.mk_equals (term_of ct, t')
   8.543 +	val hyps = hyps_of r
   8.544 +	val shyptab = shyptab_of r
   8.545 +	fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
   8.546 +	fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
   8.547 +	val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (eq::hyps) shyptab)
   8.548 +	val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
   8.549      in
   8.550 -        Logic.mk_equals (term_of ct, t')
   8.551 +        fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps eq
   8.552      end
   8.553 +  | compute_oracle _ = raise Match
   8.554 +
   8.555 +
   8.556 +val setup = (fn thy => (writeln "install oracle"; Theory.add_oracle ("compute", compute_oracle) thy))
   8.557 +
   8.558 +(*val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))*)
   8.559  
   8.560  end
   8.561 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Mon Jul 09 17:36:25 2007 +0200
     9.3 @@ -0,0 +1,392 @@
     9.4 +(*  Title:      Tools/Compute_Oracle/Linker.ML
     9.5 +    ID:         $$
     9.6 +    Author:     Steven Obua
     9.7 +
     9.8 +    Linker.ML solves the problem that the computing oracle does not instantiate polymorphic rules.
     9.9 +    By going through the PCompute interface, all possible instantiations are resolved by compiling new programs, if necessary.
    9.10 +    The obvious disadvantage of this approach is that in the worst case for each new term to be rewritten, a new program may be compiled.
    9.11 +*)
    9.12 +
    9.13 +(*    
    9.14 +   Given constants/frees c_1::t_1, c_2::t_2, ...., c_n::t_n,
    9.15 +   and constants/frees d_1::d_1, d_2::s_2, ..., d_m::s_m
    9.16 +
    9.17 +   Find all substitutions S such that
    9.18 +   a) the domain of S is tvars (t_1, ..., t_n)   
    9.19 +   b) there are indices i_1, ..., i_k, and j_1, ..., j_k with
    9.20 +      1. S (c_i_1::t_i_1) = d_j_1::s_j_1, ..., S (c_i_k::t_i_k) = d_j_k::s_j_k
    9.21 +      2. tvars (t_i_1, ..., t_i_k) = tvars (t_1, ..., t_n)
    9.22 +*)
    9.23 +signature LINKER = 
    9.24 +sig
    9.25 +    exception Link of string
    9.26 +    
    9.27 +    datatype constant = Constant of bool * string * typ
    9.28 +    val constant_of : term -> constant
    9.29 +
    9.30 +    type instances
    9.31 +    type subst = Type.tyenv
    9.32 +    
    9.33 +    val empty : constant list -> instances
    9.34 +    val typ_of_constant : constant -> typ
    9.35 +    val add_instances : Type.tsig -> instances -> constant list -> subst list * instances
    9.36 +    val substs_of : instances -> subst list
    9.37 +    val is_polymorphic : constant -> bool
    9.38 +    val distinct_constants : constant list -> constant list
    9.39 +    val collect_consts : term list -> constant list
    9.40 +end
    9.41 +
    9.42 +structure Linker : LINKER = struct
    9.43 +
    9.44 +exception Link of string;
    9.45 +
    9.46 +type subst = Type.tyenv
    9.47 +
    9.48 +datatype constant = Constant of bool * string * typ
    9.49 +fun constant_of (Const (name, ty)) = Constant (false, name, ty)
    9.50 +  | constant_of (Free (name, ty)) = Constant (true, name, ty)
    9.51 +  | constant_of _ = raise Link "constant_of"
    9.52 +
    9.53 +fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
    9.54 +fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
    9.55 +fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
    9.56 +
    9.57 +
    9.58 +structure Consttab = TableFun(type key = constant val ord = constant_ord);
    9.59 +structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord);
    9.60 +
    9.61 +fun typ_of_constant (Constant (_, _, ty)) = ty
    9.62 +
    9.63 +val empty_subst = (Vartab.empty : Type.tyenv)
    9.64 +
    9.65 +fun merge_subst (A:Type.tyenv) (B:Type.tyenv) = 
    9.66 +    SOME (Vartab.fold (fn (v, t) => 
    9.67 +		       fn tab => 
    9.68 +			  (case Vartab.lookup tab v of 
    9.69 +			       NONE => Vartab.update (v, t) tab 
    9.70 +			     | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
    9.71 +    handle Type.TYPE_MATCH => NONE
    9.72 +
    9.73 +fun subst_ord (A:Type.tyenv, B:Type.tyenv) = 
    9.74 +    (list_ord (prod_ord Term.fast_indexname_ord (prod_ord Term.sort_ord Term.typ_ord))) (Vartab.dest A, Vartab.dest B)
    9.75 +
    9.76 +structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
    9.77 +
    9.78 +val substtab_union = Substtab.fold Substtab.update
    9.79 +fun substtab_unions [] = Substtab.empty
    9.80 +  | substtab_unions [c] = c
    9.81 +  | substtab_unions (c::cs) = substtab_union c (substtab_unions cs)
    9.82 +
    9.83 +datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
    9.84 +
    9.85 +fun is_polymorphic (Constant (_, _, ty)) = not (null (typ_tvars ty))		
    9.86 +
    9.87 +fun distinct_constants cs =
    9.88 +    Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
    9.89 +
    9.90 +fun empty cs = 
    9.91 +    let				   
    9.92 +	val cs = distinct_constants (filter is_polymorphic cs)
    9.93 +	val old_cs = cs
    9.94 +(*	fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (typ_tvars ty) tab
    9.95 +	val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
    9.96 +	fun tvars_of ty = collect_tvars ty Typtab.empty
    9.97 +	val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
    9.98 +
    9.99 +	fun tyunion A B = 
   9.100 +	    Typtab.fold 
   9.101 +		(fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
   9.102 +		A B
   9.103 +
   9.104 +        fun is_essential A B =
   9.105 +	    Typtab.fold
   9.106 +	    (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
   9.107 +	    A false
   9.108 +
   9.109 +	fun add_minimal (c', tvs') (tvs, cs) =
   9.110 +	    let
   9.111 +		val tvs = tyunion tvs' tvs
   9.112 +		val cs = (c', tvs')::cs
   9.113 +	    in
   9.114 +		if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
   9.115 +		    SOME (tvs, cs)
   9.116 +		else 
   9.117 +		    NONE
   9.118 +	    end
   9.119 +
   9.120 +	fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)
   9.121 +
   9.122 +	fun generate_minimal_subsets subsets [] = subsets
   9.123 +	  | generate_minimal_subsets subsets (c::cs) = 
   9.124 +	    let
   9.125 +		val subsets' = map_filter (add_minimal c) subsets
   9.126 +	    in
   9.127 +		generate_minimal_subsets (subsets@subsets') cs
   9.128 +	    end*)
   9.129 +
   9.130 +	val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)
   9.131 +
   9.132 +	val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)
   9.133 +
   9.134 +    in
   9.135 +	Instances (
   9.136 +	fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
   9.137 +	Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants), 
   9.138 +	minimal_subsets, Substtab.empty)
   9.139 +    end
   9.140 +
   9.141 +local
   9.142 +fun calc ctab substtab [] = substtab
   9.143 +  | calc ctab substtab (c::cs) = 
   9.144 +    let
   9.145 +	val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
   9.146 +	fun merge_substs substtab subst = 
   9.147 +	    Substtab.fold (fn (s,_) => 
   9.148 +			   fn tab => 
   9.149 +			      (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
   9.150 +			  substtab Substtab.empty
   9.151 +	val substtab = substtab_unions (map (merge_substs substtab) csubsts)
   9.152 +    in
   9.153 +	calc ctab substtab cs
   9.154 +    end
   9.155 +in
   9.156 +fun calc_substs ctab (cs:constant list) = calc ctab (Substtab.update (empty_subst, ()) Substtab.empty) cs
   9.157 +end
   9.158 +	      			    
   9.159 +fun add_instances tsig (Instances (cfilter, ctab,minsets,substs)) cs = 
   9.160 +    let	
   9.161 +(*	val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
   9.162 +	fun calc_instantiations (constant as Constant (free, name, ty)) instantiations = 
   9.163 +	    Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>  
   9.164 +			   fn instantiations =>
   9.165 +			      if free <> free' orelse name <> name' then
   9.166 +				  instantiations
   9.167 +			      else case Consttab.lookup insttab constant of
   9.168 +				       SOME _ => instantiations
   9.169 +				     | NONE => ((constant', (constant, Type.typ_match tsig (ty', ty) empty_subst))::instantiations
   9.170 +						handle TYPE_MATCH => instantiations))
   9.171 +			  ctab instantiations
   9.172 +	val instantiations = fold calc_instantiations cs []
   9.173 +	(*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
   9.174 +	fun update_ctab (constant', entry) ctab = 
   9.175 +	    (case Consttab.lookup ctab constant' of
   9.176 +		 NONE => raise Link "internal error: update_ctab"
   9.177 +	       | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
   9.178 +	val ctab = fold update_ctab instantiations ctab	
   9.179 +	val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs) 
   9.180 +			      minsets Substtab.empty
   9.181 +	val (added_substs, substs) = 
   9.182 +	    Substtab.fold (fn (ns, _) => 
   9.183 +			   fn (added, substtab) => 
   9.184 +			      (case Substtab.lookup substs ns of
   9.185 +				   NONE => (ns::added, Substtab.update (ns, ()) substtab)
   9.186 +				 | SOME () => (added, substtab)))
   9.187 +			  new_substs ([], substs)
   9.188 +    in
   9.189 +	(added_substs, Instances (cfilter, ctab, minsets, substs))
   9.190 +    end
   9.191 +	    	
   9.192 +
   9.193 +fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
   9.194 +
   9.195 +local
   9.196 +    fun get_thm thmname = PureThy.get_thm (theory "Main") (Name thmname)
   9.197 +    val eq_th = get_thm "HOL.eq_reflection"
   9.198 +in
   9.199 +  fun eq_to_meta th = (eq_th OF [th] handle _ => th)
   9.200 +end
   9.201 +
   9.202 +				     
   9.203 +local
   9.204 +
   9.205 +fun collect (Var x) tab = tab
   9.206 +  | collect (Bound _) tab = tab
   9.207 +  | collect (a $ b) tab = collect b (collect a tab)
   9.208 +  | collect (Abs (_, _, body)) tab = collect body tab
   9.209 +  | collect t tab = Consttab.update (constant_of t, ()) tab
   9.210 +
   9.211 +in
   9.212 +  fun collect_consts tms = Consttab.keys (fold collect tms Consttab.empty)
   9.213 +end
   9.214 +
   9.215 +end
   9.216 +
   9.217 +signature PCOMPUTE =
   9.218 +sig
   9.219 +
   9.220 +    type pcomputer
   9.221 +	 
   9.222 +    val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer
   9.223 +
   9.224 +(*    val add_thms : pcomputer -> thm list -> bool*)
   9.225 +
   9.226 +    val add_instances : pcomputer -> Linker.constant list -> bool 
   9.227 +
   9.228 +    val rewrite : pcomputer -> cterm list -> thm list
   9.229 +
   9.230 +end
   9.231 +
   9.232 +structure PCompute : PCOMPUTE = struct
   9.233 +
   9.234 +exception PCompute of string
   9.235 +
   9.236 +datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
   9.237 +
   9.238 +datatype pcomputer = PComputer of Compute.machine * theory_ref * Compute.computer ref * theorem list ref
   9.239 +
   9.240 +(*fun collect_consts (Var x) = []
   9.241 +  | collect_consts (Bound _) = []
   9.242 +  | collect_consts (a $ b) = (collect_consts a)@(collect_consts b)
   9.243 +  | collect_consts (Abs (_, _, body)) = collect_consts body
   9.244 +  | collect_consts t = [Linker.constant_of t]*)
   9.245 +
   9.246 +fun collect_consts_of_thm th = 
   9.247 +    let
   9.248 +	val th = prop_of th
   9.249 +	val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th)
   9.250 +	val (left, right) = Logic.dest_equals th
   9.251 +    in
   9.252 +	(Linker.collect_consts [left], Linker.collect_consts (right::prems))
   9.253 +    end 
   9.254 +
   9.255 +fun create_theorem th =
   9.256 +let    
   9.257 +    val (left, right) = collect_consts_of_thm th
   9.258 +    val polycs = filter Linker.is_polymorphic left
   9.259 +    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
   9.260 +    fun check_const (c::cs) cs' = 
   9.261 +	let
   9.262 +	    val tvars = typ_tvars (Linker.typ_of_constant c)
   9.263 +	    val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
   9.264 +	in
   9.265 +	    if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
   9.266 +	    else 
   9.267 +		if null (tvars) then
   9.268 +		    check_const cs (c::cs')
   9.269 +		else
   9.270 +		    check_const cs cs'
   9.271 +	end
   9.272 +      | check_const [] cs' = cs'
   9.273 +    val monocs = check_const right [] 
   9.274 +in
   9.275 +    if null (polycs) then 
   9.276 +	(monocs, MonoThm th)
   9.277 +    else
   9.278 +	(monocs, PolyThm (th, Linker.empty polycs, []))
   9.279 +end
   9.280 +
   9.281 +fun create_computer machine thy ths = 
   9.282 +    let
   9.283 +	fun add (MonoThm th) ths = th::ths
   9.284 +	  | add (PolyThm (_, _, ths')) ths = ths'@ths
   9.285 +	val ths = fold_rev add ths []
   9.286 +    in
   9.287 +	Compute.make machine thy ths
   9.288 +    end
   9.289 +
   9.290 +fun conv_subst thy (subst : Type.tyenv) =
   9.291 +    map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst)
   9.292 +
   9.293 +fun add_monos thy monocs ths = 
   9.294 +    let
   9.295 +	val tsig = Sign.tsig_of thy
   9.296 +	val changed = ref false
   9.297 +	fun add monocs (th as (MonoThm _)) = ([], th)
   9.298 +	  | add monocs (PolyThm (th, instances, instanceths)) = 
   9.299 +	    let
   9.300 +		val (newsubsts, instances) = Linker.add_instances tsig instances monocs
   9.301 +		val _ = if not (null newsubsts) then changed := true else ()
   9.302 +		val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
   9.303 +(*		val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
   9.304 +		val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
   9.305 +	    in
   9.306 +		(newmonos, PolyThm (th, instances, instanceths@newths))
   9.307 +	    end
   9.308 +	fun step monocs ths = 
   9.309 +	    fold_rev (fn th => 
   9.310 +		      fn (newmonos, ths) => 
   9.311 +			 let val (newmonos', th') = add monocs th in
   9.312 +			     (newmonos'@newmonos, th'::ths)
   9.313 +			 end)
   9.314 +		     ths ([], [])
   9.315 +	fun loop monocs ths = 
   9.316 +	    let val (monocs', ths') = step monocs ths in
   9.317 +		if null (monocs') then 
   9.318 +		    ths' 
   9.319 +		else 
   9.320 +		    loop monocs' ths'
   9.321 +	    end
   9.322 +	val result = loop monocs ths
   9.323 +    in
   9.324 +	(!changed, result)
   9.325 +    end	    
   9.326 +
   9.327 +datatype cthm = ComputeThm of term list * sort list * term
   9.328 +
   9.329 +fun thm2cthm th = 
   9.330 +    let
   9.331 +	val {hyps, prop, shyps, ...} = Thm.rep_thm th
   9.332 +    in
   9.333 +	ComputeThm (hyps, shyps, prop)
   9.334 +    end
   9.335 +
   9.336 +val cthm_ord' = prod_ord (prod_ord (list_ord Term.term_ord) (list_ord Term.sort_ord)) Term.term_ord
   9.337 +
   9.338 +fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
   9.339 +
   9.340 +structure CThmtab = TableFun (type key = cthm val ord = cthm_ord)
   9.341 +    
   9.342 +fun remove_duplicates ths =
   9.343 +    let
   9.344 +	val counter = ref 0 
   9.345 +	val tab = ref (CThmtab.empty : unit CThmtab.table)
   9.346 +	val thstab = ref (Inttab.empty : thm Inttab.table)
   9.347 +	fun update th = 
   9.348 +	    let
   9.349 +		val key = thm2cthm th
   9.350 +	    in
   9.351 +		case CThmtab.lookup (!tab) key of
   9.352 +		    NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
   9.353 +		  | _ => ()
   9.354 +	    end
   9.355 +	val _ = map update ths
   9.356 +    in
   9.357 +	map snd (Inttab.dest (!thstab))
   9.358 +    end
   9.359 +    
   9.360 +
   9.361 +fun make machine thy ths cs =
   9.362 +    let
   9.363 +	val ths = remove_duplicates ths
   9.364 +	val (monocs, ths) = fold_rev (fn th => 
   9.365 +				      fn (monocs, ths) => 
   9.366 +					 let val (m, t) = create_theorem th in 
   9.367 +					     (m@monocs, t::ths)
   9.368 +					 end)
   9.369 +				     ths (cs, [])
   9.370 +	val (_, ths) = add_monos thy monocs ths
   9.371 +    in
   9.372 +	PComputer (machine, Theory.self_ref thy, ref (create_computer machine thy ths), ref ths)
   9.373 +    end
   9.374 +
   9.375 +fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs = 
   9.376 +    let
   9.377 +	val thy = Theory.deref thyref
   9.378 +	val (changed, ths) = add_monos thy cs (!rths)
   9.379 +    in
   9.380 +	if changed then 
   9.381 +	    (rcomputer := create_computer machine thy ths;
   9.382 +	     rths := ths;
   9.383 +	     true)
   9.384 +	else
   9.385 +	    false
   9.386 +    end
   9.387 +
   9.388 +fun rewrite (pc as PComputer (_, _, rcomputer, _)) cts =
   9.389 +    let
   9.390 +	val _ = map (fn ct => add_instances pc (Linker.collect_consts [term_of ct])) cts
   9.391 +    in
   9.392 +	map (fn ct => Compute.rewrite (!rcomputer) ct) cts
   9.393 +    end
   9.394 +		 							      			    
   9.395 +end
   9.396 \ No newline at end of file