Adapted to new interface of instantiation and unification / matching functions.
authorberghofe
Thu Apr 21 18:57:18 2005 +0200 (2005-04-21)
changeset 157945de27a5fc5ed
parent 15793 acfdd493f5c4
child 15795 997884600e0a
Adapted to new interface of instantiation and unification / matching functions.
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/reconstruction.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/specification_package.ML
src/HOLCF/adm.ML
src/Provers/induct_method.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Apr 21 18:56:03 2005 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 21 18:57:18 2005 +0200
     1.3 @@ -1362,10 +1362,10 @@
     1.4  	val tys_before = add_term_tfrees (prop_of th,[])
     1.5  	val th1 = varifyT th
     1.6  	val tys_after = add_term_tvars (prop_of th1,[])
     1.7 -	val tyinst = map (fn (bef,(i,_)) =>
     1.8 +	val tyinst = map (fn (bef, iS) =>
     1.9  			     (case try (Lib.assoc (TFree bef)) lambda of
    1.10 -				  SOME ty => (i,ctyp_of sg ty)
    1.11 -				| NONE => (i,ctyp_of sg (TFree bef))
    1.12 +				  SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty)
    1.13 +				| NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef))
    1.14  			     ))
    1.15  			 (zip tys_before tys_after)
    1.16  	val res = Drule.instantiate (tyinst,[]) th1
     2.1 --- a/src/HOL/Import/shuffler.ML	Thu Apr 21 18:56:03 2005 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Thu Apr 21 18:57:18 2005 +0200
     2.3 @@ -268,12 +268,14 @@
     2.4    | inst_tfrees sg ((name,U)::rest) thm = 
     2.5      let
     2.6  	val cU = ctyp_of sg U
     2.7 -	val tfree_names = add_term_tfree_names (prop_of thm,[])
     2.8 -	val (thm',rens) = varifyT' (tfree_names \ name) thm
     2.9 +	val tfrees = add_term_tfrees (prop_of thm,[])
    2.10 +	val (thm',rens) = varifyT'
    2.11 +    (gen_rem (op = o apfst fst) (tfrees, name)) thm
    2.12  	val mid = 
    2.13  	    case rens of
    2.14  		[] => thm'
    2.15 -	      | [(_,idx)] => instantiate ([(idx,cU)],[]) thm'
    2.16 +	      | [((_, S), idx)] => instantiate
    2.17 +            ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm'
    2.18  	      | _ => error "Shuffler.inst_tfrees internal error"
    2.19      in
    2.20  	inst_tfrees sg rest mid
     3.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Apr 21 18:56:03 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Thu Apr 21 18:57:18 2005 +0200
     3.3 @@ -122,7 +122,7 @@
     3.4  (*******************************************)
     3.5  
     3.6  fun mksubstlist [] sublist = sublist
     3.7 -   |mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b 
     3.8 +   |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b 
     3.9                                            val avar = Var(a,vartype)
    3.10                                            val newlist = ((avar,b)::sublist) in
    3.11                                            mksubstlist rest newlist
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Apr 21 18:56:03 2005 +0200
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Apr 21 18:57:18 2005 +0200
     4.3 @@ -193,10 +193,8 @@
     4.4            (env, (replicate (length consts) cT) ~~ consts)
     4.5        end;
     4.6      val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
     4.7 -    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
     4.8 -      in if T = T' then T else typ_subst_TVars_2 env T' end;
     4.9      val subst = fst o Type.freeze_thaw o
    4.10 -      (map_term_types (typ_subst_TVars_2 env))
    4.11 +      (map_term_types (Envir.norm_type env))
    4.12  
    4.13    in (map subst cs', map subst intr_ts')
    4.14    end) handle Type.TUNIFY =>
     5.1 --- a/src/HOL/Tools/reconstruction.ML	Thu Apr 21 18:56:03 2005 +0200
     5.2 +++ b/src/HOL/Tools/reconstruction.ML	Thu Apr 21 18:57:18 2005 +0200
     5.3 @@ -16,7 +16,7 @@
     5.4  (**************************************************************)
     5.5  
     5.6  fun mksubstlist [] sublist = sublist
     5.7 -  | mksubstlist ((a,b)::rest) sublist = 
     5.8 +  | mksubstlist ((a, (_, b)) :: rest) sublist = 
     5.9        let val vartype = type_of b
    5.10            val avar = Var(a,vartype)
    5.11            val newlist = ((avar,b)::sublist) 
     6.1 --- a/src/HOL/Tools/refute.ML	Thu Apr 21 18:56:03 2005 +0200
     6.2 +++ b/src/HOL/Tools/refute.ML	Thu Apr 21 18:57:18 2005 +0200
     6.3 @@ -448,8 +448,8 @@
     6.4  		in
     6.5  			map_term_types
     6.6  				(map_type_tvar
     6.7 -					(fn (v,_) =>
     6.8 -						case Vartab.lookup (typeSubs, v) of
     6.9 +					(fn v =>
    6.10 +						case Type.lookup (typeSubs, v) of
    6.11  						  NONE =>
    6.12  							(* schematic type variable not instantiated *)
    6.13  							raise REFUTE ("collect_axioms", "term " ^ Sign.string_of_term (sign_of thy) t ^ " still has a polymorphic type (after instantiating type of " ^ quote s ^ ")")
    6.14 @@ -459,11 +459,11 @@
    6.15  		end
    6.16  		(* applies a type substitution 'typeSubs' for all type variables in a  *)
    6.17  		(* term 't'                                                            *)
    6.18 -		(* Term.typ Term.Vartab.table -> Term.term -> Term.term *)
    6.19 +		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
    6.20  		fun monomorphic_term typeSubs t =
    6.21  			map_term_types (map_type_tvar
    6.22 -				(fn (v, _) =>
    6.23 -					case Vartab.lookup (typeSubs, v) of
    6.24 +				(fn v =>
    6.25 +					case Type.lookup (typeSubs, v) of
    6.26  					  NONE =>
    6.27  						(* schematic type variable not instantiated *)
    6.28  						raise ERROR
    6.29 @@ -483,11 +483,11 @@
    6.30  						(* (string * Term.term) list *)
    6.31  						val monomorphic_class_axioms = map (fn (axname, ax) =>
    6.32  							let
    6.33 -								val (idx, _) = (case term_tvars ax of
    6.34 +								val (idx, S) = (case term_tvars ax of
    6.35  									  [is] => is
    6.36  									| _    => raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^ Sign.string_of_term (sign_of thy) ax ^ ") does not contain exactly one type variable"))
    6.37  							in
    6.38 -								(axname, monomorphic_term (Vartab.make [(idx, T)]) ax)
    6.39 +								(axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
    6.40  							end) class_axioms
    6.41  						(* Term.term list * (string * Term.term) list -> Term.term list *)
    6.42  						fun collect_axiom (axs, (axname, ax)) =
     7.1 --- a/src/HOL/Tools/specification_package.ML	Thu Apr 21 18:56:03 2005 +0200
     7.2 +++ b/src/HOL/Tools/specification_package.ML	Thu Apr 21 18:57:18 2005 +0200
     7.3 @@ -110,7 +110,7 @@
     7.4  	fun unthaw (f as (a,S)) =
     7.5  	    (case assoc (fmap',a) of
     7.6  		 NONE => TVar f
     7.7 -	       | SOME b => TFree (b,S))
     7.8 +	       | SOME (b, _) => TFree (b,S))
     7.9      in
    7.10  	map_term_types (map_type_tvar unthaw) t
    7.11      end
     8.1 --- a/src/HOLCF/adm.ML	Thu Apr 21 18:56:03 2005 +0200
     8.2 +++ b/src/HOLCF/adm.ML	Thu Apr 21 18:57:18 2005 +0200
     8.3 @@ -125,10 +125,11 @@
     8.4        val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
     8.5                       (make_term t [] paths 0));
     8.6        val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
     8.7 -      val tye' = Vartab.dest (Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt))));
     8.8 -      val ctye = map (fn (x, y) => (x, ctyp_of sign y)) tye';
     8.9 -      val tv = cterm_of sign (Var (("t", j), typ_subst_TVars tye' tT));
    8.10 -      val Pv = cterm_of sign (Var (("P", j), typ_subst_TVars tye' PT));
    8.11 +      val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
    8.12 +      val ctye = map (fn (ixn, (S, T)) =>
    8.13 +        (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
    8.14 +      val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
    8.15 +      val Pv = cterm_of sign (Var (("P", j), Envir.typ_subst_TVars tye' PT));
    8.16        val rule' = instantiate (ctye, [(tv, tt), (Pv, Pt)]) rule
    8.17    in rule' end;
    8.18  
     9.1 --- a/src/Provers/induct_method.ML	Thu Apr 21 18:56:03 2005 +0200
     9.2 +++ b/src/Provers/induct_method.ML	Thu Apr 21 18:57:18 2005 +0200
     9.3 @@ -191,12 +191,13 @@
     9.4  
     9.5  (* divinate rule instantiation (cannot handle pending goal parameters) *)
     9.6  
     9.7 -fun dest_env sign (env as Envir.Envir {asol, iTs, ...}) =
     9.8 +fun dest_env sign (env as Envir.Envir {iTs, ...}) =
     9.9    let
    9.10 -    val pairs = Vartab.dest asol;
    9.11 -    val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2) pairs;
    9.12 +    val pairs = Envir.alist_of env;
    9.13 +    val ts = map (Thm.cterm_of sign o Envir.norm_term env o #2 o #2) pairs;
    9.14      val xs = map2 (Thm.cterm_of sign o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
    9.15 -  in (map (apsnd (Thm.ctyp_of sign)) (Vartab.dest iTs), xs ~~ ts) end;
    9.16 +    val cert = Thm.ctyp_of sign;
    9.17 +  in (map (fn (ixn, (S, T)) => (cert (TVar (ixn, S)), cert T)) (Vartab.dest iTs), xs ~~ ts) end;
    9.18  
    9.19  fun divinate_inst rule i st =
    9.20    let