(* Copyright (C) 2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) let debug = false let debug_print s = if debug then begin prerr_endline ""; prerr_endline s; prerr_endline "" end (** if set to true each number will have a different insance number and can * thus be interpreted differently than others *) let use_fresh_num_instances = false (** does the lexer return COMMENT tokens? *) let return_comments = false open Printf open DisambiguateTypes exception Parse_error of Token.flocation * string let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments () let fresh_num_instance = let n = ref 0 in if use_fresh_num_instances then (fun () -> incr n; !n) else (fun () -> 0) let choice_of_uri uri = let term = CicUtil.term_of_uri uri in (uri, (fun _ _ _ -> term)) let grammar = Grammar.gcreate cic_lexer let term = Grammar.Entry.create grammar "term" let term0 = Grammar.Entry.create grammar "term0" let tactic = Grammar.Entry.create grammar "tactic" let tactical = Grammar.Entry.create grammar "tactical" let tactical0 = Grammar.Entry.create grammar "tactical0" let command = Grammar.Entry.create grammar "command" let alias_spec = Grammar.Entry.create grammar "alias_spec" let macro = Grammar.Entry.create grammar "macro" let script = Grammar.Entry.create grammar "script" let statement = Grammar.Entry.create grammar "statement" let statements = Grammar.Entry.create grammar "statements" let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) let fail floc msg = let (x, y) = CicAst.loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) let name_of_string = function | "_" -> Cic.Anonymous | s -> Cic.Name s let string_of_name = function | Cic.Anonymous -> "_" | Cic.Name s -> s let int_opt = function | None -> None | Some lexeme -> Some (int_of_string lexeme) let int_of_string s = try Pervasives.int_of_string s with Failure _ -> failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s) (** the uri of an inductive type (a ".ind" uri) is not meaningful without an * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind" * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive * type in a block of mutual inductive types. * * This function performs the expansion foo.ind -> foo#xpointer..., if needed *) let ind_expansion uri = let len = String.length uri in if len >= 4 && String.sub uri (len - 4) 4 = ".ind" then uri ^ "#xpointer(1/1)" else uri let mk_binder_ast binder typ vars body = List.fold_right (fun var body -> let name = name_of_string var in CicAst.Binder (binder, (name, typ), body)) vars body EXTEND GLOBAL: term term0 statement statements; int: [ [ num = NUM -> try int_of_string num with Failure _ -> raise (Parse_error (loc, "integer literal expected")) ] ]; meta_subst: [ [ s = SYMBOL "_" -> None | t = term -> Some t ] ]; binder_low: [ [ SYMBOL <:unicode> (* Π *) -> `Pi | SYMBOL <:unicode> (* ∃ *) -> `Exists | SYMBOL <:unicode> (* ∀ *) -> `Forall ] ]; binder_high: [ [ SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; sort: [ [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp ] ]; typed_name: [ [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" -> (Cic.Name i, Some typ) | i = IDENT -> (Cic.Name i, None) ] ]; subst: [ [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) PAREN "["; substs = LIST1 [ i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) ] SEP SYMBOL ";"; PAREN "]" -> substs ] ]; substituted_name: [ (* a subs.name is an explicit substitution subject *) [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst) | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst) ] ]; name: [ (* as substituted_name with no explicit substitution *) [ s = [ IDENT | SYMBOL ] -> s ] ]; pattern: [ [ n = name -> (n, []) | PAREN "("; head = name; vars = LIST1 typed_name; PAREN ")" -> (head, vars) ] ]; arg: [ [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; ty = term; PAREN ")" -> names,ty | name = IDENT -> [name],CicAst.Implicit ] ]; let_defs:[ [ defs = LIST1 [ name = IDENT; args = LIST1 [arg = arg -> arg]; index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; ty = OPT [ SYMBOL ":" ; t = term -> t ]; SYMBOL <:unicode> (* ≝ *); t1 = term -> let rec list_of_binder binder ty final_term = function | [] -> final_term | name::tl -> CicAst.Binder (binder, (Cic.Name name, Some ty), list_of_binder binder ty final_term tl) in let rec binder_of_arg_list binder final_term = function | [] -> final_term | (l,ty)::tl -> list_of_binder binder ty (binder_of_arg_list binder final_term tl) l in let t1' = binder_of_arg_list `Lambda t1 args in let ty' = match ty with | None -> None | Some ty -> Some (binder_of_arg_list `Pi ty args) in let rec get_position_of name n = function | [] -> (None,n) | nam::tl -> if nam = name then (Some n,n) else (get_position_of name (n+1) tl) in let rec find_arg name n = function | [] -> (fail loc (sprintf "Argument %s not found" name)) | (l,_)::tl -> let (got,len) = get_position_of name 0 l in (match got with | None -> (find_arg name (n+len) tl) | Some where -> n + where) in let index = (match index_name with | None -> 0 | (Some name) -> find_arg name 0 args) in ((Cic.Name name,ty'), t1', index) ] SEP "and" -> defs ]]; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; binder_vars: [ [ vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ","; typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ) ] ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: [ "letin" NONA [ "let"; var = typed_name; SYMBOL <:unicode> (* ≝ *); t1 = term; "in"; t2 = term -> return_term loc (CicAst.LetIn (var, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs; "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] | "binder" RIGHTA [ b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term -> let binder = mk_binder_ast b typ vars body in return_term loc binder | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term -> let binder = mk_binder_ast b typ vars body in return_term loc binder | t1 = term; SYMBOL <:unicode> (* → *); t2 = term -> return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) ] | "logic_add" LEFTA [ (* nothing here by default *) ] | "logic_mult" LEFTA [ (* nothing here by default *) ] | "logic_inv" NONA [ (* nothing here by default *) ] | "relop" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) ] | "add" LEFTA [ (* nothing here by default *) ] | "mult" LEFTA [ (* nothing here by default *) ] | "power" LEFTA [ (* nothing here by default *) ] | "inv" NONA [ (* nothing here by default *) ] | "apply" LEFTA [ t1 = term; t2 = term -> let rec aux = function | CicAst.Appl (hd :: tl) -> aux hd @ tl | term -> [term] in CicAst.Appl (aux t1 @ [t2]) ] | "simple" NONA [ sort = sort -> CicAst.Sort sort | n = substituted_name -> return_term loc n | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ()))) | IMPLICIT -> return_term loc CicAst.Implicit | PLACEHOLDER -> return_term loc CicAst.UserInput | m = META; substs = [ PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> substs ] -> let index = try int_of_string (String.sub m 1 (String.length m - 1)) with Failure "int_of_string" -> fail loc ("Invalid meta variable number: " ^ m) in return_term loc (CicAst.Meta (index, substs)) | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; indty_ident = OPT ["in" ; id = IDENT -> id ]; "with"; PAREN "["; patterns = LIST0 [ lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term -> ((lhs: CicAst.case_pattern), rhs) ] SEP SYMBOL "|"; PAREN "]" -> return_term loc (CicAst.Case (t, indty_ident, outtyp, patterns)) | PAREN "("; t1 = term; SYMBOL ":"; t2 = term; PAREN ")" -> return_term loc (CicAst.Appl [CicAst.Symbol ("cast", 0); t1; t2]) | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; ident_list1: [ [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl | [ IDENT "whd" ] -> `Whd | [ IDENT "normalize" ] -> `Normalize ] ]; tactic: [ [ [ IDENT "absurd" ]; t = tactic_term -> TacticAst.Absurd (loc, t) | [ IDENT "apply" ]; t = tactic_term -> TacticAst.Apply (loc, t) | [ IDENT "assumption" ] -> TacticAst.Assumption loc | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> TacticAst.Auto (loc,num) | [ IDENT "change" ]; t1 = tactic_term; "with"; t2 = tactic_term; where = tactic_where -> TacticAst.Change (loc, t1, t2, where) (* TODO Change_pattern *) | [ IDENT "contradiction" ] -> TacticAst.Contradiction loc | [ IDENT "cut" ]; t = tactic_term -> TacticAst.Cut (loc, t) | [ IDENT "decompose" ]; principles = ident_list1; where = IDENT -> TacticAst.Decompose (loc, where, principles) | [ IDENT "discriminate" ]; hyp = IDENT -> TacticAst.Discriminate (loc, hyp) | [ IDENT "elimType" ]; t = tactic_term -> TacticAst.ElimType (loc, t) | [ IDENT "elim" ]; t1 = tactic_term; using = OPT [ "using"; using = tactic_term -> using ] -> TacticAst.Elim (loc, t1, using) | [ IDENT "exact" ]; t = tactic_term -> TacticAst.Exact (loc, t) | [ IDENT "exists" ] -> TacticAst.Exists loc | [ IDENT "fold" ]; kind = reduction_kind; t = tactic_term -> TacticAst.Fold (loc, kind, t) | [ IDENT "fourier" ] -> TacticAst.Fourier loc | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) | [ IDENT "injection" ]; ident = IDENT -> TacticAst.Injection (loc, ident) | [ IDENT "intros" ]; num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> let idents = match idents with None -> [] | Some idents -> idents in TacticAst.Intros (loc, num, idents) | [ IDENT "intro" ] -> TacticAst.Intros (loc, Some 1, []) | [ IDENT "left" ] -> TacticAst.Left loc | [ IDENT "letin" ]; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) | kind = reduction_kind; pat = OPT [ "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] -> pat ]; terms = LIST0 term SEP SYMBOL "," -> (match (pat, terms) with | None, [] -> TacticAst.Reduce (loc, kind, None) | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal)) | Some pat, [] -> fail loc "Missing term [list]" | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat))) | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term -> TacticAst.ReduceAt (loc, kind, where, pat) | [ IDENT "reflexivity" ] -> TacticAst.Reflexivity loc | [ IDENT "replace" ]; t1 = tactic_term; "with"; t2 = tactic_term -> TacticAst.Replace (loc, t1, t2) | [ IDENT "rewrite" ; IDENT "left" ] ; t = term -> TacticAst.Rewrite (loc,`Left, t, None) | [ IDENT "rewrite" ; IDENT "right" ] ; t = term -> TacticAst.Rewrite (loc,`Right, t, None) (* TODO Replace_pattern *) | [ IDENT "right" ] -> TacticAst.Right loc | [ IDENT "ring" ] -> TacticAst.Ring loc | [ IDENT "split" ] -> TacticAst.Split loc | [ IDENT "symmetry" ] -> TacticAst.Symmetry loc | [ IDENT "transitivity" ]; t = tactic_term -> TacticAst.Transitivity (loc, t) ] ]; tactical: [ "sequence" LEFTA [ tacticals = LIST1 NEXT SEP SYMBOL ";" -> TacticAst.Seq (loc, tacticals) ] | "then" NONA [ tac = tactical; PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA [ [ IDENT "do" ]; count = int; tac = tactical -> TacticAst.Do (loc, count, tac) | [ IDENT "repeat" ]; tac = tactical -> TacticAst.Repeat (loc, tac) ] | "simple" NONA [ IDENT "tries"; PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> TacticAst.Tries (loc, tacs) | IDENT "try"; tac = NEXT -> TacticAst.Try (loc, tac) | IDENT "fail" -> TacticAst.Fail loc | IDENT "id" -> TacticAst.IdTac loc | PAREN "("; tac = tactical; PAREN ")" -> tac | tac = tactic -> TacticAst.Tactic (loc, tac) ] ]; theorem_flavour: [ [ [ IDENT "definition" ] -> `Definition | [ IDENT "fact" ] -> `Fact | [ IDENT "lemma" ] -> `Lemma | [ IDENT "remark" ] -> `Remark | [ IDENT "theorem" ] -> `Theorem ] ]; inductive_spec: [ [ fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; fst_constructors = LIST0 constructor SEP SYMBOL "|"; tl = OPT [ "with"; types = LIST1 [ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> (name, true, typ, constructors) ] SEP "with" -> types ] -> let params = List.fold_right (fun (names, typ) acc -> (List.map (fun name -> (name, typ)) names) @ acc) params [] in let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in let tl_ind_types = match tl with None -> [] | Some types -> types in let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; macro: [ [ [ IDENT "quit" ] -> TacticAst.Quit loc (* | [ IDENT "abort" ] -> TacticAst.Abort loc *) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) (* | [ IDENT "undo" ]; steps = OPT NUM -> TacticAst.Undo (loc, int_opt steps) | [ IDENT "redo" ]; steps = OPT NUM -> TacticAst.Redo (loc, int_opt steps) *) | [ IDENT "check" ]; t = term -> TacticAst.Check (loc, t) | [ IDENT "hint" ] -> TacticAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> TacticAst.WMatch (loc,t) | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> TacticAst.WInstance (loc,t) | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> TacticAst.WLocate (loc,id) | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> TacticAst.WElim (loc, t) | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> TacticAst.WHint (loc,t) | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name) ] ]; alias_spec: [ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> let alpha = "[a-zA-Z]" in let num = "[0-9]+" in let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in let rex = Str.regexp ("^"^ident^"$") in if Str.string_match rex id 0 then let rex = Str.regexp ("^\\(cic:/\\|theory:/\\)"^ident^ "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^ "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$") in if Str.string_match rex uri 0 then TacticAst.Ident_alias (id, uri) else raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri)) else raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id)) | IDENT "symbol"; symbol = QSTRING; instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; SYMBOL "="; dsc = QSTRING -> let instance = match instance with Some i -> int_of_string i | None -> 0 in TacticAst.Symbol_alias (symbol, instance, dsc) | IDENT "num"; instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ]; SYMBOL "="; dsc = QSTRING -> let instance = match instance with Some i -> int_of_string i | None -> 0 in TacticAst.Number_alias (instance, dsc) ] ]; command: [[ [ IDENT "set" ]; n = QSTRING; v = QSTRING -> TacticAst.Set (loc, n, v) | [ IDENT "qed" ] -> TacticAst.Qed loc | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> TacticAst.Theorem (loc, flavour, name, typ, body) | flavour = theorem_flavour; name = OPT IDENT; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> TacticAst.Theorem (loc, flavour, name, CicAst.Implicit, body) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = let_defs -> let name,ty = match defs with | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit | _ -> assert false in let body = CicAst.Ident (name,None) in TacticAst.Theorem(loc, `Definition, Some name, ty, Some (CicAst.LetRec (ind_kind, defs, body))) | [ IDENT "inductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in TacticAst.Inductive (loc, params, ind_types) | [ IDENT "coinductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in let ind_types = (* set inductive flags to false (coinductive) *) List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) ind_types in TacticAst.Inductive (loc, params, ind_types) | [ IDENT "coercion" ] ; name = IDENT -> TacticAst.Coercion (loc, CicAst.Ident (name,Some [])) | [ IDENT "coercion" ] ; name = URI -> TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) | [ IDENT "alias" ]; spec = alias_spec -> TacticAst.Alias (loc, spec) ]]; executable: [ [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd) | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac) | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac) ] ]; comment: [ [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> TacticAst.Code (loc, ex) | str = NOTE -> TacticAst.Note (loc, str) ] ]; statement: [ [ ex = executable -> TacticAst.Executable (loc,ex) | com = comment -> TacticAst.Comment (loc, com) ] ]; statements: [ [ l = LIST0 [ statement ] -> l ] ]; END let exc_located_wrapper f = try f () with | Stdpp.Exc_located (floc, Stream.Error msg) -> raise (Parse_error (floc, msg)) | Stdpp.Exc_located (floc, exn) -> raise (Parse_error (floc, (Printexc.to_string exn))) let parse_term stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream)) let parse_statement stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream)) let parse_statements stream = exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream)) (**/**) (** {2 Interface for gTopLevel} *) module EnvironmentP3 = struct type t = environment let empty = "" let aliases_grammar = Grammar.gcreate cic_lexer let aliases = Grammar.Entry.create aliases_grammar "aliases" let to_string env = let aliases = Environment.fold (fun domain_item (dsc, _) acc -> let s = match domain_item with | Id id -> TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "." | Symbol (symb, i) -> TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc)) ^ "." | Num i -> TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "." in s :: acc) env [] in String.concat "\n" (List.sort compare aliases) EXTEND GLOBAL: aliases; aliases: [ (* build an environment from an aliases list *) [ aliases = LIST0 alias; EOI -> List.fold_left (fun env (domain_item, codomain_item) -> Environment.add domain_item codomain_item env) Environment.empty aliases ] ]; alias: [ (* return a pair from an alias *) [ IDENT "alias"; choice = [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI -> (Id id, choice_of_uri uri) | IDENT "symbol"; symbol = QSTRING; PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; SYMBOL "="; dsc = QSTRING -> (Symbol (symbol, int_of_string instance), DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) | IDENT "num"; PAREN "("; IDENT "instance"; instance = NUM; PAREN ")"; SYMBOL "="; dsc = QSTRING -> (Num (int_of_string instance), DisambiguateChoices.lookup_num_by_dsc dsc) ] -> choice ] ]; END let of_string s = if s = empty then Environment.empty else exc_located_wrapper (fun () -> Grammar.Entry.parse aliases (Stream.of_string s)) end (* vim:set encoding=utf8: *)