src/Pure/drule.ML
changeset 10403 2955ee2424ce
parent 9862 96138f29545e
child 10414 f7aeff3e9e1e
equal deleted inserted replaced
10402:5e82d6cafb5f 10403:2955ee2424ce
   176 
   176 
   177 fun inst_failure ixn =
   177 fun inst_failure ixn =
   178   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   178   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   179 
   179 
   180 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
   180 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
   181 let val {tsig,...} = Sign.rep_sg sign
   181 let
   182     fun split([],tvs,vs) = (tvs,vs)
   182     fun split([],tvs,vs) = (tvs,vs)
   183       | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
   183       | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
   184                   "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
   184                   "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
   185                 | cs => split(l,tvs,(Syntax.indexname cs,st)::vs));
   185                 | cs => split(l,tvs,(Syntax.indexname cs,st)::vs));
   186     val (tvs,vs) = split(insts,[],[]);
   186     val (tvs,vs) = split(insts,[],[]);
   187     fun readT((a,i),st) =
   187     fun readT((a,i),st) =
   188         let val ixn = ("'" ^ a,i);
   188         let val ixn = ("'" ^ a,i);
   189             val S = case rsorts ixn of Some S => S | None => absent ixn;
   189             val S = case rsorts ixn of Some S => S | None => absent ixn;
   190             val T = Sign.read_typ (sign,sorts) st;
   190             val T = Sign.read_typ (sign,sorts) st;
   191         in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   191         in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
   192            else inst_failure ixn
   192            else inst_failure ixn
   193         end
   193         end
   194     val tye = map readT tvs;
   194     val tye = map readT tvs;
   195     fun mkty(ixn,st) = (case rtypes ixn of
   195     fun mkty(ixn,st) = (case rtypes ixn of
   196                           Some T => (ixn,(st,typ_subst_TVars tye T))
   196                           Some T => (ixn,(st,typ_subst_TVars tye T))
   652     let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   652     let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   653         and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   653         and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   654         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   654         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   655         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   655         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   656         val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
   656         val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
   657           handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])
   657           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
   658     in  (sign', tye', maxi')  end;
   658     in  (sign', tye', maxi')  end;
   659 in
   659 in
   660 fun cterm_instantiate ctpairs0 th =
   660 fun cterm_instantiate ctpairs0 th =
   661   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
   661   let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
   662       val tsig = #tsig(Sign.rep_sg sign);
       
   663       fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
   662       fun instT(ct,cu) = let val inst = subst_TVars_Vartab tye
   664                          in (cterm_fun inst ct, cterm_fun inst cu) end
   663                          in (cterm_fun inst ct, cterm_fun inst cu) end
   665       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   664       fun ctyp2 (ix,T) = (ix, ctyp_of sign T)
   666   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   665   in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   667   handle TERM _ =>
   666   handle TERM _ =>