removed separate logtypes field of syntax;
authorwenzelm
Wed Jun 09 18:54:26 2004 +0200 (2004-06-09)
changeset 14903d264b8ad3eec
parent 14902 bef0dc694c48
child 14904 7d8dc92fcb7f
removed separate logtypes field of syntax;
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Jun 09 18:54:07 2004 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Jun 09 18:54:26 2004 +0200
     1.3 @@ -42,10 +42,8 @@
     1.4  signature MIXFIX =
     1.5  sig
     1.6    include MIXFIX1
     1.7 -  val syn_ext_types: string list -> (string * int * mixfix) list
     1.8 -    -> SynExt.syn_ext
     1.9 -  val syn_ext_consts: string list -> (string * typ * mixfix) list
    1.10 -    -> SynExt.syn_ext
    1.11 +  val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
    1.12 +  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
    1.13  end;
    1.14  
    1.15  
    1.16 @@ -133,7 +131,7 @@
    1.17  
    1.18  (* syn_ext_types *)
    1.19  
    1.20 -fun syn_ext_types logtypes type_decls =
    1.21 +fun syn_ext_types type_decls =
    1.22    let
    1.23      fun name_of (t, _, mx) = type_name t mx;
    1.24  
    1.25 @@ -151,17 +149,17 @@
    1.26          | (sy, 2, Infix p) => Some (mk_infix sy t (p + 1) (p + 1) p)
    1.27          | (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p)
    1.28          | (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p)
    1.29 -        | _ => error ("Bad mixfix declaration for type " ^ quote t))
    1.30 +        | _ => error ("Bad mixfix declaration for type: " ^ quote t))
    1.31        end;
    1.32  
    1.33      val mfix = mapfilter mfix_of type_decls;
    1.34      val xconsts = map name_of type_decls;
    1.35 -  in SynExt.syn_ext logtypes mfix xconsts ([], [], [], []) [] ([], []) end;
    1.36 +  in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
    1.37  
    1.38  
    1.39  (* syn_ext_consts *)
    1.40  
    1.41 -fun syn_ext_consts logtypes const_decls =
    1.42 +fun syn_ext_consts is_logtype const_decls =
    1.43    let
    1.44      fun name_of (c, _, mx) = const_name c mx;
    1.45  
    1.46 @@ -171,7 +169,7 @@
    1.47  
    1.48      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    1.49            [Type ("idts", []), ty2] ---> ty3
    1.50 -      | binder_typ c _ = error ("Bad type of binder " ^ quote c);
    1.51 +      | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
    1.52  
    1.53      fun mfix_of decl =
    1.54        let val c = name_of decl in
    1.55 @@ -198,7 +196,10 @@
    1.56      val binder_trs = map SynTrans.mk_binder_tr binders;
    1.57      val binder_trs' =
    1.58        map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;
    1.59 -  in SynExt.syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) end;
    1.60 +  in
    1.61 +    SynExt.syn_ext' true is_logtype
    1.62 +      mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
    1.63 +  end;
    1.64  
    1.65  
    1.66  
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Jun 09 18:54:07 2004 +0200
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 09 18:54:26 2004 +0200
     2.3 @@ -34,7 +34,6 @@
     2.4    datatype mfix = Mfix of string * typ * string * int list * int
     2.5    datatype syn_ext =
     2.6      SynExt of {
     2.7 -      logtypes: string list,
     2.8        xprods: xprod list,
     2.9        consts: string list,
    2.10        prmodes: string list,
    2.11 @@ -47,27 +46,25 @@
    2.12        token_translation: (string * string * (string -> string * real)) list}
    2.13    val mfix_args: string -> int
    2.14    val escape_mfix: string -> string
    2.15 -  val mk_syn_ext: bool -> string list -> mfix list ->
    2.16 +  val syn_ext': bool -> (string -> bool) -> mfix list ->
    2.17      string list -> (string * (Ast.ast list -> Ast.ast)) list *
    2.18      (string * (term list -> term)) list *
    2.19      (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    2.20      -> (string * string * (string -> string * real)) list
    2.21      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.22 -  val syn_ext: string list -> mfix list -> string list ->
    2.23 +  val syn_ext: mfix list -> string list ->
    2.24      (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    2.25      (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    2.26      -> (string * string * (string -> string * real)) list
    2.27      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.28 -  val syn_ext_logtypes: string list -> syn_ext
    2.29 -  val syn_ext_const_names: string list -> string list -> syn_ext
    2.30 -  val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.31 -  val syn_ext_trfuns: string list ->
    2.32 +  val syn_ext_const_names: string list -> syn_ext
    2.33 +  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    2.34 +  val syn_ext_trfuns:
    2.35      (string * (Ast.ast list -> Ast.ast)) list *
    2.36      (string * (term list -> term)) list *
    2.37      (string * (bool -> typ -> term list -> term)) list *
    2.38      (string * (Ast.ast list -> Ast.ast)) list -> syn_ext
    2.39 -  val syn_ext_tokentrfuns: string list
    2.40 -    -> (string * string * (string -> string * real)) list -> syn_ext
    2.41 +  val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    2.42    val pure_ext: syn_ext
    2.43  end;
    2.44  
    2.45 @@ -224,7 +221,7 @@
    2.46  
    2.47  (* mfix_to_xprod *)
    2.48  
    2.49 -fun mfix_to_xprod convert logtypes (mfix as Mfix (sy, typ, const, pris, pri)) =
    2.50 +fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
    2.51    let
    2.52      fun check_pri p =
    2.53        if p >= 0 andalso p <= max_pri then ()
    2.54 @@ -260,7 +257,7 @@
    2.55        | rem_pri sym = sym;
    2.56  
    2.57      fun logify_types copy_prod (a as (Argument (s, p))) =
    2.58 -          if s mem logtypes then Argument (logic, p) else a
    2.59 +          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
    2.60        | logify_types _ a = a;
    2.61  
    2.62  
    2.63 @@ -292,8 +289,7 @@
    2.64          andalso not (exists is_delim symbs);
    2.65      val lhs' =
    2.66        if convert andalso not copy_prod then
    2.67 -       (if lhs mem logtypes then logic
    2.68 -        else if lhs = "prop" then sprop else lhs)
    2.69 +       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
    2.70        else lhs;
    2.71      val symbs' = map (logify_types copy_prod) symbs;
    2.72      val xprod = XProd (lhs', symbs', const', pri);
    2.73 @@ -315,7 +311,6 @@
    2.74  
    2.75  datatype syn_ext =
    2.76    SynExt of {
    2.77 -    logtypes: string list,
    2.78      xprods: xprod list,
    2.79      consts: string list,
    2.80      prmodes: string list,
    2.81 @@ -330,18 +325,16 @@
    2.82  
    2.83  (* syn_ext *)
    2.84  
    2.85 -fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
    2.86 +fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
    2.87    let
    2.88      val (parse_ast_translation, parse_translation, print_translation,
    2.89        print_ast_translation) = trfuns;
    2.90 -    val logtypes' = logtypes \ "prop";
    2.91  
    2.92 -    val (xprods, parse_rules') = map (mfix_to_xprod convert logtypes') mfixes
    2.93 +    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
    2.94        |> split_list |> apsnd (rev o flat);
    2.95      val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    2.96    in
    2.97      SynExt {
    2.98 -      logtypes = logtypes',
    2.99        xprods = xprods,
   2.100        consts = consts union_string mfix_consts,
   2.101        prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
   2.102 @@ -355,27 +348,17 @@
   2.103    end;
   2.104  
   2.105  
   2.106 -val syn_ext = mk_syn_ext true;
   2.107 -
   2.108 -fun syn_ext_logtypes logtypes =
   2.109 -  syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
   2.110 -
   2.111 -fun syn_ext_const_names logtypes cs =
   2.112 -  syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
   2.113 +val syn_ext = syn_ext' true (K false);
   2.114  
   2.115 -fun syn_ext_rules logtypes rules =
   2.116 -  syn_ext logtypes [] [] ([], [], [], []) [] rules;
   2.117 -
   2.118 -fun syn_ext_trfuns logtypes trfuns =
   2.119 -  syn_ext logtypes [] [] trfuns [] ([], []);
   2.120 -
   2.121 -fun syn_ext_tokentrfuns logtypes tokentrfuns =
   2.122 -  syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
   2.123 +fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
   2.124 +fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
   2.125 +fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
   2.126 +fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
   2.127  
   2.128  
   2.129  (* pure_ext *)
   2.130  
   2.131 -val pure_ext = mk_syn_ext false []
   2.132 +val pure_ext = syn_ext' false (K false)
   2.133    [Mfix ("_", spropT --> propT, "", [0], 0),
   2.134     Mfix ("_", logicT --> anyT, "", [0], 0),
   2.135     Mfix ("_", spropT --> anyT, "", [0], 0),
     3.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Jun 09 18:54:07 2004 +0200
     3.2 +++ b/src/Pure/Syntax/type_ext.ML	Wed Jun 09 18:54:26 2004 +0200
     3.3 @@ -189,7 +189,7 @@
     3.4  
     3.5  local open Lexicon SynExt in
     3.6  
     3.7 -val type_ext = mk_syn_ext false ["dummy"]
     3.8 +val type_ext = syn_ext' false (K false)
     3.9    [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    3.10     Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    3.11     Mfix ("_",           idT --> typeT,                 "", [], max_pri),