src/Pure/sign.ML
changeset 2979 db6941221197
parent 2963 f3b5af1c5a67
child 3552 f348e8a2db4b
equal deleted inserted replaced
2978:83a4c4f79dcd 2979:db6941221197
    34   val pprint_term: sg -> term -> pprint_args -> unit
    34   val pprint_term: sg -> term -> pprint_args -> unit
    35   val pprint_typ: sg -> typ -> pprint_args -> unit
    35   val pprint_typ: sg -> typ -> pprint_args -> unit
    36   val certify_typ: sg -> typ -> typ
    36   val certify_typ: sg -> typ -> typ
    37   val certify_term: sg -> term -> term * typ * int
    37   val certify_term: sg -> term -> term * typ * int
    38   val read_typ: sg * (indexname -> sort option) -> string -> typ
    38   val read_typ: sg * (indexname -> sort option) -> string -> typ
    39   val exn_type_msg: sg -> string * typ list * term list -> string
       
    40   val infer_types: sg -> (indexname -> typ option) ->
    39   val infer_types: sg -> (indexname -> typ option) ->
    41     (indexname -> sort option) -> string list -> bool
    40     (indexname -> sort option) -> string list -> bool
    42     -> term list * typ -> int * term * (indexname * typ) list
    41     -> term list * typ -> int * term * (indexname * typ) list
    43   val add_classes: (class * class list) list -> sg -> sg
    42   val add_classes: (class * class list) list -> sg -> sg
    44   val add_classrel: (class * class) list -> sg -> sg
    43   val add_classrel: (class * class) list -> sg -> sg
    75   end;
    74   end;
    76 
    75 
    77 structure Sign : SIGN =
    76 structure Sign : SIGN =
    78 struct
    77 struct
    79 
    78 
       
    79 
    80 (** datatype sg **)
    80 (** datatype sg **)
    81 
    81 
    82 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    82 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    83   impossible to forge a signature*)
    83   impossible to forge a signature*)
    84 
    84 
    91 
    91 
    92 fun rep_sg (Sg args) = args;
    92 fun rep_sg (Sg args) = args;
    93 val tsig_of = #tsig o rep_sg;
    93 val tsig_of = #tsig o rep_sg;
    94 
    94 
    95 
    95 
    96 (* stamps *)
    96 (* inclusion and equality *)
    97 
    97 
    98 (*inclusion, equality*)
       
    99 local
    98 local
   100   (*avoiding polymorphic equality: factor 10 speedup*)
    99   (*avoiding polymorphic equality: factor 10 speedup*)
   101   fun mem_stamp (_:string ref, []) = false
   100   fun mem_stamp (_:string ref, []) = false
   102     | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
   101     | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
   103 
   102 
   134   | is_draft _ = false;
   133   | is_draft _ = false;
   135 
   134 
   136 
   135 
   137 (* consts *)
   136 (* consts *)
   138 
   137 
   139 fun const_type (Sg {const_tab, ...}) c =
   138 fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
   140   Symtab.lookup (const_tab, c);
       
   141 
   139 
   142 
   140 
   143 (* classes and sorts *)
   141 (* classes and sorts *)
   144 
   142 
   145 val classes = #classes o Type.rep_tsig o tsig_of;
   143 val classes = #classes o Type.rep_tsig o tsig_of;
   146 
   144 
   147 val subsort = Type.subsort o tsig_of;
   145 val subsort = Type.subsort o tsig_of;
   148 val norm_sort = Type.norm_sort o tsig_of;
   146 val norm_sort = Type.norm_sort o tsig_of;
   149 val nonempty_sort = Type.nonempty_sort o tsig_of;
   147 val nonempty_sort = Type.nonempty_sort o tsig_of;
   150 
   148 
       
   149 (* FIXME move to Sorts? *)
   151 fun pretty_sort [c] = Pretty.str c
   150 fun pretty_sort [c] = Pretty.str c
   152   | pretty_sort cs = Pretty.str_list "{" "}" cs;
   151   | pretty_sort cs = Pretty.str_list "{" "}" cs;
   153 
   152 
   154 
   153 
   155 
   154 
   191     val {classes, classrel, default, tycons, abbrs, arities} =
   190     val {classes, classrel, default, tycons, abbrs, arities} =
   192       Type.rep_tsig tsig;
   191       Type.rep_tsig tsig;
   193   in
   192   in
   194     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   193     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   195     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   194     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   196     Pretty.writeln (Pretty.big_list "classrel:"
   195     Pretty.writeln (Pretty.big_list "classrel:" (map pretty_classrel classrel));
   197                       (map pretty_classrel classrel));
       
   198     Pretty.writeln (pretty_default default);
   196     Pretty.writeln (pretty_default default);
   199     Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
   197     Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
   200     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
   198     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
   201     Pretty.writeln (Pretty.big_list "arities:"
   199     Pretty.writeln (Pretty.big_list "arities:"
   202                       (List.concat (map pretty_arities arities)));
   200       (List.concat (map pretty_arities arities)));
   203     Pretty.writeln (Pretty.big_list "consts:"
   201     Pretty.writeln (Pretty.big_list "consts:"
   204                       (map (pretty_const syn) (Symtab.dest const_tab)))
   202       (map (pretty_const syn) (Symtab.dest const_tab)))
   205   end;
   203   end;
   206 
   204 
   207 
   205 
   208 fun pretty_sg (Sg {stamps, ...}) =
   206 fun pretty_sg (Sg {stamps, ...}) =
   209   Pretty.str_list "{" "}" (stamp_names stamps);
   207   Pretty.str_list "{" "}" (stamp_names stamps);
   249 
   247 
   250 (** certify types and terms **)   (*exception TYPE*)
   248 (** certify types and terms **)   (*exception TYPE*)
   251 
   249 
   252 fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
   250 fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
   253 
   251 
   254 (* check for duplicate TVars with distinct sorts *)
   252 (*check for duplicate TVars with distinct sorts*)
   255 fun nodup_TVars(tvars,T) = (case T of
   253 fun nodup_TVars (tvars, T) =
   256       Type(_,Ts) => nodup_TVars_list (tvars,Ts)
   254   (case T of
   257     | TFree _ => tvars
   255     Type (_, Ts) => nodup_TVars_list (tvars, Ts)
   258     | TVar(v as (a,S)) =>
   256   | TFree _ => tvars
   259         (case assoc_string_int(tvars,a) of
   257   | TVar (v as (a, S)) =>
   260            Some(S') => if S=S' then tvars
   258       (case assoc_string_int (tvars, a) of
   261                        else raise_type
   259         Some S' =>
   262                             ("Type variable "^Syntax.string_of_vname a^
   260           if S = S' then tvars
   263                              " has two distinct sorts") [TVar(a,S'),T] []
   261           else raise_type ("Type variable " ^ Syntax.string_of_vname a ^
   264          | None => v::tvars))
   262             " has two distinct sorts") [TVar (a, S'), T] []
   265 and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
   263       | None => v :: tvars))
   266     nodup_TVars_list (tvars,[]) = tvars
   264 (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
   267   | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
   265 and nodup_TVars_list (tvars, []) = tvars
   268 						      Ts);
   266   | nodup_TVars_list (tvars, T :: Ts) =
   269 
   267       nodup_TVars_list (nodup_TVars (tvars, T), Ts);
   270 (* check for duplicate Vars with distinct types *)
   268 
       
   269 (*check for duplicate Vars with distinct types*)
   271 fun nodup_Vars tm =
   270 fun nodup_Vars tm =
   272 let fun nodups vars tvars tm = (case tm of
   271   let
   273           Const(c,T) => (vars, nodup_TVars(tvars,T))
   272     fun nodups vars tvars tm =
   274         | Free(a,T) => (vars, nodup_TVars(tvars,T))
   273       (case tm of
   275         | Var(v as (ixn,T)) =>
   274         Const (c, T) => (vars, nodup_TVars (tvars, T))
   276             (case assoc_string_int(vars,ixn) of
   275       | Free (a, T) => (vars, nodup_TVars (tvars, T))
   277                Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
   276       | Var (v as (ixn, T)) =>
   278                            else raise_type
   277           (case assoc_string_int (vars, ixn) of
   279                              ("Variable "^Syntax.string_of_vname ixn^
   278             Some T' =>
   280                               " has two distinct types") [T',T] []
   279               if T = T' then (vars, nodup_TVars (tvars, T))
   281              | None => (v::vars,tvars))
   280               else raise_type ("Variable " ^ Syntax.string_of_vname ixn ^
   282         | Bound _ => (vars,tvars)
   281                 " has two distinct types") [T', T] []
   283         | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t
   282           | None => (v :: vars, tvars))
   284         | s$t => let val (vars',tvars') = nodups vars tvars s
   283       | Bound _ => (vars, tvars)
   285                  in nodups vars' tvars' t end);
   284       | Abs(_, T, t) => nodups vars (nodup_TVars (tvars, T)) t
   286 in nodups [] [] tm; () end;
   285       | s $ t =>
       
   286           let val (vars',tvars') = nodups vars tvars s in
       
   287             nodups vars' tvars' t
       
   288           end);
       
   289   in nodups [] [] tm; () end;
       
   290 
   287 
   291 
   288 fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   292 fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   289   | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   293   | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   290   | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
   294   | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
       
   295 
   291 
   296 
   292 fun certify_term (sg as Sg {tsig, ...}) tm =
   297 fun certify_term (sg as Sg {tsig, ...}) tm =
   293   let
   298   let
   294     fun valid_const a T =
   299     fun valid_const a T =
   295       (case const_type sg a of
   300       (case const_type sg a of
   314       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   319       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   315     | errs => raise_type (cat_lines errs) [] [norm_tm])
   320     | errs => raise_type (cat_lines errs) [] [norm_tm])
   316   end;
   321   end;
   317 
   322 
   318 
   323 
   319 (*package error messages from type checking*)
       
   320 fun exn_type_msg sg (msg, Ts, ts) =
       
   321   let
       
   322     val show_typ = string_of_typ sg;
       
   323     val show_term = set_ap Syntax.show_brackets true (string_of_term sg);
       
   324 
       
   325     fun term_err [] = ""
       
   326       | term_err [t] = "\n\nInvolving this term:\n" ^ show_term t
       
   327       | term_err ts =
       
   328           "\n\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
       
   329   in
       
   330     "\nType checking error: " ^ msg ^ "\n" ^
       
   331       cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
       
   332   end;
       
   333 
       
   334 
       
   335 
   324 
   336 (** infer_types **)         (*exception ERROR*)
   325 (** infer_types **)         (*exception ERROR*)
   337 
   326 
   338 (*ts is the list of alternative parses; only one is hoped to be type-correct.
   327 (*
   339   T is the expected type for the correct term.
   328   ts: list of alternative parses (hopefully only one is type-correct)
   340   Other standard arguments:
   329   T: expected type
   341     types is a partial map from indexnames to types (constrains Free, Var).
   330 
   342     sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   331   def_type: partial map from indexnames to types (constrains Frees, Vars)
   343     used is the list of already used type variables.
   332   def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
   344     If freeze then internal TVars are turned into TFrees, else TVars.*)
   333   used: list of already used type variables
   345 fun infer_types sg types sorts used freeze (ts, T) =
   334   freeze: if true then generated parameters are turned into TFrees, else TVars
       
   335 *)
       
   336 
       
   337 fun infer_types sg def_type def_sort used freeze (ts, T) =
   346   let
   338   let
   347     val Sg {tsig, ...} = sg;
   339     val Sg {tsig, ...} = sg;
   348 
   340     val prt = setmp Syntax.show_brackets true (pretty_term sg);
   349     val T' = certify_typ sg T handle TYPE arg => error (exn_type_msg sg arg);
   341     val prT = pretty_typ sg;
   350 
   342     val infer = Type.infer_types prt prT tsig (const_type sg)
   351     val ct = const_type sg;
   343       def_type def_sort used freeze;
   352 
   344 
   353     fun warn() =
   345     val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg;
   354       if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
   346 
       
   347     fun warn () =
       
   348       if length ts > 1 andalso length ts <= ! Syntax.ambiguity_level
   355       then (*no warning shown yet*)
   349       then (*no warning shown yet*)
   356            warning "Currently parsed input \
   350         warning "Currently parsed input \
   357                    \produces more than one parse tree.\n\
   351           \produces more than one parse tree.\n\
   358                    \For more information lower Syntax.ambiguity_level."
   352           \For more information lower Syntax.ambiguity_level."
   359       else ();
   353       else ();
   360 
   354 
   361     datatype result = One of int * term * (indexname * typ) list
   355     datatype result =
   362                     | Errs of (string * typ list * term list)list
   356       One of int * term * (indexname * typ) list |
   363                     | Ambigs of term list;
   357       Errs of string list |
   364 
   358       Ambigs of term list;
   365     fun process_term(res,(t,i)) =
   359 
   366        let val ([u],tye) = 
   360     fun process_term (res, (t, i)) =
   367 	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   361       let val ([u], tye) = infer [T'] [t] in
   368        in case res of
   362         (case res of
   369             One(_,t0,_) => Ambigs([u,t0])
   363           One (_, t0, _) => Ambigs ([u, t0])
   370           | Errs _ => One(i,u,tye)
   364         | Errs _ => One (i, u, tye)
   371           | Ambigs(us) => Ambigs(u::us)
   365         | Ambigs us => Ambigs (u :: us))
   372        end
   366       end handle TYPE (msg, _, _) =>
   373        handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
   367         (case res of
   374                                      | _ => res);
   368           Errs errs => Errs (msg :: errs)
   375 
   369         | _ => res);
   376   in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
   370   in
   377        One(res) =>
   371     (case foldl process_term (Errs [], ts ~~ (0 upto (length ts - 1))) of
   378          (if length ts > !Syntax.ambiguity_level
   372       One res =>
   379           then writeln "Fortunately, only one parse tree is type correct.\n\
   373        (if length ts > ! Syntax.ambiguity_level then
       
   374           writeln "Fortunately, only one parse tree is type correct.\n\
   380             \It helps (speed!) if you disambiguate your grammar or your input."
   375             \It helps (speed!) if you disambiguate your grammar or your input."
   381           else ();
   376         else (); res)
   382           res)
   377     | Errs errs => (warn (); error (cat_lines errs))
   383      | Errs(errs) => (warn(); error(cat_lines(map (exn_type_msg sg) errs)))
   378     | Ambigs us =>
   384      | Ambigs(us) =>
   379         (warn (); error ("Error: More than one term is type correct:\n" ^
   385          (warn();
   380           (cat_lines (map (Pretty.string_of o prt) us)))))
   386           let val old_show_brackets = !show_brackets
   381   end;
   387               val dummy = show_brackets := true;
   382 
   388               val errs = cat_lines(map (string_of_term sg) us)
       
   389           in show_brackets := old_show_brackets;
       
   390              error("Error: More than one term is type correct:\n" ^ errs)
       
   391           end)
       
   392   end;
       
   393 
   383 
   394 
   384 
   395 (** extend signature **)    (*exception ERROR*)
   385 (** extend signature **)    (*exception ERROR*)
   396 
   386 
   397 (** signature extension functions **)  (*exception ERROR*)
   387 (** signature extension functions **)  (*exception ERROR*)
   459   (c, read_raw_typ syn tsig (K None) ty_src, mx)
   449   (c, read_raw_typ syn tsig (K None) ty_src, mx)
   460     handle ERROR => err_in_const (Syntax.const_name c mx);
   450     handle ERROR => err_in_const (Syntax.const_name c mx);
   461 
   451 
   462 fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   452 fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   463   let
   453   let
   464     fun prep_const (c, ty, mx) = 
   454     fun prep_const (c, ty, mx) =
   465      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   455      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   466        handle TYPE (msg, _, _)
   456        handle TYPE (msg, _, _)
   467          => (writeln msg; err_in_const (Syntax.const_name c mx));
   457          => (writeln msg; err_in_const (Syntax.const_name c mx));
   468 
   458 
   469     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   459     val consts = map (prep_const o rd_const syn tsig) raw_consts;