Elimination of fully-functorial style.
authorpaulson
Fri Feb 16 12:34:18 1996 +0100 (1996-02-16)
changeset 1501bb7f99a0a6f0
parent 1500 b2de3b3277b8
child 1502 b612093c8bff
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
src/Pure/pattern.ML
src/Pure/sequence.ML
src/Pure/sign.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/pattern.ML	Fri Feb 16 12:19:47 1996 +0100
     1.2 +++ b/src/Pure/pattern.ML	Fri Feb 16 12:34:18 1996 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  *)
     1.5  
     1.6  signature PATTERN =
     1.7 -sig
     1.8 +  sig
     1.9    type type_sig
    1.10    type sg
    1.11    type env
    1.12 @@ -25,13 +25,11 @@
    1.13    exception Unif
    1.14    exception MATCH
    1.15    exception Pattern
    1.16 -end;
    1.17 +  end;
    1.18  
    1.19 -functor PatternFun(structure Sign:SIGN and Envir:ENVIR): PATTERN =
    1.20 +structure Pattern : PATTERN =
    1.21  struct
    1.22  
    1.23 -structure Type = Sign.Type;
    1.24 -
    1.25  type type_sig = Type.type_sig
    1.26  type sg = Sign.sg
    1.27  type env = Envir.env
     2.1 --- a/src/Pure/sequence.ML	Fri Feb 16 12:19:47 1996 +0100
     2.2 +++ b/src/Pure/sequence.ML	Fri Feb 16 12:34:18 1996 +0100
     2.3 @@ -35,7 +35,7 @@
     2.4    end;
     2.5  
     2.6  
     2.7 -functor SequenceFun () : SEQUENCE = 
     2.8 +structure Sequence : SEQUENCE = 
     2.9  struct
    2.10      
    2.11  datatype 'a seq = Seq of unit -> ('a * 'a seq)option;
     3.1 --- a/src/Pure/sign.ML	Fri Feb 16 12:19:47 1996 +0100
     3.2 +++ b/src/Pure/sign.ML	Fri Feb 16 12:34:18 1996 +0100
     3.3 @@ -6,84 +6,71 @@
     3.4  *)
     3.5  
     3.6  signature SIGN =
     3.7 -sig
     3.8 -  structure Symtab: SYMTAB
     3.9 -  structure Syntax: SYNTAX
    3.10 -  structure Type: TYPE
    3.11 -  sharing Symtab = Type.Symtab
    3.12 -  local open Type Syntax in
    3.13 -    type sg
    3.14 -    val rep_sg: sg ->
    3.15 -      {tsig: type_sig,
    3.16 -       const_tab: typ Symtab.table,
    3.17 -       syn: syntax,
    3.18 -       stamps: string ref list}
    3.19 -    val subsig: sg * sg -> bool
    3.20 -    val eq_sg: sg * sg -> bool
    3.21 -    val same_sg: sg * sg -> bool
    3.22 -    val is_draft: sg -> bool
    3.23 -    val const_type: sg -> string -> typ option
    3.24 -    val classes: sg -> class list
    3.25 -    val subsort: sg -> sort * sort -> bool
    3.26 -    val nodup_Vars: term -> unit
    3.27 -    val norm_sort: sg -> sort -> sort
    3.28 -    val nonempty_sort: sg -> sort list -> sort -> bool
    3.29 -    val print_sg: sg -> unit
    3.30 -    val pretty_sg: sg -> Pretty.T
    3.31 -    val pprint_sg: sg -> pprint_args -> unit
    3.32 -    val pretty_term: sg -> term -> Pretty.T
    3.33 -    val pretty_typ: sg -> typ -> Pretty.T
    3.34 -    val pretty_sort: sort -> Pretty.T
    3.35 -    val string_of_term: sg -> term -> string
    3.36 -    val string_of_typ: sg -> typ -> string
    3.37 -    val pprint_term: sg -> term -> pprint_args -> unit
    3.38 -    val pprint_typ: sg -> typ -> pprint_args -> unit
    3.39 -    val certify_typ: sg -> typ -> typ
    3.40 -    val certify_term: sg -> term -> term * typ * int
    3.41 -    val read_typ: sg * (indexname -> sort option) -> string -> typ
    3.42 -    val exn_type_msg: sg -> string * typ list * term list -> string
    3.43 -    val infer_types: sg -> (indexname -> typ option) ->
    3.44 -      (indexname -> sort option) -> string list -> bool
    3.45 -      -> term list * typ -> int * term * (indexname * typ) list
    3.46 -    val add_classes: (class * class list) list -> sg -> sg
    3.47 -    val add_classrel: (class * class) list -> sg -> sg
    3.48 -    val add_defsort: sort -> sg -> sg
    3.49 -    val add_types: (string * int * mixfix) list -> sg -> sg
    3.50 -    val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    3.51 -    val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
    3.52 -    val add_arities: (string * sort list * sort) list -> sg -> sg
    3.53 -    val add_consts: (string * string * mixfix) list -> sg -> sg
    3.54 -    val add_consts_i: (string * typ * mixfix) list -> sg -> sg
    3.55 -    val add_syntax: (string * string * mixfix) list -> sg -> sg
    3.56 -    val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
    3.57 -    val add_trfuns:
    3.58 -      (string * (ast list -> ast)) list *
    3.59 -      (string * (term list -> term)) list *
    3.60 -      (string * (term list -> term)) list *
    3.61 -      (string * (ast list -> ast)) list -> sg -> sg
    3.62 -    val add_trrules: (string * string) trrule list -> sg -> sg
    3.63 -    val add_trrules_i: ast trrule list -> sg -> sg
    3.64 -    val add_name: string -> sg -> sg
    3.65 -    val make_draft: sg -> sg
    3.66 -    val merge: sg * sg -> sg
    3.67 -    val proto_pure: sg
    3.68 -    val pure: sg
    3.69 -    val cpure: sg
    3.70 -    val const_of_class: class -> string
    3.71 -    val class_of_const: string -> class
    3.72 -  end
    3.73 -end;
    3.74 +  sig
    3.75 +  type sg
    3.76 +  val rep_sg: sg -> {tsig: Type.type_sig,
    3.77 +		     const_tab: typ Symtab.table,
    3.78 +		     syn: Syntax.syntax,
    3.79 +		     stamps: string ref list}
    3.80 +  val subsig: sg * sg -> bool
    3.81 +  val eq_sg: sg * sg -> bool
    3.82 +  val same_sg: sg * sg -> bool
    3.83 +  val is_draft: sg -> bool
    3.84 +  val const_type: sg -> string -> typ option
    3.85 +  val classes: sg -> class list
    3.86 +  val subsort: sg -> sort * sort -> bool
    3.87 +  val nodup_Vars: term -> unit
    3.88 +  val norm_sort: sg -> sort -> sort
    3.89 +  val nonempty_sort: sg -> sort list -> sort -> bool
    3.90 +  val print_sg: sg -> unit
    3.91 +  val pretty_sg: sg -> Pretty.T
    3.92 +  val pprint_sg: sg -> pprint_args -> unit
    3.93 +  val pretty_term: sg -> term -> Pretty.T
    3.94 +  val pretty_typ: sg -> typ -> Pretty.T
    3.95 +  val pretty_sort: sort -> Pretty.T
    3.96 +  val string_of_term: sg -> term -> string
    3.97 +  val string_of_typ: sg -> typ -> string
    3.98 +  val pprint_term: sg -> term -> pprint_args -> unit
    3.99 +  val pprint_typ: sg -> typ -> pprint_args -> unit
   3.100 +  val certify_typ: sg -> typ -> typ
   3.101 +  val certify_term: sg -> term -> term * typ * int
   3.102 +  val read_typ: sg * (indexname -> sort option) -> string -> typ
   3.103 +  val exn_type_msg: sg -> string * typ list * term list -> string
   3.104 +  val infer_types: sg -> (indexname -> typ option) ->
   3.105 +    (indexname -> sort option) -> string list -> bool
   3.106 +    -> term list * typ -> int * term * (indexname * typ) list
   3.107 +  val add_classes: (class * class list) list -> sg -> sg
   3.108 +  val add_classrel: (class * class) list -> sg -> sg
   3.109 +  val add_defsort: sort -> sg -> sg
   3.110 +  val add_types: (string * int * mixfix) list -> sg -> sg
   3.111 +  val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
   3.112 +  val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
   3.113 +  val add_arities: (string * sort list * sort) list -> sg -> sg
   3.114 +  val add_consts: (string * string * mixfix) list -> sg -> sg
   3.115 +  val add_consts_i: (string * typ * mixfix) list -> sg -> sg
   3.116 +  val add_syntax: (string * string * mixfix) list -> sg -> sg
   3.117 +  val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
   3.118 +  val add_trfuns:
   3.119 +    (string * (ast list -> ast)) list *
   3.120 +    (string * (term list -> term)) list *
   3.121 +    (string * (term list -> term)) list *
   3.122 +    (string * (ast list -> ast)) list -> sg -> sg
   3.123 +  val add_trrules: (string * string) trrule list -> sg -> sg
   3.124 +  val add_trrules_i: ast trrule list -> sg -> sg
   3.125 +  val add_name: string -> sg -> sg
   3.126 +  val make_draft: sg -> sg
   3.127 +  val merge: sg * sg -> sg
   3.128 +  val proto_pure: sg
   3.129 +  val pure: sg
   3.130 +  val cpure: sg
   3.131 +  val const_of_class: class -> string
   3.132 +  val class_of_const: string -> class
   3.133 +  end;
   3.134  
   3.135 -functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
   3.136 +structure Sign : SIGN =
   3.137  struct
   3.138  
   3.139 -structure Symtab = Type.Symtab;
   3.140 -structure Syntax = Syntax;
   3.141 -structure BasicSyntax: BASIC_SYNTAX = Syntax;
   3.142 -structure Pretty = Syntax.Pretty;
   3.143 -structure Type = Type;
   3.144 -open BasicSyntax Type;
   3.145 -
   3.146 +local open Type Syntax in
   3.147  
   3.148  (** datatype sg **)
   3.149  
   3.150 @@ -92,7 +79,7 @@
   3.151  
   3.152  datatype sg =
   3.153    Sg of {
   3.154 -    tsig: type_sig,                 (*order-sorted signature of types*)
   3.155 +    tsig: Type.type_sig,                 (*order-sorted signature of types*)
   3.156      const_tab: typ Symtab.table,    (*types of constants*)
   3.157      syn: Syntax.syntax,             (*syntax for parsing and printing*)
   3.158      stamps: string ref list};       (*unique theory indentifier*)
   3.159 @@ -605,4 +592,5 @@
   3.160    |> add_syntax Syntax.pure_applC_syntax
   3.161    |> add_name "CPure";
   3.162  
   3.163 +end
   3.164  end;
     4.1 --- a/src/Pure/tactic.ML	Fri Feb 16 12:19:47 1996 +0100
     4.2 +++ b/src/Pure/tactic.ML	Fri Feb 16 12:34:18 1996 +0100
     4.3 @@ -7,24 +7,21 @@
     4.4  *)
     4.5  
     4.6  signature TACTIC =
     4.7 -sig
     4.8 -  structure Tactical: TACTICAL and Net: NET
     4.9 -  local open Tactical Tactical.Thm Net
    4.10 -  in
    4.11 +  sig
    4.12    val ares_tac: thm list -> int -> tactic
    4.13    val asm_rewrite_goal_tac:
    4.14          bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    4.15    val assume_tac: int -> tactic
    4.16    val atac: int ->tactic
    4.17    val bimatch_from_nets_tac: 
    4.18 -      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
    4.19 +      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    4.20    val bimatch_tac: (bool*thm)list -> int -> tactic
    4.21    val biresolve_from_nets_tac: 
    4.22 -      (int*(bool*thm)) net * (int*(bool*thm)) net -> int -> tactic
    4.23 +      (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net -> int -> tactic
    4.24    val biresolve_tac: (bool*thm)list -> int -> tactic
    4.25 -  val build_net: thm list -> (int*thm) net
    4.26 -  val build_netpair:    (int*(bool*thm)) net * (int*(bool*thm)) net ->
    4.27 -      (bool*thm)list -> (int*(bool*thm)) net * (int*(bool*thm)) net
    4.28 +  val build_net: thm list -> (int*thm) Net.net
    4.29 +  val build_netpair:    (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net ->
    4.30 +      (bool*thm)list -> (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net
    4.31    val compose_inst_tac: (string*string)list -> (bool*thm*int) -> int -> tactic
    4.32    val compose_tac: (bool * thm * int) -> int -> tactic 
    4.33    val cut_facts_tac: thm list -> int -> tactic
    4.34 @@ -47,13 +44,13 @@
    4.35    val forw_inst_tac: (string*string)list -> thm -> int -> tactic
    4.36    val freeze: thm -> thm   
    4.37    val insert_tagged_brl:  ('a*(bool*thm)) * 
    4.38 -                    (('a*(bool*thm))net * ('a*(bool*thm))net) ->
    4.39 -                    ('a*(bool*thm))net * ('a*(bool*thm))net
    4.40 +                    (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
    4.41 +                    ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    4.42    val is_fact: thm -> bool
    4.43    val lessb: (bool * thm) * (bool * thm) -> bool
    4.44    val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    4.45    val make_elim: thm -> thm
    4.46 -  val match_from_net_tac: (int*thm) net -> int -> tactic
    4.47 +  val match_from_net_tac: (int*thm) Net.net -> int -> tactic
    4.48    val match_tac: thm list -> int -> tactic
    4.49    val metacut_tac: thm -> int -> tactic   
    4.50    val net_bimatch_tac: (bool*thm) list -> int -> tactic
    4.51 @@ -65,7 +62,7 @@
    4.52    val prune_params_tac: tactic
    4.53    val rename_tac: string -> int -> tactic
    4.54    val rename_last_tac: string -> string list -> int -> tactic
    4.55 -  val resolve_from_net_tac: (int*thm) net -> int -> tactic
    4.56 +  val resolve_from_net_tac: (int*thm) Net.net -> int -> tactic
    4.57    val resolve_tac: thm list -> int -> tactic
    4.58    val res_inst_tac: (string*string)list -> thm -> int -> tactic   
    4.59    val rewrite_goals_tac: thm list -> tactic
    4.60 @@ -78,28 +75,18 @@
    4.61    val subgoals_tac: string list -> int -> tactic
    4.62    val subgoals_of_brl: bool * thm -> int
    4.63    val trace_goalno_tac: (int -> tactic) -> int -> tactic
    4.64 -  end
    4.65 -end;
    4.66 +  end;
    4.67  
    4.68  
    4.69 -functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 
    4.70 -		   Tactical: TACTICAL and Net: NET
    4.71 -	  sharing Drule.Thm = Tactical.Thm) : TACTIC = 
    4.72 +structure Tactic : TACTIC = 
    4.73  struct
    4.74 -structure Tactical = Tactical;
    4.75 -structure Thm = Tactical.Thm;
    4.76 -structure Net = Net;
    4.77 -structure Sequence = Thm.Sequence;
    4.78 -structure Sign = Thm.Sign;
    4.79 -local open Tactical Tactical.Thm Drule
    4.80 -in
    4.81  
    4.82 -(*Discover what goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    4.83 -fun trace_goalno_tac tf i = Tactic (fn state => 
    4.84 -    case Sequence.pull(tapply(tf i, state)) of
    4.85 +(*Discover which goal is chosen:  SOMEGOAL(trace_goalno_tac tac) *)
    4.86 +fun trace_goalno_tac tac i st =  
    4.87 +    case Sequence.pull(tac i st) of
    4.88  	None    => Sequence.null
    4.89        | seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
    4.90 -    			 Sequence.seqof(fn()=> seqcell)));
    4.91 +    			 Sequence.seqof(fn()=> seqcell));
    4.92  
    4.93  fun string_of (a,0) = a
    4.94    | string_of (a,i) = a ^ "_" ^ string_of_int i;
    4.95 @@ -115,16 +102,15 @@
    4.96    in  instantiate ([],insts) fth  end;
    4.97  
    4.98  (*Makes a rule by applying a tactic to an existing rule*)
    4.99 -fun rule_by_tactic (Tactic tf) rl =
   4.100 -    case Sequence.pull(tf (freeze (standard rl))) of
   4.101 +fun rule_by_tactic tac rl =
   4.102 +    case Sequence.pull(tac (freeze (standard rl))) of
   4.103  	None        => raise THM("rule_by_tactic", 0, [rl])
   4.104        | Some(rl',_) => standard rl';
   4.105   
   4.106  (*** Basic tactics ***)
   4.107  
   4.108  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
   4.109 -fun PRIMSEQ thmfun = Tactic (fn state => thmfun state
   4.110 -			                 handle THM _ => Sequence.null);
   4.111 +fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Sequence.null;
   4.112  
   4.113  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
   4.114  fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun);
   4.115 @@ -182,9 +168,9 @@
   4.116  val flexflex_tac = PRIMSEQ flexflex_rule;
   4.117  
   4.118  (*Lift and instantiate a rule wrt the given state and subgoal number *)
   4.119 -fun lift_inst_rule (state, i, sinsts, rule) =
   4.120 -let val {maxidx,sign,...} = rep_thm state
   4.121 -    val (_, _, Bi, _) = dest_state(state,i)
   4.122 +fun lift_inst_rule (st, i, sinsts, rule) =
   4.123 +let val {maxidx,sign,...} = rep_thm st
   4.124 +    val (_, _, Bi, _) = dest_state(st,i)
   4.125      val params = Logic.strip_params Bi	        (*params of subgoal i*)
   4.126      val params = rev(rename_wrt_term Bi params) (*as they are printed*)
   4.127      val paramTs = map #2 params
   4.128 @@ -198,14 +184,14 @@
   4.129      fun lifttvar((a,i),ctyp) =
   4.130  	let val {T,sign} = rep_ctyp ctyp
   4.131  	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
   4.132 -    val rts = types_sorts rule and (types,sorts) = types_sorts state
   4.133 +    val rts = types_sorts rule and (types,sorts) = types_sorts st
   4.134      fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
   4.135        | types'(ixn) = types ixn;
   4.136      val used = add_term_tvarnames
   4.137 -                  (#prop(rep_thm state) $ #prop(rep_thm rule),[])
   4.138 +                  (#prop(rep_thm st) $ #prop(rep_thm rule),[])
   4.139      val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts
   4.140  in instantiate (map lifttvar Tinsts, map liftpair insts)
   4.141 -               (lift_rule (state,i) rule)
   4.142 +               (lift_rule (st,i) rule)
   4.143  end;
   4.144  
   4.145  
   4.146 @@ -214,8 +200,8 @@
   4.147  
   4.148  (*compose version: arguments are as for bicompose.*)
   4.149  fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
   4.150 -  STATE ( fn state => 
   4.151 -	   compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule),
   4.152 +  STATE ( fn st => 
   4.153 +	   compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule),
   4.154  			nsubgoal) i
   4.155  	   handle TERM (msg,_) => (writeln msg;  no_tac)
   4.156  		| THM  (msg,_,_) => (writeln msg;  no_tac) );
   4.157 @@ -232,7 +218,7 @@
   4.158  fun res_inst_tac sinsts rule i =
   4.159      compose_inst_tac sinsts (false, rule, nprems_of rule) i;
   4.160  
   4.161 -(*eresolve (elimination) version*)
   4.162 +(*eresolve elimination version*)
   4.163  fun eres_inst_tac sinsts rule i =
   4.164      compose_inst_tac sinsts (true, rule, nprems_of rule) i;
   4.165  
   4.166 @@ -400,7 +386,7 @@
   4.167  (*** Meta-Rewriting Tactics ***)
   4.168  
   4.169  fun result1 tacf mss thm =
   4.170 -  case Sequence.pull(tapply(tacf mss,thm)) of
   4.171 +  case Sequence.pull(tacf mss thm) of
   4.172      None => None
   4.173    | Some(thm,_) => Some(thm);
   4.174  
   4.175 @@ -417,7 +403,7 @@
   4.176  fun rewtac def = rewrite_goals_tac [def];
   4.177  
   4.178  
   4.179 -(*** Tactic for folding definitions, handling critical pairs ***)
   4.180 +(*** for folding definitions, handling critical pairs ***)
   4.181  
   4.182  (*The depth of nesting in a term*)
   4.183  fun term_depth (Abs(a,T,t)) = 1 + term_depth t
   4.184 @@ -458,8 +444,8 @@
   4.185      | c::_ => error ("Illegal character: " ^ c)
   4.186    end;
   4.187  
   4.188 -(*Rename recent parameters using names generated from (a) and the suffixes,
   4.189 -  provided the string (a), which represents a term, is an identifier. *)
   4.190 +(*Rename recent parameters using names generated from a and the suffixes,
   4.191 +  provided the string a, which represents a term, is an identifier. *)
   4.192  fun rename_last_tac a sufs i = 
   4.193    let val names = map (curry op^ a) sufs
   4.194    in  if Syntax.is_identifier a
   4.195 @@ -470,9 +456,8 @@
   4.196  (*Prunes all redundant parameters from the proof state by rewriting*)
   4.197  val prune_params_tac = rewrite_tac [triv_forall_equality];
   4.198  
   4.199 -(* rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   4.200 - * right to left if n is positive, and from left to right if n is negative.
   4.201 - *)
   4.202 +(*rotate_tac n i: rotate the assumptions of subgoal i by n positions, from
   4.203 +  right to left if n is positive, and from left to right if n is negative.*)
   4.204  fun rotate_tac n =
   4.205    let fun rot(n) = EVERY'(replicate n (dtac asm_rl));
   4.206    in if n >= 0 then rot n
   4.207 @@ -480,4 +465,5 @@
   4.208    end;
   4.209  
   4.210  end;
   4.211 -end;
   4.212 +
   4.213 +open Tactic;