src/Pure/Syntax/syn_ext.ML
changeset 14903 d264b8ad3eec
parent 14819 4dae1cb304a4
child 14981 e73f8140af78
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jun 09 18:54:07 2004 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 09 18:54:26 2004 +0200
     1.3 @@ -34,7 +34,6 @@
     1.4    datatype mfix = Mfix of string * typ * string * int list * int
     1.5    datatype syn_ext =
     1.6      SynExt of {
     1.7 -      logtypes: string list,
     1.8        xprods: xprod list,
     1.9        consts: string list,
    1.10        prmodes: string list,
    1.11 @@ -47,27 +46,25 @@
    1.12        token_translation: (string * string * (string -> string * real)) list}
    1.13    val mfix_args: string -> int
    1.14    val escape_mfix: string -> string
    1.15 -  val mk_syn_ext: bool -> string list -> mfix list ->
    1.16 +  val syn_ext': bool -> (string -> bool) -> mfix list ->
    1.17      string list -> (string * (Ast.ast list -> Ast.ast)) list *
    1.18      (string * (term list -> term)) list *
    1.19      (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.20      -> (string * string * (string -> string * real)) list
    1.21      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.22 -  val syn_ext: string list -> mfix list -> string list ->
    1.23 +  val syn_ext: mfix list -> string list ->
    1.24      (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    1.25      (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.26      -> (string * string * (string -> string * real)) list
    1.27      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.28 -  val syn_ext_logtypes: string list -> syn_ext
    1.29 -  val syn_ext_const_names: string list -> string list -> syn_ext
    1.30 -  val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.31 -  val syn_ext_trfuns: string list ->
    1.32 +  val syn_ext_const_names: string list -> syn_ext
    1.33 +  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.34 +  val syn_ext_trfuns:
    1.35      (string * (Ast.ast list -> Ast.ast)) list *
    1.36      (string * (term list -> term)) list *
    1.37      (string * (bool -> typ -> term list -> term)) list *
    1.38      (string * (Ast.ast list -> Ast.ast)) list -> syn_ext
    1.39 -  val syn_ext_tokentrfuns: string list
    1.40 -    -> (string * string * (string -> string * real)) list -> syn_ext
    1.41 +  val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    1.42    val pure_ext: syn_ext
    1.43  end;
    1.44  
    1.45 @@ -224,7 +221,7 @@
    1.46  
    1.47  (* mfix_to_xprod *)
    1.48  
    1.49 -fun mfix_to_xprod convert logtypes (mfix as Mfix (sy, typ, const, pris, pri)) =
    1.50 +fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
    1.51    let
    1.52      fun check_pri p =
    1.53        if p >= 0 andalso p <= max_pri then ()
    1.54 @@ -260,7 +257,7 @@
    1.55        | rem_pri sym = sym;
    1.56  
    1.57      fun logify_types copy_prod (a as (Argument (s, p))) =
    1.58 -          if s mem logtypes then Argument (logic, p) else a
    1.59 +          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
    1.60        | logify_types _ a = a;
    1.61  
    1.62  
    1.63 @@ -292,8 +289,7 @@
    1.64          andalso not (exists is_delim symbs);
    1.65      val lhs' =
    1.66        if convert andalso not copy_prod then
    1.67 -       (if lhs mem logtypes then logic
    1.68 -        else if lhs = "prop" then sprop else lhs)
    1.69 +       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
    1.70        else lhs;
    1.71      val symbs' = map (logify_types copy_prod) symbs;
    1.72      val xprod = XProd (lhs', symbs', const', pri);
    1.73 @@ -315,7 +311,6 @@
    1.74  
    1.75  datatype syn_ext =
    1.76    SynExt of {
    1.77 -    logtypes: string list,
    1.78      xprods: xprod list,
    1.79      consts: string list,
    1.80      prmodes: string list,
    1.81 @@ -330,18 +325,16 @@
    1.82  
    1.83  (* syn_ext *)
    1.84  
    1.85 -fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
    1.86 +fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
    1.87    let
    1.88      val (parse_ast_translation, parse_translation, print_translation,
    1.89        print_ast_translation) = trfuns;
    1.90 -    val logtypes' = logtypes \ "prop";
    1.91  
    1.92 -    val (xprods, parse_rules') = map (mfix_to_xprod convert logtypes') mfixes
    1.93 +    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
    1.94        |> split_list |> apsnd (rev o flat);
    1.95      val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    1.96    in
    1.97      SynExt {
    1.98 -      logtypes = logtypes',
    1.99        xprods = xprods,
   1.100        consts = consts union_string mfix_consts,
   1.101        prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
   1.102 @@ -355,27 +348,17 @@
   1.103    end;
   1.104  
   1.105  
   1.106 -val syn_ext = mk_syn_ext true;
   1.107 -
   1.108 -fun syn_ext_logtypes logtypes =
   1.109 -  syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
   1.110 -
   1.111 -fun syn_ext_const_names logtypes cs =
   1.112 -  syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
   1.113 +val syn_ext = syn_ext' true (K false);
   1.114  
   1.115 -fun syn_ext_rules logtypes rules =
   1.116 -  syn_ext logtypes [] [] ([], [], [], []) [] rules;
   1.117 -
   1.118 -fun syn_ext_trfuns logtypes trfuns =
   1.119 -  syn_ext logtypes [] [] trfuns [] ([], []);
   1.120 -
   1.121 -fun syn_ext_tokentrfuns logtypes tokentrfuns =
   1.122 -  syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
   1.123 +fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
   1.124 +fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
   1.125 +fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
   1.126 +fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
   1.127  
   1.128  
   1.129  (* pure_ext *)
   1.130  
   1.131 -val pure_ext = mk_syn_ext false []
   1.132 +val pure_ext = syn_ext' false (K false)
   1.133    [Mfix ("_", spropT --> propT, "", [0], 0),
   1.134     Mfix ("_", logicT --> anyT, "", [0], 0),
   1.135     Mfix ("_", spropT --> anyT, "", [0], 0),