src/Pure/sign.ML
changeset 623 ca9f5dbab880
parent 620 f787eb061618
child 679 a682bbf70dc6
     1.1 --- a/src/Pure/sign.ML	Tue Sep 27 14:23:46 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Oct 04 13:01:17 1994 +0100
     1.3 @@ -39,7 +39,8 @@
     1.4      val certify_term: sg -> term -> term * typ * int
     1.5      val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.6      val infer_types: sg -> (indexname -> typ option) ->
     1.7 -      (indexname -> sort option) -> term * typ -> term * (indexname * typ) list
     1.8 +      (indexname -> sort option) -> bool -> term list * typ ->
     1.9 +      int * term * (indexname * typ) list
    1.10      val add_classes: (class * class list) list -> sg -> sg
    1.11      val add_classrel: (class * class) list -> sg -> sg
    1.12      val add_defsort: sort -> sg -> sg
    1.13 @@ -243,7 +244,7 @@
    1.14  
    1.15  (** infer_types **)         (*exception ERROR*)
    1.16  
    1.17 -fun infer_types sg types sorts (t, T) =
    1.18 +fun infer_types sg types sorts print_msg (ts, T) =
    1.19    let
    1.20      val Sg {tsig, ...} = sg;
    1.21      val show_typ = string_of_typ sg;
    1.22 @@ -251,17 +252,57 @@
    1.23  
    1.24      fun term_err [] = ""
    1.25        | term_err [t] = "\nInvolving this term:\n" ^ show_term t
    1.26 -      | term_err ts = "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.27 +      | term_err ts = 
    1.28 +          "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.29  
    1.30      val T' = certify_typ sg T
    1.31        handle TYPE (msg, _, _) => error msg;
    1.32 -    val (t', tye) = Type.infer_types (tsig, const_type sg, types, sorts, T', t)
    1.33 -      handle TYPE (msg, Ts, ts) => error ("Type checking error: " ^ msg ^ "\n"
    1.34 -        ^ cat_lines (map show_typ Ts) ^ term_err ts);
    1.35 -  in (t', tye) end;
    1.36 +
    1.37 +    val ct = const_type sg;
    1.38 +
    1.39 +    fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
    1.40 +         let fun mk_some (x, y) = (Some x, Some y);
    1.41 +
    1.42 +             val ((infrd_t', tye'), msg') = 
    1.43 +              (mk_some (Type.infer_types (tsig, ct, types, sorts, T', t)), msg)
    1.44 +              handle TYPE (tmsg, Ts, ts) => 
    1.45 +                ((None, None), msg ^ "Type checking error: " ^ tmsg ^ "\n" ^
    1.46 +                 cat_lines (map show_typ Ts) ^ term_err ts ^ "\n")
    1.47 +
    1.48 +             val old_show_brackets = !show_brackets;
    1.49 +
    1.50 +             val _ = (show_brackets := true);
    1.51 +
    1.52 +             val msg'' = 
    1.53 +               if is_none idx then (if is_none infrd_t' then msg' else "")
    1.54 +               else if is_none infrd_t' then "" 
    1.55 +               else (if msg' = "" then 
    1.56 +                "Error: More than one term is type correct:\n" ^
    1.57 +                (show_term (the infrd_t)) else msg') ^ "\n" ^ 
    1.58 +                (show_term (the infrd_t')) ^ "\n";
    1.59 +
    1.60 +             val _ = (show_brackets := old_show_brackets);
    1.61 +         in if is_none infrd_t' then
    1.62 +              process_terms ts (idx, infrd_t, tye) msg'' (n+1)
    1.63 +            else
    1.64 +              process_terms ts (Some n, infrd_t', tye') msg'' (n+1)
    1.65 +         end
    1.66 +      | process_terms [] (idx, infrd_t, tye) msg _ = 
    1.67 +          if msg = "" then (the idx, the infrd_t, the tye) 
    1.68 +          else error msg;
    1.69 +
    1.70 +    val (idx, infrd_t, tye) = process_terms ts (None, None, None) "" 0;
    1.71 +  in if print_msg andalso length ts > 1 then
    1.72 +       writeln "Fortunately, only one parse tree is type correct.\n\
    1.73 +         \It helps (speed!) if you disambiguate your grammar or your input."
    1.74 +     else ();
    1.75 +     (idx, infrd_t, tye)
    1.76 +  end;
    1.77  
    1.78  
    1.79  
    1.80 +(** extend signature **)    (*exception ERROR*)
    1.81 +
    1.82  (** signature extension functions **)  (*exception ERROR*)
    1.83  
    1.84  fun decls_of name_of mfixs =
    1.85 @@ -385,7 +426,9 @@
    1.86    (Syntax.extend_trfuns syn trfuns, tsig, ctab);
    1.87  
    1.88  fun ext_trrules (syn, tsig, ctab) xrules =
    1.89 -  (Syntax.extend_trrules syn xrules, tsig, ctab);
    1.90 +  (Syntax.extend_trrules syn
    1.91 +  (infer_types (Sg {tsig = tsig, const_tab = ctab, syn = syn, 
    1.92 +                   stamps = [ref "#"]}) (K None) (K None)) xrules, tsig, ctab);
    1.93  
    1.94  
    1.95  (* build signature *)
    1.96 @@ -491,4 +534,3 @@
    1.97  
    1.98  
    1.99  end;
   1.100 -