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.
--- 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 =
--- 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*)
--- 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;