Sign.typ_match;
authorwenzelm
Thu Jul 28 15:19:51 2005 +0200 (2005-07-28)
changeset 169354d7f19d340e8
parent 16934 9ef19e3c7fdd
child 16936 93772bd33871
Sign.typ_match;
TFL/casesplit.ML
TFL/thry.ML
src/HOL/Tools/refute.ML
src/HOLCF/adm_tac.ML
src/Provers/splitter.ML
     1.1 --- a/TFL/casesplit.ML	Thu Jul 28 15:19:49 2005 +0200
     1.2 +++ b/TFL/casesplit.ML	Thu Jul 28 15:19:51 2005 +0200
     1.3 @@ -156,13 +156,12 @@
     1.4  
     1.5        val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
     1.6         
     1.7 -      val tsig = Sign.tsig_of sgn;
     1.8        val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
     1.9        val (Pv, Dv, type_insts) = 
    1.10            case (Thm.concl_of case_thm) of 
    1.11              (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => 
    1.12              (Pv, Dv, 
    1.13 -             Type.typ_match tsig (Vartab.empty, (Dty, ty)))
    1.14 +             Sign.typ_match sgn (Dty, ty) Vartab.empty)
    1.15            | _ => raise ERROR_MESSAGE ("not a valid case thm");
    1.16        val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T))
    1.17          (Vartab.dest type_insts);
     2.1 --- a/TFL/thry.ML	Thu Jul 28 15:19:49 2005 +0200
     2.2 +++ b/TFL/thry.ML	Thu Jul 28 15:19:51 2005 +0200
     2.3 @@ -40,8 +40,8 @@
     2.4    in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
     2.5    end;
     2.6  
     2.7 -fun match_type thry pat ob = map tybind (Vartab.dest
     2.8 -  (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob))));
     2.9 +fun match_type thry pat ob =
    2.10 +  map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty));
    2.11  
    2.12  end;
    2.13  
     3.1 --- a/src/HOL/Tools/refute.ML	Thu Jul 28 15:19:49 2005 +0200
     3.2 +++ b/src/HOL/Tools/refute.ML	Thu Jul 28 15:19:51 2005 +0200
     3.3 @@ -434,7 +434,7 @@
     3.4  		let
     3.5  			fun find_typeSubs (Const (s', T')) =
     3.6  				(if s=s' then
     3.7 -					SOME (Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))) handle Type.TYPE_MATCH => NONE
     3.8 +					SOME (Sign.typ_match thy (T', T) Vartab.empty) handle Type.TYPE_MATCH => NONE
     3.9  				else
    3.10  					NONE)
    3.11  			  | find_typeSubs (Free _)           = NONE
    3.12 @@ -543,7 +543,7 @@
    3.13  							  SOME T' =>
    3.14  								let
    3.15  									val T''      = (domain_type o domain_type) T'
    3.16 -									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T'', T))
    3.17 +									val typeSubs = Sign.typ_match thy (T'', T) Vartab.empty
    3.18  								in
    3.19  									SOME (axname, monomorphic_term typeSubs ax)
    3.20  								end
    3.21 @@ -642,7 +642,7 @@
    3.22  						in
    3.23  							if s=s' then
    3.24  								let
    3.25 -									val typeSubs = Type.typ_match (Sign.tsig_of (sign_of thy)) (Vartab.empty, (T', T))
    3.26 +									val typeSubs = Sign.typ_match thy (T', T) Vartab.empty
    3.27  								in
    3.28  									SOME (axname, monomorphic_term typeSubs ax)
    3.29  								end
    3.30 @@ -668,7 +668,7 @@
    3.31  								Library.exists (fn c =>
    3.32  									(case c of
    3.33  									  Const (cname, ctype) =>
    3.34 -										cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T, ctype)
    3.35 +										cname = s andalso Sign.typ_instance thy (T, ctype)
    3.36  									| _ =>
    3.37  										raise REFUTE ("collect_axioms", "IDT constructor is not a constant")))
    3.38  									constrs
    3.39 @@ -1738,7 +1738,7 @@
    3.40  									())
    3.41  							(* split the constructors into those occuring before/after 'Const (s, T)' *)
    3.42  							val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
    3.43 -								not (cname = s andalso Type.typ_instance (Sign.tsig_of (sign_of thy)) (T,
    3.44 +								not (cname = s andalso Sign.typ_instance thy (T,
    3.45  									map (typ_of_dtyp descr typ_assoc) ctypes ---> Type (s', Ts')))) constrs
    3.46  						in
    3.47  							case constrs2 of
     4.1 --- a/src/HOLCF/adm_tac.ML	Thu Jul 28 15:19:49 2005 +0200
     4.2 +++ b/src/HOLCF/adm_tac.ML	Thu Jul 28 15:19:51 2005 +0200
     4.3 @@ -112,7 +112,6 @@
     4.4  fun inst_adm_subst_thm state i params s T subt t paths =
     4.5    let val {sign, maxidx, ...} = rep_thm state;
     4.6        val j = maxidx+1;
     4.7 -      val tsig = Sign.tsig_of sign;
     4.8        val parTs = map snd (rev params);
     4.9        val rule = lift_rule (state, i) adm_subst;
    4.10        val types = valOf o (fst (types_sorts rule));
    4.11 @@ -123,8 +122,8 @@
    4.12        val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);
    4.13        val Pt = cterm_of sign (mk_abs (params @ [(s, fastype_of1 (T::parTs, subt))])
    4.14                       (make_term t [] paths 0));
    4.15 -      val tye = Type.typ_match tsig (Vartab.empty, (tT, #T (rep_cterm tt)));
    4.16 -      val tye' = Type.typ_match tsig (tye, (PT, #T (rep_cterm Pt)));
    4.17 +      val tye = Sign.typ_match sign (tT, #T (rep_cterm tt)) Vartab.empty;
    4.18 +      val tye' = Sign.typ_match sign (PT, #T (rep_cterm Pt)) tye;
    4.19        val ctye = map (fn (ixn, (S, T)) =>
    4.20          (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)) (Vartab.dest tye');
    4.21        val tv = cterm_of sign (Var (("t", j), Envir.typ_subst_TVars tye' tT));
     5.1 --- a/src/Provers/splitter.ML	Thu Jul 28 15:19:49 2005 +0200
     5.2 +++ b/src/Provers/splitter.ML	Thu Jul 28 15:19:51 2005 +0200
     5.3 @@ -202,19 +202,19 @@
     5.4  local
     5.5  exception MATCH
     5.6  in
     5.7 -fun typ_match tsig args = (Type.typ_match tsig args)
     5.8 +fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
     5.9                            handle Type.TYPE_MATCH => raise MATCH;
    5.10 -fun fomatch tsig args =
    5.11 +fun fomatch sg args =
    5.12    let
    5.13      fun mtch tyinsts = fn
    5.14 -        (Ts,Var(_,T), t)  => typ_match tsig (tyinsts, (T, fastype_of1(Ts,t)))
    5.15 +        (Ts,Var(_,T), t)  => typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
    5.16        | (_,Free (a,T), Free (b,U)) =>
    5.17 -          if a=b then typ_match tsig (tyinsts,(T,U)) else raise MATCH
    5.18 +          if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
    5.19        | (_,Const (a,T), Const (b,U))  =>
    5.20 -          if a=b then typ_match tsig (tyinsts,(T,U)) else raise MATCH
    5.21 +          if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
    5.22        | (_,Bound i, Bound j)  =>  if  i=j  then tyinsts else raise MATCH
    5.23        | (Ts,Abs(_,T,t), Abs(_,U,u))  =>
    5.24 -          mtch (typ_match tsig (tyinsts,(T,U))) (U::Ts,t,u)
    5.25 +          mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
    5.26        | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
    5.27        | _ => raise MATCH
    5.28    in (mtch Vartab.empty args; true) handle MATCH => false end;
    5.29 @@ -236,7 +236,7 @@
    5.30                        | find ((gcT, pat, thm, T, n)::tups) =
    5.31                            let val t2 = list_comb (h, Library.take (n, ts))
    5.32                            in if Sign.typ_instance sg (cT, gcT)
    5.33 -                                andalso fomatch (Sign.tsig_of sg) (Ts,pat,t2)
    5.34 +                                andalso fomatch sg (Ts,pat,t2)
    5.35                               then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
    5.36                               else find tups
    5.37                            end