# HG changeset patch # User clasohm # Date 781272136 -3600 # Node ID 33b9b5da3e6faee6ca6969d17e79634d49e5b46a # Parent ca9f5dbab8804a3995b66d8a9b4d1eb37e6a23d5 made major changes to grammar; added call of Type.infer_types to automatically eliminate ambiguities diff -r ca9f5dbab880 -r 33b9b5da3e6f src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Oct 04 13:01:17 1994 +0100 +++ b/src/Pure/Syntax/mixfix.ML Tue Oct 04 13:02:16 1994 +0100 @@ -140,7 +140,7 @@ val pure_types = map (fn t => (t, 0, NoSyn)) (terminals @ [logic, "type", "types", "sort", "classes", args, "idt", - "idts", "aprop", "asms"]); + "idts", "aprop", "asms", "any"]); val pure_syntax = [("_lambda", "[idts, 'a] => ('b => 'a)", Mixfix ("(3%_./ _)", [], 0)), @@ -162,8 +162,10 @@ ("_ofclass", "[type, 'a] => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), ("_K", "'a", NoSyn), ("_explode", "'a", NoSyn), - ("_implode", "'a", NoSyn)]; - + ("_implode", "'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 ("_::_", [max_pri, 0], 999))] end; - diff -r ca9f5dbab880 -r 33b9b5da3e6f src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue Oct 04 13:01:17 1994 +0100 +++ b/src/Pure/Syntax/parser.ML Tue Oct 04 13:02:16 1994 +0100 @@ -12,7 +12,7 @@ local open Lexicon SynExt SynExt.Ast in type gram val empty_gram: gram - val extend_gram: gram -> xprod list -> gram + val extend_gram: gram -> string list -> xprod list -> gram val merge_grams: gram -> gram -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = @@ -257,17 +257,42 @@ val empty_gram = mk_gram []; -fun extend_gram (gram1 as Gram (prods1, _)) xprods2 = +fun extend_gram (gram1 as Gram (prods1, _)) roots xprods2 = let - fun symb_of (Delim s) = Some (Terminal (Token s)) - | symb_of (Argument (s, p)) = + 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)) = (case predef_term s of - None => Some (Nonterminal (s, p)) + None => Some (Nonterminal (simplify preserve s, p)) | Some tk => Some (Terminal tk)) - | symb_of _ = None; + | symb_of _ _ = None; fun prod_of (XProd (lhs, xsymbs, const, pri)) = - (lhs, (mapfilter symb_of 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; val prods2 = distinct (map prod_of xprods2); in @@ -553,10 +578,14 @@ 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 " ^ - quote startsymbol); + | None => error ("parse: Unknown startsymbol " ^ + quote startsymbol); val S0 = [(ref [], 0, [], [Nonterm (rhss_ref, 0), Term EndToken], "", 0)]; val s = length indata + 1; val Estate = Array.array (s, []); @@ -564,15 +593,17 @@ Array.update (Estate, 0, S0); let val l = produce Estate 0 indata EndToken(*dummy*); + val p_trees = get_trees l; in p_trees end end; fun parse (Gram (_, prod_tab)) start toks = +let val r = (case earley prod_tab start toks of [] => sys_error "parse: no parse trees" | pts => pts); +in r end end; - diff -r ca9f5dbab880 -r 33b9b5da3e6f src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Tue Oct 04 13:01:17 1994 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Tue Oct 04 13:02:16 1994 +0100 @@ -79,6 +79,9 @@ val funT = Type ("fun", []); +val any = "any" +val anyT = Type (any, []); + (* constants *) @@ -143,7 +146,7 @@ (* typ_to_nonterm *) fun typ_to_nonterm (Type (c, _)) = c - | typ_to_nonterm _ = logic; + | typ_to_nonterm _ = any; fun typ_to_nonterm1 (Type (c, _)) = c | typ_to_nonterm1 _ = logic1; @@ -256,78 +259,26 @@ print_ast_translation) = trfuns; val (parse_rules, print_rules) = rules; - val Troots = map (apr (Type, [])) new_roots; - val Troots' = Troots \\ [typeT, propT]; - - fun change_name T ext = - let val Type (name, ts) = T - in Type ("@" ^ name ^ ext, ts) end; - - (* Append "_H" to lhs if production is not a copy or chain production *) - fun hide_xprod roots (XProd (lhs, symbs, const, pri)) = - let fun is_delim (Delim _) = true - | is_delim _ = false - in if const <> "" andalso lhs mem roots andalso exists is_delim symbs then - XProd ("@" ^ lhs ^ "_H", symbs, const, pri) - else XProd (lhs, symbs, const, pri) - end; - - (* Make descend production and append "_H" to rhs nonterminal *) - fun descend_right (from, to) = - Mfix ("_", change_name to "_H" --> from, "", [0], 0); - - (* Make descend production and append "_H" to lhs *) - fun descend_left (from, to) = - Mfix ("_", to --> change_name from "_H", "", [0], 0); - - (* Make descend production and append "_A" to lhs *) - fun descend1 (from, to) = - Mfix ("_", to --> change_name from "_A", "", [0], 0); - - (* Make parentheses production for 'hidden' and 'automatic' nonterminal *) - fun parents T = - if T = typeT then - [Mfix ("'(_')", T --> T, "", [0], max_pri)] - else - [Mfix ("'(_')", change_name T "_H" --> change_name T "_H", "", [0], max_pri), - Mfix ("'(_')", change_name T "_A" --> change_name T "_A", "", [0], max_pri)]; - - fun mkappl T = - Mfix ("(1_/(1'(_')))", [funT, argsT] ---> change_name T "_A", applC, - [max_pri, 0], max_pri); - - fun mkid T = - Mfix ("_", idT --> change_name T "_A", "", [], max_pri); - - fun mkvar T = - Mfix ("_", varT --> change_name T "_A", "", [], max_pri); - - fun constrain T = - Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC, - [4, 0], 3) - - fun unhide T = - if T <> logicT then - [Mfix ("_", change_name T "_H" --> T, "", [0], 0), - Mfix ("_", change_name T "_A" --> T, "", [0], 0)] - else - [Mfix ("_", change_name T "_A" --> T, "", [0], 0)]; - - val mfixes' = flat (map parents Troots) @ map mkappl Troots' @ - map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @ - map (apl (logicT, descend_right)) (Troots \\ [logicT, typeT]) @ - map (apr (descend1, logic1T)) (Troots') @ - flat (map unhide (Troots \\ [typeT])); - val mfix_consts = - distinct (map (fn (Mfix (_, _, c, _, _)) => c) (mfixes @ mfixes')); - val xprods = map mfix_to_xprod mfixes; - val xprods' = map mfix_to_xprod mfixes'; + 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'; in SynExt { roots = new_roots, - xprods = (map (hide_xprod (all_roots \\ ["logic", "type"])) xprods) - @ xprods', (* hide only productions that weren't created - automatically *) + xprods = xprods, consts = filter is_xid (consts union mfix_consts), parse_ast_translation = parse_ast_translation, parse_rules = parse_rules, @@ -352,4 +303,3 @@ end; - diff -r ca9f5dbab880 -r 33b9b5da3e6f src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Oct 04 13:01:17 1994 +0100 +++ b/src/Pure/Syntax/syntax.ML Tue Oct 04 13:02:16 1994 +0100 @@ -43,14 +43,15 @@ (string * (term list -> term)) list * (string * (term list -> term)) list * (string * (ast list -> ast)) list -> syntax - val extend_trrules: syntax -> xrule list -> syntax + val extend_trrules: syntax -> + (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax val merge_syntaxes: syntax -> syntax -> syntax val type_syn: syntax val print_gram: syntax -> unit val print_trans: syntax -> unit val print_syntax: syntax -> unit val test_read: syntax -> string -> string -> unit - val read: syntax -> typ -> string -> term + val read: syntax -> typ -> string -> term list val read_typ: syntax -> (indexname -> sort) -> string -> typ val simple_read_typ: string -> typ val pretty_term: syntax -> term -> Pretty.T @@ -176,7 +177,7 @@ Syntax { lexicon = extend_lexicon lexicon (delims_of xprods), roots = extend_list roots1 roots2, - gram = extend_gram gram xprods, + gram = extend_gram gram (roots1 @ roots2) xprods, consts = consts2 union consts1, parse_ast_trtab = extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation", @@ -285,7 +286,7 @@ val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs; val toks = tokenize lexicon false str; - val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks)) + val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks)); fun show_pt pt = let @@ -301,20 +302,20 @@ (* read_ast *) -fun read_ast (Syntax tabs) xids root str = +fun read_asts (Syntax tabs) print_msg xids root str = let - val {lexicon, gram, parse_ast_trtab, ...} = tabs; - val pts = parse gram root (tokenize lexicon xids str); + 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 pts = parse gram root' (tokenize lexicon xids str); - fun show_pt pt = - writeln (str_of_ast (pt_to_ast (K None) pt)); + fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt)); in - (case pts of - [pt] => pt_to_ast (lookup_trtab parse_ast_trtab) pt - | _ => - (writeln ("Ambiguous input " ^ quote str); - writeln "produces the following parse trees:"; seq show_pt pts; - error "Please disambiguate the grammar or your input.")) + if print_msg andalso length pts > 1 then + (writeln ("Warning: Ambiguous input " ^ quote str); + writeln "produces the following parse trees:"; seq show_pt pts) + else (); + map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts end; @@ -323,10 +324,10 @@ fun read (syn as Syntax tabs) ty str = let val {parse_ruletab, parse_trtab, ...} = tabs; - val ast = read_ast syn false (typ_to_nonterm ty) str; + val asts = read_asts syn true false (typ_to_nonterm ty) str; in - ast_to_term (lookup_trtab parse_trtab) - (normalize_ast (lookup_ruletab parse_ruletab) ast) + map (ast_to_term (lookup_trtab parse_trtab)) + (map (normalize_ast (lookup_ruletab parse_ruletab)) asts) end; @@ -334,7 +335,11 @@ fun read_typ syn def_sort str = let - val t = read syn typeT str; + val ts = read syn typeT str; + val t = case ts of + [t'] => t' + | _ => error "This should not happen while parsing a type.\n\ + \Please check your type syntax for ambiguities!"; val sort_env = raw_term_sorts t; in typ_of_term sort_env def_sort t @@ -345,7 +350,9 @@ (* read rules *) -fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) = +fun read_rule (syn as Syntax tabs) print_msg + (check_types: bool -> term list * typ -> int * term * 'a) + (xrule as ((_, lhs_src), (_, rhs_src))) = let val Syntax {consts, ...} = syn; @@ -355,8 +362,20 @@ | constantify (Appl asts) = Appl (map constantify asts); fun read_pat (root, str) = - constantify (read_ast syn true root str) - handle ERROR => error ("The error above occurred in " ^ quote str); + let val {parse_ruletab, parse_trtab, ...} = tabs; + val asts = read_asts syn print_msg true root str; + val ts = map (ast_to_term (lookup_trtab parse_trtab)) + (map (normalize_ast (lookup_ruletab parse_ruletab)) asts); + + val idx = if length ts = 1 then 0 + else (if print_msg then + writeln ("This occured in syntax translation rule: " ^ + quote lhs_src ^ " -> " ^ quote rhs_src) + else (); + #1 (check_types print_msg (ts, Type (root, [])))) + in constantify (nth_elem (idx, asts)) + handle ERROR => error ("The error above occurred in " ^ quote str) + end; val rule as (lhs, rhs) = (pairself read_pat) xrule; in @@ -374,7 +393,7 @@ op <-| of (string * string) * (string * string) | op <-> of (string * string) * (string * string); -fun read_xrules syn xrules = +fun read_xrules syn check_types xrules = let fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2) | right_rule (xpat1 <-| xpat2) = None @@ -383,9 +402,12 @@ fun left_rule (xpat1 |-> xpat2) = None | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1) | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1); + + val rrules = mapfilter right_rule xrules; + val lrules = mapfilter left_rule xrules; in - (map (read_rule syn) (mapfilter right_rule xrules), - map (read_rule syn) (mapfilter left_rule xrules)) + (map (read_rule syn true check_types) rrules, + map (read_rule syn (rrules = []) check_types) lrules) end; @@ -429,9 +451,7 @@ val extend_trfuns = ext_syntax syn_ext_trfuns; -fun extend_trrules syn xrules = - ext_syntax syn_ext_rules syn (read_xrules syn xrules); - +fun extend_trrules syn check_types xrules = + ext_syntax syn_ext_rules syn (read_xrules syn check_types xrules); end; - diff -r ca9f5dbab880 -r 33b9b5da3e6f src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Tue Oct 04 13:01:17 1994 +0100 +++ b/src/Pure/Syntax/type_ext.ML Tue Oct 04 13:02:16 1994 +0100 @@ -177,7 +177,8 @@ Mfix ("_", typeT --> typesT, "", [], max_pri), Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri), Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0), - Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0)] + Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0), + Mfix ("'(_')", typeT --> typeT, "", [0], max_pri)] [] ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)], [],