src/Pure/sign.ML
changeset 2197 e895937fcd56
parent 2187 07c471510cf1
child 2211 0487add593b5
     1.1 --- a/src/Pure/sign.ML	Mon Nov 18 17:28:19 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Nov 18 17:28:40 1996 +0100
     1.3 @@ -8,10 +8,11 @@
     1.4  signature SIGN =
     1.5    sig
     1.6    type sg
     1.7 -  val rep_sg: sg -> {tsig: Type.type_sig,
     1.8 -		     const_tab: typ Symtab.table,
     1.9 -		     syn: Syntax.syntax,
    1.10 -		     stamps: string ref list}
    1.11 +  val rep_sg: sg ->
    1.12 +   {tsig: Type.type_sig,
    1.13 +    const_tab: typ Symtab.table,
    1.14 +    syn: Syntax.syntax,
    1.15 +    stamps: string ref list}
    1.16    val subsig: sg * sg -> bool
    1.17    val eq_sg: sg * sg -> bool
    1.18    val same_sg: sg * sg -> bool
    1.19 @@ -50,6 +51,8 @@
    1.20    val add_consts_i: (string * typ * mixfix) list -> sg -> sg
    1.21    val add_syntax: (string * string * mixfix) list -> sg -> sg
    1.22    val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
    1.23 +  val add_modesyntax: string * (string * string * mixfix) list -> sg -> sg
    1.24 +  val add_modesyntax_i: string * (string * typ * mixfix) list -> sg -> sg
    1.25    val add_trfuns:
    1.26      (string * (ast list -> ast)) list *
    1.27      (string * (term list -> term)) list *
    1.28 @@ -449,7 +452,7 @@
    1.29    (c, read_raw_typ syn tsig (K None) ty_src, mx)
    1.30      handle ERROR => err_in_const (Syntax.const_name c mx);
    1.31  
    1.32 -fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
    1.33 +fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
    1.34    let
    1.35      fun prep_const (c, ty, mx) = 
    1.36       (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
    1.37 @@ -461,15 +464,17 @@
    1.38        if syn_only then []
    1.39        else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
    1.40    in
    1.41 -    (Syntax.extend_const_gram syn consts, tsig,
    1.42 +    (Syntax.extend_const_gram syn prmode consts, tsig,
    1.43        Symtab.extend_new (ctab, decls)
    1.44          handle Symtab.DUPS cs => err_dup_consts cs)
    1.45    end;
    1.46  
    1.47 -val ext_consts_i = ext_cnsts (K (K I)) false;
    1.48 -val ext_consts = ext_cnsts read_const false;
    1.49 -val ext_syntax_i = ext_cnsts (K (K I)) true;
    1.50 -val ext_syntax = ext_cnsts read_const true;
    1.51 +val ext_consts_i = ext_cnsts (K (K I)) false "";
    1.52 +val ext_consts = ext_cnsts read_const false "";
    1.53 +val ext_syntax_i = ext_cnsts (K (K I)) true "";
    1.54 +val ext_syntax = ext_cnsts read_const true "";
    1.55 +fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts (K (K I)) true prmode sg consts;
    1.56 +fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts;
    1.57  
    1.58  
    1.59  (* add type classes *)
    1.60 @@ -530,20 +535,22 @@
    1.61  
    1.62  (* the external interfaces *)
    1.63  
    1.64 -val add_classes   = extend_sign ext_classes "#";
    1.65 -val add_classrel  = extend_sign ext_classrel "#";
    1.66 -val add_defsort   = extend_sign ext_defsort "#";
    1.67 -val add_types     = extend_sign ext_types "#";
    1.68 -val add_tyabbrs   = extend_sign ext_tyabbrs "#";
    1.69 -val add_tyabbrs_i = extend_sign ext_tyabbrs_i "#";
    1.70 -val add_arities   = extend_sign ext_arities "#";
    1.71 -val add_consts    = extend_sign ext_consts "#";
    1.72 -val add_consts_i  = extend_sign ext_consts_i "#";
    1.73 -val add_syntax    = extend_sign ext_syntax "#";
    1.74 -val add_syntax_i  = extend_sign ext_syntax_i "#";
    1.75 -val add_trfuns    = extend_sign (ext_syn Syntax.extend_trfuns) "#";
    1.76 -val add_trrules   = extend_sign (ext_syn Syntax.extend_trrules) "#";
    1.77 -val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
    1.78 +val add_classes      = extend_sign ext_classes "#";
    1.79 +val add_classrel     = extend_sign ext_classrel "#";
    1.80 +val add_defsort      = extend_sign ext_defsort "#";
    1.81 +val add_types        = extend_sign ext_types "#";
    1.82 +val add_tyabbrs      = extend_sign ext_tyabbrs "#";
    1.83 +val add_tyabbrs_i    = extend_sign ext_tyabbrs_i "#";
    1.84 +val add_arities      = extend_sign ext_arities "#";
    1.85 +val add_consts       = extend_sign ext_consts "#";
    1.86 +val add_consts_i     = extend_sign ext_consts_i "#";
    1.87 +val add_syntax       = extend_sign ext_syntax "#";
    1.88 +val add_syntax_i     = extend_sign ext_syntax_i "#";
    1.89 +val add_modesyntax   = extend_sign ext_modesyntax "#";
    1.90 +val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
    1.91 +val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
    1.92 +val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
    1.93 +val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
    1.94  
    1.95  fun add_name name sg = extend_sign K name () sg;
    1.96  val make_draft = add_name "#";
    1.97 @@ -604,11 +611,12 @@
    1.98      ("prop", [], logicS),
    1.99      ("itself", [logicS], logicS)]
   1.100    |> add_syntax Syntax.pure_syntax
   1.101 +  |> add_modesyntax ("symbolfont", Syntax.pure_symfont_syntax)
   1.102    |> add_trfuns Syntax.pure_trfuns
   1.103    |> add_consts
   1.104 -   [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
   1.105 -    ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
   1.106 -    ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   1.107 +   [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   1.108 +    ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   1.109 +    ("==>", "[prop, prop] => prop", InfixrName ("==>", 1)),
   1.110      ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   1.111      ("TYPE", "'a itself", NoSyn)]
   1.112    |> add_name "ProtoPure";