# HG changeset patch
# User wenzelm
# Date 1128795334 -7200
# Node ID 5b18c334302810a6a525aa312469d91922b835eb
# Parent  87fe1dd02d342b360cd9a30fe33443b1e84ee13c
minor tweaks for Poplog/PML;

diff -r 87fe1dd02d34 -r 5b18c3343028 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Provers/blast.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -78,7 +78,7 @@
     | Var   of term option ref
     | Bound of int
     | Abs   of string*term
-    | op $  of term*term;
+    | $  of term*term;
   type branch
   val depth_tac 	: claset -> int -> int -> tactic
   val depth_limit : int ref
@@ -833,7 +833,7 @@
   next branch have been updated.*)
 fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow 
 					     backtracking over bad proofs*)
-  | prune (nbrs, nxtVars, choices) =
+  | prune (nbrs: int, nxtVars, choices) =
       let fun traceIt last =
 		let val ll = length last
 		    and lc = length choices
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Provers/classical.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -578,14 +578,14 @@
 
 (*Remove a safe wrapper*)
 fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
-  let val swrappers' = filter_out (equal name o #1) swrappers in
+  let val swrappers' = filter_out (equal name o fst) swrappers in
     if length swrappers <> length swrappers' then swrappers'
     else (warning ("No such safe wrapper in claset: "^ name); swrappers)
   end);
 
 (*Remove an unsafe wrapper*)
 fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
-  let val uwrappers' = filter_out (equal name o #1) uwrappers in
+  let val uwrappers' = filter_out (equal name o fst) uwrappers in
     if length uwrappers <> length uwrappers' then uwrappers'
     else (warning ("No such unsafe wrapper in claset: " ^ name); uwrappers)
   end);
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Provers/eqsubst.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -33,18 +33,8 @@
   exception eqsubst_occL_exp of
             string * (int list) * (thm list) * int * thm;
 
-
-  type match =
-       ((indexname * (sort * typ)) list (* type instantiations *)
-        * (indexname * (typ * term)) list) (* term instantiations *)
-       * (string * typ) list (* fake named type abs env *)
-       * (string * typ) list (* type abs env *)
-       * term (* outer term *)
-
-  type searchinfo =
-       theory (* sign for matching *)
-       * int (* maxidx *)
-       * BasicIsaFTerm.FcTerm (* focusterm to search under *)
+  type match
+  type searchinfo
 
   val prep_subst_in_asm :
          int (* subgoal to subst in *)
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Pure/IsaPlanner/focus_term_lib.ML
--- a/src/Pure/IsaPlanner/focus_term_lib.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -35,7 +35,7 @@
   type LeafT (* type for other leaf types in term sturcture *)
 
   (* the type to be encoded into *)
-  datatype TermT = op $ of TermT * TermT
+  datatype TermT = $ of TermT * TermT
     | Abs of string * TypeT * TermT
     | lf of LeafT
 
@@ -56,10 +56,10 @@
      exception focus_term_exp of string;
      exception out_of_term_exception of string;
 
-     type Term = MinTermS.TermT;
-     type Type = MinTermS.TypeT;
+     type Term (* = MinTermS.TermT *)
+     type Type (* = MinTermS.TypeT *)
 
-     type UpTerm = (Term,Type) UpTermLib.T;
+     type UpTerm (* = (Term,Type) UpTermLib.T *)
 
 (*   datatype
        UpTerm =
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Pure/IsaPlanner/isa_fterm.ML
--- a/src/Pure/IsaPlanner/isa_fterm.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Pure/IsaPlanner/isa_fterm.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -13,18 +13,26 @@
 *)   
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
 
-signature ISA_ENCODE_TERM = 
-  F_ENCODE_TERM_SIG
-    where type term = Term.term type TypeT = Term.typ;
-
+signature ISA_ENCODE_TERM =  (* cf. F_ENCODE_TERM_SIG *)
+sig
+  type term
+  type typ
+  type LeafT
+  datatype TermT = $ of TermT * TermT
+    | Abs of string * typ * TermT
+    | lf of LeafT
+  val fakebounds : string * typ -> term -> term
+  val encode : term -> TermT
+  val decode : TermT -> term
+end;
 
 (* signature BASIC_ISA_FTERM = 
 FOCUS_TERM_SIG where type Term = ISA_ENCODE_TERM.Term *)
 
 signature ISA_FTERM =
   sig
-    type Term = EncodeIsaFTerm.TermT
-    type Type = Term.typ
+    type Term (*= EncodeIsaFTerm.TermT*)
+    type Type (*= Term.typ*)
     type UpTerm
     datatype FcTerm = focus of Term * UpTerm
     structure MinTermS : F_ENCODE_TERM_SIG
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Pure/Tools/am_compiler.ML
--- a/src/Pure/Tools/am_compiler.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Pure/Tools/am_compiler.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -15,7 +15,7 @@
   val list_map : ('a -> 'b) -> 'a list -> 'b list
 end
 
-structure AM_Compiler :> COMPILING_AM = struct
+structure AM_Compiler : COMPILING_AM = struct
 
 val list_nth = List.nth;
 val list_map = map;
@@ -86,7 +86,7 @@
 
 	val (n, pattern) = print_pattern 0 p
 	val pattern =
-            if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")"
+            if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")"
             else pattern
 	
 	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
@@ -178,7 +178,7 @@
 		"  | strong_last stack clos = (stack, clos)",
 		""]
 	
-	val ic = "(case c of "^(String.concat (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"						  	
+	val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"						  	
 	val _ = writelist [
 		"fun importTerm ("^sname^".Var x) = Var x",
 		"  | importTerm ("^sname^".Const c) =  "^ic,
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Pure/Tools/am_interpreter.ML
--- a/src/Pure/Tools/am_interpreter.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Pure/Tools/am_interpreter.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -20,7 +20,7 @@
 
 end
 
-structure AM_Interpreter :> ABSTRACT_MACHINE = struct
+structure AM_Interpreter : ABSTRACT_MACHINE = struct
 
 datatype term = Var of int | Const of int | App of term * term | Abs of term
 
@@ -32,7 +32,7 @@
 
 structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
 
-type program = ((pattern * closure) list) prog_struct.table
+datatype program = Program of ((pattern * closure) list) prog_struct.table
 
 datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
 
@@ -95,7 +95,7 @@
         val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
                                      (pattern_key p, (p, clos_of_term r)))) eqs
     in
-        prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
+        Program (prog_struct.make (map (fn (k, a) => (k, [a])) eqs))
     end
 
 fun match_rules n [] clos = NONE
@@ -104,7 +104,7 @@
         NONE => match_rules (n+1) rs clos
       | SOME args => SOME (Closure (args, eq))
 
-fun match_closure prog clos =
+fun match_closure (Program prog) clos =
     case len_head_of_closure 0 clos of
         (len, CConst c) =>
         (case prog_struct.lookup prog (c, len) of
diff -r 87fe1dd02d34 -r 5b18c3343028 src/Pure/Tools/compute.ML
--- a/src/Pure/Tools/compute.ML	Sat Oct 08 20:15:33 2005 +0200
+++ b/src/Pure/Tools/compute.ML	Sat Oct 08 20:15:34 2005 +0200
@@ -20,7 +20,7 @@
 
 end
 
-structure Compute :> COMPUTE = struct
+structure Compute : COMPUTE = struct
 
 exception Make of string;
 
@@ -36,8 +36,8 @@
 
 structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)
 
-fun add x y = Int.+ (x, y)
-fun inc x = Int.+ (x, 1)
+fun add x y = x + y : int;
+fun inc x = x + 1;
 
 exception Mono of term;
 
@@ -153,8 +153,9 @@
         infer
     end
 
-type computer = theory_ref * (AbstractMachine.term Termtab.table * term AMTermTab.table * int *
-                              AbstractMachine.program)
+datatype computer =
+  Computer of theory_ref *
+    (AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program)
 
 fun basic_make thy raw_ths =
     let
@@ -240,9 +241,7 @@
 
         val prog = AbstractMachine.compile rules
 
-    in
-        (Theory.self_ref thy, (table, invtable, ccount, prog))
-    end
+    in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end
 
 fun make thy ths =
     let
@@ -253,7 +252,7 @@
       basic_make thy (app mk (app mk_eq_True ths))
     end
 
-fun compute r naming ct =
+fun compute (Computer r) naming ct =
     let
         val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct
         val (rthy, (table, invtable, ccount, prog)) = r
@@ -265,7 +264,7 @@
         t
     end
 
-fun theory_of (rthy, _) = Theory.deref rthy
+fun theory_of (Computer (rthy, _)) = Theory.deref rthy
 
 fun default_naming i = "v_" ^ Int.toString i