--- a/src/Pure/sign.ML Fri Feb 16 12:19:47 1996 +0100
+++ b/src/Pure/sign.ML Fri Feb 16 12:34:18 1996 +0100
@@ -6,84 +6,71 @@
*)
signature SIGN =
-sig
- structure Symtab: SYMTAB
- structure Syntax: SYNTAX
- structure Type: TYPE
- sharing Symtab = Type.Symtab
- local open Type Syntax in
- type sg
- val rep_sg: sg ->
- {tsig: type_sig,
- const_tab: typ Symtab.table,
- syn: syntax,
- stamps: string ref list}
- val subsig: sg * sg -> bool
- val eq_sg: sg * sg -> bool
- val same_sg: sg * sg -> bool
- val is_draft: sg -> bool
- val const_type: sg -> string -> typ option
- val classes: sg -> class list
- val subsort: sg -> sort * sort -> bool
- val nodup_Vars: term -> unit
- val norm_sort: sg -> sort -> sort
- val nonempty_sort: sg -> sort list -> sort -> bool
- val print_sg: sg -> unit
- val pretty_sg: sg -> Pretty.T
- val pprint_sg: sg -> pprint_args -> unit
- val pretty_term: sg -> term -> Pretty.T
- val pretty_typ: sg -> typ -> Pretty.T
- val pretty_sort: sort -> Pretty.T
- val string_of_term: sg -> term -> string
- val string_of_typ: sg -> typ -> string
- val pprint_term: sg -> term -> pprint_args -> unit
- val pprint_typ: sg -> typ -> pprint_args -> unit
- val certify_typ: sg -> typ -> typ
- val certify_term: sg -> term -> term * typ * int
- val read_typ: sg * (indexname -> sort option) -> string -> typ
- val exn_type_msg: sg -> string * typ list * term list -> string
- val infer_types: sg -> (indexname -> typ option) ->
- (indexname -> sort option) -> string list -> bool
- -> term list * typ -> int * term * (indexname * typ) list
- val add_classes: (class * class list) list -> sg -> sg
- val add_classrel: (class * class) list -> sg -> sg
- val add_defsort: sort -> sg -> sg
- val add_types: (string * int * mixfix) list -> sg -> sg
- val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
- val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
- val add_arities: (string * sort list * sort) list -> sg -> sg
- val add_consts: (string * string * mixfix) list -> sg -> sg
- val add_consts_i: (string * typ * mixfix) list -> sg -> sg
- val add_syntax: (string * string * mixfix) list -> sg -> sg
- val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
- val add_trfuns:
- (string * (ast list -> ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (ast list -> ast)) list -> sg -> sg
- val add_trrules: (string * string) trrule list -> sg -> sg
- val add_trrules_i: ast trrule list -> sg -> sg
- val add_name: string -> sg -> sg
- val make_draft: sg -> sg
- val merge: sg * sg -> sg
- val proto_pure: sg
- val pure: sg
- val cpure: sg
- val const_of_class: class -> string
- val class_of_const: string -> class
- end
-end;
+ sig
+ type sg
+ val rep_sg: sg -> {tsig: Type.type_sig,
+ const_tab: typ Symtab.table,
+ syn: Syntax.syntax,
+ stamps: string ref list}
+ val subsig: sg * sg -> bool
+ val eq_sg: sg * sg -> bool
+ val same_sg: sg * sg -> bool
+ val is_draft: sg -> bool
+ val const_type: sg -> string -> typ option
+ val classes: sg -> class list
+ val subsort: sg -> sort * sort -> bool
+ val nodup_Vars: term -> unit
+ val norm_sort: sg -> sort -> sort
+ val nonempty_sort: sg -> sort list -> sort -> bool
+ val print_sg: sg -> unit
+ val pretty_sg: sg -> Pretty.T
+ val pprint_sg: sg -> pprint_args -> unit
+ val pretty_term: sg -> term -> Pretty.T
+ val pretty_typ: sg -> typ -> Pretty.T
+ val pretty_sort: sort -> Pretty.T
+ val string_of_term: sg -> term -> string
+ val string_of_typ: sg -> typ -> string
+ val pprint_term: sg -> term -> pprint_args -> unit
+ val pprint_typ: sg -> typ -> pprint_args -> unit
+ val certify_typ: sg -> typ -> typ
+ val certify_term: sg -> term -> term * typ * int
+ val read_typ: sg * (indexname -> sort option) -> string -> typ
+ val exn_type_msg: sg -> string * typ list * term list -> string
+ val infer_types: sg -> (indexname -> typ option) ->
+ (indexname -> sort option) -> string list -> bool
+ -> term list * typ -> int * term * (indexname * typ) list
+ val add_classes: (class * class list) list -> sg -> sg
+ val add_classrel: (class * class) list -> sg -> sg
+ val add_defsort: sort -> sg -> sg
+ val add_types: (string * int * mixfix) list -> sg -> sg
+ val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
+ val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
+ val add_arities: (string * sort list * sort) list -> sg -> sg
+ val add_consts: (string * string * mixfix) list -> sg -> sg
+ val add_consts_i: (string * typ * mixfix) list -> sg -> sg
+ val add_syntax: (string * string * mixfix) list -> sg -> sg
+ val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
+ val add_trfuns:
+ (string * (ast list -> ast)) list *
+ (string * (term list -> term)) list *
+ (string * (term list -> term)) list *
+ (string * (ast list -> ast)) list -> sg -> sg
+ val add_trrules: (string * string) trrule list -> sg -> sg
+ val add_trrules_i: ast trrule list -> sg -> sg
+ val add_name: string -> sg -> sg
+ val make_draft: sg -> sg
+ val merge: sg * sg -> sg
+ val proto_pure: sg
+ val pure: sg
+ val cpure: sg
+ val const_of_class: class -> string
+ val class_of_const: string -> class
+ end;
-functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
+structure Sign : SIGN =
struct
-structure Symtab = Type.Symtab;
-structure Syntax = Syntax;
-structure BasicSyntax: BASIC_SYNTAX = Syntax;
-structure Pretty = Syntax.Pretty;
-structure Type = Type;
-open BasicSyntax Type;
-
+local open Type Syntax in
(** datatype sg **)
@@ -92,7 +79,7 @@
datatype sg =
Sg of {
- tsig: type_sig, (*order-sorted signature of types*)
+ tsig: Type.type_sig, (*order-sorted signature of types*)
const_tab: typ Symtab.table, (*types of constants*)
syn: Syntax.syntax, (*syntax for parsing and printing*)
stamps: string ref list}; (*unique theory indentifier*)
@@ -605,4 +592,5 @@
|> add_syntax Syntax.pure_applC_syntax
|> add_name "CPure";
+end
end;
--- a/src/Pure/tactic.ML Fri Feb 16 12:19:47 1996 +0100
+++ b/src/Pure/tactic.ML Fri Feb 16 12:34:18 1996 +0100
@@ -7,24 +7,21 @@
*)
signature TACTIC =
-sig
- structure Tactical: TACTICAL and Net: NET
- local open Tactical Tactical.Thm Net
- in
+ sig
val ares_tac: thm list -> int -> tactic
val asm_rewrite_goal_tac:
bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
val assume_tac: int -> tactic
val atac: int ->tactic
val bimatch_from_nets_tac:
- (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
+ (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
val bimatch_tac: (bool*thm)list -> int -> tactic
val biresolve_from_nets_tac:
- (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
+ (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
val biresolve_tac: (bool*thm)list -> int -> tactic
- val build_net: thm list -> (int*thm) net
- val build_netpair: (int*(bool*thm)) net * (int*(bool*thm)) net ->
- (bool*thm)list -> (int*(bool*thm)) net * (int*(bool*thm)) net
+ val build_net: thm list -> (int*thm) Net.net
+ val build_netpair: (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
+ (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
val compose_tac: (bool * thm * int) -> int -> tactic
val cut_facts_tac: thm list -> int -> tactic
@@ -47,13 +44,13 @@
val forw_inst_tac: (string*string)list -> thm -> int -> tactic
val freeze: thm -> thm
val insert_tagged_brl: ('a*(bool*thm)) *
- (('a*(bool*thm))net * ('a*(bool*thm))net) ->
- ('a*(bool*thm))net * ('a*(bool*thm))net
+ (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
+ ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
val is_fact: thm -> bool
val lessb: (bool * thm) * (bool * thm) -> bool
val lift_inst_rule: thm * int * (string*string)list * thm -> thm
val make_elim: thm -> thm
- val match_from_net_tac: (int*thm) net -> int -> tactic
+ val match_from_net_tac: (int*thm) Net.net -> int -> tactic
val match_tac: thm list -> int -> tactic
val metacut_tac: thm -> int -> tactic
val net_bimatch_tac: (bool*thm) list -> int -> tactic
@@ -65,7 +62,7 @@
val prune_params_tac: tactic
val rename_tac: string -> int -> tactic
val rename_last_tac: string -> string list -> int -> tactic
- val resolve_from_net_tac: (int*thm) net -> int -> tactic
+ val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic
val resolve_tac: thm list -> int -> tactic
val res_inst_tac: (string*string)list -> thm -> int -> tactic
val rewrite_goals_tac: thm list -> tactic
@@ -78,28 +75,18 @@
val subgoals_tac: string list -> int -> tactic
val subgoals_of_brl: bool * thm -> int
val trace_goalno_tac: (int -> tactic) -> int -> tactic
- end
-end;
+ end;
-functor TacticFun (structure Logic: LOGIC and Drule: DRULE and
- Tactical: TACTICAL and Net: NET
- sharing Drule.Thm = Tactical.Thm) : TACTIC =
+structure Tactic : TACTIC =
struct
-structure Tactical = Tactical;
-structure Thm = Tactical.Thm;
-structure Net = Net;
-structure Sequence = Thm.Sequence;
-structure Sign = Thm.Sign;
-local open Tactical Tactical.Thm Drule
-in
-(*Discover what goal is chosen: SOMEGOAL(trace_goalno_tac tac) *)
-fun trace_goalno_tac tf i = Tactic (fn state =>
- case Sequence.pull(tapply(tf i, state)) of
+(*Discover which goal is chosen: SOMEGOAL(trace_goalno_tac tac) *)
+fun trace_goalno_tac tac i st =
+ case Sequence.pull(tac i st) of
None => Sequence.null
| seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n");
- Sequence.seqof(fn()=> seqcell)));
+ Sequence.seqof(fn()=> seqcell));
fun string_of (a,0) = a
| string_of (a,i) = a ^ "_" ^ string_of_int i;
@@ -115,16 +102,15 @@
in instantiate ([],insts) fth end;
(*Makes a rule by applying a tactic to an existing rule*)
-fun rule_by_tactic (Tactic tf) rl =
- case Sequence.pull(tf (freeze (standard rl))) of
+fun rule_by_tactic tac rl =
+ case Sequence.pull(tac (freeze (standard rl))) of
None => raise THM("rule_by_tactic", 0, [rl])
| Some(rl',_) => standard rl';
(*** Basic tactics ***)
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
-fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
- handle THM _ => Sequence.null);
+fun PRIMSEQ thmfun st = thmfun st handle THM _ => Sequence.null;
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
@@ -182,9 +168,9 @@
val flexflex_tac = PRIMSEQ flexflex_rule;
(*Lift and instantiate a rule wrt the given state and subgoal number *)
-fun lift_inst_rule (state, i, sinsts, rule) =
-let val {maxidx,sign,...} = rep_thm state
- val (_, _, Bi, _) = dest_state(state,i)
+fun lift_inst_rule (st, i, sinsts, rule) =
+let val {maxidx,sign,...} = rep_thm st
+ val (_, _, Bi, _) = dest_state(st,i)
val params = Logic.strip_params Bi (*params of subgoal i*)
val params = rev(rename_wrt_term Bi params) (*as they are printed*)
val paramTs = map #2 params
@@ -198,14 +184,14 @@
fun lifttvar((a,i),ctyp) =
let val {T,sign} = rep_ctyp ctyp
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
- val rts = types_sorts rule and (types,sorts) = types_sorts state
+ val rts = types_sorts rule and (types,sorts) = types_sorts st
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
| types'(ixn) = types ixn;
val used = add_term_tvarnames
- (#prop(rep_thm state) $ #prop(rep_thm rule),[])
+ (#prop(rep_thm st) $ #prop(rep_thm rule),[])
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
in instantiate (map lifttvar Tinsts, map liftpair insts)
- (lift_rule (state,i) rule)
+ (lift_rule (st,i) rule)
end;
@@ -214,8 +200,8 @@
(*compose version: arguments are as for bicompose.*)
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
- STATE ( fn state =>
- compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
+ STATE ( fn st =>
+ compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule),
nsubgoal) i
handle TERM (msg,_) => (writeln msg; no_tac)
| THM (msg,_,_) => (writeln msg; no_tac) );
@@ -232,7 +218,7 @@
fun res_inst_tac sinsts rule i =
compose_inst_tac sinsts (false, rule, nprems_of rule) i;
-(*eresolve (elimination) version*)
+(*eresolve elimination version*)
fun eres_inst_tac sinsts rule i =
compose_inst_tac sinsts (true, rule, nprems_of rule) i;
@@ -400,7 +386,7 @@
(*** Meta-Rewriting Tactics ***)
fun result1 tacf mss thm =
- case Sequence.pull(tapply(tacf mss,thm)) of
+ case Sequence.pull(tacf mss thm) of
None => None
| Some(thm,_) => Some(thm);
@@ -417,7 +403,7 @@
fun rewtac def = rewrite_goals_tac [def];
-(*** Tactic for folding definitions, handling critical pairs ***)
+(*** for folding definitions, handling critical pairs ***)
(*The depth of nesting in a term*)
fun term_depth (Abs(a,T,t)) = 1 + term_depth t
@@ -458,8 +444,8 @@
| c::_ => error ("Illegal character: " ^ c)
end;
-(*Rename recent parameters using names generated from (a) and the suffixes,
- provided the string (a), which represents a term, is an identifier. *)
+(*Rename recent parameters using names generated from a and the suffixes,
+ provided the string a, which represents a term, is an identifier. *)
fun rename_last_tac a sufs i =
let val names = map (curry op^ a) sufs
in if Syntax.is_identifier a
@@ -470,9 +456,8 @@
(*Prunes all redundant parameters from the proof state by rewriting*)
val prune_params_tac = rewrite_tac [triv_forall_equality];
-(* rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
- * right to left if n is positive, and from left to right if n is negative.
- *)
+(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
+ right to left if n is positive, and from left to right if n is negative.*)
fun rotate_tac n =
let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
in if n >= 0 then rot n
@@ -480,4 +465,5 @@
end;
end;
-end;
+
+open Tactic;