# HG changeset patch # User wenzelm # Date 1086800066 -7200 # Node ID d264b8ad3eecaf6ec1edfb714f1fca5e8ba28605 # Parent bef0dc694c480413bc14ceb85be8188e56767106 removed separate logtypes field of syntax; diff -r bef0dc694c48 -r d264b8ad3eec src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Wed Jun 09 18:54:07 2004 +0200 +++ b/src/Pure/Syntax/mixfix.ML Wed Jun 09 18:54:26 2004 +0200 @@ -42,10 +42,8 @@ signature MIXFIX = sig include MIXFIX1 - val syn_ext_types: string list -> (string * int * mixfix) list - -> SynExt.syn_ext - val syn_ext_consts: string list -> (string * typ * mixfix) list - -> SynExt.syn_ext + val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext + val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext end; @@ -133,7 +131,7 @@ (* syn_ext_types *) -fun syn_ext_types logtypes type_decls = +fun syn_ext_types type_decls = let fun name_of (t, _, mx) = type_name t mx; @@ -151,17 +149,17 @@ | (sy, 2, Infix p) => Some (mk_infix sy t (p + 1) (p + 1) p) | (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p) | (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p) - | _ => error ("Bad mixfix declaration for type " ^ quote t)) + | _ => error ("Bad mixfix declaration for type: " ^ quote t)) end; val mfix = mapfilter mfix_of type_decls; val xconsts = map name_of type_decls; - in SynExt.syn_ext logtypes mfix xconsts ([], [], [], []) [] ([], []) end; + in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end; (* syn_ext_consts *) -fun syn_ext_consts logtypes const_decls = +fun syn_ext_consts is_logtype const_decls = let fun name_of (c, _, mx) = const_name c mx; @@ -171,7 +169,7 @@ fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = [Type ("idts", []), ty2] ---> ty3 - | binder_typ c _ = error ("Bad type of binder " ^ quote c); + | binder_typ c _ = error ("Bad type of binder: " ^ quote c); fun mfix_of decl = let val c = name_of decl in @@ -198,7 +196,10 @@ val binder_trs = map SynTrans.mk_binder_tr binders; val binder_trs' = map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders; - in SynExt.syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) end; + in + SynExt.syn_ext' true is_logtype + mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) + end; diff -r bef0dc694c48 -r d264b8ad3eec src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Wed Jun 09 18:54:07 2004 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Wed Jun 09 18:54:26 2004 +0200 @@ -34,7 +34,6 @@ datatype mfix = Mfix of string * typ * string * int list * int datatype syn_ext = SynExt of { - logtypes: string list, xprods: xprod list, consts: string list, prmodes: string list, @@ -47,27 +46,25 @@ token_translation: (string * string * (string -> string * real)) list} val mfix_args: string -> int val escape_mfix: string -> string - val mk_syn_ext: bool -> string list -> mfix list -> + val syn_ext': bool -> (string -> bool) -> mfix list -> string list -> (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list * (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list -> (string * string * (string -> string * real)) list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext: string list -> mfix list -> string list -> + val syn_ext: mfix list -> string list -> (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list * (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list -> (string * string * (string -> string * real)) list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext_logtypes: string list -> syn_ext - val syn_ext_const_names: string list -> string list -> syn_ext - val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext_trfuns: string list -> + val syn_ext_const_names: string list -> syn_ext + val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + val syn_ext_trfuns: (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list * (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list -> syn_ext - val syn_ext_tokentrfuns: string list - -> (string * string * (string -> string * real)) list -> syn_ext + val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext val pure_ext: syn_ext end; @@ -224,7 +221,7 @@ (* mfix_to_xprod *) -fun mfix_to_xprod convert logtypes (mfix as Mfix (sy, typ, const, pris, pri)) = +fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) = let fun check_pri p = if p >= 0 andalso p <= max_pri then () @@ -260,7 +257,7 @@ | rem_pri sym = sym; fun logify_types copy_prod (a as (Argument (s, p))) = - if s mem logtypes then Argument (logic, p) else a + if s <> "prop" andalso is_logtype s then Argument (logic, p) else a | logify_types _ a = a; @@ -292,8 +289,7 @@ andalso not (exists is_delim symbs); val lhs' = if convert andalso not copy_prod then - (if lhs mem logtypes then logic - else if lhs = "prop" then sprop else lhs) + (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs) else lhs; val symbs' = map (logify_types copy_prod) symbs; val xprod = XProd (lhs', symbs', const', pri); @@ -315,7 +311,6 @@ datatype syn_ext = SynExt of { - logtypes: string list, xprods: xprod list, consts: string list, prmodes: string list, @@ -330,18 +325,16 @@ (* syn_ext *) -fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns (parse_rules, print_rules) = +fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) = let val (parse_ast_translation, parse_translation, print_translation, print_ast_translation) = trfuns; - val logtypes' = logtypes \ "prop"; - val (xprods, parse_rules') = map (mfix_to_xprod convert logtypes') mfixes + val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes |> split_list |> apsnd (rev o flat); val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods); in SynExt { - logtypes = logtypes', xprods = xprods, consts = consts union_string mfix_consts, prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns), @@ -355,27 +348,17 @@ end; -val syn_ext = mk_syn_ext true; - -fun syn_ext_logtypes logtypes = - syn_ext logtypes [] [] ([], [], [], []) [] ([], []); - -fun syn_ext_const_names logtypes cs = - syn_ext logtypes [] cs ([], [], [], []) [] ([], []); +val syn_ext = syn_ext' true (K false); -fun syn_ext_rules logtypes rules = - syn_ext logtypes [] [] ([], [], [], []) [] rules; - -fun syn_ext_trfuns logtypes trfuns = - syn_ext logtypes [] [] trfuns [] ([], []); - -fun syn_ext_tokentrfuns logtypes tokentrfuns = - syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []); +fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []); +fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules; +fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []); +fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []); (* pure_ext *) -val pure_ext = mk_syn_ext false [] +val pure_ext = syn_ext' false (K false) [Mfix ("_", spropT --> propT, "", [0], 0), Mfix ("_", logicT --> anyT, "", [0], 0), Mfix ("_", spropT --> anyT, "", [0], 0), diff -r bef0dc694c48 -r d264b8ad3eec src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Wed Jun 09 18:54:07 2004 +0200 +++ b/src/Pure/Syntax/type_ext.ML Wed Jun 09 18:54:26 2004 +0200 @@ -189,7 +189,7 @@ local open Lexicon SynExt in -val type_ext = mk_syn_ext false ["dummy"] +val type_ext = syn_ext' false (K false) [Mfix ("_", tidT --> typeT, "", [], max_pri), Mfix ("_", tvarT --> typeT, "", [], max_pri), Mfix ("_", idT --> typeT, "", [], max_pri),