src/Pure/sign.ML
changeset 19513 77ff7cd602d7
parent 19482 9f11af8f7ef9
child 19642 ea7162f84677
equal deleted inserted replaced
19512:94cd541dc8fa 19513:77ff7cd602d7
    13   val add_types: (bstring * int * mixfix) list -> theory -> theory
    13   val add_types: (bstring * int * mixfix) list -> theory -> theory
    14   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    14   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    15   val add_nonterminals: bstring list -> theory -> theory
    15   val add_nonterminals: bstring list -> theory -> theory
    16   val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
    16   val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
    17   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
    17   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
    18   val add_arities: (xstring * string list * string) list -> theory -> theory
       
    19   val add_arities_i: (string * sort list * sort) list -> theory -> theory
       
    20   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    18   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    21   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    19   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    22   val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    20   val add_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    23   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
    24   val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    22   val del_modesyntax: (string * bool) -> (bstring * string * mixfix) list -> theory -> theory
    27   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    25   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    28   val add_abbrevs: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    26   val add_abbrevs: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    29   val add_abbrevs_i: string * bool -> (bstring * term * mixfix) list -> theory -> theory
    27   val add_abbrevs_i: string * bool -> (bstring * term * mixfix) list -> theory -> theory
    30   val add_const_constraint: xstring * string option -> theory -> theory
    28   val add_const_constraint: xstring * string option -> theory -> theory
    31   val add_const_constraint_i: string * typ option -> theory -> theory
    29   val add_const_constraint_i: string * typ option -> theory -> theory
    32   val add_classes: (bstring * xstring list) list -> theory -> theory
    30   val primitive_class: string * class list -> theory -> theory
    33   val add_classes_i: (bstring * class list) list -> theory -> theory
    31   val primitive_classrel: class * class -> theory -> theory
    34   val add_classrel: (xstring * xstring) list -> theory -> theory
    32   val primitive_arity: arity -> theory -> theory
    35   val add_classrel_i: (class * class) list -> theory -> theory
       
    36   val add_trfuns:
    33   val add_trfuns:
    37     (string * (ast list -> ast)) list *
    34     (string * (ast list -> ast)) list *
    38     (string * (term list -> term)) list *
    35     (string * (term list -> term)) list *
    39     (string * (term list -> term)) list *
    36     (string * (term list -> term)) list *
    40     (string * (ast list -> ast)) list -> theory -> theory
    37     (string * (ast list -> ast)) list -> theory -> theory
   525 
   522 
   526 (* type arities *)
   523 (* type arities *)
   527 
   524 
   528 fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
   525 fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
   529   let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
   526   let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
   530   in Type.add_arities (pp thy) [arity] (tsig_of thy); arity end;
   527   in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
   531 
   528 
   532 val read_arity = prep_arity intern_type read_sort;
   529 val read_arity = prep_arity intern_type read_sort;
   533 val cert_arity = prep_arity (K I) certify_sort;
   530 val cert_arity = prep_arity (K I) certify_sort;
   534 
   531 
   535 
   532 
   696 
   693 
   697 val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
   694 val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
   698 val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
   695 val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
   699 
   696 
   700 
   697 
   701 (* add type arities *)
       
   702 
       
   703 fun gen_add_arities int_type prep_sort arities thy = thy |> map_tsig (fn tsig =>
       
   704   let
       
   705     fun prep_arity (a, Ss, S) = (int_type thy a, map (prep_sort thy) Ss, prep_sort thy S)
       
   706       handle ERROR msg => cat_error msg ("in arity for type " ^ quote a);
       
   707     val tsig' = Type.add_arities (pp thy) (map prep_arity arities) tsig;
       
   708   in tsig' end);
       
   709 
       
   710 val add_arities = gen_add_arities intern_type read_sort;
       
   711 val add_arities_i = gen_add_arities (K I) certify_sort;
       
   712 
       
   713 
       
   714 (* modify syntax *)
   698 (* modify syntax *)
   715 
   699 
   716 fun gen_syntax change_gram prep_typ prmode args thy =
   700 fun gen_syntax change_gram prep_typ prmode args thy =
   717   let
   701   let
   718     fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
   702     fun prep (c, T, mx) = (c, prep_typ thy T, mx) handle ERROR msg =>
   797 
   781 
   798 val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
   782 val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
   799 val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
   783 val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
   800 
   784 
   801 
   785 
   802 (* add type classes *)
   786 (* primitive classes and arities *)
   803 
   787 
   804 fun gen_add_class int_class (bclass, raw_classes) thy =
   788 fun primitive_class (bclass, classes) thy =
   805   thy |> map_sign (fn (naming, syn, tsig, consts) =>
   789   thy |> map_sign (fn (naming, syn, tsig, consts) =>
   806     let
   790     let
   807       val classes = map (int_class thy) raw_classes;
       
   808       val syn' = Syntax.extend_consts [bclass] syn;
   791       val syn' = Syntax.extend_consts [bclass] syn;
   809       val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig;
   792       val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
   810     in (naming, syn', tsig', consts) end)
   793     in (naming, syn', tsig', consts) end)
   811   |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   794   |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   812 
   795 
   813 val add_classes = fold (gen_add_class intern_class);
   796 fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (pp thy) arg);
   814 val add_classes_i = fold (gen_add_class (K I));
   797 fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (pp thy) arg);
   815 
       
   816 
       
   817 (* add to classrel *)
       
   818 
       
   819 fun gen_add_classrel int_class raw_pairs thy = thy |> map_tsig (fn tsig =>
       
   820   let
       
   821     val pairs = map (pairself (int_class thy)) raw_pairs;
       
   822     val tsig' = Type.add_classrel (pp thy) pairs tsig;
       
   823   in tsig' end);
       
   824 
       
   825 val add_classrel = gen_add_classrel intern_class;
       
   826 val add_classrel_i = gen_add_classrel (K I);
       
   827 
   798 
   828 
   799 
   829 (* add translation functions *)
   800 (* add translation functions *)
   830 
   801 
   831 local
   802 local