src/Pure/sign.ML
changeset 2185 f9686e7e6d4d
parent 2184 99805d7652a9
child 2187 07c471510cf1
equal deleted inserted replaced
2184:99805d7652a9 2185:f9686e7e6d4d
    68   end;
    68   end;
    69 
    69 
    70 structure Sign : SIGN =
    70 structure Sign : SIGN =
    71 struct
    71 struct
    72 
    72 
    73 local open Type Syntax in
    73 (*local open Type Syntax in*)
    74 
    74 
    75 (** datatype sg **)
    75 (** datatype sg **)
    76 
    76 
    77 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    77 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    78   impossible to forge a signature*)
    78   impossible to forge a signature*)
    79 
    79 
    80 datatype sg =
    80 datatype sg =
    81   Sg of {
    81   Sg of {
    82     tsig: Type.type_sig,                 (*order-sorted signature of types*)
    82     tsig: Type.type_sig,            (*order-sorted signature of types*)
    83     const_tab: typ Symtab.table,    (*types of constants*)
    83     const_tab: typ Symtab.table,    (*types of constants*)
    84     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    84     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    85     stamps: string ref list};       (*unique theory indentifier*)
    85     stamps: string ref list};       (*unique theory indentifier*)
    86 
    86 
    87 fun rep_sg (Sg args) = args;
    87 fun rep_sg (Sg args) = args;
    88 val tsig_of = #tsig o rep_sg;
    88 val tsig_of = #tsig o rep_sg;
    89 
    89 
    90 
    90 
    91 (*** Stamps ***)
    91 (* stamps *)
    92 
    92 
    93 (*Avoiding polymorphic equality: 10* speedup*)
    93 (*inclusion, equality*)
    94 fun mem_stamp (_:string ref, []) = false
    94 local
    95   | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
    95   (*avoiding polymorphic equality: factor 10 speedup*)
    96 
    96   fun mem_stamp (_:string ref, []) = false
    97 fun subset_stamp ([], ys) = true
    97     | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
    98   | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
    98 
    99 
    99   fun subset_stamp ([], ys) = true
   100 fun eq_set_stamp (xs, ys) =
   100     | subset_stamp (x :: xs, ys) =
   101     xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
   101         mem_stamp (x, ys) andalso subset_stamp (xs, ys);
   102 
   102 
       
   103   (*fast partial test*)
       
   104   fun fast_sub ([]: string ref list, _) = true
       
   105     | fast_sub (_, []) = false
       
   106     | fast_sub (x :: xs, y :: ys) =
       
   107         if x = y then fast_sub (xs, ys)
       
   108         else fast_sub (x :: xs, ys);
       
   109 in
       
   110   fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
       
   111     s1 = s2 orelse subset_stamp (s1, s2);
       
   112 
       
   113   fun fast_subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
       
   114     s1 = s2 orelse fast_sub (s1, s2);
       
   115 
       
   116   fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
       
   117     s1 = s2 orelse (subset_stamp (s1, s2) andalso subset_stamp (s2, s1));
       
   118 end;
       
   119 
       
   120 
       
   121 (*test if same theory names are contained in signatures' stamps,
       
   122   i.e. if signatures belong to same theory but not necessarily to the
       
   123   same version of it*)
       
   124 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
       
   125   eq_set_string (pairself (map (op !)) (s1, s2));
       
   126 
       
   127 (*test for drafts*)
   103 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   128 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   104   | is_draft _ = false;
   129   | is_draft _ = false;
   105 
       
   106 fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) =
       
   107   s1 = s2 orelse subset_stamp (s1, s2);
       
   108 
       
   109 fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
       
   110 
       
   111 (* test if same theory names are contained in signatures' stamps,
       
   112    i.e. if signatures belong to same theory but not necessarily to the same
       
   113    version of it*)
       
   114 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
       
   115   eq_set_string (pairself (map (op !)) (s1, s2));
       
   116 
   130 
   117 
   131 
   118 (* consts *)
   132 (* consts *)
   119 
   133 
   120 fun const_type (Sg {const_tab, ...}) c =
   134 fun const_type (Sg {const_tab, ...}) c =
   167     fun pretty_const syn (c, ty) = Pretty.block
   181     fun pretty_const syn (c, ty) = Pretty.block
   168       [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
   182       [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
   169 
   183 
   170 
   184 
   171     val Sg {tsig, const_tab, syn, stamps} = sg;
   185     val Sg {tsig, const_tab, syn, stamps} = sg;
   172     val {classes, subclass, default, tycons, abbrs, arities} = rep_tsig tsig;
   186     val {classes, subclass, default, tycons, abbrs, arities} =
       
   187       Type.rep_tsig tsig;
   173   in
   188   in
   174     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   189     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   175     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   190     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   176     Pretty.writeln (Pretty.big_list "subclass:"
   191     Pretty.writeln (Pretty.big_list "subclass:"
   177                       (map pretty_subclass subclass));
   192                       (map pretty_subclass subclass));
   215 
   230 
   216 fun err_in_type s =
   231 fun err_in_type s =
   217   error ("The error(s) above occurred in type " ^ quote s);
   232   error ("The error(s) above occurred in type " ^ quote s);
   218 
   233 
   219 fun read_raw_typ syn tsig sort_of str =
   234 fun read_raw_typ syn tsig sort_of str =
   220   Syntax.read_typ syn (fn x => if_none (sort_of x) (defaultS tsig)) str
   235   Syntax.read_typ syn (fn x => if_none (sort_of x) (Type.defaultS tsig)) str
   221     handle ERROR => err_in_type str;
   236     handle ERROR => err_in_type str;
   222 
   237 
   223 (*read and certify typ wrt a signature*)
   238 (*read and certify typ wrt a signature*)
   224 fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   239 fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   225   cert_typ tsig (read_raw_typ syn tsig sort_of str)
   240   Type.cert_typ tsig (read_raw_typ syn tsig sort_of str)
   226     handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   241     handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   227 
   242 
   228 
   243 
   229 
   244 
   230 (** certify types and terms **)   (*exception TYPE*)
   245 (** certify types and terms **)   (*exception TYPE*)
   231 
   246 
   232 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   247 fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
   233 
   248 
   234 (* check for duplicate TVars with distinct sorts *)
   249 (* check for duplicate TVars with distinct sorts *)
   235 fun nodup_TVars(tvars,T) = (case T of
   250 fun nodup_TVars(tvars,T) = (case T of
   236       Type(_,Ts) => nodup_TVars_list (tvars,Ts)
   251       Type(_,Ts) => nodup_TVars_list (tvars,Ts)
   237     | TFree _ => tvars
   252     | TFree _ => tvars
   271 
   286 
   272 fun certify_term (sg as Sg {tsig, ...}) tm =
   287 fun certify_term (sg as Sg {tsig, ...}) tm =
   273   let
   288   let
   274     fun valid_const a T =
   289     fun valid_const a T =
   275       (case const_type sg a of
   290       (case const_type sg a of
   276         Some U => typ_instance (tsig, T, U)
   291         Some U => Type.typ_instance (tsig, T, U)
   277       | _ => false);
   292       | _ => false);
   278 
   293 
   279     fun atom_err (Const (a, T)) =
   294     fun atom_err (Const (a, T)) =
   280           if valid_const a T then None
   295           if valid_const a T then None
   281           else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   296           else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   283       | atom_err (Var ((x, i), _)) =
   298       | atom_err (Var ((x, i), _)) =
   284           if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   299           if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   285       | atom_err _ = None;
   300       | atom_err _ = None;
   286 
   301 
   287     val norm_tm =
   302     val norm_tm =
   288       (case it_term_types (typ_errors tsig) (tm, []) of
   303       (case it_term_types (Type.typ_errors tsig) (tm, []) of
   289         [] => map_term_types (norm_typ tsig) tm
   304         [] => map_term_types (Type.norm_typ tsig) tm
   290       | errs => raise_type (cat_lines errs) [] [tm]);
   305       | errs => raise_type (cat_lines errs) [] [tm]);
   291     val _ = nodup_Vars norm_tm;
   306     val _ = nodup_Vars norm_tm;
   292   in
   307   in
   293     (case mapfilt_atoms atom_err norm_tm of
   308     (case mapfilt_atoms atom_err norm_tm of
   294       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   309       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   378 
   393 
   379 
   394 
   380 (* add default sort *)
   395 (* add default sort *)
   381 
   396 
   382 fun ext_defsort (syn, tsig, ctab) defsort =
   397 fun ext_defsort (syn, tsig, ctab) defsort =
   383   (syn, ext_tsig_defsort tsig defsort, ctab);
   398   (syn, Type.ext_tsig_defsort tsig defsort, ctab);
   384 
   399 
   385 
   400 
   386 (* add type constructors *)
   401 (* add type constructors *)
   387 
   402 
   388 fun ext_types (syn, tsig, ctab) types =
   403 fun ext_types (syn, tsig, ctab) types =
   389   (Syntax.extend_type_gram syn types,
   404   (Syntax.extend_type_gram syn types,
   390     ext_tsig_types tsig (decls_of Syntax.type_name types),
   405     Type.ext_tsig_types tsig (decls_of Syntax.type_name types),
   391     ctab);
   406     ctab);
   392 
   407 
   393 
   408 
   394 (* add type abbreviations *)
   409 (* add type abbreviations *)
   395 
   410 
   403     val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs);
   418     val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs);
   404 
   419 
   405     fun decl_of (t, vs, rhs, mx) =
   420     fun decl_of (t, vs, rhs, mx) =
   406       rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs);
   421       rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs);
   407   in
   422   in
   408     (syn1, ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   423     (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   409   end;
   424   end;
   410 
   425 
   411 val ext_tyabbrs_i = ext_abbrs (K (K I));
   426 val ext_tyabbrs_i = ext_abbrs (K (K I));
   412 val ext_tyabbrs = ext_abbrs read_abbr;
   427 val ext_tyabbrs = ext_abbrs read_abbr;
   413 
   428 
   414 
   429 
   415 (* add type arities *)
   430 (* add type arities *)
   416 
   431 
   417 fun ext_arities (syn, tsig, ctab) arities =
   432 fun ext_arities (syn, tsig, ctab) arities =
   418   let
   433   let
   419     val tsig1 = ext_tsig_arities tsig arities;
   434     val tsig1 = Type.ext_tsig_arities tsig arities;
   420     val log_types = logical_types tsig1;
   435     val log_types = Type.logical_types tsig1;
   421   in
   436   in
   422     (Syntax.extend_log_types syn log_types, tsig1, ctab)
   437     (Syntax.extend_log_types syn log_types, tsig1, ctab)
   423   end;
   438   end;
   424 
   439 
   425 
   440 
   437     handle ERROR => err_in_const (Syntax.const_name c mx);
   452     handle ERROR => err_in_const (Syntax.const_name c mx);
   438 
   453 
   439 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   454 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   440   let
   455   let
   441     fun prep_const (c, ty, mx) = 
   456     fun prep_const (c, ty, mx) = 
   442 	  (c, 
   457      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   443 	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
   458        handle TYPE (msg, _, _)
   444 	   mx)
   459          => (writeln msg; err_in_const (Syntax.const_name c mx));
   445       handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
       
   446 
   460 
   447     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   461     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   448     val decls =
   462     val decls =
   449       if syn_only then []
   463       if syn_only then []
   450       else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
   464       else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
   478     val names = map fst classes;
   492     val names = map fst classes;
   479     val consts =
   493     val consts =
   480       map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   494       map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   481   in
   495   in
   482     ext_consts_i
   496     ext_consts_i
   483       (Syntax.extend_consts syn names, ext_tsig_classes tsig classes, ctab)
   497       (Syntax.extend_consts syn names, Type.ext_tsig_classes tsig classes, ctab)
   484       consts
   498       consts
   485   end;
   499   end;
   486 
   500 
   487 
   501 
   488 (* add to subclass relation *)
   502 (* add to subclass relation *)
   489 
   503 
   490 fun ext_classrel (syn, tsig, ctab) pairs =
   504 fun ext_classrel (syn, tsig, ctab) pairs =
   491   (syn, ext_tsig_subclass tsig pairs, ctab);
   505   (syn, Type.ext_tsig_subclass tsig pairs, ctab);
   492 
   506 
   493 
   507 
   494 (* add to syntax *)
   508 (* add to syntax *)
   495 
   509 
   496 fun ext_syn extfun (syn, tsig, ctab) args =
   510 fun ext_syn extfun (syn, tsig, ctab) args =
   539 
   553 
   540 
   554 
   541 (** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
   555 (** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
   542 
   556 
   543 fun merge (sg1, sg2) =
   557 fun merge (sg1, sg2) =
   544   if subsig (sg2, sg1) then sg1
   558   if fast_subsig (sg2, sg1) then sg1
       
   559   else if fast_subsig (sg1, sg2) then sg2
       
   560   else if subsig (sg2, sg1) then sg1
   545   else if subsig (sg1, sg2) then sg2
   561   else if subsig (sg1, sg2) then sg2
   546   else if is_draft sg1 orelse is_draft sg2 then
   562   else if is_draft sg1 orelse is_draft sg2 then
   547     raise_term "Illegal merge of draft signatures" []
   563     raise_term "Illegal merge of draft signatures" []
   548   else
   564   else
   549     (*neither is union already; must form union*)
   565     (*neither is union already; must form union*)
   559         (case duplicates (stamp_names stamps) of
   575         (case duplicates (stamp_names stamps) of
   560           [] => ()
   576           [] => ()
   561         | dups => raise_term ("Attempt to merge different versions of theories "
   577         | dups => raise_term ("Attempt to merge different versions of theories "
   562             ^ commas_quote dups) []);
   578             ^ commas_quote dups) []);
   563 
   579 
   564       val tsig = merge_tsigs (tsig1, tsig2);
   580       val tsig = Type.merge_tsigs (tsig1, tsig2);
   565 
   581 
   566       val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   582       val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   567         handle Symtab.DUPS cs =>
   583         handle Symtab.DUPS cs =>
   568           raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) [];
   584           raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) [];
   569 
   585 
   575 
   591 
   576 
   592 
   577 (** the Pure signature **)
   593 (** the Pure signature **)
   578 
   594 
   579 val proto_pure =
   595 val proto_pure =
   580   make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#"
   596   make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null) [] "#"
   581   |> add_types
   597   |> add_types
   582    (("fun", 2, NoSyn) ::
   598    (("fun", 2, NoSyn) ::
   583     ("prop", 0, NoSyn) ::
   599     ("prop", 0, NoSyn) ::
   584     ("itself", 1, NoSyn) ::
   600     ("itself", 1, NoSyn) ::
   585     Syntax.pure_types)
   601     Syntax.pure_types)
   605 
   621 
   606 val cpure = proto_pure
   622 val cpure = proto_pure
   607   |> add_syntax Syntax.pure_applC_syntax
   623   |> add_syntax Syntax.pure_applC_syntax
   608   |> add_name "CPure";
   624   |> add_name "CPure";
   609 
   625 
   610 end
   626 (*end*)
   611 end;
   627 end;