# HG changeset patch # User nipkow # Date 795174004 -3600 # Node ID 9e10962866b02248401e0a2fda4c6839ebdd183f # Parent 682139612060dfa079e03f1e767ad40d4176a851 Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments. diff -r 682139612060 -r 9e10962866b0 src/Pure/drule.ML --- a/src/Pure/drule.ML Tue Mar 14 09:47:28 1995 +0100 +++ b/src/Pure/drule.ML Tue Mar 14 10:40:04 1995 +0100 @@ -249,6 +249,11 @@ fun inst_failure ixn = error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails"); +(* this code is a bit of a mess. add_cterm could be simplified greatly if + simultaneous instantiations were read or at least type checked + simultaneously rather than one after the other. This would make the tricky + composition of implicit type instantiations (parameter tye) superfluous. +*) fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = let val {tsig,...} = Sign.rep_sg sign fun split([],tvs,vs) = (tvs,vs) @@ -269,11 +274,14 @@ Some T => typ_subst_TVars tye T | None => absent ixn; val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T); - val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T)) + val cts' = (ixn,T,ct)::cts + fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct) val used' = add_term_tvarnames(term_of ct,used); - in ((cv,ct)::cts,tye2 @ tye,used') end + in (map inst cts',tye2 @ tye,used') end val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs); -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end; +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', + map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms) +end; @@ -585,7 +593,8 @@ (*Instantiate theorem th, reading instantiations under signature sg*) fun read_instantiate_sg sg sinsts th = let val ts = types_sorts th; - in instantiate (read_insts sg ts ts [] sinsts) th end; + val used = add_term_tvarnames(#prop(rep_thm th),[]); + in instantiate (read_insts sg ts ts used sinsts) th end; (*Instantiate theorem th, reading instantiations under theory of th*) fun read_instantiate sinsts th = diff -r 682139612060 -r 9e10962866b0 src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Mar 14 09:47:28 1995 +0100 +++ b/src/Pure/sign.ML Tue Mar 14 10:40:04 1995 +0100 @@ -272,52 +272,47 @@ val ct = const_type sg; - fun process_terms (t::ts) (idx, infrd_t, tye) msg n = - let val (infrd_t', tye', msg') = - let val (T,tye) = - Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t) - in (Some T, Some tye, msg) end - handle TYPE arg => (None, None, exn_type_msg arg) - - val old_show_brackets = !show_brackets; + fun warn() = + if length ts > 1 andalso length ts <= !Syntax.ambiguity_level + then (*no warning shown yet*) + writeln "Warning: Currently parsed input \ + \produces more than one parse tree.\n\ + \For more information lower Syntax.ambiguity_level." + else (); - val _ = (show_brackets := true); - - val msg'' = - if is_none idx then (if is_none infrd_t' then msg' else "") - else if is_none infrd_t' then "" - else (if msg' = "" then - "Error: More than one term is type correct:\n" ^ - (show_term (the infrd_t)) else msg') ^ "\n" ^ - (show_term (the infrd_t')) ^ "\n"; + datatype result = One of int * term * (indexname * typ) list + | Errs of (string * typ list * term list)list + | Ambigs of term list; - in show_brackets := old_show_brackets; - if is_none infrd_t' then - process_terms ts (idx, infrd_t, tye) msg'' (n+1) - else - process_terms ts (Some n, infrd_t', tye') msg'' (n+1) - end - | process_terms [] (idx, infrd_t, tye) msg _ = - if msg = "" then (the idx, the infrd_t, the tye) - else - (if length ts > 1 andalso length ts <= !Syntax.ambiguity_level then - (*no warning shown yet?*) - writeln "Warning: Currently parsed input \ - \produces more than one parse tree.\n\ - \For more information lower Syntax.ambiguity_level." - else (); - error msg) + fun process_term(res,(t,i)) = + let val (u,tye) = Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t) + in case res of + One(_,t0,_) => Ambigs([u,t0]) + | Errs _ => One(i,u,tye) + | Ambigs(us) => Ambigs(u::us) + end + handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs) + | _ => res); - val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0; - in if print_msg andalso length ts > !Syntax.ambiguity_level then - writeln "Fortunately, only one parse tree is type correct.\n\ - \It helps (speed!) if you disambiguate your grammar or your input." - else (); - (idx, infrd_t, tye) + in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of + One(res) => + (if length ts > !Syntax.ambiguity_level + then writeln "Fortunately, only one parse tree is type correct.\n\ + \It helps (speed!) if you disambiguate your grammar or your input." + else (); + res) + | Errs(errs) => (warn(); error(cat_lines(map exn_type_msg errs))) + | Ambigs(us) => + (warn(); + let val old_show_brackets = !show_brackets + val _ = show_brackets := true; + val errs = cat_lines(map show_term us) + in show_brackets := old_show_brackets; + error("Error: More than one term is type correct:\n" ^ errs) + end) end; - (** extend signature **) (*exception ERROR*) (** signature extension functions **) (*exception ERROR*) diff -r 682139612060 -r 9e10962866b0 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Tue Mar 14 09:47:28 1995 +0100 +++ b/src/Pure/tactic.ML Tue Mar 14 10:40:04 1995 +0100 @@ -220,15 +220,10 @@ terms that are substituted contain (term or type) unknowns from the goal, because it is unable to instantiate goal unknowns at the same time. - The type checker freezes all flexible type vars that were introduced during - type inference and still remain in the term at the end. This avoids the - introduction of flexible type vars in goals and other places where they - could cause complications. If you really want a flexible type var, you - have to put it in yourself as a constraint. - - This policy breaks down when a list of substitutions is type checked: later - pairs may force type instantiations in earlier pairs, which is impossible, - because the type vars in the earlier pairs are already frozen. + The type checker is instructed not to freezes flexible type vars that + were introduced during type inference and still remain in the term at the + end. This increases flexibility but can introduce schematic type vars in + goals. *) fun res_inst_tac sinsts rule i = compose_inst_tac sinsts (false, rule, nprems_of rule) i;