src/Pure/drule.ML
changeset 4281 6c6073b13600
parent 4270 957c887b89b5
child 4285 05af145a61d4
     1.1 --- a/src/Pure/drule.ML	Sat Nov 22 13:27:02 1997 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Nov 24 16:43:43 1997 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4     simultaneous instantiations were read or at least type checked
     1.5     simultaneously rather than one after the other. This would make the tricky
     1.6     composition of implicit type instantiations (parameter tye) superfluous.
     1.7 -*)
     1.8 +
     1.9  fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    1.10  let val {tsig,...} = Sign.rep_sg sign
    1.11      fun split([],tvs,vs) = (tvs,vs)
    1.12 @@ -152,6 +152,37 @@
    1.13  in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
    1.14      map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
    1.15  end;
    1.16 +*)
    1.17 +
    1.18 +fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    1.19 +let val {tsig,...} = Sign.rep_sg sign
    1.20 +    fun split([],tvs,vs) = (tvs,vs)
    1.21 +      | split((sv,st)::l,tvs,vs) = (case explode sv of
    1.22 +                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
    1.23 +                | cs => split(l,tvs,(indexname cs,st)::vs));
    1.24 +    val (tvs,vs) = split(insts,[],[]);
    1.25 +    fun readT((a,i),st) =
    1.26 +        let val ixn = ("'" ^ a,i);
    1.27 +            val S = case rsorts ixn of Some S => S | None => absent ixn;
    1.28 +            val T = Sign.read_typ (sign,sorts) st;
    1.29 +        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
    1.30 +           else inst_failure ixn
    1.31 +        end
    1.32 +    val tye = map readT tvs;
    1.33 +    fun mkty(ixn,st) = (case rtypes ixn of
    1.34 +                          Some T => (ixn,(st,typ_subst_TVars tye T))
    1.35 +                        | None => absent ixn);
    1.36 +    val ixnsTs = map mkty vs;
    1.37 +    val ixns = map fst ixnsTs
    1.38 +    and sTs  = map snd ixnsTs
    1.39 +    val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs;
    1.40 +    fun mkcVar(ixn,T) =
    1.41 +        let val U = typ_subst_TVars tye2 T
    1.42 +        in cterm_of sign (Var(ixn,U)) end
    1.43 +    val ixnTs = ListPair.zip(ixns, map snd sTs)
    1.44 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye),
    1.45 +    ListPair.zip(map mkcVar ixnTs,cts))
    1.46 +end;
    1.47  
    1.48  
    1.49  (*** Find the type (sort) associated with a (T)Var or (T)Free in a term