made major changes to grammar; Isabelle94-1
authorclasohm
Tue Oct 04 13:02:16 1994 +0100 (1994-10-04)
changeset 62433b9b5da3e6f
parent 623 ca9f5dbab880
child 625 119391dd1d59
made major changes to grammar;
added call of Type.infer_types to automatically eliminate ambiguities
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Oct 04 13:01:17 1994 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 04 13:02:16 1994 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4  val pure_types =
     1.5    map (fn t => (t, 0, NoSyn))
     1.6      (terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
     1.7 -      "idts", "aprop", "asms"]);
     1.8 +      "idts", "aprop", "asms", "any"]);
     1.9  
    1.10  val pure_syntax =
    1.11   [("_lambda",   "[idts, 'a] => ('b => 'a)",       Mixfix ("(3%_./ _)", [], 0)),
    1.12 @@ -162,8 +162,10 @@
    1.13    ("_ofclass",  "[type, 'a] => prop",             Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    1.14    ("_K",        "'a",                             NoSyn),
    1.15    ("_explode",  "'a",                             NoSyn),
    1.16 -  ("_implode",  "'a",                             NoSyn)];
    1.17 -
    1.18 +  ("_implode",  "'a",                             NoSyn),
    1.19 +  ("",          "id => logic",                    Delimfix "_"),
    1.20 +  ("",          "var => logic",                   Delimfix "_"),
    1.21 +  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
    1.22 +  ("_constrain", "[logic, type] => logic",        Mixfix ("_::_", [max_pri, 0], 999))]
    1.23  
    1.24  end;
    1.25 -
     2.1 --- a/src/Pure/Syntax/parser.ML	Tue Oct 04 13:01:17 1994 +0100
     2.2 +++ b/src/Pure/Syntax/parser.ML	Tue Oct 04 13:02:16 1994 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4    local open Lexicon SynExt SynExt.Ast in
     2.5      type gram
     2.6      val empty_gram: gram
     2.7 -    val extend_gram: gram -> xprod list -> gram
     2.8 +    val extend_gram: gram -> string list -> xprod list -> gram
     2.9      val merge_grams: gram -> gram -> gram
    2.10      val pretty_gram: gram -> Pretty.T list
    2.11      datatype parsetree =
    2.12 @@ -257,17 +257,42 @@
    2.13  
    2.14  val empty_gram = mk_gram [];
    2.15  
    2.16 -fun extend_gram (gram1 as Gram (prods1, _)) xprods2 =
    2.17 +fun extend_gram (gram1 as Gram (prods1, _)) roots xprods2 =
    2.18    let
    2.19 -    fun symb_of (Delim s) = Some (Terminal (Token s))
    2.20 -      | symb_of (Argument (s, p)) =
    2.21 +    fun simplify preserve s = 
    2.22 +      if preserve then 
    2.23 +        (if s mem (roots \\ ["type", "prop", "any"]) then "logic" else s)
    2.24 +      else (if s = "prop" then "@prop_H" else
    2.25 +              (if s mem (roots \\ ["type", "prop", "any"]) then 
    2.26 +                 "@logic_H" 
    2.27 +               else s));
    2.28 +
    2.29 +    fun not_delim (Delim _) = false
    2.30 +      | not_delim _ = true
    2.31 +
    2.32 +    fun symb_of _ (Delim s) = Some (Terminal (Token s))
    2.33 +      | symb_of preserve (Argument (s, p)) =
    2.34            (case predef_term s of
    2.35 -            None => Some (Nonterminal (s, p))
    2.36 +            None => Some (Nonterminal (simplify preserve s, p))
    2.37            | Some tk => Some (Terminal tk))
    2.38 -      | symb_of _ = None;
    2.39 +      | symb_of _ _ = None;
    2.40  
    2.41      fun prod_of (XProd (lhs, xsymbs, const, pri)) =
    2.42 -      (lhs, (mapfilter symb_of xsymbs, const, pri));
    2.43 +      let val copy_prod = (lhs = "prop" andalso forall not_delim xsymbs andalso
    2.44 +                           const <> "");
    2.45 +
    2.46 +          val preserve = copy_prod 
    2.47 +                         orelse pri = chain_pri andalso lhs = "logic"
    2.48 +                         orelse lhs mem ["@prop_H", "@logic_H", "any"];
    2.49 +
    2.50 +          val lhs' = if copy_prod then "@prop_H" else
    2.51 +                     if lhs = "logic" andalso pri = chain_pri
    2.52 +                        then "@logic_H"
    2.53 +                     else if lhs mem ("logic1" :: (roots \\ ["type", "prop"])) 
    2.54 +                        then "logic"
    2.55 +                     else lhs;
    2.56 +      in (lhs', (mapfilter (symb_of preserve) xsymbs, const, pri))
    2.57 +      end;
    2.58  
    2.59      val prods2 = distinct (map prod_of xprods2);
    2.60    in
    2.61 @@ -553,10 +578,14 @@
    2.62  
    2.63  fun earley grammar startsymbol indata =
    2.64    let
    2.65 +    val startsymbol' = case startsymbol of
    2.66 +                           "logic" => "@logic_H"
    2.67 +                         | "prop"  => "@prop_H"
    2.68 +                         | other   => other;
    2.69      val rhss_ref = case assoc (grammar, startsymbol) of
    2.70                         Some r => r
    2.71 -                     | None => error ("parse: Unknown startsymbol " ^ 
    2.72 -                                      quote startsymbol);
    2.73 +                     | None   => error ("parse: Unknown startsymbol " ^ 
    2.74 +                                        quote startsymbol);
    2.75      val S0 = [(ref [], 0, [], [Nonterm (rhss_ref, 0), Term EndToken], "", 0)];
    2.76      val s = length indata + 1;
    2.77      val Estate = Array.array (s, []);
    2.78 @@ -564,15 +593,17 @@
    2.79      Array.update (Estate, 0, S0);
    2.80      let
    2.81        val l = produce Estate 0 indata EndToken(*dummy*);
    2.82 +
    2.83        val p_trees = get_trees l;
    2.84      in p_trees end
    2.85    end;
    2.86  
    2.87  
    2.88  fun parse (Gram (_, prod_tab)) start toks =
    2.89 +let val r =
    2.90    (case earley prod_tab start toks of
    2.91      [] => sys_error "parse: no parse trees"
    2.92    | pts => pts);
    2.93 +in r end
    2.94  
    2.95  end;
    2.96 -
     3.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Oct 04 13:01:17 1994 +0100
     3.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Oct 04 13:02:16 1994 +0100
     3.3 @@ -79,6 +79,9 @@
     3.4  
     3.5  val funT = Type ("fun", []);
     3.6  
     3.7 +val any = "any"
     3.8 +val anyT = Type (any, []);
     3.9 +
    3.10  
    3.11  (* constants *)
    3.12  
    3.13 @@ -143,7 +146,7 @@
    3.14  (* typ_to_nonterm *)
    3.15  
    3.16  fun typ_to_nonterm (Type (c, _)) = c
    3.17 -  | typ_to_nonterm _ = logic;
    3.18 +  | typ_to_nonterm _ = any;
    3.19  
    3.20  fun typ_to_nonterm1 (Type (c, _)) = c
    3.21    | typ_to_nonterm1 _ = logic1;
    3.22 @@ -256,78 +259,26 @@
    3.23        print_ast_translation) = trfuns;
    3.24      val (parse_rules, print_rules) = rules;
    3.25  
    3.26 -    val Troots = map (apr (Type, [])) new_roots;
    3.27 -    val Troots' = Troots \\ [typeT, propT];
    3.28 -
    3.29 -    fun change_name T ext =
    3.30 -      let val Type (name, ts) = T
    3.31 -      in Type ("@" ^ name ^ ext, ts) end;
    3.32 -
    3.33 -    (* Append "_H" to lhs if production is not a copy or chain production *)
    3.34 -    fun hide_xprod roots (XProd (lhs, symbs, const, pri)) =
    3.35 -      let fun is_delim (Delim _) = true
    3.36 -            | is_delim _ = false
    3.37 -      in if const <> "" andalso lhs mem roots andalso exists is_delim symbs then
    3.38 -           XProd ("@" ^ lhs ^ "_H", symbs, const, pri)
    3.39 -         else XProd (lhs, symbs, const, pri)
    3.40 -      end;
    3.41 -
    3.42 -    (* Make descend production and append "_H" to rhs nonterminal *)
    3.43 -    fun descend_right (from, to) =
    3.44 -      Mfix ("_", change_name to "_H" --> from, "", [0], 0);
    3.45 -
    3.46 -    (* Make descend production and append "_H" to lhs *)
    3.47 -    fun descend_left (from, to) =
    3.48 -      Mfix ("_", to --> change_name from "_H", "", [0], 0);
    3.49 -
    3.50 -    (* Make descend production and append "_A" to lhs *)
    3.51 -    fun descend1 (from, to) =
    3.52 -      Mfix ("_", to --> change_name from "_A", "", [0], 0);
    3.53 -
    3.54 -    (* Make parentheses production for 'hidden' and 'automatic' nonterminal *)
    3.55 -    fun parents T =
    3.56 -      if T = typeT then
    3.57 -        [Mfix ("'(_')", T --> T, "", [0], max_pri)]
    3.58 -      else
    3.59 -        [Mfix ("'(_')", change_name T "_H" --> change_name T "_H", "", [0], max_pri),
    3.60 -         Mfix ("'(_')", change_name T "_A" --> change_name T "_A", "", [0], max_pri)];
    3.61 -
    3.62 -    fun mkappl T =
    3.63 -      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> change_name T "_A", applC,
    3.64 -            [max_pri, 0], max_pri);
    3.65 -
    3.66 -    fun mkid T =
    3.67 -      Mfix ("_", idT --> change_name T "_A", "", [], max_pri);
    3.68 -
    3.69 -    fun mkvar T =
    3.70 -      Mfix ("_", varT --> change_name T "_A", "", [], max_pri);
    3.71 -
    3.72 -    fun constrain T =
    3.73 -      Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC,
    3.74 -            [4, 0], 3)
    3.75 -
    3.76 -    fun unhide T =
    3.77 -      if T <> logicT then
    3.78 -        [Mfix ("_", change_name T "_H" --> T, "", [0], 0),
    3.79 -         Mfix ("_", change_name T "_A" --> T, "", [0], 0)]
    3.80 -      else
    3.81 -        [Mfix ("_", change_name T "_A" --> T, "", [0], 0)];
    3.82 -
    3.83 -    val mfixes' = flat (map parents Troots) @ map mkappl Troots' @
    3.84 -      map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
    3.85 -      map (apl (logicT, descend_right)) (Troots \\ [logicT, typeT]) @
    3.86 -      map (apr (descend1, logic1T)) (Troots') @
    3.87 -      flat (map unhide (Troots \\ [typeT]));
    3.88 -    val mfix_consts =
    3.89 -      distinct (map (fn (Mfix (_, _, c, _, _)) => c) (mfixes @ mfixes'));
    3.90 -    val xprods = map mfix_to_xprod mfixes;
    3.91 -    val xprods' = map mfix_to_xprod mfixes';
    3.92 +    val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
    3.93 +    val mfixes' = (if "prop" mem new_roots then
    3.94 +                     [Mfix ("'(_')", Type ("@prop_H", [])
    3.95 +                            --> Type ("@prop_H", []), "", [0], max_pri),
    3.96 +                      Mfix ("'(_')", Type ("@logic_H", []) 
    3.97 +                            --> Type ("@logic_H", []), "", [0], max_pri),
    3.98 +                      Mfix ("'(_')", anyT --> anyT, "", [0], max_pri),
    3.99 +                      Mfix ("_", propT --> Type ("@prop_H", []), "", [0], 0),
   3.100 +                      Mfix ("_", propT --> anyT, "", [0], 0)]
   3.101 +                   else []) @
   3.102 +                   (if all_roots = new_roots then
   3.103 +                     [Mfix ("_", logicT --> Type ("@logic_H", []), "", [0], 0),
   3.104 +                      Mfix ("_", logicT --> anyT, "", [0], 0)]
   3.105 +                    else [])    
   3.106 +    val xprods = map mfix_to_xprod mfixes 
   3.107 +                 @ map mfix_to_xprod mfixes';
   3.108    in
   3.109      SynExt {
   3.110        roots = new_roots,
   3.111 -      xprods = (map (hide_xprod (all_roots \\ ["logic", "type"])) xprods)
   3.112 -               @ xprods',    (* hide only productions that weren't created
   3.113 -                                automatically *)
   3.114 +      xprods = xprods,
   3.115        consts = filter is_xid (consts union mfix_consts),
   3.116        parse_ast_translation = parse_ast_translation,
   3.117        parse_rules = parse_rules,
   3.118 @@ -352,4 +303,3 @@
   3.119  
   3.120  
   3.121  end;
   3.122 -
     4.1 --- a/src/Pure/Syntax/syntax.ML	Tue Oct 04 13:01:17 1994 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Oct 04 13:02:16 1994 +0100
     4.3 @@ -43,14 +43,15 @@
     4.4      (string * (term list -> term)) list *
     4.5      (string * (term list -> term)) list *
     4.6      (string * (ast list -> ast)) list -> syntax
     4.7 -  val extend_trrules: syntax -> xrule list -> syntax
     4.8 +  val extend_trrules: syntax ->
     4.9 +    (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
    4.10    val merge_syntaxes: syntax -> syntax -> syntax
    4.11    val type_syn: syntax
    4.12    val print_gram: syntax -> unit
    4.13    val print_trans: syntax -> unit
    4.14    val print_syntax: syntax -> unit
    4.15    val test_read: syntax -> string -> string -> unit
    4.16 -  val read: syntax -> typ -> string -> term
    4.17 +  val read: syntax -> typ -> string -> term list
    4.18    val read_typ: syntax -> (indexname -> sort) -> string -> typ
    4.19    val simple_read_typ: string -> typ
    4.20    val pretty_term: syntax -> term -> Pretty.T
    4.21 @@ -176,7 +177,7 @@
    4.22      Syntax {
    4.23        lexicon = extend_lexicon lexicon (delims_of xprods),
    4.24        roots = extend_list roots1 roots2,
    4.25 -      gram = extend_gram gram xprods,
    4.26 +      gram = extend_gram gram (roots1 @ roots2) xprods,
    4.27        consts = consts2 union consts1,
    4.28        parse_ast_trtab =
    4.29          extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
    4.30 @@ -285,7 +286,7 @@
    4.31      val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
    4.32  
    4.33      val toks = tokenize lexicon false str;
    4.34 -    val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks))
    4.35 +    val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
    4.36  
    4.37      fun show_pt pt =
    4.38        let
    4.39 @@ -301,20 +302,20 @@
    4.40  
    4.41  (* read_ast *)
    4.42  
    4.43 -fun read_ast (Syntax tabs) xids root str =
    4.44 +fun read_asts (Syntax tabs) print_msg xids root str =
    4.45    let
    4.46 -    val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    4.47 -    val pts = parse gram root (tokenize lexicon xids str);
    4.48 +    val {lexicon, gram, parse_ast_trtab, roots, ...} = tabs;
    4.49 +    val root' = if root mem (roots \\ ["type", "prop"]) then "@logic_H"
    4.50 +                else if root = "prop" then "@prop_H" else root;
    4.51 +    val pts = parse gram root' (tokenize lexicon xids str);
    4.52  
    4.53 -    fun show_pt pt =
    4.54 -      writeln (str_of_ast (pt_to_ast (K None) pt));
    4.55 +    fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
    4.56    in
    4.57 -    (case pts of
    4.58 -      [pt] => pt_to_ast (lookup_trtab parse_ast_trtab) pt
    4.59 -    | _ =>
    4.60 -      (writeln ("Ambiguous input " ^ quote str);
    4.61 -        writeln "produces the following parse trees:"; seq show_pt pts;
    4.62 -        error "Please disambiguate the grammar or your input."))
    4.63 +    if print_msg andalso length pts > 1 then
    4.64 +      (writeln ("Warning: Ambiguous input " ^ quote str);
    4.65 +       writeln "produces the following parse trees:"; seq show_pt pts)
    4.66 +    else ();
    4.67 +    map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
    4.68    end;
    4.69  
    4.70  
    4.71 @@ -323,10 +324,10 @@
    4.72  fun read (syn as Syntax tabs) ty str =
    4.73    let
    4.74      val {parse_ruletab, parse_trtab, ...} = tabs;
    4.75 -    val ast = read_ast syn false (typ_to_nonterm ty) str;
    4.76 +    val asts = read_asts syn true false (typ_to_nonterm ty) str;
    4.77    in
    4.78 -    ast_to_term (lookup_trtab parse_trtab)
    4.79 -      (normalize_ast (lookup_ruletab parse_ruletab) ast)
    4.80 +    map (ast_to_term (lookup_trtab parse_trtab))
    4.81 +      (map (normalize_ast (lookup_ruletab parse_ruletab)) asts)
    4.82    end;
    4.83  
    4.84  
    4.85 @@ -334,7 +335,11 @@
    4.86  
    4.87  fun read_typ syn def_sort str =
    4.88    let
    4.89 -    val t = read syn typeT str;
    4.90 +    val ts = read syn typeT str;
    4.91 +    val t = case ts of
    4.92 +                [t'] => t'
    4.93 +              | _ => error "This should not happen while parsing a type.\n\
    4.94 +                           \Please check your type syntax for ambiguities!";
    4.95      val sort_env = raw_term_sorts t;
    4.96    in
    4.97      typ_of_term sort_env def_sort t
    4.98 @@ -345,7 +350,9 @@
    4.99  
   4.100  (* read rules *)
   4.101  
   4.102 -fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
   4.103 +fun read_rule (syn as Syntax tabs) print_msg
   4.104 +              (check_types: bool -> term list * typ -> int * term * 'a)
   4.105 +              (xrule as ((_, lhs_src), (_, rhs_src))) =
   4.106    let
   4.107      val Syntax {consts, ...} = syn;
   4.108  
   4.109 @@ -355,8 +362,20 @@
   4.110        | constantify (Appl asts) = Appl (map constantify asts);
   4.111  
   4.112      fun read_pat (root, str) =
   4.113 -      constantify (read_ast syn true root str)
   4.114 -        handle ERROR => error ("The error above occurred in " ^ quote str);
   4.115 +      let val {parse_ruletab, parse_trtab, ...} = tabs;
   4.116 +          val asts = read_asts syn print_msg true root str;
   4.117 +          val ts = map (ast_to_term (lookup_trtab parse_trtab))
   4.118 +                     (map (normalize_ast (lookup_ruletab parse_ruletab)) asts);
   4.119 +
   4.120 +          val idx = if length ts = 1 then 0
   4.121 +            else (if print_msg then
   4.122 +                    writeln ("This occured in syntax translation rule: " ^
   4.123 +                             quote lhs_src ^ "  ->  " ^ quote rhs_src)
   4.124 +                  else ();
   4.125 +                  #1 (check_types print_msg (ts, Type (root, []))))
   4.126 +      in constantify (nth_elem (idx, asts))
   4.127 +           handle ERROR => error ("The error above occurred in " ^ quote str)
   4.128 +      end;
   4.129  
   4.130      val rule as (lhs, rhs) = (pairself read_pat) xrule;
   4.131    in
   4.132 @@ -374,7 +393,7 @@
   4.133    op <-| of (string * string) * (string * string) |
   4.134    op <-> of (string * string) * (string * string);
   4.135  
   4.136 -fun read_xrules syn xrules =
   4.137 +fun read_xrules syn check_types xrules =
   4.138    let
   4.139      fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
   4.140        | right_rule (xpat1 <-| xpat2) = None
   4.141 @@ -383,9 +402,12 @@
   4.142      fun left_rule (xpat1 |-> xpat2) = None
   4.143        | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
   4.144        | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
   4.145 +
   4.146 +    val rrules = mapfilter right_rule xrules;
   4.147 +    val lrules = mapfilter left_rule xrules;
   4.148    in
   4.149 -    (map (read_rule syn) (mapfilter right_rule xrules),
   4.150 -     map (read_rule syn) (mapfilter left_rule xrules))
   4.151 +    (map (read_rule syn true check_types) rrules,
   4.152 +     map (read_rule syn (rrules = []) check_types) lrules)
   4.153    end;
   4.154  
   4.155  
   4.156 @@ -429,9 +451,7 @@
   4.157  
   4.158  val extend_trfuns = ext_syntax syn_ext_trfuns;
   4.159  
   4.160 -fun extend_trrules syn xrules =
   4.161 -  ext_syntax syn_ext_rules syn (read_xrules syn xrules);
   4.162 -
   4.163 +fun extend_trrules syn check_types xrules =
   4.164 +  ext_syntax syn_ext_rules syn (read_xrules syn check_types xrules);
   4.165  
   4.166  end;
   4.167 -
     5.1 --- a/src/Pure/Syntax/type_ext.ML	Tue Oct 04 13:01:17 1994 +0100
     5.2 +++ b/src/Pure/Syntax/type_ext.ML	Tue Oct 04 13:02:16 1994 +0100
     5.3 @@ -177,7 +177,8 @@
     5.4     Mfix ("_",           typeT --> typesT,              "", [], max_pri),
     5.5     Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
     5.6     Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
     5.7 -   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
     5.8 +   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
     5.9 +   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
    5.10    []
    5.11    ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    5.12     [],