--- 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
--- 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);
--- 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 *)
--- 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 =
--- 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
--- 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,
--- 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
--- 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