simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
authorwenzelm
Tue May 04 12:30:15 2010 +0200 (2010-05-04 ago)
changeset 36620e6bb250402b5
parent 36619 deadcd0ec431
child 36621 2fd4e2c76636
simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;
src/Pure/Proof/extraction.ML
src/Pure/Proof/reconstruct.ML
src/Pure/proofterm.ML
src/Pure/term_subst.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue May 04 11:02:50 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue May 04 12:30:15 2010 +0200
     1.3 @@ -136,8 +136,7 @@
     1.4    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
     1.5    | strip_abs _ _ = error "strip_abs: not an abstraction";
     1.6  
     1.7 -fun prf_subst_TVars tye =
     1.8 -  map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
     1.9 +val prf_subst_TVars = map_proof_types o typ_subst_TVars;
    1.10  
    1.11  fun relevant_vars types prop = List.foldr (fn
    1.12        (Var ((a, _), T), vs) => (case strip_type T of
     2.1 --- a/src/Pure/Proof/reconstruct.ML	Tue May 04 11:02:50 2010 +0200
     2.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue May 04 12:30:15 2010 +0200
     2.3 @@ -376,8 +376,7 @@
     2.4              val varify = map_type_tfree (fn p as (a, S) =>
     2.5                if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
     2.6            in
     2.7 -            (maxidx', prfs', map_proof_terms (subst_TVars tye o
     2.8 -               map_types varify) (typ_subst_TVars tye o varify) prf)
     2.9 +            (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
    2.10            end
    2.11        | expand maxidx prfs prf = (maxidx, prfs, prf);
    2.12  
     3.1 --- a/src/Pure/proofterm.ML	Tue May 04 11:02:50 2010 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Tue May 04 12:30:15 2010 +0200
     3.3 @@ -58,8 +58,10 @@
     3.4    val strip_combt: proof -> proof * term option list
     3.5    val strip_combP: proof -> proof * proof list
     3.6    val strip_thm: proof_body -> proof_body
     3.7 -  val map_proof_terms_option: (term -> term option) -> (typ -> typ option) -> proof -> proof
     3.8 +  val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
     3.9 +  val map_proof_types_same: typ Same.operation -> proof Same.operation
    3.10    val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
    3.11 +  val map_proof_types: (typ -> typ) -> proof -> proof
    3.12    val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
    3.13    val maxidx_proof: proof -> int -> int
    3.14    val size_of_proof: proof -> int
    3.15 @@ -273,10 +275,8 @@
    3.16  val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
    3.17  fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
    3.18  
    3.19 -fun map_proof_terms_option f g =
    3.20 +fun map_proof_same term typ ofclass =
    3.21    let
    3.22 -    val term = Same.function f;
    3.23 -    val typ = Same.function g;
    3.24      val typs = Same.map typ;
    3.25  
    3.26      fun proof (Abst (s, T, prf)) =
    3.27 @@ -292,22 +292,23 @@
    3.28            (proof prf1 %% Same.commit proof prf2
    3.29              handle Same.SAME => prf1 %% proof prf2)
    3.30        | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
    3.31 -      | proof (OfClass (T, c)) = OfClass (typ T, c)
    3.32 +      | proof (OfClass T_c) = ofclass T_c
    3.33        | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
    3.34        | proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
    3.35        | proof (PThm (i, ((a, prop, SOME Ts), body))) =
    3.36            PThm (i, ((a, prop, SOME (typs Ts)), body))
    3.37        | proof _ = raise Same.SAME;
    3.38 -  in Same.commit proof end;
    3.39 +  in proof end;
    3.40 +
    3.41 +fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
    3.42 +fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
    3.43  
    3.44  fun same eq f x =
    3.45    let val x' = f x
    3.46    in if eq (x, x') then raise Same.SAME else x' end;
    3.47  
    3.48 -fun map_proof_terms f g =
    3.49 -  map_proof_terms_option
    3.50 -   (fn t => SOME (same (op =) f t) handle Same.SAME => NONE)
    3.51 -   (fn T => SOME (same (op =) g T) handle Same.SAME => NONE);
    3.52 +fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
    3.53 +fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
    3.54  
    3.55  fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
    3.56    | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
    3.57 @@ -696,17 +697,17 @@
    3.58  (***** generalization *****)
    3.59  
    3.60  fun generalize (tfrees, frees) idx =
    3.61 -  map_proof_terms_option
    3.62 -    (Term_Subst.generalize_option (tfrees, frees) idx)
    3.63 -    (Term_Subst.generalizeT_option tfrees idx);
    3.64 +  Same.commit (map_proof_terms_same
    3.65 +    (Term_Subst.generalize_same (tfrees, frees) idx)
    3.66 +    (Term_Subst.generalizeT_same tfrees idx));
    3.67  
    3.68  
    3.69  (***** instantiation *****)
    3.70  
    3.71  fun instantiate (instT, inst) =
    3.72 -  map_proof_terms_option
    3.73 -    (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
    3.74 -    (Term_Subst.instantiateT_option instT);
    3.75 +  Same.commit (map_proof_terms_same
    3.76 +    (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
    3.77 +    (Term_Subst.instantiateT_same instT));
    3.78  
    3.79  
    3.80  (***** lifting *****)
    3.81 @@ -757,9 +758,8 @@
    3.82    end;
    3.83  
    3.84  fun incr_indexes i =
    3.85 -  map_proof_terms_option
    3.86 -    (Same.capture (Logic.incr_indexes_same ([], i)))
    3.87 -    (Same.capture (Logic.incr_tvar_same i));
    3.88 +  Same.commit (map_proof_terms_same
    3.89 +    (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
    3.90  
    3.91  
    3.92  (***** proof by assumption *****)
     4.1 --- a/src/Pure/term_subst.ML	Tue May 04 11:02:50 2010 +0200
     4.2 +++ b/src/Pure/term_subst.ML	Tue May 04 12:30:15 2010 +0200
     4.3 @@ -13,6 +13,8 @@
     4.4    val map_atyps_option: (typ -> typ option) -> term -> term option
     4.5    val map_types_option: (typ -> typ option) -> term -> term option
     4.6    val map_aterms_option: (term -> term option) -> term -> term option
     4.7 +  val generalizeT_same: string list -> int -> typ Same.operation
     4.8 +  val generalize_same: string list * string list -> int -> term Same.operation
     4.9    val generalize: string list * string list -> int -> term -> term
    4.10    val generalizeT: string list -> int -> typ -> typ
    4.11    val generalize_option: string list * string list -> int -> term -> term option
    4.12 @@ -21,12 +23,12 @@
    4.13    val instantiate_maxidx:
    4.14      ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
    4.15      term -> int -> term * int
    4.16 +  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    4.17    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    4.18      term -> term
    4.19 -  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    4.20 -  val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    4.21 -    term -> term option
    4.22 -  val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
    4.23 +  val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
    4.24 +  val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
    4.25 +    term Same.operation
    4.26    val zero_var_indexes: term -> term
    4.27    val zero_var_indexes_inst: term list ->
    4.28      ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    4.29 @@ -70,8 +72,6 @@
    4.30  
    4.31  (* generalization of fixed variables *)
    4.32  
    4.33 -local
    4.34 -
    4.35  fun generalizeT_same [] _ _ = raise Same.SAME
    4.36    | generalizeT_same tfrees idx ty =
    4.37        let
    4.38 @@ -99,16 +99,12 @@
    4.39            | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
    4.40        in gen tm end;
    4.41  
    4.42 -in
    4.43 -
    4.44 -fun generalize names i tm = generalize_same names i tm handle Same.SAME => tm;
    4.45 -fun generalizeT names i ty = generalizeT_same names i ty handle Same.SAME => ty;
    4.46 +fun generalize names i tm = Same.commit (generalize_same names i) tm;
    4.47 +fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
    4.48  
    4.49  fun generalize_option names i tm = SOME (generalize_same names i tm) handle Same.SAME => NONE;
    4.50  fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle Same.SAME => NONE;
    4.51  
    4.52 -end;
    4.53 -
    4.54  
    4.55  (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
    4.56  
    4.57 @@ -118,7 +114,7 @@
    4.58  fun no_indexes1 inst = map no_index inst;
    4.59  fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
    4.60  
    4.61 -fun instantiateT_same maxidx instT ty =
    4.62 +fun instT_same maxidx instT ty =
    4.63    let
    4.64      fun maxify i = if i > ! maxidx then maxidx := i else ();
    4.65  
    4.66 @@ -134,11 +130,11 @@
    4.67        | subst_typs [] = raise Same.SAME;
    4.68    in subst_typ ty end;
    4.69  
    4.70 -fun instantiate_same maxidx (instT, inst) tm =
    4.71 +fun inst_same maxidx (instT, inst) tm =
    4.72    let
    4.73      fun maxify i = if i > ! maxidx then maxidx := i else ();
    4.74  
    4.75 -    val substT = instantiateT_same maxidx instT;
    4.76 +    val substT = instT_same maxidx instT;
    4.77      fun subst (Const (c, T)) = Const (c, substT T)
    4.78        | subst (Free (x, T)) = Free (x, substT T)
    4.79        | subst (Var ((x, i), T)) =
    4.80 @@ -158,31 +154,23 @@
    4.81  
    4.82  fun instantiateT_maxidx instT ty i =
    4.83    let val maxidx = Unsynchronized.ref i
    4.84 -  in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
    4.85 +  in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end;
    4.86  
    4.87  fun instantiate_maxidx insts tm i =
    4.88    let val maxidx = Unsynchronized.ref i
    4.89 -  in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
    4.90 +  in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
    4.91  
    4.92  fun instantiateT [] ty = ty
    4.93 -  | instantiateT instT ty =
    4.94 -      (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
    4.95 -        handle Same.SAME => ty);
    4.96 +  | instantiateT instT ty = Same.commit (instT_same (Unsynchronized.ref ~1) (no_indexes1 instT)) ty;
    4.97  
    4.98  fun instantiate ([], []) tm = tm
    4.99 -  | instantiate insts tm =
   4.100 -      (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
   4.101 -        handle Same.SAME => tm);
   4.102 +  | instantiate insts tm = Same.commit (inst_same (Unsynchronized.ref ~1) (no_indexes2 insts)) tm;
   4.103  
   4.104 -fun instantiateT_option [] _ = NONE
   4.105 -  | instantiateT_option instT ty =
   4.106 -      (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
   4.107 -        handle Same.SAME => NONE);
   4.108 +fun instantiateT_same [] _ = raise Same.SAME
   4.109 +  | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
   4.110  
   4.111 -fun instantiate_option ([], []) _ = NONE
   4.112 -  | instantiate_option insts tm =
   4.113 -      (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
   4.114 -        handle Same.SAME => NONE);
   4.115 +fun instantiate_same ([], []) _ = raise Same.SAME
   4.116 +  | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
   4.117  
   4.118  end;
   4.119  
     5.1 --- a/src/Pure/variable.ML	Tue May 04 11:02:50 2010 +0200
     5.2 +++ b/src/Pure/variable.ML	Tue May 04 12:30:15 2010 +0200
     5.3 @@ -376,9 +376,9 @@
     5.4      val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
     5.5      val tfrees = mk_tfrees [];
     5.6      val idx = Proofterm.maxidx_proof prf ~1 + 1;
     5.7 -    val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
     5.8 -    val gen_typ = Term_Subst.generalizeT_option tfrees idx;
     5.9 -  in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
    5.10 +    val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
    5.11 +    val gen_typ = Term_Subst.generalizeT_same tfrees idx;
    5.12 +  in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
    5.13  
    5.14  
    5.15  fun gen_export (mk_tfrees, frees) ths =