src/Pure/sign.ML
changeset 4249 34b7aafdc1bc
parent 4228 22e3f0368c85
child 4256 e768c42069bb
     1.1 --- a/src/Pure/sign.ML	Thu Nov 20 12:49:25 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Nov 20 12:50:57 1997 +0100
     1.3 @@ -58,13 +58,14 @@
     1.4    val intern_typ: sg -> xtyp -> typ
     1.5    val intern_term: sg -> xterm -> term
     1.6    val intern_tycons: sg -> xtyp -> typ
     1.7 -  val print_sg: sg -> unit
     1.8    val pretty_sg: sg -> Pretty.T
     1.9    val str_of_sg: sg -> string
    1.10    val pprint_sg: sg -> pprint_args -> unit
    1.11    val pretty_term: sg -> term -> Pretty.T
    1.12    val pretty_typ: sg -> typ -> Pretty.T
    1.13    val pretty_sort: sg -> sort -> Pretty.T
    1.14 +  val pretty_classrel: sg -> class * class -> Pretty.T
    1.15 +  val pretty_arity: sg -> string * sort list * sort -> Pretty.T
    1.16    val string_of_term: sg -> term -> string
    1.17    val string_of_typ: sg -> typ -> string
    1.18    val string_of_sort: sg -> sort -> string
    1.19 @@ -79,7 +80,10 @@
    1.20    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.21    val infer_types: sg -> (indexname -> typ option) ->
    1.22      (indexname -> sort option) -> string list -> bool
    1.23 -    -> xterm list * typ -> int * term * (indexname * typ) list
    1.24 +    -> xterm list * typ -> term * (indexname * typ) list
    1.25 +  val infer_types_simult: sg -> (indexname -> typ option) ->
    1.26 +    (indexname -> sort option) -> string list -> bool
    1.27 +    -> (xterm list * typ) list -> term list * (indexname * typ) list
    1.28    val add_classes: (bclass * xclass list) list -> sg -> sg
    1.29    val add_classes_i: (bclass * class list) list -> sg -> sg
    1.30    val add_classrel: (xclass * xclass) list -> sg -> sg
    1.31 @@ -124,7 +128,7 @@
    1.32    val class_of_const: string -> class
    1.33  end;
    1.34  
    1.35 -structure Sign : SIGN =
    1.36 +structure Sign: SIGN =
    1.37  struct
    1.38  
    1.39  
    1.40 @@ -370,11 +374,11 @@
    1.41  
    1.42  
    1.43  
    1.44 -(** pretty printing of terms and types **)
    1.45 +(** pretty printing of terms, types etc. **)
    1.46  
    1.47 -fun pretty_term (sg as Sg (_, {syn, spaces, ...})) t =
    1.48 +fun pretty_term (sg as Sg ({stamps, ...}, {syn, spaces, ...})) t =
    1.49    Syntax.pretty_term syn
    1.50 -    ("CPure" mem_string (stamp_names_of sg))
    1.51 +    (exists (equal "CPure" o !) stamps)
    1.52      (if ! long_names then t else extrn_term spaces t);
    1.53  
    1.54  fun pretty_typ (Sg (_, {syn, spaces, ...})) T =
    1.55 @@ -412,66 +416,6 @@
    1.56  
    1.57  
    1.58  
    1.59 -(** print signature **)
    1.60 -
    1.61 -fun print_sg sg =
    1.62 -  let
    1.63 -    fun prt_cls c = pretty_sort sg [c];
    1.64 -    fun prt_sort S = pretty_sort sg S;
    1.65 -    fun prt_arity t (c, Ss) = pretty_arity sg (t, Ss, [c]);
    1.66 -    fun prt_typ ty = Pretty.quote (pretty_typ sg ty);
    1.67 -
    1.68 -    val ext_class = cond_extern sg classK;
    1.69 -    val ext_tycon = cond_extern sg typeK;
    1.70 -    val ext_const = cond_extern sg constK;
    1.71 -
    1.72 -
    1.73 -    fun pretty_space (kind, space) = Pretty.block (Pretty.breaks
    1.74 -      (map Pretty.str (kind ^ ":" :: map quote (NameSpace.dest space))));
    1.75 -
    1.76 -    fun pretty_classes cs = Pretty.block
    1.77 -      (Pretty.breaks (Pretty.str "classes:" :: map prt_cls cs));
    1.78 -
    1.79 -    fun pretty_classrel (c, cs) = Pretty.block
    1.80 -      (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
    1.81 -        Pretty.commas (map prt_cls cs));
    1.82 -
    1.83 -    fun pretty_default S = Pretty.block
    1.84 -      [Pretty.str "default:", Pretty.brk 1, pretty_sort sg S];
    1.85 -
    1.86 -    fun pretty_ty (t, n) = Pretty.block
    1.87 -      [Pretty.str (ext_tycon t), Pretty.str (" " ^ string_of_int n)];
    1.88 -
    1.89 -    fun pretty_abbr (t, (vs, rhs)) = Pretty.block
    1.90 -      [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.91 -        Pretty.str " =", Pretty.brk 1, prt_typ rhs];
    1.92 -
    1.93 -    fun pretty_arities (t, ars) = map (prt_arity t) ars;
    1.94 -
    1.95 -    fun pretty_const (c, ty) = Pretty.block
    1.96 -      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
    1.97 -
    1.98 -    val Sg (_, {self = _, tsig, const_tab, syn = _, path, spaces, data}) = sg;
    1.99 -    val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
   1.100 -    val {classes, classrel, default, tycons, abbrs, arities} =
   1.101 -      Type.rep_tsig tsig;
   1.102 -    val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
   1.103 -  in
   1.104 -    Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names_of sg));
   1.105 -    Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data));
   1.106 -    Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
   1.107 -    Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
   1.108 -    Pretty.writeln (pretty_classes classes);
   1.109 -    Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
   1.110 -    Pretty.writeln (pretty_default default);
   1.111 -    Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
   1.112 -    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs));
   1.113 -    Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities arities)));
   1.114 -    Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
   1.115 -  end;
   1.116 -
   1.117 -
   1.118 -
   1.119  (** read types **)  (*exception ERROR*)
   1.120  
   1.121  fun err_in_type s =
   1.122 @@ -574,61 +518,58 @@
   1.123  (** infer_types **)         (*exception ERROR*)
   1.124  
   1.125  (*
   1.126 -  ts: list of alternative parses (hopefully only one is type-correct)
   1.127 -  T: expected type
   1.128 -
   1.129    def_type: partial map from indexnames to types (constrains Frees, Vars)
   1.130    def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   1.131    used: list of already used type variables
   1.132    freeze: if true then generated parameters are turned into TFrees, else TVars
   1.133 +
   1.134 +  termss: lists of alternative parses (only one combination should be type-correct)
   1.135 +  typs: expected types
   1.136  *)
   1.137  
   1.138 -fun infer_types sg def_type def_sort used freeze (ts, T) =
   1.139 +fun infer_types_simult sg def_type def_sort used freeze args =
   1.140    let
   1.141      val tsig = tsig_of sg;
   1.142      val prt =
   1.143        setmp Syntax.show_brackets true
   1.144          (setmp long_names true (pretty_term sg));
   1.145      val prT = setmp long_names true (pretty_typ sg);
   1.146 -    val infer = Type.infer_types prt prT tsig (const_type sg) def_type def_sort
   1.147 -      (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze;
   1.148 +
   1.149 +    val termss = foldr multiply (map fst args, [[]]);
   1.150 +    val typs =
   1.151 +      map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   1.152  
   1.153 -    val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg;
   1.154 +    fun infer ts = OK
   1.155 +      (Type.infer_types prt prT tsig (const_type sg) def_type def_sort
   1.156 +        (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze typs ts)
   1.157 +      handle TYPE (msg, _, _) => Error msg;
   1.158  
   1.159 -    fun warn () =
   1.160 -      if length ts > 1 andalso length ts <= ! Syntax.ambiguity_level
   1.161 -      then (*no warning shown yet*)
   1.162 -        warning "Got more than one parse tree.\n\
   1.163 +    val err_results = map infer termss;
   1.164 +    val errs = mapfilter get_error err_results;
   1.165 +    val results = mapfilter get_ok err_results;
   1.166 +
   1.167 +    val ambiguity = length termss;	(* FIXME !? *)
   1.168 +    (* FIXME to syntax.ML!? *)
   1.169 +    fun ambig_msg () =
   1.170 +      if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level
   1.171 +      then
   1.172 +        error_msg "Got more than one parse tree.\n\
   1.173            \Retry with smaller Syntax.ambiguity_level for more information."
   1.174        else ();
   1.175 -
   1.176 -    datatype result =
   1.177 -      One of int * term * (indexname * typ) list |
   1.178 -      Errs of string list |
   1.179 -      Ambigs of term list;
   1.180 +  in
   1.181 +    if null results then (ambig_msg (); error (cat_lines errs))
   1.182 +    else if length results = 1 then
   1.183 +      (if ambiguity > ! Syntax.ambiguity_level then
   1.184 +        warning "Fortunately, only one parse tree is type correct.\n\
   1.185 +          \You may still want to disambiguate your grammar or your input."
   1.186 +      else (); hd results)
   1.187 +    else (ambig_msg (); error ("More than one term is type correct:\n" ^
   1.188 +      (cat_lines (map (Pretty.string_of o prt) (flat (map fst results))))))
   1.189 +  end;
   1.190  
   1.191 -    fun process_term (res, (t, i)) =
   1.192 -      let val ([u], tye) = infer [T'] [t] in
   1.193 -        (case res of
   1.194 -          One (_, t0, _) => Ambigs ([u, t0])
   1.195 -        | Errs _ => One (i, u, tye)
   1.196 -        | Ambigs us => Ambigs (u :: us))
   1.197 -      end handle TYPE (msg, _, _) =>
   1.198 -        (case res of
   1.199 -          Errs errs => Errs (msg :: errs)
   1.200 -        | _ => res);
   1.201 -  in
   1.202 -    (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
   1.203 -      One res =>
   1.204 -       (if length ts > ! Syntax.ambiguity_level then
   1.205 -          warning "Fortunately, only one parse tree is type correct.\n\
   1.206 -            \You may still want to disambiguate your grammar or your input."
   1.207 -        else (); res)
   1.208 -    | Errs errs => (warn (); error (cat_lines errs))
   1.209 -    | Ambigs us =>
   1.210 -        (warn (); error ("More than one term is type correct:\n" ^
   1.211 -          (cat_lines (map (Pretty.string_of o prt) us)))))
   1.212 -  end;
   1.213 +
   1.214 +fun infer_types sg def_type def_sort used freeze tsT =
   1.215 +  apfst hd (infer_types_simult sg def_type def_sort used freeze [tsT]);
   1.216  
   1.217  
   1.218