src/Pure/sign.ML
changeset 19658 0cff73279f34
parent 19642 ea7162f84677
child 19673 853f5a3cc06e
equal deleted inserted replaced
19657:25eaa3660123 19658:0cff73279f34
    21   val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    21   val add_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    22   val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    22   val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    23   val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    23   val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
    24   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    24   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    25   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    25   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    26   val add_abbrevs: string * bool -> (bstring * string * mixfix) list -> theory -> theory
       
    27   val add_abbrevs_i: string * bool -> (bstring * term * mixfix) list -> theory -> theory
       
    28   val add_const_constraint: xstring * string option -> theory -> theory
    26   val add_const_constraint: xstring * string option -> theory -> theory
    29   val add_const_constraint_i: string * typ option -> theory -> theory
    27   val add_const_constraint_i: string * typ option -> theory -> theory
    30   val primitive_class: string * class list -> theory -> theory
    28   val primitive_class: string * class list -> theory -> theory
    31   val primitive_classrel: class * class -> theory -> theory
    29   val primitive_classrel: class * class -> theory -> theory
    32   val primitive_arity: arity -> theory -> theory
    30   val primitive_arity: arity -> theory -> theory
   191     theory * (indexname -> typ option) * (indexname -> sort option) ->
   189     theory * (indexname -> typ option) * (indexname -> sort option) ->
   192     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   190     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   193   val simple_read_term: theory -> typ -> string -> term
   191   val simple_read_term: theory -> typ -> string -> term
   194   val read_term: theory -> string -> term
   192   val read_term: theory -> string -> term
   195   val read_prop: theory -> string -> term
   193   val read_prop: theory -> string -> term
       
   194   val add_const_syntax: string * bool -> (string * mixfix) list -> theory -> theory
       
   195   val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
       
   196   val add_abbrevs: string * bool -> (bstring * term * mixfix) list -> theory -> theory
   196   include SIGN_THEORY
   197   include SIGN_THEORY
   197 end
   198 end
   198 
   199 
   199 structure Sign: SIGN =
   200 structure Sign: SIGN =
   200 struct
   201 struct
   708 val add_syntax = add_modesyntax Syntax.default_mode;
   709 val add_syntax = add_modesyntax Syntax.default_mode;
   709 val add_syntax_i = add_modesyntax_i Syntax.default_mode;
   710 val add_syntax_i = add_modesyntax_i Syntax.default_mode;
   710 val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
   711 val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
   711 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
   712 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
   712 
   713 
       
   714 fun add_const_syntax prmode args thy =
       
   715   thy |> add_modesyntax_i prmode (map (Consts.syntax (consts_of thy)) args);
       
   716 
   713 
   717 
   714 (* add constants *)
   718 (* add constants *)
   715 
   719 
   716 local
   720 local
   717 
   721 
   718 fun gen_add_consts prep_typ raw_args thy =
   722 fun gen_add_consts prep_typ early raw_args thy =
   719   let
   723   let
   720     val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
   724     val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
   721     fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
   725     fun prep (raw_c, raw_T, raw_mx) =
   722       handle ERROR msg =>
   726       let
   723         cat_error msg ("in declaration of constant " ^ quote (Syntax.const_name c mx));
   727         val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
       
   728         val (c', b) = if early then (c, true) else Syntax.mixfix_const (full_name thy c) mx;
       
   729         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
       
   730           cat_error msg ("in declaration of constant " ^ quote c);
       
   731       in (((c, T), b), (c', T, mx)) end;
   724     val args = map prep raw_args;
   732     val args = map prep raw_args;
   725     val decls = args |> map (fn (c, T, mx) => ((Syntax.const_name c mx, T), true));
       
   726   in
   733   in
   727     thy
   734     thy
   728     |> map_consts (fold (Consts.declare (naming_of thy)) decls)
   735     |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
   729     |> add_syntax_i args
   736     |> map_syn (Syntax.extend_consts (map (#1 o #1 o #1) args))
       
   737     |> add_syntax_i (map #2 args)
   730   end;
   738   end;
   731 
   739 
   732 in
   740 in
   733 
   741 
   734 val add_consts = gen_add_consts (read_typ o no_def_sort);
   742 val add_consts = gen_add_consts (read_typ o no_def_sort) true;
   735 val add_consts_i = gen_add_consts certify_typ;
   743 val add_consts_i = gen_add_consts certify_typ true;
       
   744 val add_consts_authentic = gen_add_consts certify_typ false;
   736 
   745 
   737 end;
   746 end;
   738 
   747 
   739 
   748 
   740 (* add abbreviations *)
   749 (* add abbreviations *)
   741 
   750 
   742 local
   751 fun add_abbrevs (mode, inout) = fold (fn (raw_c, raw_t, raw_mx) => fn thy =>
   743 
   752   let
   744 fun gen_abbrevs prep_term (mode, inout) = fold (fn (raw_c, raw_t, raw_mx) => fn thy =>
   753     val prep_tm = Compress.term thy o Logic.varify o no_vars (pp thy) o
   745   let
   754       Term.no_dummy_patterns o cert_term_abbrev thy;
   746     val prep_tm =
       
   747       Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy;
       
   748 
   755 
   749     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
   756     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
   750     val (c', b) = Syntax.mixfix_const (full_name thy c) mx;
   757     val (c', b) = Syntax.mixfix_const (full_name thy c) mx;
   751     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
   758     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
   752       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   759       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
   756     |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), b))
   763     |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) mode ((c, t), b))
   757     |> map_syn (Syntax.extend_consts [c])
   764     |> map_syn (Syntax.extend_consts [c])
   758     |> add_modesyntax_i (mode, inout) [(c', T, mx)]
   765     |> add_modesyntax_i (mode, inout) [(c', T, mx)]
   759   end);
   766   end);
   760 
   767 
   761 in
       
   762 
       
   763 val add_abbrevs = gen_abbrevs read_term;
       
   764 val add_abbrevs_i = gen_abbrevs cert_term_abbrev;
       
   765 
       
   766 end;
       
   767 
       
   768 
   768 
   769 (* add constraints *)
   769 (* add constraints *)
   770 
   770 
   771 fun gen_add_constraint int_const prep_typ (raw_c, opt_T) thy =
   771 fun gen_add_constraint int_const prep_typ (raw_c, opt_T) thy =
   772   let
   772   let