Removed an old bug which made some simultaneous instantiations fail if they
authornipkow
Tue Mar 14 10:40:04 1995 +0100 (1995-03-14)
changeset 9529e10962866b0
parent 951 682139612060
child 953 17d7fad9c9a2
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.
src/Pure/drule.ML
src/Pure/sign.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/drule.ML	Tue Mar 14 09:47:28 1995 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Mar 14 10:40:04 1995 +0100
     1.3 @@ -249,6 +249,11 @@
     1.4  fun inst_failure ixn =
     1.5    error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
     1.6  
     1.7 +(* this code is a bit of a mess. add_cterm could be simplified greatly if
     1.8 +   simultaneous instantiations were read or at least type checked
     1.9 +   simultaneously rather than one after the other. This would make the tricky
    1.10 +   composition of implicit type instantiations (parameter tye) superfluous.
    1.11 +*)
    1.12  fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    1.13  let val {tsig,...} = Sign.rep_sg sign
    1.14      fun split([],tvs,vs) = (tvs,vs)
    1.15 @@ -269,11 +274,14 @@
    1.16                        Some T => typ_subst_TVars tye T
    1.17                      | None => absent ixn;
    1.18              val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
    1.19 -            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
    1.20 +            val cts' = (ixn,T,ct)::cts
    1.21 +            fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
    1.22              val used' = add_term_tvarnames(term_of ct,used);
    1.23 -        in ((cv,ct)::cts,tye2 @ tye,used') end
    1.24 +        in (map inst cts',tye2 @ tye,used') end
    1.25      val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
    1.26 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
    1.27 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
    1.28 +    map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
    1.29 +end;
    1.30  
    1.31  
    1.32  
    1.33 @@ -585,7 +593,8 @@
    1.34  (*Instantiate theorem th, reading instantiations under signature sg*)
    1.35  fun read_instantiate_sg sg sinsts th =
    1.36      let val ts = types_sorts th;
    1.37 -    in  instantiate (read_insts sg ts ts [] sinsts) th  end;
    1.38 +        val used = add_term_tvarnames(#prop(rep_thm th),[]);
    1.39 +    in  instantiate (read_insts sg ts ts used sinsts) th  end;
    1.40  
    1.41  (*Instantiate theorem th, reading instantiations under theory of th*)
    1.42  fun read_instantiate sinsts th =
     2.1 --- a/src/Pure/sign.ML	Tue Mar 14 09:47:28 1995 +0100
     2.2 +++ b/src/Pure/sign.ML	Tue Mar 14 10:40:04 1995 +0100
     2.3 @@ -272,52 +272,47 @@
     2.4  
     2.5      val ct = const_type sg;
     2.6  
     2.7 -    fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
     2.8 -         let val (infrd_t', tye', msg') = 
     2.9 -              let val (T,tye) =
    2.10 -                    Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    2.11 -              in (Some T, Some tye, msg) end
    2.12 -              handle TYPE arg => (None, None, exn_type_msg arg)
    2.13 -
    2.14 -             val old_show_brackets = !show_brackets;
    2.15 +    fun warn() =
    2.16 +      if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
    2.17 +      then (*no warning shown yet*)
    2.18 +           writeln "Warning: Currently parsed input \
    2.19 +                   \produces more than one parse tree.\n\
    2.20 +                   \For more information lower Syntax.ambiguity_level."
    2.21 +      else ();
    2.22  
    2.23 -             val _ = (show_brackets := true);
    2.24 -
    2.25 -             val msg'' = 
    2.26 -               if is_none idx then (if is_none infrd_t' then msg' else "")
    2.27 -               else if is_none infrd_t' then "" 
    2.28 -               else (if msg' = "" then 
    2.29 -                "Error: More than one term is type correct:\n" ^
    2.30 -                (show_term (the infrd_t)) else msg') ^ "\n" ^ 
    2.31 -                (show_term (the infrd_t')) ^ "\n";
    2.32 +    datatype result = One of int * term * (indexname * typ) list
    2.33 +                    | Errs of (string * typ list * term list)list
    2.34 +                    | Ambigs of term list;
    2.35  
    2.36 -         in show_brackets := old_show_brackets;
    2.37 -            if is_none infrd_t' then
    2.38 -              process_terms ts (idx, infrd_t, tye) msg'' (n+1)
    2.39 -            else
    2.40 -              process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
    2.41 -         end
    2.42 -      | process_terms [] (idx, infrd_t, tye) msg _ = 
    2.43 -          if msg = "" then (the idx, the infrd_t, the tye) 
    2.44 -          else
    2.45 -            (if length ts > 1 andalso length ts <= !Syntax.ambiguity_level then
    2.46 -                                                      (*no warning shown yet?*)
    2.47 -               writeln "Warning: Currently parsed input \
    2.48 -                       \produces more than one parse tree.\n\
    2.49 -                       \For more information lower Syntax.ambiguity_level."
    2.50 -             else ();
    2.51 -             error msg)
    2.52 +    fun process_term(res,(t,i)) =
    2.53 +       let val (u,tye) = Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    2.54 +       in case res of
    2.55 +            One(_,t0,_) => Ambigs([u,t0])
    2.56 +          | Errs _ => One(i,u,tye)
    2.57 +          | Ambigs(us) => Ambigs(u::us)
    2.58 +       end
    2.59 +       handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
    2.60 +                                     | _ => res);
    2.61  
    2.62 -    val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0;
    2.63 -  in if print_msg andalso length ts > !Syntax.ambiguity_level then
    2.64 -       writeln "Fortunately, only one parse tree is type correct.\n\
    2.65 -         \It helps (speed!) if you disambiguate your grammar or your input."
    2.66 -     else ();
    2.67 -     (idx, infrd_t, tye)
    2.68 +  in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
    2.69 +       One(res) =>
    2.70 +         (if length ts > !Syntax.ambiguity_level
    2.71 +          then writeln "Fortunately, only one parse tree is type correct.\n\
    2.72 +            \It helps (speed!) if you disambiguate your grammar or your input."
    2.73 +          else ();
    2.74 +          res)
    2.75 +     | Errs(errs) => (warn(); error(cat_lines(map exn_type_msg errs)))
    2.76 +     | Ambigs(us) =>
    2.77 +         (warn();
    2.78 +          let val old_show_brackets = !show_brackets
    2.79 +              val _ = show_brackets := true;
    2.80 +              val errs = cat_lines(map show_term us)
    2.81 +          in show_brackets := old_show_brackets;
    2.82 +             error("Error: More than one term is type correct:\n" ^ errs)
    2.83 +          end)
    2.84    end;
    2.85  
    2.86  
    2.87 -
    2.88  (** extend signature **)    (*exception ERROR*)
    2.89  
    2.90  (** signature extension functions **)  (*exception ERROR*)
     3.1 --- a/src/Pure/tactic.ML	Tue Mar 14 09:47:28 1995 +0100
     3.2 +++ b/src/Pure/tactic.ML	Tue Mar 14 10:40:04 1995 +0100
     3.3 @@ -220,15 +220,10 @@
     3.4    terms that are substituted contain (term or type) unknowns from the
     3.5    goal, because it is unable to instantiate goal unknowns at the same time.
     3.6  
     3.7 -  The type checker freezes all flexible type vars that were introduced during
     3.8 -  type inference and still remain in the term at the end.  This avoids the
     3.9 -  introduction of flexible type vars in goals and other places where they
    3.10 -  could cause complications.  If you really want a flexible type var, you
    3.11 -  have to put it in yourself as a constraint.
    3.12 -
    3.13 -  This policy breaks down when a list of substitutions is type checked: later
    3.14 -  pairs may force type instantiations in earlier pairs, which is impossible,
    3.15 -  because the type vars in the earlier pairs are already frozen.
    3.16 +  The type checker is instructed not to freezes flexible type vars that
    3.17 +  were introduced during type inference and still remain in the term at the
    3.18 +  end.  This increases flexibility but can introduce schematic type vars in
    3.19 +  goals.
    3.20  *)
    3.21  fun res_inst_tac sinsts rule i =
    3.22      compose_inst_tac sinsts (false, rule, nprems_of rule) i;