# HG changeset patch # User clasohm # Date 786887185 -3600 # Node ID b60e77395d1a6df826aedd3ce74ae878219c1877 # Parent d5a626aacdd32bcce338a795a259466b2b3b0262 changed Pure's grammar and the way types are converted to nonterminals diff -r d5a626aacdd3 -r b60e77395d1a src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Thu Dec 08 12:45:28 1994 +0100 +++ b/src/Pure/Syntax/mixfix.ML Thu Dec 08 12:46:25 1994 +0100 @@ -78,7 +78,7 @@ (* syn_ext_types *) -fun syn_ext_types all_roots type_decls = +fun syn_ext_types logtypes type_decls = let fun name_of (t, _, mx) = type_name t mx; @@ -95,13 +95,13 @@ val mfix = mapfilter mfix_of type_decls; val xconsts = map name_of type_decls; in - syn_ext all_roots [] mfix xconsts ([], [], [], []) ([], []) + syn_ext logtypes mfix xconsts ([], [], [], []) ([], []) end; (* syn_ext_consts *) -fun syn_ext_consts all_roots const_decls = +fun syn_ext_consts logtypes const_decls = let fun name_of (c, _, mx) = const_name c mx; @@ -130,7 +130,7 @@ val binder_trs = map mk_binder_tr binders; val binder_trs' = map (mk_binder_tr' o swap) binders; in - syn_ext all_roots [] mfix xconsts ([], binder_trs, binder_trs', []) ([], []) + syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) ([], []) end; @@ -140,7 +140,7 @@ val pure_types = map (fn t => (t, 0, NoSyn)) (terminals @ [logic, "type", "types", "sort", "classes", args, "idt", - "idts", "aprop", "asms", "any"]); + "idts", "aprop", "asms"]); val pure_syntax = [("_lambda", "[idts, 'a] => ('b => 'a)", Mixfix ("(3%_./ _)", [], 0)), @@ -163,7 +163,6 @@ ("_K", "'a", NoSyn), ("", "id => logic", Delimfix "_"), ("", "var => logic", Delimfix "_"), - ("_appl", "[logic, args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)), - ("_constrain", "[logic, type] => logic", Mixfix ("_::_", [4, 0], 3))] + ("_appl", "[logic, args] => logic", Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))] end; diff -r d5a626aacdd3 -r b60e77395d1a src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Dec 08 12:45:28 1994 +0100 +++ b/src/Pure/Syntax/parser.ML Thu Dec 08 12:46:25 1994 +0100 @@ -260,40 +260,15 @@ fun extend_gram (gram1 as Gram (prods1, _)) roots xprods2 = let - fun simplify preserve s = - if preserve then - (if s mem (roots \\ ["type", "prop", "any"]) then "logic" else s) - else (if s = "prop" then "@prop_H" else - (if s mem (roots \\ ["type", "prop", "any"]) then - "@logic_H" - else s)); - - fun not_delim (Delim _) = false - | not_delim _ = true - - fun symb_of _ (Delim s) = Some (Terminal (Token s)) - | symb_of preserve (Argument (s, p)) = + fun symb_of (Delim s) = Some (Terminal (Token s)) + | symb_of (Argument (s, p)) = (case predef_term s of - None => Some (Nonterminal (simplify preserve s, p)) + None => Some (Nonterminal (s, p)) | Some tk => Some (Terminal tk)) - | symb_of _ _ = None; + | symb_of _ = None; fun prod_of (XProd (lhs, xsymbs, const, pri)) = - let val copy_prod = (lhs = "prop" andalso forall not_delim xsymbs andalso - const <> ""); - - val preserve = copy_prod - orelse pri = chain_pri andalso lhs = "logic" - orelse lhs mem ["@prop_H", "@logic_H", "any"]; - - val lhs' = if copy_prod then "@prop_H" else - if lhs = "logic" andalso pri = chain_pri - then "@logic_H" - else if lhs mem ("logic1" :: (roots \\ ["type", "prop"])) - then "logic" - else lhs; - in (lhs', (mapfilter (symb_of preserve) xsymbs, const, pri)) - end; + (lhs, (mapfilter symb_of xsymbs, const, pri)); val prods2 = distinct (map prod_of xprods2); in @@ -583,10 +558,6 @@ fun earley grammar startsymbol indata = let - val startsymbol' = case startsymbol of - "logic" => "@logic_H" - | "prop" => "@prop_H" - | other => other; val rhss_ref = case assoc (grammar, startsymbol) of Some r => r | None => error ("parse: Unknown startsymbol " ^ diff -r d5a626aacdd3 -r b60e77395d1a src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Thu Dec 08 12:45:28 1994 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Thu Dec 08 12:46:25 1994 +0100 @@ -32,7 +32,7 @@ datatype mfix = Mfix of string * typ * string * int list * int datatype syn_ext = SynExt of { - roots: string list, + logtypes: string list, xprods: xprod list, consts: string list, parse_ast_translation: (string * (ast list -> ast)) list, @@ -41,17 +41,23 @@ print_translation: (string * (term list -> term)) list, print_rules: (ast * ast) list, print_ast_translation: (string * (ast list -> ast)) list} - val syn_ext: string list -> string list -> mfix list -> string list -> + val mk_syn_ext: bool -> string list -> mfix list -> + string list -> (string * (ast list -> ast)) list * + (string * (term list -> term)) list * + (string * (term list -> term)) list * (string * (ast list -> ast)) list + -> (ast * ast) list * (ast * ast) list -> syn_ext + val syn_ext: string list -> mfix list -> string list -> (string * (ast list -> ast)) list * (string * (term list -> term)) list * (string * (term list -> term)) list * (string * (ast list -> ast)) list -> (ast * ast) list * (ast * ast) list -> syn_ext - val syn_ext_roots: string list -> string 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) list * (ast * ast) list -> syn_ext val syn_ext_trfuns: string list -> (string * (ast list -> ast)) list * (string * (term list -> term)) list * (string * (term list -> term)) list * (string * (ast list -> ast)) list -> syn_ext + val pure_ext: syn_ext end end; @@ -70,19 +76,18 @@ val logicT = Type (logic, []); val logic1 = "logic1"; -val logic1T = Type (logic1, []); val args = "args"; val argsT = Type (args, []); val typeT = Type ("type", []); -val funT = Type ("fun", []); +val sprop = "#prop"; +val spropT = Type (sprop, []); -val any = "any" +val any = "any"; val anyT = Type (any, []); - (* constants *) val applC = "_appl"; @@ -145,19 +150,22 @@ (* typ_to_nonterm *) -fun typ_to_nonterm (Type (c, _)) = c +(*get nonterminal for rhs*) +fun typ_to_nonterm (Type (c, _)) = if c="fun" then logic else c | typ_to_nonterm _ = any; -fun typ_to_nonterm1 (Type (c, _)) = c - | typ_to_nonterm1 _ = logic1; +(*get nonterminal for lhs*) +fun typ_to_nonterm1 (ty as Type (c, _)) = typ_to_nonterm ty + | typ_to_nonterm1 _ = logic; (* mfix_to_xprod *) -fun mfix_to_xprod (Mfix (sy, typ, const, pris, pri)) = +fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) = let fun err msg = - (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const); + (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " + ^ quote const); error msg); fun check_pri p = @@ -218,21 +226,37 @@ fun rem_pri (Argument (s, _)) = Argument (s, chain_pri) | rem_pri sym = sym; + fun is_delim (Delim _) = true + | is_delim _ = false; + + (*replace logical types on rhs by "logic"*) + fun unify_logtypes copy_prod (a as (Argument (s, p))) = + if s mem logtypes then Argument (logic, p) + else a + | unify_logtypes _ a = a; val (raw_symbs, _) = repeat scan_symb (explode sy); val (symbs, lhs) = add_args raw_symbs typ pris; - val xprod = XProd (lhs, symbs, const, pri); + val copy_prod = lhs mem ["prop", "logic"] + andalso const <> "" + 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) + else lhs; + val symbs' = map (unify_logtypes copy_prod) symbs; + val xprod = XProd (lhs', symbs', const, pri); in seq check_pri pris; check_pri pri; - check_blocks symbs; + check_blocks symbs'; - if is_terminal lhs then err ("illegal lhs: " ^ lhs) + if is_terminal lhs' then err ("illegal lhs: " ^ lhs') else if const <> "" then xprod - else if length (filter is_arg symbs) <> 1 then + else if length (filter is_arg symbs') <> 1 then err "copy production must have exactly one argument" - else if exists is_term symbs then xprod - else XProd (lhs, map rem_pri symbs, "", chain_pri) + else if exists is_term symbs' then xprod + else XProd (lhs', map rem_pri symbs', "", chain_pri) end; @@ -240,7 +264,7 @@ datatype syn_ext = SynExt of { - roots: string list, + logtypes: string list, xprods: xprod list, consts: string list, parse_ast_translation: (string * (ast list -> ast)) list, @@ -253,31 +277,18 @@ (* syn_ext *) -fun syn_ext all_roots new_roots mfixes consts trfuns rules = +fun mk_syn_ext convert logtypes mfixes consts trfuns rules = let val (parse_ast_translation, parse_translation, print_translation, print_ast_translation) = trfuns; val (parse_rules, print_rules) = rules; + val logtypes' = logtypes \ "prop"; val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes); - val mfixes' = (if "prop" mem new_roots then - [Mfix ("'(_')", Type ("@prop_H", []) - --> Type ("@prop_H", []), "", [0], max_pri), - Mfix ("'(_')", Type ("@logic_H", []) - --> Type ("@logic_H", []), "", [0], max_pri), - Mfix ("'(_')", anyT --> anyT, "", [0], max_pri), - Mfix ("_", propT --> Type ("@prop_H", []), "", [0], 0), - Mfix ("_", propT --> anyT, "", [0], 0)] - else []) @ - (if all_roots = new_roots then - [Mfix ("_", logicT --> Type ("@logic_H", []), "", [0], 0), - Mfix ("_", logicT --> anyT, "", [0], 0)] - else []) - val xprods = map mfix_to_xprod mfixes - @ map mfix_to_xprod mfixes'; + val xprods = map (mfix_to_xprod convert logtypes') mfixes; in SynExt { - roots = new_roots, + logtypes = logtypes', xprods = xprods, consts = filter is_xid (consts union mfix_consts), parse_ast_translation = parse_ast_translation, @@ -288,18 +299,32 @@ print_ast_translation = print_ast_translation} end; +val syn_ext = mk_syn_ext true; -fun syn_ext_roots roots new_roots = - syn_ext roots new_roots [] [] ([], [], [], []) ([], []); +fun syn_ext_logtypes logtypes = + syn_ext logtypes [] [] ([], [], [], []) ([], []); + +fun syn_ext_const_names logtypes cs = + syn_ext logtypes [] cs ([], [], [], []) ([], []); -fun syn_ext_const_names roots cs = - syn_ext roots [] [] cs ([], [], [], []) ([], []); +fun syn_ext_rules logtypes rules = + syn_ext logtypes [] [] ([], [], [], []) rules; + +fun syn_ext_trfuns logtypes trfuns = + syn_ext logtypes [] [] trfuns ([], []); -fun syn_ext_rules roots rules = - syn_ext roots [] [] [] ([], [], [], []) rules; +(* pure_ext *) -fun syn_ext_trfuns roots trfuns = - syn_ext roots [] [] [] trfuns ([], []); - +val pure_ext = mk_syn_ext false [] + [Mfix ("_", spropT --> propT, "", [0], 0), + Mfix ("_", logicT --> anyT, "", [0], 0), + Mfix ("_", spropT --> anyT, "", [0], 0), + Mfix ("'(_')", logicT --> logicT, "", [0], max_pri), + Mfix ("'(_')", spropT --> spropT, "", [0], max_pri), + Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3), + Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)] + [] + ([], [], [], []) + ([], []); end; diff -r d5a626aacdd3 -r b60e77395d1a src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Dec 08 12:45:28 1994 +0100 +++ b/src/Pure/Syntax/syntax.ML Thu Dec 08 12:46:25 1994 +0100 @@ -47,6 +47,7 @@ (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax val merge_syntaxes: syntax -> syntax -> syntax val type_syn: syntax + val pure_syn: syntax val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit @@ -134,7 +135,7 @@ datatype syntax = Syntax of { lexicon: lexicon, - roots: string list, + logtypes: string list, gram: gram, consts: string list, parse_ast_trtab: ast trtab, @@ -151,7 +152,7 @@ val empty_syntax = Syntax { lexicon = empty_lexicon, - roots = [], + logtypes = [], gram = empty_gram, consts = [], parse_ast_trtab = empty_trtab, @@ -167,17 +168,17 @@ fun extend_syntax (Syntax tabs) syn_ext = let - val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab, + val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtab} = tabs; - val SynExt {roots = roots2, xprods, consts = consts2, parse_ast_translation, + val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; in Syntax { lexicon = extend_lexicon lexicon (delims_of xprods), - roots = extend_list roots1 roots2, - gram = extend_gram gram (roots1 @ roots2) xprods, + logtypes = extend_list logtypes1 logtypes2, + gram = extend_gram gram (logtypes1 @ logtypes2) xprods, consts = consts2 union consts1, parse_ast_trtab = extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation", @@ -195,13 +196,13 @@ fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) = let - val {lexicon = lexicon1, roots = roots1, gram = gram1, consts = consts1, + val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1, print_trtab = print_trtab1, print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1, prtab = prtab1} = tabs1; - val {lexicon = lexicon2, roots = roots2, gram = gram2, consts = consts2, + val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2, @@ -209,7 +210,7 @@ in Syntax { lexicon = merge_lexicons lexicon1 lexicon2, - roots = merge_lists roots1 roots2, + logtypes = merge_lists logtypes1 logtypes2, gram = merge_grams gram1 gram2, consts = merge_lists consts1 consts2, parse_ast_trtab = @@ -227,7 +228,7 @@ (* type_syn *) val type_syn = extend_syntax empty_syntax type_ext; - +val pure_syn = extend_syntax type_syn pure_ext; (** inspect syntax **) @@ -240,10 +241,10 @@ fun print_gram (Syntax tabs) = let - val {lexicon, roots, gram, ...} = tabs; + val {lexicon, logtypes, gram, ...} = tabs; in Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon)); - Pretty.writeln (Pretty.strs ("roots:" :: roots)); + Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes)); Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram)) end; @@ -304,9 +305,8 @@ fun read_asts (Syntax tabs) print_msg xids root str = let - val {lexicon, gram, parse_ast_trtab, roots, ...} = tabs; - val root' = if root mem (roots \\ ["type", "prop"]) then "@logic_H" - else if root = "prop" then "@prop_H" else root; + val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs; + val root' = if root mem logtypes then logic else root; val pts = parse gram root' (tokenize lexicon xids str); fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt)); @@ -436,12 +436,12 @@ (** extend syntax (external interfaces) **) -fun ext_syntax mk_syn_ext (syn as Syntax {roots, ...}) decls = - extend_syntax syn (mk_syn_ext roots decls); +fun ext_syntax mk_syn_ext (syn as Syntax {logtypes, ...}) decls = + extend_syntax syn (mk_syn_ext logtypes decls); -fun extend_log_types (syn as Syntax {roots, ...}) all_roots = - extend_syntax syn (syn_ext_roots all_roots (all_roots \\ roots)); +fun extend_log_types syn logtypes = + extend_syntax syn (syn_ext_logtypes logtypes); val extend_type_gram = ext_syntax syn_ext_types; diff -r d5a626aacdd3 -r b60e77395d1a src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Thu Dec 08 12:45:28 1994 +0100 +++ b/src/Pure/Syntax/type_ext.ML Thu Dec 08 12:46:25 1994 +0100 @@ -157,8 +157,7 @@ val classesT = Type ("classes", []); val typesT = Type ("types", []); -val type_ext = syn_ext - [logic, "type"] [logic, "type"] +val type_ext = mk_syn_ext false [] [Mfix ("_", tidT --> typeT, "", [], max_pri), Mfix ("_", tvarT --> typeT, "", [], max_pri), Mfix ("_", idT --> typeT, "", [], max_pri), @@ -185,4 +184,3 @@ end; -