src/Pure/sign.ML
changeset 16941 0bda949449ee
parent 16894 40f80823b451
child 16988 02cd0c8b96d9
equal deleted inserted replaced
16940:d14ec6f2d29b 16941:0bda949449ee
    23   val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    23   val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    24   val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    24   val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    25   val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    25   val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    26   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    26   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    27   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    27   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
       
    28   val add_const_constraint: xstring * string -> theory -> theory
       
    29   val add_const_constraint_i: string * typ -> theory -> theory
    28   val add_classes: (bstring * xstring list) list -> theory -> theory
    30   val add_classes: (bstring * xstring list) list -> theory -> theory
    29   val add_classes_i: (bstring * class list) list -> theory -> theory
    31   val add_classes_i: (bstring * class list) list -> theory -> theory
    30   val add_classrel: (xstring * xstring) list -> theory -> theory
    32   val add_classrel: (xstring * xstring) list -> theory -> theory
    31   val add_classrel_i: (class * class) list -> theory -> theory
    33   val add_classrel_i: (class * class) list -> theory -> theory
    32   val add_trfuns:
    34   val add_trfuns:
    74   val init_data: theory -> theory
    76   val init_data: theory -> theory
    75   val rep_sg: theory ->
    77   val rep_sg: theory ->
    76    {naming: NameSpace.naming,
    78    {naming: NameSpace.naming,
    77     syn: Syntax.syntax,
    79     syn: Syntax.syntax,
    78     tsig: Type.tsig,
    80     tsig: Type.tsig,
    79     consts: (typ * stamp) NameSpace.table}
    81     consts: (typ * stamp) NameSpace.table * typ Symtab.table}
    80   val naming_of: theory -> NameSpace.naming
    82   val naming_of: theory -> NameSpace.naming
    81   val base_name: string -> bstring
    83   val base_name: string -> bstring
    82   val full_name: theory -> bstring -> string
    84   val full_name: theory -> bstring -> string
    83   val full_name_path: theory -> string -> bstring -> string
    85   val full_name_path: theory -> string -> bstring -> string
    84   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    86   val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
    90   val of_sort: theory -> typ * sort -> bool
    92   val of_sort: theory -> typ * sort -> bool
    91   val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
    93   val witness_sorts: theory -> sort list -> sort list -> (typ * sort) list
    92   val universal_witness: theory -> (typ * sort) option
    94   val universal_witness: theory -> (typ * sort) option
    93   val all_sorts_nonempty: theory -> bool
    95   val all_sorts_nonempty: theory -> bool
    94   val typ_instance: theory -> typ * typ -> bool
    96   val typ_instance: theory -> typ * typ -> bool
       
    97   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
       
    98   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
    95   val is_logtype: theory -> string -> bool
    99   val is_logtype: theory -> string -> bool
       
   100   val const_constraint: theory -> string -> typ option
    96   val const_type: theory -> string -> typ option
   101   val const_type: theory -> string -> typ option
    97   val the_const_type: theory -> string -> typ
   102   val the_const_type: theory -> string -> typ
    98   val declared_tyname: theory -> string -> bool
   103   val declared_tyname: theory -> string -> bool
    99   val declared_const: theory -> string -> bool
   104   val declared_const: theory -> string -> bool
   100   val class_space: theory -> NameSpace.T
   105   val class_space: theory -> NameSpace.T
   176 
   181 
   177 datatype sign = Sign of
   182 datatype sign = Sign of
   178  {naming: NameSpace.naming,                 (*common naming conventions*)
   183  {naming: NameSpace.naming,                 (*common naming conventions*)
   179   syn: Syntax.syntax,                       (*concrete syntax for terms, types, sorts*)
   184   syn: Syntax.syntax,                       (*concrete syntax for terms, types, sorts*)
   180   tsig: Type.tsig,                          (*order-sorted signature of types*)
   185   tsig: Type.tsig,                          (*order-sorted signature of types*)
   181   consts: (typ * stamp) NameSpace.table};   (*type schemes of term constants*)
   186   consts:
       
   187     (typ * stamp) NameSpace.table *         (*type schemes of declared term constants*)
       
   188     typ Symtab.table};                      (*type constraints for constants*)
       
   189 
   182 
   190 
   183 fun make_sign (naming, syn, tsig, consts) =
   191 fun make_sign (naming, syn, tsig, consts) =
   184   Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
   192   Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
   185 
   193 
   186 fun err_dup_consts cs =
   194 fun err_dup_consts cs =
   187   error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   195   error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
       
   196 
       
   197 fun err_inconsistent_constraints cs =
       
   198   error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
   188 
   199 
   189 structure SignData = TheoryDataFun
   200 structure SignData = TheoryDataFun
   190 (struct
   201 (struct
   191   val name = "Pure/sign";
   202   val name = "Pure/sign";
   192   type T = sign;
   203   type T = sign;
   193   val copy = I;
   204   val copy = I;
   194   val extend = I;
   205   val extend = I;
   195 
   206 
   196   val empty =
   207   val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
   197     make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, NameSpace.empty_table);
   208     (NameSpace.empty_table, Symtab.empty));
   198 
   209 
   199   fun merge pp (sign1, sign2) =
   210   fun merge pp (sign1, sign2) =
   200     let
   211     let
   201       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   212       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = (consts1, constraints1)} = sign1;
   202       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   213       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = (consts2, constraints2)} = sign2;
   203 
   214 
   204       val naming = NameSpace.default_naming;
   215       val naming = NameSpace.default_naming;
   205       val syn = Syntax.merge_syntaxes syn1 syn2;
   216       val syn = Syntax.merge_syntaxes syn1 syn2;
   206       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
   217       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
   207       val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
   218       val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
   208         handle Symtab.DUPS cs => err_dup_consts cs;
   219         handle Symtab.DUPS cs => err_dup_consts cs;
   209     in make_sign (naming, syn, tsig, consts) end;
   220       val constraints = Symtab.merge (op =) (constraints1, constraints2)
       
   221         handle Symtab.DUPS cs => err_inconsistent_constraints cs;
       
   222     in make_sign (naming, syn, tsig, (consts, constraints)) end;
   210 
   223 
   211   fun print _ _ = ();
   224   fun print _ _ = ();
   212 end);
   225 end);
   213 
   226 
   214 val init_data = SignData.init;
   227 val init_data = SignData.init;
   247 val of_sort = Type.of_sort o tsig_of;
   260 val of_sort = Type.of_sort o tsig_of;
   248 val witness_sorts = Type.witness_sorts o tsig_of;
   261 val witness_sorts = Type.witness_sorts o tsig_of;
   249 val universal_witness = Type.universal_witness o tsig_of;
   262 val universal_witness = Type.universal_witness o tsig_of;
   250 val all_sorts_nonempty = is_some o universal_witness;
   263 val all_sorts_nonempty = is_some o universal_witness;
   251 val typ_instance = Type.typ_instance o tsig_of;
   264 val typ_instance = Type.typ_instance o tsig_of;
       
   265 val typ_match = Type.typ_match o tsig_of;
       
   266 val typ_unify = Type.unify o tsig_of;
   252 fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
   267 fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
   253 
   268 
   254 
   269 
   255 (* consts signature *)
   270 (* consts signature *)
   256 
   271 
   257 fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#consts (rep_sg thy)), c));
   272 fun const_constraint thy c =
       
   273   let val ((_, consts), constraints) = #consts (rep_sg thy) in
       
   274     (case Symtab.lookup (constraints, c) of
       
   275       NONE => Option.map #1 (Symtab.lookup (consts, c))
       
   276     | some => some)
       
   277   end;
       
   278 
       
   279 fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
   258 
   280 
   259 fun the_const_type thy c =
   281 fun the_const_type thy c =
   260   (case const_type thy c of SOME T => T
   282   (case const_type thy c of SOME T => T
   261   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   283   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   262 
   284 
   267 
   289 
   268 (** intern / extern names **)
   290 (** intern / extern names **)
   269 
   291 
   270 val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
   292 val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
   271 val type_space = #1 o #types o Type.rep_tsig o tsig_of;
   293 val type_space = #1 o #types o Type.rep_tsig o tsig_of;
   272 val const_space = #1 o #consts o rep_sg
   294 val const_space = #1 o #1 o #consts o rep_sg
   273 
   295 
   274 val intern_class = NameSpace.intern o class_space;
   296 val intern_class = NameSpace.intern o class_space;
   275 val extern_class = NameSpace.extern o class_space;
   297 val extern_class = NameSpace.extern o class_space;
   276 val intern_type = NameSpace.intern o type_space;
   298 val intern_type = NameSpace.intern o type_space;
   277 val extern_type = NameSpace.extern o type_space;
   299 val extern_type = NameSpace.extern o type_space;
   507     val termss = foldr multiply [[]] (map fst args);
   529     val termss = foldr multiply [[]] (map fst args);
   508     val typs =
   530     val typs =
   509       map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   531       map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
   510 
   532 
   511     fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   533     fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
   512         (const_type thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   534         (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
   513         (intern_sort thy) used freeze typs ts)
   535         (intern_sort thy) used freeze typs ts)
   514       handle TYPE (msg, _, _) => Error msg;
   536       handle TYPE (msg, _, _) => Error msg;
   515 
   537 
   516     val err_results = map infer termss;
   538     val err_results = map infer termss;
   517     val errs = List.mapPartial get_error err_results;
   539     val errs = List.mapPartial get_error err_results;
   658 
   680 
   659     fun extend_consts consts = NameSpace.extend_table (naming_of thy) (consts, decls)
   681     fun extend_consts consts = NameSpace.extend_table (naming_of thy) (consts, decls)
   660       handle Symtab.DUPS cs => err_dup_consts cs;
   682       handle Symtab.DUPS cs => err_dup_consts cs;
   661   in
   683   in
   662     thy
   684     thy
   663     |> map_consts extend_consts
   685     |> map_consts (apfst extend_consts)
   664     |> add_syntax_i args
   686     |> add_syntax_i args
   665   end;
   687   end;
   666 
   688 
   667 val add_consts = gen_add_consts (read_typ o no_def_sort);
   689 val add_consts = gen_add_consts (read_typ o no_def_sort);
   668 val add_consts_i = gen_add_consts certify_typ;
   690 val add_consts_i = gen_add_consts certify_typ;
       
   691 
       
   692 
       
   693 (* add constraints *)
       
   694 
       
   695 fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy =
       
   696   let
       
   697     val c = int_const thy raw_c;
       
   698     val T = Term.zero_var_indexesT (Term.no_dummyT (prep_typ thy raw_T))
       
   699       handle TYPE (msg, _, _) => error msg;
       
   700     val _ = cert_term thy (Const (c, T))
       
   701       handle TYPE (msg, _, _) => error msg;
       
   702   in thy |> map_consts (apsnd (curry Symtab.update (c, T))) end;
       
   703 
       
   704 val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
       
   705 val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
   669 
   706 
   670 
   707 
   671 (* add type classes *)
   708 (* add type classes *)
   672 
   709 
   673 val classN = "_class";
   710 val classN = "_class";
   755 fun hide_classes b xs thy = thy |> map_tsig (Type.hide_classes b (map (intern_class thy) xs));
   792 fun hide_classes b xs thy = thy |> map_tsig (Type.hide_classes b (map (intern_class thy) xs));
   756 val hide_classes_i = map_tsig oo Type.hide_classes;
   793 val hide_classes_i = map_tsig oo Type.hide_classes;
   757 fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs));
   794 fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs));
   758 val hide_types_i = map_tsig oo Type.hide_types;
   795 val hide_types_i = map_tsig oo Type.hide_types;
   759 fun hide_consts b xs thy =
   796 fun hide_consts b xs thy =
   760   thy |> map_consts (apfst (fold (NameSpace.hide b o intern_const thy) xs));
   797   thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs)));
   761 val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide);
   798 val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide);
   762 
   799 
   763 end;
   800 end;