src/Pure/sign.ML
changeset 2979 db6941221197
parent 2963 f3b5af1c5a67
child 3552 f348e8a2db4b
     1.1 --- a/src/Pure/sign.ML	Thu Apr 17 18:45:43 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 17 18:46:58 1997 +0200
     1.3 @@ -36,7 +36,6 @@
     1.4    val certify_typ: sg -> typ -> typ
     1.5    val certify_term: sg -> term -> term * typ * int
     1.6    val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.7 -  val exn_type_msg: sg -> string * typ list * term list -> string
     1.8    val infer_types: sg -> (indexname -> typ option) ->
     1.9      (indexname -> sort option) -> string list -> bool
    1.10      -> term list * typ -> int * term * (indexname * typ) list
    1.11 @@ -77,6 +76,7 @@
    1.12  structure Sign : SIGN =
    1.13  struct
    1.14  
    1.15 +
    1.16  (** datatype sg **)
    1.17  
    1.18  (*the "ref" in stamps ensures that no two signatures are identical -- it is
    1.19 @@ -93,9 +93,8 @@
    1.20  val tsig_of = #tsig o rep_sg;
    1.21  
    1.22  
    1.23 -(* stamps *)
    1.24 +(* inclusion and equality *)
    1.25  
    1.26 -(*inclusion, equality*)
    1.27  local
    1.28    (*avoiding polymorphic equality: factor 10 speedup*)
    1.29    fun mem_stamp (_:string ref, []) = false
    1.30 @@ -136,8 +135,7 @@
    1.31  
    1.32  (* consts *)
    1.33  
    1.34 -fun const_type (Sg {const_tab, ...}) c =
    1.35 -  Symtab.lookup (const_tab, c);
    1.36 +fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
    1.37  
    1.38  
    1.39  (* classes and sorts *)
    1.40 @@ -148,6 +146,7 @@
    1.41  val norm_sort = Type.norm_sort o tsig_of;
    1.42  val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.43  
    1.44 +(* FIXME move to Sorts? *)
    1.45  fun pretty_sort [c] = Pretty.str c
    1.46    | pretty_sort cs = Pretty.str_list "{" "}" cs;
    1.47  
    1.48 @@ -193,15 +192,14 @@
    1.49    in
    1.50      Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
    1.51      Pretty.writeln (Pretty.strs ("classes:" :: classes));
    1.52 -    Pretty.writeln (Pretty.big_list "classrel:"
    1.53 -                      (map pretty_classrel classrel));
    1.54 +    Pretty.writeln (Pretty.big_list "classrel:" (map pretty_classrel classrel));
    1.55      Pretty.writeln (pretty_default default);
    1.56      Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
    1.57      Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
    1.58      Pretty.writeln (Pretty.big_list "arities:"
    1.59 -                      (List.concat (map pretty_arities arities)));
    1.60 +      (List.concat (map pretty_arities arities)));
    1.61      Pretty.writeln (Pretty.big_list "consts:"
    1.62 -                      (map (pretty_const syn) (Symtab.dest const_tab)))
    1.63 +      (map (pretty_const syn) (Symtab.dest const_tab)))
    1.64    end;
    1.65  
    1.66  
    1.67 @@ -251,44 +249,51 @@
    1.68  
    1.69  fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
    1.70  
    1.71 -(* check for duplicate TVars with distinct sorts *)
    1.72 -fun nodup_TVars(tvars,T) = (case T of
    1.73 -      Type(_,Ts) => nodup_TVars_list (tvars,Ts)
    1.74 -    | TFree _ => tvars
    1.75 -    | TVar(v as (a,S)) =>
    1.76 -        (case assoc_string_int(tvars,a) of
    1.77 -           Some(S') => if S=S' then tvars
    1.78 -                       else raise_type
    1.79 -                            ("Type variable "^Syntax.string_of_vname a^
    1.80 -                             " has two distinct sorts") [TVar(a,S'),T] []
    1.81 -         | None => v::tvars))
    1.82 -and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
    1.83 -    nodup_TVars_list (tvars,[]) = tvars
    1.84 -  | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
    1.85 -						      Ts);
    1.86 +(*check for duplicate TVars with distinct sorts*)
    1.87 +fun nodup_TVars (tvars, T) =
    1.88 +  (case T of
    1.89 +    Type (_, Ts) => nodup_TVars_list (tvars, Ts)
    1.90 +  | TFree _ => tvars
    1.91 +  | TVar (v as (a, S)) =>
    1.92 +      (case assoc_string_int (tvars, a) of
    1.93 +        Some S' =>
    1.94 +          if S = S' then tvars
    1.95 +          else raise_type ("Type variable " ^ Syntax.string_of_vname a ^
    1.96 +            " has two distinct sorts") [TVar (a, S'), T] []
    1.97 +      | None => v :: tvars))
    1.98 +(*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
    1.99 +and nodup_TVars_list (tvars, []) = tvars
   1.100 +  | nodup_TVars_list (tvars, T :: Ts) =
   1.101 +      nodup_TVars_list (nodup_TVars (tvars, T), Ts);
   1.102  
   1.103 -(* check for duplicate Vars with distinct types *)
   1.104 +(*check for duplicate Vars with distinct types*)
   1.105  fun nodup_Vars tm =
   1.106 -let fun nodups vars tvars tm = (case tm of
   1.107 -          Const(c,T) => (vars, nodup_TVars(tvars,T))
   1.108 -        | Free(a,T) => (vars, nodup_TVars(tvars,T))
   1.109 -        | Var(v as (ixn,T)) =>
   1.110 -            (case assoc_string_int(vars,ixn) of
   1.111 -               Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
   1.112 -                           else raise_type
   1.113 -                             ("Variable "^Syntax.string_of_vname ixn^
   1.114 -                              " has two distinct types") [T',T] []
   1.115 -             | None => (v::vars,tvars))
   1.116 -        | Bound _ => (vars,tvars)
   1.117 -        | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t
   1.118 -        | s$t => let val (vars',tvars') = nodups vars tvars s
   1.119 -                 in nodups vars' tvars' t end);
   1.120 -in nodups [] [] tm; () end;
   1.121 +  let
   1.122 +    fun nodups vars tvars tm =
   1.123 +      (case tm of
   1.124 +        Const (c, T) => (vars, nodup_TVars (tvars, T))
   1.125 +      | Free (a, T) => (vars, nodup_TVars (tvars, T))
   1.126 +      | Var (v as (ixn, T)) =>
   1.127 +          (case assoc_string_int (vars, ixn) of
   1.128 +            Some T' =>
   1.129 +              if T = T' then (vars, nodup_TVars (tvars, T))
   1.130 +              else raise_type ("Variable " ^ Syntax.string_of_vname ixn ^
   1.131 +                " has two distinct types") [T', T] []
   1.132 +          | None => (v :: vars, tvars))
   1.133 +      | Bound _ => (vars, tvars)
   1.134 +      | Abs(_, T, t) => nodups vars (nodup_TVars (tvars, T)) t
   1.135 +      | s $ t =>
   1.136 +          let val (vars',tvars') = nodups vars tvars s in
   1.137 +            nodups vars' tvars' t
   1.138 +          end);
   1.139 +  in nodups [] [] tm; () end;
   1.140 +
   1.141  
   1.142  fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   1.143    | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   1.144    | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
   1.145  
   1.146 +
   1.147  fun certify_term (sg as Sg {tsig, ...}) tm =
   1.148    let
   1.149      fun valid_const a T =
   1.150 @@ -316,82 +321,67 @@
   1.151    end;
   1.152  
   1.153  
   1.154 -(*package error messages from type checking*)
   1.155 -fun exn_type_msg sg (msg, Ts, ts) =
   1.156 -  let
   1.157 -    val show_typ = string_of_typ sg;
   1.158 -    val show_term = set_ap Syntax.show_brackets true (string_of_term sg);
   1.159 -
   1.160 -    fun term_err [] = ""
   1.161 -      | term_err [t] = "\n\nInvolving this term:\n" ^ show_term t
   1.162 -      | term_err ts =
   1.163 -          "\n\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   1.164 -  in
   1.165 -    "\nType checking error: " ^ msg ^ "\n" ^
   1.166 -      cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
   1.167 -  end;
   1.168 -
   1.169 -
   1.170  
   1.171  (** infer_types **)         (*exception ERROR*)
   1.172  
   1.173 -(*ts is the list of alternative parses; only one is hoped to be type-correct.
   1.174 -  T is the expected type for the correct term.
   1.175 -  Other standard arguments:
   1.176 -    types is a partial map from indexnames to types (constrains Free, Var).
   1.177 -    sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   1.178 -    used is the list of already used type variables.
   1.179 -    If freeze then internal TVars are turned into TFrees, else TVars.*)
   1.180 -fun infer_types sg types sorts used freeze (ts, T) =
   1.181 +(*
   1.182 +  ts: list of alternative parses (hopefully only one is type-correct)
   1.183 +  T: expected type
   1.184 +
   1.185 +  def_type: partial map from indexnames to types (constrains Frees, Vars)
   1.186 +  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   1.187 +  used: list of already used type variables
   1.188 +  freeze: if true then generated parameters are turned into TFrees, else TVars
   1.189 +*)
   1.190 +
   1.191 +fun infer_types sg def_type def_sort used freeze (ts, T) =
   1.192    let
   1.193      val Sg {tsig, ...} = sg;
   1.194 +    val prt = setmp Syntax.show_brackets true (pretty_term sg);
   1.195 +    val prT = pretty_typ sg;
   1.196 +    val infer = Type.infer_types prt prT tsig (const_type sg)
   1.197 +      def_type def_sort used freeze;
   1.198  
   1.199 -    val T' = certify_typ sg T handle TYPE arg => error (exn_type_msg sg arg);
   1.200 -
   1.201 -    val ct = const_type sg;
   1.202 +    val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg;
   1.203  
   1.204 -    fun warn() =
   1.205 -      if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
   1.206 +    fun warn () =
   1.207 +      if length ts > 1 andalso length ts <= ! Syntax.ambiguity_level
   1.208        then (*no warning shown yet*)
   1.209 -           warning "Currently parsed input \
   1.210 -                   \produces more than one parse tree.\n\
   1.211 -                   \For more information lower Syntax.ambiguity_level."
   1.212 +        warning "Currently parsed input \
   1.213 +          \produces more than one parse tree.\n\
   1.214 +          \For more information lower Syntax.ambiguity_level."
   1.215        else ();
   1.216  
   1.217 -    datatype result = One of int * term * (indexname * typ) list
   1.218 -                    | Errs of (string * typ list * term list)list
   1.219 -                    | Ambigs of term list;
   1.220 -
   1.221 -    fun process_term(res,(t,i)) =
   1.222 -       let val ([u],tye) = 
   1.223 -	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   1.224 -       in case res of
   1.225 -            One(_,t0,_) => Ambigs([u,t0])
   1.226 -          | Errs _ => One(i,u,tye)
   1.227 -          | Ambigs(us) => Ambigs(u::us)
   1.228 -       end
   1.229 -       handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
   1.230 -                                     | _ => res);
   1.231 +    datatype result =
   1.232 +      One of int * term * (indexname * typ) list |
   1.233 +      Errs of string list |
   1.234 +      Ambigs of term list;
   1.235  
   1.236 -  in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
   1.237 -       One(res) =>
   1.238 -         (if length ts > !Syntax.ambiguity_level
   1.239 -          then writeln "Fortunately, only one parse tree is type correct.\n\
   1.240 +    fun process_term (res, (t, i)) =
   1.241 +      let val ([u], tye) = infer [T'] [t] in
   1.242 +        (case res of
   1.243 +          One (_, t0, _) => Ambigs ([u, t0])
   1.244 +        | Errs _ => One (i, u, tye)
   1.245 +        | Ambigs us => Ambigs (u :: us))
   1.246 +      end handle TYPE (msg, _, _) =>
   1.247 +        (case res of
   1.248 +          Errs errs => Errs (msg :: errs)
   1.249 +        | _ => res);
   1.250 +  in
   1.251 +    (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
   1.252 +      One res =>
   1.253 +       (if length ts > ! Syntax.ambiguity_level then
   1.254 +          writeln "Fortunately, only one parse tree is type correct.\n\
   1.255              \It helps (speed!) if you disambiguate your grammar or your input."
   1.256 -          else ();
   1.257 -          res)
   1.258 -     | Errs(errs) => (warn(); error(cat_lines(map (exn_type_msg sg) errs)))
   1.259 -     | Ambigs(us) =>
   1.260 -         (warn();
   1.261 -          let val old_show_brackets = !show_brackets
   1.262 -              val dummy = show_brackets := true;
   1.263 -              val errs = cat_lines(map (string_of_term sg) us)
   1.264 -          in show_brackets := old_show_brackets;
   1.265 -             error("Error: More than one term is type correct:\n" ^ errs)
   1.266 -          end)
   1.267 +        else (); res)
   1.268 +    | Errs errs => (warn (); error (cat_lines errs))
   1.269 +    | Ambigs us =>
   1.270 +        (warn (); error ("Error: More than one term is type correct:\n" ^
   1.271 +          (cat_lines (map (Pretty.string_of o prt) us)))))
   1.272    end;
   1.273  
   1.274  
   1.275 +
   1.276  (** extend signature **)    (*exception ERROR*)
   1.277  
   1.278  (** signature extension functions **)  (*exception ERROR*)
   1.279 @@ -461,7 +451,7 @@
   1.280  
   1.281  fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   1.282    let
   1.283 -    fun prep_const (c, ty, mx) = 
   1.284 +    fun prep_const (c, ty, mx) =
   1.285       (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.286         handle TYPE (msg, _, _)
   1.287           => (writeln msg; err_in_const (Syntax.const_name c mx));