From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- parsing/egramcoq.ml | 483 ------------------- parsing/egramcoq.mli | 19 - parsing/egramml.ml | 84 ---- parsing/egramml.mli | 33 -- parsing/extend.ml | 126 +++++ parsing/g_constr.ml4 | 519 -------------------- parsing/g_constr.mlg | 526 ++++++++++++++++++++ parsing/g_prim.ml4 | 122 ----- parsing/g_prim.mlg | 123 +++++ parsing/g_proofs.ml4 | 133 ------ parsing/g_vernac.ml4 | 1195 ---------------------------------------------- parsing/notation_gram.ml | 43 ++ parsing/notgram_ops.ml | 71 +++ parsing/notgram_ops.mli | 20 + parsing/parsing.mllib | 8 +- parsing/pcoq.ml | 299 ++++++------ parsing/pcoq.mli | 252 +++++----- parsing/ppextend.ml | 77 +++ parsing/ppextend.mli | 51 ++ 19 files changed, 1317 insertions(+), 2867 deletions(-) delete mode 100644 parsing/egramcoq.ml delete mode 100644 parsing/egramcoq.mli delete mode 100644 parsing/egramml.ml delete mode 100644 parsing/egramml.mli create mode 100644 parsing/extend.ml delete mode 100644 parsing/g_constr.ml4 create mode 100644 parsing/g_constr.mlg delete mode 100644 parsing/g_prim.ml4 create mode 100644 parsing/g_prim.mlg delete mode 100644 parsing/g_proofs.ml4 delete mode 100644 parsing/g_vernac.ml4 create mode 100644 parsing/notation_gram.ml create mode 100644 parsing/notgram_ops.ml create mode 100644 parsing/notgram_ops.mli create mode 100644 parsing/ppextend.ml create mode 100644 parsing/ppextend.mli (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml deleted file mode 100644 index 5f63d21c..00000000 --- a/parsing/egramcoq.ml +++ /dev/null @@ -1,483 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* false - | Extend.RightA, Some Extend.LeftA -> false - | _ -> true - -let create_assoc = function - | None -> Extend.RightA - | Some a -> a - -let error_level_assoc p current expected = - let open Pp in - let pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in - user_err - (str "Level " ++ int p ++ str " is already declared " ++ - pr_assoc current ++ str " associative while it is now expected to be " ++ - pr_assoc expected ++ str " associative.") - -let create_pos = function - | None -> Extend.First - | Some lev -> Extend.After (constr_level lev) - -let find_position_gen current ensure assoc lev = - match lev with - | None -> - current, (None, None, None, None) - | Some n -> - let after = ref None in - let init = ref None in - let rec add_level q = function - | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l - | (p,a,reinit)::l when Int.equal p n -> - if reinit then - let a' = create_assoc assoc in - (init := Some (a',create_pos q); (p,a',false)::l) - else if admissible_assoc (a,assoc) then - raise Exit - else - error_level_assoc p a (Option.get assoc) - | l -> after := q; (n,create_assoc assoc,ensure)::l - in - try - let updated = add_level None current in - let assoc = create_assoc assoc in - begin match !init with - | None -> - (* Create the entry *) - updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None) - | _ -> - (* The reinit flag has been updated *) - updated, (Some (Extend.Level (constr_level n)), None, None, !init) - end - with - (* Nothing has changed *) - Exit -> - (* Just inherit the existing associativity and name (None) *) - current, (Some (Extend.Level (constr_level n)), None, None, None) - -let rec list_mem_assoc_triple x = function - | [] -> false - | (a,b,c) :: l -> Int.equal a x || list_mem_assoc_triple x l - -let register_empty_levels accu forpat levels = - let rec filter accu = function - | [] -> ([], accu) - | n :: rem -> - let rem, accu = filter accu rem in - let (clev, plev) = accu in - let levels = if forpat then plev else clev in - if not (list_mem_assoc_triple n levels) then - let nlev, ans = find_position_gen levels true None (Some n) in - let nlev = if forpat then (clev, nlev) else (nlev, plev) in - ans :: rem, nlev - else rem, accu - in - filter accu levels - -let find_position accu forpat assoc level = - let (clev, plev) = accu in - let levels = if forpat then plev else clev in - let nlev, ans = find_position_gen levels false assoc level in - let nlev = if forpat then (clev, nlev) else (nlev, plev) in - (ans, nlev) - -(**************************************************************************) -(* - * --- Note on the mapping of grammar productions to camlp5 actions --- - * - * Translation of environments: a production - * [ nt1(x1) ... nti(xi) ] -> act(x1..xi) - * is written (with camlp5 conventions): - * (fun vi -> .... (fun v1 -> act(v1 .. vi) )..) - * where v1..vi are the values generated by non-terminals nt1..nti. - * Since the actions are executed by substituting an environment, - * the make_*_action family build the following closure: - * - * ((fun env -> - * (fun vi -> - * (fun env -> ... - * - * (fun v1 -> - * (fun env -> gram_action .. env act) - * ((x1,v1)::env)) - * ...) - * ((xi,vi)::env))) - * []) - *) - -(**********************************************************************) -(** Declare Notations grammar rules *) - -(**********************************************************************) -(* Binding constr entry keys to entries *) - -(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp5_assoc = function - | Some NonA | Some RightA -> RightA - | None | Some LeftA -> LeftA - -let assoc_eq al ar = match al, ar with -| NonA, NonA -| RightA, RightA -| LeftA, LeftA -> true -| _, _ -> false - -(* [adjust_level assoc from prod] where [assoc] and [from] are the name - and associativity of the level where to add the rule; the meaning of - the result is - - None = SELF - Some None = NEXT - Some (Some (n,cur)) = constr LEVEL n - s.t. if [cur] is set then [n] is the same as the [from] level *) -let adjust_level assoc from = function -(* Associativity is None means force the level *) - | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true)) -(* Compute production name on the right side *) - (* If NonA or LeftA on the right-hand side, set to NEXT *) - | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) -> - Some None - (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some RightA)) -> - Some (Some (n,true)) -(* Compute production name on the left side *) - (* If NonA on the left-hand side, adopt the current assoc ?? *) - | (NumLevel n,BorderProd (Left,Some NonA)) -> None - (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> - None - (* Otherwise, force the level, n or n-1, according to expected assoc *) - | (NumLevel n,BorderProd (Left,Some a)) -> - begin match a with - | LeftA -> Some (Some (n, true)) - | _ -> Some None - end - (* None means NEXT *) - | (NextLevel,_) -> Some None -(* Compute production name elsewhere *) - | (NumLevel n,InternalProd) -> - if from = n + 1 then Some None else Some (Some (n, Int.equal n from)) - -type _ target = -| ForConstr : constr_expr target -| ForPattern : cases_pattern_expr target - -type prod_info = production_level * production_position - -type (_, _) entry = -| TTName : ('self, Misctypes.lname) entry -| TTReference : ('self, reference) entry -| TTBigint : ('self, Constrexpr.raw_natural_number) entry -| TTConstr : prod_info * 'r target -> ('r, 'r) entry -| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry -| TTPattern : int -> ('self, cases_pattern_expr) entry -| TTOpenBinderList : ('self, local_binder_expr list) entry -| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry - -type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry - -(* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = - fun forpat level -> match forpat with - | ForConstr -> - if level = 200 then Constr.binder_constr, None - else Constr.operconstr, Some level - | ForPattern -> Constr.pattern, Some level - -let target_entry : type s. s target -> s Gram.entry = function -| ForConstr -> Constr.operconstr -| ForPattern -> Constr.pattern - -let is_self from e = match e with -| (NumLevel n, BorderProd (Right, _ (* Some(NonA|LeftA) *))) -> false -| (NumLevel n, BorderProd (Left, _)) -> Int.equal from n -| _ -> false - -let is_binder_level from e = match e with -| (NumLevel 200, (BorderProd (Right, _) | InternalProd)) -> from = 200 -| _ -> false - -let make_sep_rules = function - | [tk] -> Atoken tk - | tkl -> - let rec mkrule : Tok.t list -> string rules = function - | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "") - | tkn :: rem -> - let Rules ({ norec_rule = r }, f) = mkrule rem in - let r = { norec_rule = Next (r, Atoken tkn) } in - Rules (r, fun _ -> f) - in - let r = mkrule (List.rev tkl) in - Arules [r] - -let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat -> - if is_binder_level from p then Aentryl (target_entry forpat, 200) - else if is_self from p then Aself - else - let g = target_entry forpat in - let lev = adjust_level assoc from p in - begin match lev with - | None -> Aentry g - | Some None -> Anext - | Some (Some (lev, cur)) -> Aentryl (g, lev) - end - -let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with -| TTConstr (p, forpat) -> symbol_of_target p assoc from forpat -| TTConstrList (typ', [], forpat) -> - Alist1 (symbol_of_target typ' assoc from forpat) -| TTConstrList (typ', tkl, forpat) -> - Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) -| TTPattern p -> Aentryl (Constr.pattern, p) -| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) -| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) -| TTName -> Aentry Prim.name -| TTOpenBinderList -> Aentry Constr.open_binders -| TTBigint -> Aentry Prim.bigint -| TTReference -> Aentry Constr.global - -let interp_entry forpat e = match e with -| ETProdName -> TTAny TTName -| ETProdReference -> TTAny TTReference -| ETProdBigint -> TTAny TTBigint -| ETProdConstr p -> TTAny (TTConstr (p, forpat)) -| ETProdPattern p -> TTAny (TTPattern p) -| ETProdOther _ -> assert false (** not used *) -| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) -| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList -| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) - -let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with - | Anonymous -> CPatAtom None - | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id)) - -type 'r env = { - constrs : 'r list; - constrlists : 'r list list; - binders : cases_pattern_expr list; - binderlists : local_binder_expr list list; -} - -let push_constr subst v = { subst with constrs = v :: subst.constrs } - -let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v -> -match e with -| TTConstr _ -> push_constr subst v -| TTName -> - begin match forpat with - | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders } - | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) - end -| TTPattern _ -> - begin match forpat with - | ForConstr -> { subst with binders = v :: subst.binders } - | ForPattern -> push_constr subst v - end -| TTOpenBinderList -> { subst with binderlists = v :: subst.binderlists } -| TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } -| TTBigint -> - begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (v,true))) - end -| TTReference -> - begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CRef (v, None)) - | ForPattern -> push_constr subst (CAst.make @@ CPatAtom (Some v)) - end -| TTConstrList _ -> { subst with constrlists = v :: subst.constrlists } - -type (_, _) ty_symbol = -| TyTerm : Tok.t -> ('s, string) ty_symbol -| TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol - -type ('self, _, 'r) ty_rule = -| TyStop : ('self, 'r, 'r) ty_rule -| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule -| TyMark : int * bool * int * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule - -type 'r gen_eval = Loc.t -> 'r env -> 'r - -let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> a = function -| TyStop -> - fun f env loc -> f loc env -| TyNext (rem, TyTerm _) -> - fun f env _ -> ty_eval rem f env -| TyNext (rem, TyNonTerm (_, _, _, false)) -> - fun f env _ -> ty_eval rem f env -| TyNext (rem, TyNonTerm (forpat, e, _, true)) -> - fun f env v -> - ty_eval rem f (push_item forpat e env v) -| TyMark (n, b, p, rem) -> - fun f env -> - let heads, constrs = List.chop n env.constrs in - let constrlists, constrs = - if b then - (* We rearrange constrs = c1..cn rem and constrlists = [d1..dr e1..ep] rem' into - constrs = e1..ep rem and constrlists [c1..cn d1..dr] rem' *) - let constrlist = List.hd env.constrlists in - let constrlist, tail = List.chop (List.length constrlist - p) constrlist in - (heads @ constrlist) :: List.tl env.constrlists, tail @ constrs - else - (* We rearrange constrs = c1..cn e1..ep rem into - constrs = e1..ep rem and add a constr list [c1..cn] *) - let constrlist, tail = List.chop (n - p) heads in - constrlist :: env.constrlists, tail @ constrs - in - ty_eval rem f { env with constrs; constrlists; } - -let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function -| TyStop -> Stop -| TyMark (_, _, _, r) -> ty_erase r -| TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) -| TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) - -type ('self, 'r) any_ty_rule = -| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule - -let make_ty_rule assoc from forpat prods = - let rec make_ty_rule = function - | [] -> AnyTyRule TyStop - | GramConstrTerminal tok :: rem -> - let AnyTyRule r = make_ty_rule rem in - AnyTyRule (TyNext (r, TyTerm tok)) - | GramConstrNonTerminal (e, var) :: rem -> - let AnyTyRule r = make_ty_rule rem in - let TTAny e = interp_entry forpat e in - let s = symbol_of_entry assoc from e in - let bind = match var with None -> false | Some _ -> true in - AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind))) - | GramConstrListMark (n, b, p) :: rem -> - let AnyTyRule r = make_ty_rule rem in - AnyTyRule (TyMark (n, b, p, r)) - in - make_ty_rule (List.rev prods) - -let target_to_bool : type r. r target -> bool = function -| ForConstr -> false -| ForPattern -> true - -let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = - let empty = (pos, [(name, p4assoc, [])]) in - if forpat then ExtendRule (Constr.pattern, reinit, empty) - else ExtendRule (Constr.operconstr, reinit, empty) - -let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with -| Stop -> [] -| Next (rem, Aentryl (_, i)) -> - let rem = pure_sublevels level rem in - begin match level with - | Some j when Int.equal i j -> rem - | _ -> i :: rem - end -| Next (rem, _) -> pure_sublevels level rem - -let make_act : type r. r target -> _ -> r gen_eval = function -| ForConstr -> fun notation loc env -> - let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in - CAst.make ~loc @@ CNotation (notation, env) -| ForPattern -> fun notation loc env -> - let env = (env.constrs, env.constrlists) in - CAst.make ~loc @@ CPatNotation (notation, env, []) - -let extend_constr state forpat ng = - let n,_,_ = ng.notgram_level in - let assoc = ng.notgram_assoc in - let (entry, level) = interp_constr_entry_key forpat n in - let fold (accu, state) pt = - let AnyTyRule r = make_ty_rule assoc n forpat pt in - let symbs = ty_erase r in - let pure_sublevels = pure_sublevels level symbs in - let isforpat = target_to_bool forpat in - let needed_levels, state = register_empty_levels state isforpat pure_sublevels in - let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in - let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in - let empty = { constrs = []; constrlists = []; binders = []; binderlists = [] } in - let act = ty_eval r (make_act forpat ng.notgram_notation) empty in - let rule = (name, p4assoc, [Rule (symbs, act)]) in - let r = ExtendRule (entry, reinit, (pos, [rule])) in - (accu @ empty_rules @ [r], state) - in - List.fold_left fold ([], state) ng.notgram_prods - -let constr_levels = GramState.field () - -let extend_constr_notation ng state = - let levels = match GramState.get state constr_levels with - | None -> default_constr_levels - | Some lev -> lev - in - (* Add the notation in constr *) - let (r, levels) = extend_constr levels ForConstr ng in - (* Add the notation in cases_pattern *) - let (r', levels) = extend_constr levels ForPattern ng in - let state = GramState.set state constr_levels levels in - (r @ r', state) - -let constr_grammar : one_notation_grammar grammar_command = - create_grammar_command "Notation" extend_constr_notation - -let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli deleted file mode 100644 index e15add10..00000000 --- a/parsing/egramcoq.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* unit -(** Add a term notation rule to the parsing system. *) diff --git a/parsing/egramml.ml b/parsing/egramml.ml deleted file mode 100644 index 90cd7d10..00000000 --- a/parsing/egramml.ml +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 's grammar_prod_item - -type 'a ty_arg = ('a -> raw_generic_argument) - -type ('self, _, 'r) ty_rule = -| TyStop : ('self, 'r, 'r) ty_rule -| TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) Extend.symbol * 'b ty_arg option -> - ('self, 'b -> 'a, 'r) ty_rule - -type ('self, 'r) any_ty_rule = -| AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule - -let rec ty_rule_of_gram = function -| [] -> AnyTyRule TyStop -| GramTerminal s :: rem -> - let AnyTyRule rem = ty_rule_of_gram rem in - let tok = Atoken (CLexer.terminal s) in - let r = TyNext (rem, tok, None) in - AnyTyRule r -| GramNonTerminal (_, (t, tok)) :: rem -> - let AnyTyRule rem = ty_rule_of_gram rem in - let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in - let r = TyNext (rem, tok, inj) in - AnyTyRule r - -let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function -| TyStop -> Extend.Stop -| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok) - -type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r - -let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = function -| TyStop -> fun f loc -> f loc [] -| TyNext (rem, tok, None) -> fun f _ -> ty_eval rem f -| TyNext (rem, tok, Some inj) -> fun f x -> - let f loc args = f loc (inj x :: args) in - ty_eval rem f - -let make_rule f prod = - let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in - let symb = ty_erase ty_rule in - let f loc l = f loc (List.rev l) in - let act = ty_eval ty_rule f in - Extend.Rule (symb, act) - -(** Vernac grammar extensions *) - -let vernac_exts = ref [] - -let get_extend_vernac_rule (s, i) = - try - let find ((name, j), _) = String.equal name s && Int.equal i j in - let (_, rules) = List.find find !vernac_exts in - rules - with - | Failure _ -> raise Not_found - -let extend_vernac_command_grammar s nt gl = - let nt = Option.default Vernac_.command nt in - vernac_exts := (s,gl) :: !vernac_exts; - let mkact loc l = VernacExtend (s, l) in - let rules = [make_rule mkact gl] in - grammar_extend nt None (None, [None, None, rules]) diff --git a/parsing/egramml.mli b/parsing/egramml.mli deleted file mode 100644 index 31aa1a98..00000000 --- a/parsing/egramml.mli +++ /dev/null @@ -1,33 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 's grammar_prod_item - -val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> - vernac_expr grammar_prod_item list -> unit - -val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list - -(** Utility function reused in Egramcoq : *) - -val make_rule : - (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> - 'a grammar_prod_item list -> 'a Extend.production_rule diff --git a/parsing/extend.ml b/parsing/extend.ml new file mode 100644 index 00000000..6fe29566 --- /dev/null +++ b/parsing/extend.ml @@ -0,0 +1,126 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* ('a list,'b list,'c list) ty_user_symbol +| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol +| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol +| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol + +(** {5 Type-safe grammar extension} *) + +type ('self, 'a) symbol = +| Atoken : Tok.t -> ('self, string) symbol +| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol +| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol +| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol +| Aself : ('self, 'self) symbol +| Anext : ('self, 'self) symbol +| Aentry : 'a entry -> ('self, 'a) symbol +| Aentryl : 'a entry * string -> ('self, 'a) symbol +| Arules : 'a rules list -> ('self, 'a) symbol + +and ('self, _, 'r) rule = +| Stop : ('self, 'r, 'r) rule +| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + +and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } + +and 'a rules = +| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules + +type 'a production_rule = +| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + +type 'a single_extend_statement = + string option * + (** Level *) + gram_assoc option * + (** Associativity *) + 'a production_rule list + (** Symbol list with the interpretation function *) + +type 'a extend_statement = + gram_position option * + 'a single_extend_statement list diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 deleted file mode 100644 index 59b74545..00000000 --- a/parsing/g_constr.ml4 +++ /dev/null @@ -1,519 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* c - | (c,(_,Some ty)) -> - let loc = Loc.merge_opt (constr_loc c) (constr_loc ty) - in CAst.make ?loc @@ CCast(c, CastConv ty) - -let binder_of_name expl { CAst.loc = loc; v = na } = - CLocalAssum ([CAst.make ?loc na], Default expl, - CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) - -let binders_of_names l = - List.map (binder_of_name Explicit) l - -let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = - let ty = match tyc with - Some ty -> ty - | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in - (id,ann,bl,ty,body) - -let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = - let _ = Option.map (fun { CAst.loc = aloc } -> - CErrors.user_err ?loc:aloc - ~hdr:"Constr:mk_cofixb" - (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in - let ty = match tyc with - Some ty -> ty - | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in - (id,bl,ty,body) - -let mk_fix(loc,kw,id,dcls) = - if kw then - let fb : fix_expr list = List.map mk_fixb dcls in - CAst.make ~loc @@ CFix(id,fb) - else - let fb : cofix_expr list = List.map mk_cofixb dcls in - CAst.make ~loc @@ CCoFix(id,fb) - -let mk_single_fix (loc,kw,dcl) = - let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) - -let err () = raise Stream.Failure - -(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) -(* admissible notation "(x t)" *) -let lpar_id_coloneq = - Gram.Entry.of_parser "test_lpar_id_coloneq" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT s -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> - stream_njunk 3 strm; - Names.Id.of_string s - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) - -let impl_ident_head = - Gram.Entry.of_parser "impl_ident_head" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "{" -> - (match stream_nth 1 strm with - | IDENT ("wf"|"struct"|"measure") -> err () - | IDENT s -> - stream_njunk 2 strm; - Names.Id.of_string s - | _ -> err ()) - | _ -> err ()) - -let name_colon = - Gram.Entry.of_parser "name_colon" - (fun strm -> - match stream_nth 0 strm with - | IDENT s -> - (match stream_nth 1 strm with - | KEYWORD ":" -> - stream_njunk 2 strm; - Name (Names.Id.of_string s) - | _ -> err ()) - | KEYWORD "_" -> - (match stream_nth 1 strm with - | KEYWORD ":" -> - stream_njunk 2 strm; - Anonymous - | _ -> err ()) - | _ -> err ()) - -let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None - -GEXTEND Gram - GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family - global constr_pattern lconstr_pattern Constr.ident - closed_binder open_binders binder binders binders_fixannot - record_declaration typeclass_constraint pattern appl_arg; - Constr.ident: - [ [ id = Prim.ident -> id ] ] - ; - Prim.name: - [ [ "_" -> CAst.make ~loc:!@loc Anonymous ] ] - ; - global: - [ [ r = Prim.reference -> r ] ] - ; - constr_pattern: - [ [ c = constr -> c ] ] - ; - lconstr_pattern: - [ [ c = lconstr -> c ] ] - ; - sort: - [ [ "Set" -> GSet - | "Prop" -> GProp - | "Type" -> GType [] - | "Type"; "@{"; u = universe; "}" -> GType u - ] ] - ; - sort_family: - [ [ "Set" -> Sorts.InSet - | "Prop" -> Sorts.InProp - | "Type" -> Sorts.InType - ] ] - ; - universe_expr: - [ [ id = global; "+"; n = natural -> Some (id,n) - | id = global -> Some (id,0) - | "_" -> None - ] ] - ; - universe: - [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids - | u = universe_expr -> [u] - ] ] - ; - lconstr: - [ [ c = operconstr LEVEL "200" -> c ] ] - ; - constr: - [ [ c = operconstr LEVEL "8" -> c - | "@"; f=global; i = instance -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ] - ; - operconstr: - [ "200" RIGHTA - [ c = binder_constr -> c ] - | "100" RIGHTA - [ c1 = operconstr; "<:"; c2 = binder_constr -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) - | c1 = operconstr; "<:"; c2 = SELF -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2) - | c1 = operconstr; "<<:"; c2 = binder_constr -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) - | c1 = operconstr; "<<:"; c2 = SELF -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2) - | c1 = operconstr; ":";c2 = binder_constr -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) - | c1 = operconstr; ":"; c2 = SELF -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2) - | c1 = operconstr; ":>" -> - CAst.make ~loc:(!@loc) @@ CCast(c1, CastCoerce) ] - | "99" RIGHTA [ ] - | "90" RIGHTA [ ] - | "10" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args) - | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) - | "@"; lid = pattern_identref; args=LIST1 identref -> - let { CAst.loc = locid; v = id } = lid in - let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in - CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] - | "9" - [ ".."; c = operconstr LEVEL "0"; ".." -> - CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ] - | "8" [ ] - | "1" LEFTA - [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> - CAst.make ~loc:(!@loc) @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) - | c=operconstr; ".("; "@"; f=global; - args=LIST0 (operconstr LEVEL "9"); ")" -> - CAst.make ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) - | c=operconstr; "%"; key=IDENT -> CAst.make ~loc:(!@loc) @@ CDelimiters (key,c) ] - | "0" - [ c=atomic_constr -> c - | c=match_constr -> c - | "("; c = operconstr LEVEL "200"; ")" -> - (match c.CAst.v with - | CPrim (Numeral (n,true)) -> - CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[])) - | _ -> c) - | "{|"; c = record_declaration; "|}" -> c - | "{"; c = binder_constr ; "}" -> - CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[])) - | "`{"; c = operconstr LEVEL "200"; "}" -> - CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c) - | "`("; c = operconstr LEVEL "200"; ")" -> - CAst.make ~loc:(!@loc) @@ CGeneralization (Explicit, None, c) - ] ] - ; - record_declaration: - [ [ fs = record_fields -> CAst.make ~loc:(!@loc) @@ CRecord fs ] ] - ; - - record_fields: - [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs - | f = record_field_declaration -> [f] - | -> [] - ] ] - ; - - record_field_declaration: - [ [ id = global; bl = binders; ":="; c = lconstr -> - (id, if bl = [] then c else mkCLambdaN ~loc:!@loc bl c) ] ] - ; - binder_constr: - [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> - mkCProdN ~loc:!@loc bl c - | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> - mkCLambdaN ~loc:!@loc bl c - | "let"; id=name; bl = binders; ty = type_cstr; ":="; - c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - let ty,c1 = match ty, c1 with - | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) - | _, _ -> ty, c1 in - CAst.make ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, - Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) - | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> - let fixp = mk_single_fix fx in - let { CAst.loc = li; v = id } = match fixp.CAst.v with - CFix(id,_) -> id - | CCoFix(id,_) -> id - | _ -> assert false in - CAst.make ~loc:!@loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) - | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; - po = return_type; - ":="; c1 = operconstr LEVEL "200"; "in"; - c2 = operconstr LEVEL "200" -> - CAst.make ~loc:!@loc @@ CLetTuple (lb,po,c1,c2) - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; - "in"; c2 = operconstr LEVEL "200" -> - CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc:!@loc ([[p]], c2)]) - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; - rt = case_type; "in"; c2 = operconstr LEVEL "200" -> - CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc:!@loc ([[p]], c2)]) - - | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; - ":="; c1 = operconstr LEVEL "200"; rt = case_type; - "in"; c2 = operconstr LEVEL "200" -> - CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc:!@loc ([[p]], c2)]) - | "if"; c=operconstr LEVEL "200"; po = return_type; - "then"; b1=operconstr LEVEL "200"; - "else"; b2=operconstr LEVEL "200" -> - CAst.make ~loc:(!@loc) @@ CIf (c, po, b1, b2) - | c=fix_constr -> c ] ] - ; - appl_arg: - [ [ id = lpar_id_coloneq; c=lconstr; ")" -> - (c,Some (CAst.make ~loc:!@loc @@ ExplByName id)) - | c=operconstr LEVEL "9" -> (c,None) ] ] - ; - atomic_constr: - [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i) - | s=sort -> CAst.make ~loc:!@loc @@ CSort s - | n=INT -> CAst.make ~loc:!@loc @@ CPrim (Numeral (n,true)) - | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s) - | "_" -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) - | "?"; "["; id=ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroIdentifier id, None) - | "?"; "["; id=pattern_ident; "]" -> CAst.make ~loc:!@loc @@ CHole (None, IntroFresh id, None) - | id=pattern_ident; inst = evar_instance -> CAst.make ~loc:!@loc @@ CEvar(id,inst) ] ] - ; - inst: - [ [ id = ident; ":="; c = lconstr -> (id,c) ] ] - ; - evar_instance: - [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> l - | -> [] ] ] - ; - instance: - [ [ "@{"; l = LIST0 universe_level; "}" -> Some l - | -> None ] ] - ; - universe_level: - [ [ "Set" -> GSet - | "Prop" -> GProp - | "Type" -> GType UUnknown - | "_" -> GType UAnonymous - | id = global -> GType (UNamed id) - ] ] - ; - fix_constr: - [ [ fx1=single_fix -> mk_single_fix fx1 - | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; - "for"; id=identref -> - mk_fix(!@loc,kw,id,dcl1::dcls) - ] ] - ; - single_fix: - [ [ kw=fix_kw; dcl=fix_decl -> (!@loc,kw,dcl) ] ] - ; - fix_kw: - [ [ "fix" -> true - | "cofix" -> false ] ] - ; - fix_decl: - [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; - c=operconstr LEVEL "200" -> - (id,fst bl,snd bl,c,ty) ] ] - ; - match_constr: - [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; - br=branches; "end" -> CAst.make ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ] - ; - case_item: - [ [ c=operconstr LEVEL "100"; - ona = OPT ["as"; id=name -> id]; - ty = OPT ["in"; t=pattern -> t] -> - (c,ona,ty) ] ] - ; - case_type: - [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ] - ; - return_type: - [ [ a = OPT [ na = OPT["as"; na=name -> na]; - ty = case_type -> (na,ty) ] -> - match a with - | None -> None, None - | Some (na,t) -> (na, Some t) - ] ] - ; - branches: - [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] - ; - mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ] - ; - eqn: - [ [ pll = LIST1 mult_pattern SEP "|"; - "=>"; rhs = lconstr -> (CAst.make ~loc:!@loc (pll,rhs)) ] ] - ; - record_pattern: - [ [ id = global; ":="; pat = pattern -> (id, pat) ] ] - ; - record_patterns: - [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps - | p = record_pattern; ";" -> [p] - | p = record_pattern-> [p] - | -> [] - ] ] - ; - pattern: - [ "200" RIGHTA [ ] - | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] - | "99" RIGHTA [ ] - | "90" RIGHTA [ ] - | "10" LEFTA - [ p = pattern; "as"; na = name -> - CAst.make ~loc:!@loc @@ CPatAlias (p, na) - | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp - | "@"; r = Prim.reference; lp = LIST0 NEXT -> - CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] - | "1" LEFTA - [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ] - | "0" - [ r = Prim.reference -> CAst.make ~loc:!@loc @@ CPatAtom (Some r) - | "{|"; pat = record_patterns; "|}" -> CAst.make ~loc:!@loc @@ CPatRecord pat - | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None - | "("; p = pattern LEVEL "200"; ")" -> - (match p.CAst.v with - | CPatPrim (Numeral (n,true)) -> - CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) - | _ -> p) - | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> - let p = - match p with - | { CAst.v = CPatPrim (Numeral (n,true)) } -> - CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[]) - | _ -> p - in - CAst.make ~loc:!@loc @@ CPatCast (p, ty) - | n = INT -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (n,true)) - | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ] - ; - impl_ident_tail: - [ [ "}" -> binder_of_name Implicit - | nal=LIST1 name; ":"; c=lconstr; "}" -> - (fun na -> CLocalAssum (na::nal,Default Implicit,c)) - | nal=LIST1 name; "}" -> - (fun na -> CLocalAssum (na::nal,Default Implicit, - CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some !@loc)) @@ - CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))) - | ":"; c=lconstr; "}" -> - (fun na -> CLocalAssum ([na],Default Implicit,c)) - ] ] - ; - fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec) - | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel) - | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> (id, CMeasureRec (m,rel)) - ] ] - ; - impl_name_head: - [ [ id = impl_ident_head -> (CAst.make ~loc:!@loc @@ Name id) ] ] - ; - binders_fixannot: - [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> - (assum na :: fst bl), snd bl - | f = fixannot -> [], f - | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl - | -> [], (None, CStructRec) - ] ] - ; - open_binders: - (* Same as binders but parentheses around a closed binder are optional if - the latter is unique *) - [ [ (* open binder *) - id = name; idl = LIST0 name; ":"; c = lconstr -> - [CLocalAssum (id::idl,Default Explicit,c)] - (* binders factorized with open binder *) - | id = name; idl = LIST0 name; bl = binders -> - binders_of_names (id::idl) @ bl - | id1 = name; ".."; id2 = name -> - [CLocalAssum ([id1;(CAst.make ~loc:!@loc (Name ldots_var));id2], - Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] - | bl = closed_binder; bl' = binders -> - bl@bl' - ] ] - ; - binders: - [ [ l = LIST0 binder -> List.flatten l ] ] - ; - binder: - [ [ id = name -> [CLocalAssum ([id],Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] - | bl = closed_binder -> bl ] ] - ; - closed_binder: - [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - [CLocalAssum (id::idl,Default Explicit,c)] - | "("; id=name; ":"; c=lconstr; ")" -> - [CLocalAssum ([id],Default Explicit,c)] - | "("; id=name; ":="; c=lconstr; ")" -> - (match c.CAst.v with - | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)] - | _ -> [CLocalDef (id,c,None)]) - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [CLocalDef (id,c,Some t)] - | "{"; id=name; "}" -> - [CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] - | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - [CLocalAssum (id::idl,Default Implicit,c)] - | "{"; id=name; ":"; c=lconstr; "}" -> - [CLocalAssum ([id],Default Implicit,c)] - | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl) - | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc - | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc - | "'"; p = pattern LEVEL "0" -> - let (p, ty) = - match p.CAst.v with - | CPatCast (p, ty) -> (p, Some ty) - | _ -> (p, None) - in - [CLocalPattern (CAst.make ~loc:!@loc (p, ty))] - ] ] - ; - typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (CAst.make ~loc:!@loc Anonymous), true, c - | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> - id, expl, c - | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> - (CAst.make ~loc:!@loc iid), expl, c - | c = operconstr LEVEL "200" -> - (CAst.make ~loc:!@loc Anonymous), false, c - ] ] - ; - - type_cstr: - [ [ c=OPT [":"; c=lconstr -> c] -> Loc.tag ~loc:!@loc c ] ] - ; - END;; diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg new file mode 100644 index 00000000..7cb5af78 --- /dev/null +++ b/parsing/g_constr.mlg @@ -0,0 +1,526 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* c + | (c,(_,Some ty)) -> + let loc = Loc.merge_opt (constr_loc c) (constr_loc ty) + in CAst.make ?loc @@ CCast(c, CastConv ty) + +let binder_of_name expl { CAst.loc = loc; v = na } = + CLocalAssum ([CAst.make ?loc na], Default expl, + CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) + +let binders_of_names l = + List.map (binder_of_name Explicit) l + +let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = + let ty = match tyc with + Some ty -> ty + | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in + (id,ann,bl,ty,body) + +let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = + let _ = Option.map (fun { CAst.loc = aloc } -> + CErrors.user_err ?loc:aloc + ~hdr:"Constr:mk_cofixb" + (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in + let ty = match tyc with + Some ty -> ty + | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in + (id,bl,ty,body) + +let mk_fix(loc,kw,id,dcls) = + if kw then + let fb : fix_expr list = List.map mk_fixb dcls in + CAst.make ~loc @@ CFix(id,fb) + else + let fb : cofix_expr list = List.map mk_cofixb dcls in + CAst.make ~loc @@ CCoFix(id,fb) + +let mk_single_fix (loc,kw,dcl) = + let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl]) + +let err () = raise Stream.Failure + +(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) +(* admissible notation "(x t)" *) +let lpar_id_coloneq = + Gram.Entry.of_parser "test_lpar_id_coloneq" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "(" -> + (match stream_nth 1 strm with + | IDENT s -> + (match stream_nth 2 strm with + | KEYWORD ":=" -> + stream_njunk 3 strm; + Names.Id.of_string s + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let impl_ident_head = + Gram.Entry.of_parser "impl_ident_head" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "{" -> + (match stream_nth 1 strm with + | IDENT ("wf"|"struct"|"measure") -> err () + | IDENT s -> + stream_njunk 2 strm; + Names.Id.of_string s + | _ -> err ()) + | _ -> err ()) + +let name_colon = + Gram.Entry.of_parser "name_colon" + (fun strm -> + match stream_nth 0 strm with + | IDENT s -> + (match stream_nth 1 strm with + | KEYWORD ":" -> + stream_njunk 2 strm; + Name (Names.Id.of_string s) + | _ -> err ()) + | KEYWORD "_" -> + (match stream_nth 1 strm with + | KEYWORD ":" -> + stream_njunk 2 strm; + Anonymous + | _ -> err ()) + | _ -> err ()) + +let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None + +} + +GRAMMAR EXTEND Gram + GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family + global constr_pattern lconstr_pattern Constr.ident + closed_binder open_binders binder binders binders_fixannot + record_declaration typeclass_constraint pattern appl_arg; + Constr.ident: + [ [ id = Prim.ident -> { id } ] ] + ; + Prim.name: + [ [ "_" -> { CAst.make ~loc Anonymous } ] ] + ; + global: + [ [ r = Prim.reference -> { r } ] ] + ; + constr_pattern: + [ [ c = constr -> { c } ] ] + ; + lconstr_pattern: + [ [ c = lconstr -> { c } ] ] + ; + sort: + [ [ "Set" -> { GSet } + | "Prop" -> { GProp } + | "Type" -> { GType [] } + | "Type"; "@{"; u = universe; "}" -> { GType u } + ] ] + ; + sort_family: + [ [ "Set" -> { Sorts.InSet } + | "Prop" -> { Sorts.InProp } + | "Type" -> { Sorts.InType } + ] ] + ; + universe_expr: + [ [ id = global; "+"; n = natural -> { Some (id,n) } + | id = global -> { Some (id,0) } + | "_" -> { None } + ] ] + ; + universe: + [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids } + | u = universe_expr -> { [u] } + ] ] + ; + lconstr: + [ [ c = operconstr LEVEL "200" -> { c } ] ] + ; + constr: + [ [ c = operconstr LEVEL "8" -> { c } + | "@"; f=global; i = instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ] + ; + operconstr: + [ "200" RIGHTA + [ c = binder_constr -> { c } ] + | "100" RIGHTA + [ c1 = operconstr; "<:"; c2 = binder_constr -> + { CAst.make ~loc @@ CCast(c1, CastVM c2) } + | c1 = operconstr; "<:"; c2 = SELF -> + { CAst.make ~loc @@ CCast(c1, CastVM c2) } + | c1 = operconstr; "<<:"; c2 = binder_constr -> + { CAst.make ~loc @@ CCast(c1, CastNative c2) } + | c1 = operconstr; "<<:"; c2 = SELF -> + { CAst.make ~loc @@ CCast(c1, CastNative c2) } + | c1 = operconstr; ":";c2 = binder_constr -> + { CAst.make ~loc @@ CCast(c1, CastConv c2) } + | c1 = operconstr; ":"; c2 = SELF -> + { CAst.make ~loc @@ CCast(c1, CastConv c2) } + | c1 = operconstr; ":>" -> + { CAst.make ~loc @@ CCast(c1, CastCoerce) } ] + | "99" RIGHTA [ ] + | "90" RIGHTA [ ] + | "10" LEFTA + [ f=operconstr; args=LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) } + | "@"; f=global; i = instance; args=LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) } + | "@"; lid = pattern_identref; args=LIST1 identref -> + { let { CAst.loc = locid; v = id } = lid in + let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in + CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ] + | "9" + [ ".."; c = operconstr LEVEL "0"; ".." -> + { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ] + | "8" [ ] + | "1" LEFTA + [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> + { CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) } + | c=operconstr; ".("; "@"; f=global; + args=LIST0 (operconstr LEVEL "9"); ")" -> + { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) } + | c=operconstr; "%"; key=IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ] + | "0" + [ c=atomic_constr -> { c } + | c=match_constr -> { c } + | "("; c = operconstr LEVEL "200"; ")" -> + { (match c.CAst.v with + | CPrim (Numeral (n,true)) -> + CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) + | _ -> c) } + | "{|"; c = record_declaration; "|}" -> { c } + | "{"; c = binder_constr ; "}" -> + { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } + | "`{"; c = operconstr LEVEL "200"; "}" -> + { CAst.make ~loc @@ CGeneralization (Implicit, None, c) } + | "`("; c = operconstr LEVEL "200"; ")" -> + { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } + ] ] + ; + record_declaration: + [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ] + ; + + record_fields: + [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs } + | f = record_field_declaration -> { [f] } + | -> { [] } + ] ] + ; + + record_field_declaration: + [ [ id = global; bl = binders; ":="; c = lconstr -> + { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ] + ; + binder_constr: + [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> + { mkCProdN ~loc bl c } + | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> + { mkCLambdaN ~loc bl c } + | "let"; id=name; bl = binders; ty = type_cstr; ":="; + c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> + { let ty,c1 = match ty, c1 with + | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *) + | _, _ -> ty, c1 in + CAst.make ~loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1, + Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) } + | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> + { let fixp = mk_single_fix fx in + let { CAst.loc = li; v = id } = match fixp.CAst.v with + CFix(id,_) -> id + | CCoFix(id,_) -> id + | _ -> assert false in + CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) } + | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ]; + po = return_type; + ":="; c1 = operconstr LEVEL "200"; "in"; + c2 = operconstr LEVEL "200" -> + { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } + | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + "in"; c2 = operconstr LEVEL "200" -> + { CAst.make ~loc @@ + CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) } + | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + rt = case_type; "in"; c2 = operconstr LEVEL "200" -> + { CAst.make ~loc @@ + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) } + + | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; + ":="; c1 = operconstr LEVEL "200"; rt = case_type; + "in"; c2 = operconstr LEVEL "200" -> + { CAst.make ~loc @@ + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) } + | "if"; c=operconstr LEVEL "200"; po = return_type; + "then"; b1=operconstr LEVEL "200"; + "else"; b2=operconstr LEVEL "200" -> + { CAst.make ~loc @@ CIf (c, po, b1, b2) } + | c=fix_constr -> { c } ] ] + ; + appl_arg: + [ [ id = lpar_id_coloneq; c=lconstr; ")" -> + { (c,Some (CAst.make ~loc @@ ExplByName id)) } + | c=operconstr LEVEL "9" -> { (c,None) } ] ] + ; + atomic_constr: + [ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) } + | s=sort -> { CAst.make ~loc @@ CSort s } + | n=INT -> { CAst.make ~loc @@ CPrim (Numeral (n,true)) } + | s=string -> { CAst.make ~loc @@ CPrim (String s) } + | "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } + | "?"; "["; id=ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) } + | "?"; "["; id=pattern_ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroFresh id, None) } + | id=pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ] + ; + inst: + [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ] + ; + evar_instance: + [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l } + | -> { [] } ] ] + ; + instance: + [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l } + | -> { None } ] ] + ; + universe_level: + [ [ "Set" -> { GSet } + | "Prop" -> { GProp } + | "Type" -> { GType UUnknown } + | "_" -> { GType UAnonymous } + | id = global -> { GType (UNamed id) } + ] ] + ; + fix_constr: + [ [ fx1=single_fix -> { mk_single_fix fx1 } + | f=single_fix; "with"; dcls=LIST1 fix_decl SEP "with"; + "for"; id=identref -> + { let (_,kw,dcl1) = f in + mk_fix(loc,kw,id,dcl1::dcls) } + ] ] + ; + single_fix: + [ [ kw=fix_kw; dcl=fix_decl -> { (loc,kw,dcl) } ] ] + ; + fix_kw: + [ [ "fix" -> { true } + | "cofix" -> { false } ] ] + ; + fix_decl: + [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":="; + c=operconstr LEVEL "200" -> + { (id,fst bl,snd bl,c,ty) } ] ] + ; + match_constr: + [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; + br=branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ] + ; + case_item: + [ [ c=operconstr LEVEL "100"; + ona = OPT ["as"; id=name -> { id } ]; + ty = OPT ["in"; t=pattern -> { t } ] -> + { (c,ona,ty) } ] ] + ; + case_type: + [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ] + ; + return_type: + [ [ a = OPT [ na = OPT["as"; na=name -> { na } ]; + ty = case_type -> { (na,ty) } ] -> + { match a with + | None -> None, None + | Some (na,t) -> (na, Some t) } + ] ] + ; + branches: + [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ] + ; + mult_pattern: + [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ] + ; + eqn: + [ [ pll = LIST1 mult_pattern SEP "|"; + "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ] + ; + record_pattern: + [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ] + ; + record_patterns: + [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps } + | p = record_pattern; ";" -> { [p] } + | p = record_pattern-> { [p] } + | -> { [] } + ] ] + ; + pattern: + [ "200" RIGHTA [ ] + | "100" RIGHTA + [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ] + | "99" RIGHTA [ ] + | "90" RIGHTA [ ] + | "10" LEFTA + [ p = pattern; "as"; na = name -> + { CAst.make ~loc @@ CPatAlias (p, na) } + | p = pattern; lp = LIST1 NEXT -> { mkAppPattern ~loc p lp } + | "@"; r = Prim.reference; lp = LIST0 NEXT -> + { CAst.make ~loc @@ CPatCstr (r, Some lp, []) } ] + | "1" LEFTA + [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ] + | "0" + [ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) } + | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat } + | "_" -> { CAst.make ~loc @@ CPatAtom None } + | "("; p = pattern LEVEL "200"; ")" -> + { (match p.CAst.v with + | CPatPrim (Numeral (n,true)) -> + CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + | _ -> p) } + | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> + { let p = + match p with + | { CAst.v = CPatPrim (Numeral (n,true)) } -> + CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) + | _ -> p + in + CAst.make ~loc @@ CPatCast (p, ty) } + | n = INT -> { CAst.make ~loc @@ CPatPrim (Numeral (n,true)) } + | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] + ; + impl_ident_tail: + [ [ "}" -> { binder_of_name Implicit } + | nal=LIST1 name; ":"; c=lconstr; "}" -> + { (fun na -> CLocalAssum (na::nal,Default Implicit,c)) } + | nal=LIST1 name; "}" -> + { (fun na -> CLocalAssum (na::nal,Default Implicit, + CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some loc)) @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))) } + | ":"; c=lconstr; "}" -> + { (fun na -> CLocalAssum ([na],Default Implicit,c)) } + ] ] + ; + fixannot: + [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) } + | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) } + | "{"; IDENT "measure"; m=constr; id=OPT identref; + rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) } + ] ] + ; + impl_name_head: + [ [ id = impl_ident_head -> { CAst.make ~loc @@ Name id } ] ] + ; + binders_fixannot: + [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> + { (assum na :: fst bl), snd bl } + | f = fixannot -> { [], f } + | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } + | -> { [], (None, CStructRec) } + ] ] + ; + open_binders: + (* Same as binders but parentheses around a closed binder are optional if + the latter is unique *) + [ [ + id = name; idl = LIST0 name; ":"; c = lconstr -> + { [CLocalAssum (id::idl,Default Explicit,c)] + (* binders factorized with open binder *) } + | id = name; idl = LIST0 name; bl = binders -> + { binders_of_names (id::idl) @ bl } + | id1 = name; ".."; id2 = name -> + { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2], + Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | bl = closed_binder; bl' = binders -> + { bl@bl' } + ] ] + ; + binders: + [ [ l = LIST0 binder -> { List.flatten l } ] ] + ; + binder: + [ [ id = name -> { [CLocalAssum ([id],Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | bl = closed_binder -> { bl } ] ] + ; + closed_binder: + [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> + { [CLocalAssum (id::idl,Default Explicit,c)] } + | "("; id=name; ":"; c=lconstr; ")" -> + { [CLocalAssum ([id],Default Explicit,c)] } + | "("; id=name; ":="; c=lconstr; ")" -> + { (match c.CAst.v with + | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)] + | _ -> [CLocalDef (id,c,None)]) } + | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> + { [CLocalDef (id,c,Some t)] } + | "{"; id=name; "}" -> + { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] } + | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> + { [CLocalAssum (id::idl,Default Implicit,c)] } + | "{"; id=name; ":"; c=lconstr; "}" -> + { [CLocalAssum ([id],Default Implicit,c)] } + | "{"; id=name; idl=LIST1 name; "}" -> + { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } + | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc } + | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc } + | "'"; p = pattern LEVEL "0" -> + { let (p, ty) = + match p.CAst.v with + | CPatCast (p, ty) -> (p, Some ty) + | _ -> (p, None) + in + [CLocalPattern (CAst.make ~loc (p, ty))] } + ] ] + ; + typeclass_constraint: + [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~loc Anonymous), true, c } + | "{"; id = name; "}"; ":" ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> + { id, expl, c } + | iid=name_colon ; expl = [ "!" -> { true } | -> { false } ] ; c = operconstr LEVEL "200" -> + { (CAst.make ~loc iid), expl, c } + | c = operconstr LEVEL "200" -> + { (CAst.make ~loc Anonymous), false, c } + ] ] + ; + + type_cstr: + [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ] + ; + END diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 deleted file mode 100644 index b25ea766..00000000 --- a/parsing/g_prim.ml4 +++ /dev/null @@ -1,122 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* 1024 * 2048 then raise Exit; - n - with Failure _ | Exit -> - CErrors.user_err ~loc (Pp.str "Cannot support a so large number.") - -GEXTEND Gram - GLOBAL: - bigint natural integer identref name ident var preident - fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation smart_global; - preident: - [ [ s = IDENT -> s ] ] - ; - ident: - [ [ s = IDENT -> Id.of_string s ] ] - ; - pattern_ident: - [ [ LEFTQMARK; id = ident -> id ] ] - ; - pattern_identref: - [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ] - ; - var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> CAst.make ~loc:!@loc id ] ] - ; - identref: - [ [ id = ident -> CAst.make ~loc:!@loc id ] ] - ; - field: - [ [ s = FIELD -> Id.of_string s ] ] - ; - fields: - [ [ id = field; (l,id') = fields -> (l@[id],id') - | id = field -> ([],id) - ] ] - ; - fullyqualid: - [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l) - | id = ident -> CAst.make ~loc:!@loc [id] - ] ] - ; - basequalid: - [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> qualid_of_ident id - ] ] - ; - name: - [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous - | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ] - ; - reference: - [ [ id = ident; (l,id') = fields -> - CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') - | id = ident -> CAst.make ~loc:!@loc @@ Ident id - ] ] - ; - by_notation: - [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ] - ; - smart_global: - [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c - | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ] - ; - qualid: - [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] - ; - ne_string: - [ [ s = STRING -> - if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s - ] ] - ; - ne_lstring: - [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ] - ; - dirpath: - [ [ id = ident; l = LIST0 field -> - DirPath.make (List.rev (id::l)) ] ] - ; - string: - [ [ s = STRING -> s ] ] - ; - lstring: - [ [ s = string -> (CAst.make ~loc:!@loc s) ] ] - ; - integer: - [ [ i = INT -> my_int_of_string (!@loc) i - | "-"; i = INT -> - my_int_of_string (!@loc) i ] ] - ; - natural: - [ [ i = INT -> my_int_of_string (!@loc) i ] ] - ; - bigint: (* Negative numbers are dealt with elsewhere *) - [ [ i = INT -> i ] ] - ; -END diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg new file mode 100644 index 00000000..dfb78890 --- /dev/null +++ b/parsing/g_prim.mlg @@ -0,0 +1,123 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + CErrors.user_err ~loc (Pp.str "This number is too large.") + +} + +GRAMMAR EXTEND Gram + GLOBAL: + bigint natural integer identref name ident var preident + fullyqualid qualid reference dirpath ne_lstring + ne_string string lstring pattern_ident pattern_identref by_notation smart_global; + preident: + [ [ s = IDENT -> { s } ] ] + ; + ident: + [ [ s = IDENT -> { Id.of_string s } ] ] + ; + pattern_ident: + [ [ LEFTQMARK; id = ident -> { id } ] ] + ; + pattern_identref: + [ [ id = pattern_ident -> { CAst.make ~loc id } ] ] + ; + var: (* as identref, but interpret as a term identifier in ltac *) + [ [ id = ident -> { CAst.make ~loc id } ] ] + ; + identref: + [ [ id = ident -> { CAst.make ~loc id } ] ] + ; + field: + [ [ s = FIELD -> { Id.of_string s } ] ] + ; + fields: + [ [ id = field; f = fields -> { let (l,id') = f in (l@[id],id') } + | id = field -> { ([],id) } + ] ] + ; + fullyqualid: + [ [ id = ident; f=fields -> { let (l,id') = f in CAst.make ~loc @@ id::List.rev (id'::l) } + | id = ident -> { CAst.make ~loc [id] } + ] ] + ; + basequalid: + [ [ id = ident; f=fields -> { let (l,id') = f in local_make_qualid loc (l@[id]) id' } + | id = ident -> { qualid_of_ident ~loc id } + ] ] + ; + name: + [ [ IDENT "_" -> { CAst.make ~loc Anonymous } + | id = ident -> { CAst.make ~loc @@ Name id } ] ] + ; + reference: + [ [ id = ident; f = fields -> { + let (l,id') = f in + local_make_qualid loc (l@[id]) id' } + | id = ident -> { local_make_qualid loc [] id } + ] ] + ; + by_notation: + [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ] + ; + smart_global: + [ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c } + | ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ] + ; + qualid: + [ [ qid = basequalid -> { qid } ] ] + ; + ne_string: + [ [ s = STRING -> + { if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s } + ] ] + ; + ne_lstring: + [ [ s = ne_string -> { CAst.make ~loc s } ] ] + ; + dirpath: + [ [ id = ident; l = LIST0 field -> + { DirPath.make (List.rev (id::l)) } ] ] + ; + string: + [ [ s = STRING -> { s } ] ] + ; + lstring: + [ [ s = string -> { CAst.make ~loc s } ] ] + ; + integer: + [ [ i = INT -> { my_int_of_string loc i } + | "-"; i = INT -> { - my_int_of_string loc i } ] ] + ; + natural: + [ [ i = INT -> { my_int_of_string loc i } ] ] + ; + bigint: (* Negative numbers are dealt with elsewhere *) + [ [ i = INT -> { i } ] ] + ; +END diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 deleted file mode 100644 index e393c2bb..00000000 --- a/parsing/g_proofs.ml4 +++ /dev/null @@ -1,133 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - Pp.strbrk - "The Focus command is deprecated; use bullets or focusing brackets instead" - ) - -let warn_deprecated_focus_n n = - CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" - (fun () -> - Pp.(str "The Focus command is deprecated;" ++ spc () - ++ str "use '" ++ int n ++ str ": {' instead") - ) - -let warn_deprecated_unfocus = - CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" - (fun () -> Pp.strbrk "The Unfocus command is deprecated") - -(* Proof commands *) -GEXTEND Gram - GLOBAL: hint command; - - opt_hintbases: - [ [ -> [] - | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ] - ; - command: - [ [ IDENT "Goal"; c = lconstr -> - VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) - | IDENT "Proof" -> VernacProof (None,None) - | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn - | IDENT "Proof"; c = lconstr -> VernacExactProof c - | IDENT "Abort" -> VernacAbort None - | IDENT "Abort"; IDENT "All" -> VernacAbortAll - | IDENT "Abort"; id = identref -> VernacAbort (Some id) - | IDENT "Existential"; n = natural; c = constr_body -> - VernacSolveExistential (n,c) - | IDENT "Admitted" -> VernacEndProof Admitted - | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None)) - | IDENT "Save"; id = identref -> - VernacEndProof (Proved (Opaque, Some id)) - | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None)) - | IDENT "Defined"; id=identref -> - VernacEndProof (Proved (Transparent,Some id)) - | IDENT "Restart" -> VernacRestart - | IDENT "Undo" -> VernacUndo 1 - | IDENT "Undo"; n = natural -> VernacUndo n - | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n - | IDENT "Focus" -> - warn_deprecated_focus ~loc:!@loc (); - VernacFocus None - | IDENT "Focus"; n = natural -> - warn_deprecated_focus_n n ~loc:!@loc (); - VernacFocus (Some n) - | IDENT "Unfocus" -> - warn_deprecated_unfocus ~loc:!@loc (); - VernacUnfocus - | IDENT "Unfocused" -> VernacUnfocused - | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) - | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) - | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) - | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript - | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials - | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses - | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames - | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof - | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) - | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) - | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id) - | IDENT "Guarded" -> VernacCheckGuard - (* Hints for Auto and EAuto *) - | IDENT "Create"; IDENT "HintDb" ; - id = IDENT ; b = [ "discriminated" -> true | -> false ] -> - VernacCreateHintDb (id, b) - | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> - VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; h = hint; - dbnames = opt_hintbases -> - VernacHints (dbnames, h) - (* Declare "Resolve" explicitly so as to be able to later extend with - "Resolve ->" and "Resolve <-" *) - | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - info = hint_info; dbnames = opt_hintbases -> - VernacHints (dbnames, - HintsResolve (List.map (fun x -> (info, true, x)) lc)) - ] ]; - reference_or_constr: - [ [ r = global -> HintsReference r - | c = constr -> HintsConstr c ] ] - ; - hint: - [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> - HintsResolve (List.map (fun x -> (info, true, x)) lc) - | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc - | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) - | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) - | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m) - | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid - | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc ] ] - ; - constr_body: - [ [ ":="; c = lconstr -> c - | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ] - ; - mode: - [ [ l = LIST1 [ "+" -> ModeInput - | "!" -> ModeNoHeadEvar - | "-" -> ModeOutput ] -> l ] ] - ; -END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 deleted file mode 100644 index 61b1de82..00000000 --- a/parsing/g_vernac.ml4 +++ /dev/null @@ -1,1195 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* ->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw - -(* Rem: do not join the different GEXTEND into one, it breaks native *) -(* compilation on PowerPC and Sun architectures *) - -let query_command = Gram.entry_create "vernac:query_command" - -let subprf = Gram.entry_create "vernac:subprf" - -let class_rawexpr = Gram.entry_create "vernac:class_rawexpr" -let thm_token = Gram.entry_create "vernac:thm_token" -let def_body = Gram.entry_create "vernac:def_body" -let decl_notation = Gram.entry_create "vernac:decl_notation" -let record_field = Gram.entry_create "vernac:record_field" -let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" -let instance_name = Gram.entry_create "vernac:instance_name" -let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" - -let make_bullet s = - let n = String.length s in - match s.[0] with - | '-' -> Dash n - | '+' -> Plus n - | '*' -> Star n - | _ -> assert false - -let parse_compat_version ?(allow_old = true) = let open Flags in function - | "8.8" -> Current - | "8.7" -> V8_7 - | "8.6" -> V8_6 - | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> - CErrors.user_err ~hdr:"get_compat_version" - Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") - | s -> - CErrors.user_err ~hdr:"get_compat_version" - Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") - -GEXTEND Gram - GLOBAL: vernac_control gallina_ext noedit_mode subprf; - vernac_control: FIRST - [ [ IDENT "Time"; c = located_vernac -> VernacTime (false,c) - | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) - | IDENT "Timeout"; n = natural; v = vernac_control -> VernacTimeout(n,v) - | IDENT "Fail"; v = vernac_control -> VernacFail v - | (f, v) = vernac -> VernacExpr(f, v) ] - ] - ; - vernac: - [ [ IDENT "Local"; (f, v) = vernac_poly -> (VernacLocal true :: f, v) - | IDENT "Global"; (f, v) = vernac_poly -> (VernacLocal false :: f, v) - - | v = vernac_poly -> v ] - ] - ; - vernac_poly: - [ [ IDENT "Polymorphic"; (f, v) = vernac_aux -> (VernacPolymorphic true :: f, v) - | IDENT "Monomorphic"; (f, v) = vernac_aux -> (VernacPolymorphic false :: f, v) - | v = vernac_aux -> v ] - ] - ; - vernac_aux: - (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) - (* "." is still in the stream and discard_to_dot works correctly *) - [ [ IDENT "Program"; g = gallina; "." -> ([VernacProgram], g) - | IDENT "Program"; g = gallina_ext; "." -> ([VernacProgram], g) - | g = gallina; "." -> ([], g) - | g = gallina_ext; "." -> ([], g) - | c = command; "." -> ([], c) - | c = syntax; "." -> ([], c) - | c = subprf -> ([], c) - ] ] - ; - vernac_aux: LAST - [ [ prfcom = command_entry -> ([], prfcom) ] ] - ; - noedit_mode: - [ [ c = query_command -> c None] ] - ; - - subprf: - [ [ s = BULLET -> VernacBullet (make_bullet s) - | "{" -> VernacSubproof None - | "}" -> VernacEndSubproof - ] ] - ; - - located_vernac: - [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ] - ; -END - -let warn_plural_command = - CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled - (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) - -let test_plural_form loc kwd = function - | [(_,([_],_))] -> - warn_plural_command ~loc:!@loc kwd - | _ -> () - -let test_plural_form_types loc kwd = function - | [([_],_)] -> - warn_plural_command ~loc:!@loc kwd - | _ -> () - -let lname_of_lident : lident -> lname = - CAst.map (fun s -> Name s) - -let name_of_ident_decl : ident_decl -> name_decl = - on_fst lname_of_lident - -(* Gallina declarations *) -GEXTEND Gram - GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl univ_decl; - - gallina: - (* Definition, Theorem, Variable, Axiom, ... *) - [ [ thm = thm_token; id = ident_decl; bl = binders; ":"; c = lconstr; - l = LIST0 - [ "with"; id = ident_decl; bl = binders; ":"; c = lconstr -> - (id,(bl,c)) ] -> - VernacStartTheoremProof (thm, (id,(bl,c))::l) - | stre = assumption_token; nl = inline; bl = assum_list -> - VernacAssumption (stre, nl, bl) - | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> - test_plural_form loc kwd bl; - VernacAssumption (stre, nl, bl) - | d = def_token; id = ident_decl; b = def_body -> - VernacDefinition (d, name_of_ident_decl id, b) - | IDENT "Let"; id = identref; b = def_body -> - VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) - (* Gallina inductive declarations *) - | cum = cumulativity_token; priv = private_token; f = finite_token; - indl = LIST1 inductive_definition SEP "with" -> - let (k,f) = f in - let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - let cum = - match cum with - Some true -> LocalCumulativity - | Some false -> LocalNonCumulativity - | None -> - if Flags.is_polymorphic_inductive_cumulativity () then - GlobalCumulativity - else - GlobalNonCumulativity - in - VernacInductive (cum, priv,f,indl) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (NoDischarge, recs) - | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (DoDischarge, recs) - | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (NoDischarge, corecs) - | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (DoDischarge, corecs) - | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l - | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; - l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) - | IDENT "Register"; IDENT "Inline"; id = identref -> - VernacRegister(id, RegisterInline) - | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l - | IDENT "Universes"; l = LIST1 identref -> VernacUniverse l - | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l - ] ] - ; - - thm_token: - [ [ "Theorem" -> Theorem - | IDENT "Lemma" -> Lemma - | IDENT "Fact" -> Fact - | IDENT "Remark" -> Remark - | IDENT "Corollary" -> Corollary - | IDENT "Proposition" -> Proposition - | IDENT "Property" -> Property ] ] - ; - def_token: - [ [ "Definition" -> (NoDischarge,Definition) - | IDENT "Example" -> (NoDischarge,Example) - | IDENT "SubClass" -> (NoDischarge,SubClass) ] ] - ; - assumption_token: - [ [ "Hypothesis" -> (DoDischarge, Logical) - | "Variable" -> (DoDischarge, Definitional) - | "Axiom" -> (NoDischarge, Logical) - | "Parameter" -> (NoDischarge, Definitional) - | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ] - ; - assumptions_token: - [ [ IDENT "Hypotheses" -> ("Hypotheses", (DoDischarge, Logical)) - | IDENT "Variables" -> ("Variables", (DoDischarge, Definitional)) - | IDENT "Axioms" -> ("Axioms", (NoDischarge, Logical)) - | IDENT "Parameters" -> ("Parameters", (NoDischarge, Definitional)) - | IDENT "Conjectures" -> ("Conjectures", (NoDischarge, Conjectural)) ] ] - ; - inline: - [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) - | IDENT "Inline" -> DefaultInline - | -> NoInline] ] - ; - univ_constraint: - [ [ l = universe_level; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; - r = universe_level -> (l, ord, r) ] ] - ; - univ_decl : - [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> true | -> false ]; - cs = [ "|"; l' = LIST0 univ_constraint SEP ","; - ext = [ "+" -> true | -> false ]; "}" -> (l',ext) - | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ] - -> - { univdecl_instance = l; - univdecl_extensible_instance = ext; - univdecl_constraints = fst cs; - univdecl_extensible_constraints = snd cs } - ] ] - ; - ident_decl: - [ [ i = identref; l = OPT univ_decl -> (i, l) - ] ] - ; - finite_token: - [ [ IDENT "Inductive" -> (Inductive_kw,Finite) - | IDENT "CoInductive" -> (CoInductive,CoFinite) - | IDENT "Variant" -> (Variant,BiFinite) - | IDENT "Record" -> (Record,BiFinite) - | IDENT "Structure" -> (Structure,BiFinite) - | IDENT "Class" -> (Class true,BiFinite) ] ] - ; - cumulativity_token: - [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] - ; - private_token: - [ [ IDENT "Private" -> true | -> false ] ] - ; - (* Simple definitions *) - def_body: - [ [ bl = binders; ":="; red = reduce; c = lconstr -> - if List.exists (function CLocalPattern _ -> true | _ -> false) bl - then - (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = mkCLambdaN ~loc:!@loc bl c in - DefineBody ([], red, c, None) - else - (match c with - | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t) - | _ -> DefineBody (bl, red, c, None)) - | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> - let ((bl, c), tyo) = - if List.exists (function CLocalPattern _ -> true | _ -> false) bl - then - (* FIXME: "red" will be applied to types in bl and Cast with remain *) - let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in - (([],mkCLambdaN ~loc:!@loc bl c), None) - else ((bl, c), Some t) - in - DefineBody (bl, red, c, tyo) - | bl = binders; ":"; t = lconstr -> - ProveBody (bl, t) ] ] - ; - reduce: - [ [ IDENT "Eval"; r = red_expr; "in" -> Some r - | -> None ] ] - ; - one_decl_notation: - [ [ ntn = ne_lstring; ":="; c = constr; - scopt = OPT [ ":"; sc = IDENT -> sc] -> (ntn,c,scopt) ] ] - ; - decl_notation: - [ [ "where"; l = LIST1 one_decl_notation SEP IDENT "and" -> l - | -> [] ] ] - ; - (* Inductives and records *) - opt_constructors_or_fields: - [ [ ":="; lc = constructor_list_or_record_decl -> lc - | -> RecordDecl (None, []) ] ] - ; - inductive_definition: - [ [ oc = opt_coercion; id = ident_decl; indpar = binders; - c = OPT [ ":"; c = lconstr -> c ]; - lc=opt_constructors_or_fields; ntn = decl_notation -> - (((oc,id),indpar,c,lc),ntn) ] ] - ; - constructor_list_or_record_decl: - [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l - | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> - Constructors ((c id)::l) - | id = identref ; c = constructor_type -> Constructors [ c id ] - | cstr = identref; "{"; fs = record_fields; "}" -> - RecordDecl (Some cstr,fs) - | "{";fs = record_fields; "}" -> RecordDecl (None,fs) - | -> Constructors [] ] ] - ; -(* - csort: - [ [ s = sort -> CSort (loc,s) ] ] - ; -*) - opt_coercion: - [ [ ">" -> true - | -> false ] ] - ; - (* (co)-fixpoints *) - rec_definition: - [ [ id = ident_decl; - bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> - let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ] - ; - corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> def]; ntn = decl_notation -> - ((id,bl,ty,def),ntn) ] ] - ; - type_cstr: - [ [ ":"; c=lconstr -> c - | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ] - ; - (* Inductive schemes *) - scheme: - [ [ kind = scheme_kind -> (None,kind) - | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ] - ; - scheme_kind: - [ [ IDENT "Induction"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> InductionScheme(true,ind,s) - | IDENT "Minimality"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> InductionScheme(false,ind,s) - | IDENT "Elimination"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> CaseScheme(true,ind,s) - | IDENT "Case"; "for"; ind = smart_global; - IDENT "Sort"; s = sort_family-> CaseScheme(false,ind,s) - | IDENT "Equality"; "for" ; ind = smart_global -> EqualityScheme(ind) ] ] - ; - (* Various Binders *) -(* - (* ... without coercions *) - binder_nodef: - [ [ b = binder_let -> - (match b with - CLocalAssum(l,ty) -> (l,ty) - | CLocalDef _ -> - Util.user_err_loc - (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] - ; -*) - (* ... with coercions *) - record_field: - [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; - ntn = decl_notation -> (bd,pri),ntn ] ] - ; - record_fields: - [ [ f = record_field; ";"; fs = record_fields -> f :: fs - | f = record_field; ";" -> [f] - | f = record_field -> [f] - | -> [] - ] ] - ; - record_binder_body: - [ [ l = binders; oc = of_type_with_opt_coercion; - t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN ~loc:!@loc l t)) - | l = binders; oc = of_type_with_opt_coercion; - t = lconstr; ":="; b = lconstr -> fun id -> - (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t))) - | l = binders; ":="; b = lconstr -> fun id -> - match b.CAst.v with - | CCast(b', (CastConv t|CastVM t|CastNative t)) -> - (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t))) - | _ -> - (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ] - ; - record_binder: - [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None))) - | id = name; f = record_binder_body -> f id ] ] - ; - assum_list: - [ [ bl = LIST1 assum_coe -> bl | b = simple_assum_coe -> [b] ] ] - ; - assum_coe: - [ [ "("; a = simple_assum_coe; ")" -> a ] ] - ; - simple_assum_coe: - [ [ idl = LIST1 ident_decl; oc = of_type_with_opt_coercion; c = lconstr -> - (not (Option.is_empty oc),(idl,c)) ] ] - ; - - constructor_type: - [[ l = binders; - t= [ coe = of_type_with_opt_coercion; c = lconstr -> - fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c)) - | -> - fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ] - -> t l - ]] -; - - constructor: - [ [ id = identref; c=constructor_type -> c id ] ] - ; - of_type_with_opt_coercion: - [ [ ":>>" -> Some false - | ":>"; ">" -> Some false - | ":>" -> Some true - | ":"; ">"; ">" -> Some false - | ":"; ">" -> Some true - | ":" -> None ] ] - ; -END - -let only_starredidentrefs = - Gram.Entry.of_parser "test_only_starredidentrefs" - (fun strm -> - let rec aux n = - match Util.stream_nth n strm with - | KEYWORD "." -> () - | KEYWORD ")" -> () - | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1) - | _ -> raise Stream.Failure in - aux 0) -let starredidentreflist_to_expr l = - match l with - | [] -> SsEmpty - | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x - -let warn_deprecated_include_type = - CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" - (fun () -> strbrk "Include Type is deprecated; use Include instead") - -(* Modules and Sections *) -GEXTEND Gram - GLOBAL: gallina_ext module_expr module_type section_subset_expr; - - gallina_ext: - [ [ (* Interactive module declaration *) - IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; sign = of_module_type; - body = is_module_expr -> - VernacDefineModule (export, id, bl, sign, body) - | IDENT "Module"; "Type"; id = identref; - bl = LIST0 module_binder; sign = check_module_types; - body = is_module_type -> - VernacDeclareModuleType (id, bl, sign, body) - | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; ":"; mty = module_type_inl -> - VernacDeclareModule (export, id, bl, mty) - (* Section beginning *) - | IDENT "Section"; id = identref -> VernacBeginSection id - | IDENT "Chapter"; id = identref -> VernacBeginSection id - - (* This end a Section a Module or a Module Type *) - | IDENT "End"; id = identref -> VernacEndSegment id - - (* Naming a set of section hyps *) - | IDENT "Collection"; id = identref; ":="; expr = section_subset_expr -> - VernacNameSectionHypSet (id, expr) - - (* Requiring an already compiled module *) - | IDENT "Require"; export = export_token; qidl = LIST1 global -> - VernacRequire (None, export, qidl) - | IDENT "From" ; ns = global ; IDENT "Require"; export = export_token - ; qidl = LIST1 global -> - VernacRequire (Some ns, export, qidl) - | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) - | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> - VernacInclude(e::l) - | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - warn_deprecated_include_type ~loc:!@loc (); - VernacInclude(e::l) ] ] - ; - export_token: - [ [ IDENT "Import" -> Some false - | IDENT "Export" -> Some true - | -> None ] ] - ; - ext_module_type: - [ [ "<+"; mty = module_type_inl -> mty ] ] - ; - ext_module_expr: - [ [ "<+"; mexpr = module_expr_inl -> mexpr ] ] - ; - check_module_type: - [ [ "<:"; mty = module_type_inl -> mty ] ] - ; - check_module_types: - [ [ mtys = LIST0 check_module_type -> mtys ] ] - ; - of_module_type: - [ [ ":"; mty = module_type_inl -> Enforce mty - | mtys = check_module_types -> Check mtys ] ] - ; - is_module_type: - [ [ ":="; mty = module_type_inl ; l = LIST0 ext_module_type -> (mty::l) - | -> [] ] ] - ; - is_module_expr: - [ [ ":="; mexpr = module_expr_inl; l = LIST0 ext_module_expr -> (mexpr::l) - | -> [] ] ] - ; - functor_app_annot: - [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> - InlineAt (int_of_string i) - | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline - | -> DefaultInline - ] ] - ; - module_expr_inl: - [ [ "!"; me = module_expr -> (me,NoInline) - | me = module_expr; a = functor_app_annot -> (me,a) ] ] - ; - module_type_inl: - [ [ "!"; me = module_type -> (me,NoInline) - | me = module_type; a = functor_app_annot -> (me,a) ] ] - ; - (* Module binder *) - module_binder: - [ [ "("; export = export_token; idl = LIST1 identref; ":"; - mty = module_type_inl; ")" -> (export,idl,mty) ] ] - ; - (* Module expressions *) - module_expr: - [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (me1,me2) - ] ] - ; - module_expr_atom: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ] - ; - with_declaration: - [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> - CWith_Definition (fqid,udecl,c) - | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> - CWith_Module (fqid,qid) - ] ] - ; - module_type: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) - | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> - CAst.make ~loc:!@loc @@ CMapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> - CAst.make ~loc:!@loc @@ CMwith (mty,decl) - ] ] - ; - (* Proof using *) - section_subset_expr: - [ [ only_starredidentrefs; l = LIST0 starredidentref -> - starredidentreflist_to_expr l - | e = ssexpr -> e ]] - ; - starredidentref: - [ [ i = identref -> SsSingl i - | i = identref; "*" -> SsFwdClose(SsSingl i) - | "Type" -> SsType - | "Type"; "*" -> SsFwdClose SsType ]] - ; - ssexpr: - [ "35" - [ "-"; e = ssexpr -> SsCompl e ] - | "50" - [ e1 = ssexpr; "-"; e2 = ssexpr->SsSubstr(e1,e2) - | e1 = ssexpr; "+"; e2 = ssexpr->SsUnion(e1,e2)] - | "0" - [ i = starredidentref -> i - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"-> - starredidentreflist_to_expr l - | "("; only_starredidentrefs; l = LIST0 starredidentref; ")"; "*" -> - SsFwdClose(starredidentreflist_to_expr l) - | "("; e = ssexpr; ")"-> e - | "("; e = ssexpr; ")"; "*" -> SsFwdClose e ] ] - ; -END - -let warn_deprecated_arguments_scope = - CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" - (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") - -let warn_deprecated_implicit_arguments = - CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" - (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") - -(* Extensions: implicits, coercions, etc. *) -GEXTEND Gram - GLOBAL: gallina_ext instance_name hint_info; - - gallina_ext: - [ [ (* Transparent and Opaque *) - IDENT "Transparent"; l = LIST1 smart_global -> - VernacSetOpacity (Conv_oracle.transparent, l) - | IDENT "Opaque"; l = LIST1 smart_global -> - VernacSetOpacity (Conv_oracle.Opaque, l) - | IDENT "Strategy"; l = - LIST1 [ v=strategy_level; "["; q=LIST1 smart_global; "]" -> (v,q)] -> - VernacSetStrategy l - (* Canonical structure *) - | IDENT "Canonical"; IDENT "Structure"; qid = global -> - VernacCanonical CAst.(make ~loc:!@loc @@ AN qid) - | IDENT "Canonical"; IDENT "Structure"; ntn = by_notation -> - VernacCanonical CAst.(make ~loc:!@loc @@ ByNotation ntn) - | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> - let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) - - (* Coercions *) - | IDENT "Coercion"; qid = global; d = def_body -> - let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) - | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (f, s, t) - | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; - t = class_rawexpr -> - VernacCoercion (CAst.make ~loc:!@loc @@ AN qid, s, t) - | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; - t = class_rawexpr -> - VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t) - - | IDENT "Context"; c = LIST1 binder -> - VernacContext (List.flatten c) - - | IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - info = hint_info ; - props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | - ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) - - | IDENT "Existing"; IDENT "Instance"; id = global; - info = hint_info -> - VernacDeclareInstances [id, info] - - | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - let info = { hint_priority = pri; hint_pattern = None } in - let insts = List.map (fun i -> (i, info)) ids in - VernacDeclareInstances insts - - | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is - - (* Arguments *) - | IDENT "Arguments"; qid = smart_global; - args = LIST0 argument_spec_block; - more_implicits = OPT - [ ","; impl = LIST1 - [ impl = LIST0 more_implicits_block -> List.flatten impl] - SEP "," -> impl - ]; - mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] -> - let mods = match mods with None -> [] | Some l -> List.flatten l in - let slash_position = ref None in - let rec parse_args i = function - | [] -> [] - | `Id x :: args -> x :: parse_args (i+1) args - | `Slash :: args -> - if Option.is_empty !slash_position then - (slash_position := Some i; parse_args i args) - else - user_err Pp.(str "The \"/\" modifier can occur only once") - in - let args = parse_args 0 (List.flatten args) in - let more_implicits = Option.default [] more_implicits in - VernacArguments (qid, args, more_implicits, !slash_position, mods) - - - (* moved there so that camlp5 factors it with the previous rule *) - | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; - "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - warn_deprecated_arguments_scope ~loc:!@loc (); - VernacArgumentsScope (qid,scl) - - (* Implicit *) - | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; - pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> - List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - warn_deprecated_implicit_arguments ~loc:!@loc (); - VernacDeclareImplicits (qid,pos) - - | IDENT "Implicit"; "Type"; bl = reserv_list -> - VernacReserve bl - - | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plural_form_types loc "Implicit Types" bl; - VernacReserve bl - - | IDENT "Generalizable"; - gen = [IDENT "All"; IDENT "Variables" -> Some [] - | IDENT "No"; IDENT "Variables" -> None - | ["Variable" | IDENT "Variables"]; - idl = LIST1 identref -> Some idl ] -> - VernacGeneralizable gen ] ] - ; - arguments_modifier: - [ [ IDENT "simpl"; IDENT "nomatch" -> [`ReductionDontExposeCase] - | IDENT "simpl"; IDENT "never" -> [`ReductionNeverUnfold] - | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits] - | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits] - | IDENT "clear"; IDENT "scopes" -> [`ClearScopes] - | IDENT "rename" -> [`Rename] - | IDENT "assert" -> [`Assert] - | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes] - | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" -> - [`ClearImplicits; `ClearScopes] - | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" -> - [`ClearImplicits; `ClearScopes] - ] ] - ; - implicit_name: - [ [ "!"; id = ident -> (id, false, true) - | id = ident -> (id,false,false) - | "["; "!"; id = ident; "]" -> (id,true,true) - | "["; id = ident; "]" -> (id,true, false) ] ] - ; - scope: - [ [ "%"; key = IDENT -> key ] ] - ; - argument_spec: [ - [ b = OPT "!"; id = name ; s = OPT scope -> - id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@loc x) s - ] - ]; - (* List of arguments implicit status, scope, modifiers *) - argument_spec_block: [ - [ item = argument_spec -> - let name, recarg_like, notation_scope = item in - [`Id { name=name; recarg_like=recarg_like; - notation_scope=notation_scope; - implicit_status = NotImplicit}] - | "/" -> [`Slash] - | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x - | Some _, Some _ -> user_err Pp.(str "scope declared twice") in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = NotImplicit}) items - | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x - | Some _, Some _ -> user_err Pp.(str "scope declared twice") in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = Implicit}) items - | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> - let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x - | Some _, Some _ -> user_err Pp.(str "scope declared twice") in - List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; - notation_scope=f notation_scope; - implicit_status = MaximallyImplicit}) items - ] - ]; - (* Same as [argument_spec_block], but with only implicit status and names *) - more_implicits_block: [ - [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)] - | "["; items = LIST1 name; "]" -> - List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items - | "{"; items = LIST1 name; "}" -> - List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items - ] - ]; - strategy_level: - [ [ IDENT "expand" -> Conv_oracle.Expand - | IDENT "opaque" -> Conv_oracle.Opaque - | n=INT -> Conv_oracle.Level (int_of_string n) - | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) - | IDENT "transparent" -> Conv_oracle.transparent ] ] - ; - instance_name: - [ [ name = ident_decl; sup = OPT binders -> - (CAst.map (fun id -> Name id) (fst name), snd name), - (Option.default [] sup) - | -> ((CAst.make ~loc:!@loc Anonymous), None), [] ] ] - ; - hint_info: - [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> - { hint_priority = i; hint_pattern = pat } - | -> { hint_priority = None; hint_pattern = None } ] ] - ; - reserv_list: - [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] - ; - reserv_tuple: - [ [ "("; a = simple_reserv; ")" -> a ] ] - ; - simple_reserv: - [ [ idl = LIST1 identref; ":"; c = lconstr -> (idl,c) ] ] - ; - -END - -GEXTEND Gram - GLOBAL: command query_command class_rawexpr gallina_ext; - - gallina_ext: - [ [ IDENT "Export"; "Set"; table = option_table; v = option_value -> - VernacSetOption (true, table, v) - | IDENT "Export"; IDENT "Unset"; table = option_table -> - VernacUnsetOption (true, table) - ] ]; - - command: - [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l - - (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) - | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; - expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - info = hint_info -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) - - (* System directory *) - | IDENT "Pwd" -> VernacChdir None - | IDENT "Cd" -> VernacChdir None - | IDENT "Cd"; dir = ne_string -> VernacChdir (Some dir) - - (* Toplevel control *) - | IDENT "Drop" -> VernacToplevelControl Drop - | IDENT "Quit" -> VernacToplevelControl Quit - - | IDENT "Load"; verbosely = [ IDENT "Verbose" -> true | -> false ]; - s = [ s = ne_string -> s | s = IDENT -> s ] -> - VernacLoad (verbosely, s) - | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string -> - VernacDeclareMLModule l - - | IDENT "Locate"; l = locatable -> VernacLocate l - - (* Managing load paths *) - | IDENT "Add"; IDENT "LoadPath"; dir = ne_string; alias = as_dirpath -> - VernacAddLoadPath (false, dir, alias) - | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = ne_string; - alias = as_dirpath -> VernacAddLoadPath (true, dir, alias) - | IDENT "Remove"; IDENT "LoadPath"; dir = ne_string -> - VernacRemoveLoadPath dir - - (* For compatibility *) - | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath -> - VernacAddLoadPath (false, dir, alias) - | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath -> - VernacAddLoadPath (true, dir, alias) - | IDENT "DelPath"; dir = ne_string -> - VernacRemoveLoadPath dir - - (* Type-Checking (pas dans le refman) *) - | "Type"; c = lconstr -> VernacGlobalCheck c - - (* Printing (careful factorization of entries) *) - | IDENT "Print"; p = printable -> VernacPrint p - | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l)) - | IDENT "Print"; IDENT "Module"; "Type"; qid = global -> - VernacPrint (PrintModuleType qid) - | IDENT "Print"; IDENT "Module"; qid = global -> - VernacPrint (PrintModule qid) - | IDENT "Print"; IDENT "Namespace" ; ns = dirpath -> - VernacPrint (PrintNamespace ns) - | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n) - - | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - VernacAddMLPath (false, dir) - | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = ne_string -> - VernacAddMLPath (true, dir) - - (* For acting on parameter tables *) - | "Set"; table = option_table; v = option_value -> - VernacSetOption (false, table, v) - | IDENT "Unset"; table = option_table -> - VernacUnsetOption (false, table) - - | IDENT "Print"; IDENT "Table"; table = option_table -> - VernacPrintOption table - - | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value - -> VernacAddOption ([table;field], v) - (* A global value below will be hidden by a field above! *) - (* In fact, we give priority to secondary tables *) - (* No syntax for tertiary tables due to conflict *) - (* (but they are unused anyway) *) - | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> - VernacAddOption ([table], v) - - | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value - -> VernacMemOption (table, v) - | IDENT "Test"; table = option_table -> - VernacPrintOption table - - | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value - -> VernacRemoveOption ([table;field], v) - | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption ([table], v) ]] - ; - query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> - fun g -> VernacCheckMayEval (Some r, g, c) - | IDENT "Compute"; c = lconstr; "." -> - fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) - | IDENT "Check"; c = lconstr; "." -> - fun g -> VernacCheckMayEval (None, g, c) - (* Searching the environment *) - | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." -> - fun g -> VernacPrint (PrintAbout (qid,l,g)) - | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchHead c,g, l) - | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchPattern c,g, l) - | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchRewrite c,g, l) - | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> - let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) - (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> - fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) - (* compatibility: SearchAbout with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules; "." -> - fun g -> VernacSearch (SearchAbout sl,g, l) - ] ] - ; - printable: - [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l) - | IDENT "All" -> PrintFullContext - | IDENT "Section"; s = global -> PrintSectionContext s - | IDENT "Grammar"; ent = IDENT -> - (* This should be in "syntax" section but is here for factorization*) - PrintGrammar ent - | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir - | IDENT "Modules" -> - user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") - | IDENT "Libraries" -> PrintModules - - | IDENT "ML"; IDENT "Path" -> PrintMLLoadPath - | IDENT "ML"; IDENT "Modules" -> PrintMLModules - | IDENT "Debug"; IDENT "GC" -> PrintDebugGC - | IDENT "Graph" -> PrintGraph - | IDENT "Classes" -> PrintClasses - | IDENT "TypeClasses" -> PrintTypeClasses - | IDENT "Instances"; qid = smart_global -> PrintInstances qid - | IDENT "Coercions" -> PrintCoercions - | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr - -> PrintCoercionPaths (s,t) - | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions - | IDENT "Tables" -> PrintTables - | IDENT "Options" -> PrintTables (* A Synonymous to Tables *) - | IDENT "Hint" -> PrintHintGoal - | IDENT "Hint"; qid = smart_global -> PrintHint qid - | IDENT "Hint"; "*" -> PrintHintDb - | IDENT "HintDb"; s = IDENT -> PrintHintDbName s - | IDENT "Scopes" -> PrintScopes - | IDENT "Scope"; s = IDENT -> PrintScope s - | IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s - | IDENT "Implicit"; qid = smart_global -> PrintImplicit qid - | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt) - | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt) - | IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, false, qid) - | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, false, qid) - | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (false, true, qid) - | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, true, qid) - | IDENT "Strategy"; qid = smart_global -> PrintStrategy (Some qid) - | IDENT "Strategies" -> PrintStrategy None ] ] - ; - class_rawexpr: - [ [ IDENT "Funclass" -> FunClass - | IDENT "Sortclass" -> SortClass - | qid = smart_global -> RefClass qid ] ] - ; - locatable: - [ [ qid = smart_global -> LocateAny qid - | IDENT "Term"; qid = smart_global -> LocateTerm qid - | IDENT "File"; f = ne_string -> LocateFile f - | IDENT "Library"; qid = global -> LocateLibrary qid - | IDENT "Module"; qid = global -> LocateModule qid ] ] - ; - option_value: - [ [ -> BoolValue true - | n = integer -> IntValue (Some n) - | s = STRING -> StringValue s ] ] - ; - option_ref_value: - [ [ id = global -> QualidRefValue id - | s = STRING -> StringRefValue s ] ] - ; - option_table: - [ [ fl = LIST1 [ x = IDENT -> x ] -> fl ]] - ; - as_dirpath: - [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] - ; - ne_in_or_out_modules: - [ [ IDENT "inside"; l = LIST1 global -> SearchInside l - | IDENT "outside"; l = LIST1 global -> SearchOutside l ] ] - ; - in_or_out_modules: - [ [ m = ne_in_or_out_modules -> m - | -> SearchOutside [] ] ] - ; - comment: - [ [ c = constr -> CommentConstr c - | s = STRING -> CommentString s - | n = natural -> CommentInt n ] ] - ; - positive_search_mark: - [ [ "-" -> false | -> true ] ] - ; - scope: - [ [ "%"; key = IDENT -> key ] ] - ; - searchabout_query: - [ [ b = positive_search_mark; s = ne_string; sc = OPT scope -> - (b, SearchString (s,sc)) - | b = positive_search_mark; p = constr_pattern -> - (b, SearchSubPattern p) - ] ] - ; - searchabout_queries: - [ [ m = ne_in_or_out_modules -> ([],m) - | s = searchabout_query; l = searchabout_queries -> - let (sl,m) = l in (s::sl,m) - | -> ([],SearchOutside []) - ] ] - ; - univ_name_list: - [ [ "@{" ; l = LIST0 name; "}" -> l ] ] - ; -END; - -GEXTEND Gram - command: - [ [ -(* State management *) - IDENT "Write"; IDENT "State"; s = IDENT -> VernacWriteState s - | IDENT "Write"; IDENT "State"; s = ne_string -> VernacWriteState s - | IDENT "Restore"; IDENT "State"; s = IDENT -> VernacRestoreState s - | IDENT "Restore"; IDENT "State"; s = ne_string -> VernacRestoreState s - -(* Resetting *) - | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial - | IDENT "Reset"; id = identref -> VernacResetName id - | IDENT "Back" -> VernacBack 1 - | IDENT "Back"; n = natural -> VernacBack n - | IDENT "BackTo"; n = natural -> VernacBackTo n - | IDENT "Backtrack"; n = natural ; m = natural ; p = natural -> - VernacBacktrack (n,m,p) - -(* Tactic Debugger *) - | IDENT "Debug"; IDENT "On" -> - VernacSetOption (false, ["Ltac";"Debug"], BoolValue true) - - | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (false, ["Ltac";"Debug"], BoolValue false) - -(* registration of a custom reduction *) - - | IDENT "Declare"; IDENT "Reduction"; s = IDENT; ":="; - r = red_expr -> - VernacDeclareReduction (s,r) - - ] ]; - END -;; - -(* Grammar extensions *) - -GEXTEND Gram - GLOBAL: syntax; - - syntax: - [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (true,sc) - - | IDENT "Close"; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (false,sc) - - | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> - VernacDelimiters (sc, Some key) - | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT -> - VernacDelimiters (sc, None) - - | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; - refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - - | IDENT "Infix"; op = ne_lstring; ":="; p = constr; - modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; - sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix ((op,modl),p,sc) - | IDENT "Notation"; id = identref; - idl = LIST0 ident; ":="; c = constr; b = only_parsing -> - VernacSyntacticDefinition - (id,(idl,c),b) - | IDENT "Notation"; s = lstring; ":="; - c = constr; - modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; - sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (c,(s,modl),sc) - | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> - VernacNotationAddFormat (n,s,fmt) - - | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> - let s = CAst.map (fun s -> "x '"^s^"' y") s in - VernacSyntaxExtension (true,(s,l)) - - | IDENT "Reserved"; IDENT "Notation"; - s = ne_lstring; - l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (false, (s,l)) - - (* "Print" "Grammar" should be here but is in "command" entry in order - to factorize with other "Print"-based vernac entries *) - ] ] - ; - only_parsing: - [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> - Some Flags.Current - | "("; IDENT "compat"; s = STRING; ")" -> - Some (parse_compat_version s) - | -> None ] ] - ; - level: - [ [ IDENT "level"; n = natural -> NumLevel n - | IDENT "next"; IDENT "level" -> NextLevel ] ] - ; - syntax_modifier: - [ [ "at"; IDENT "level"; n = natural -> SetLevel n - | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA - | IDENT "right"; IDENT "associativity" -> SetAssoc RightA - | IDENT "no"; IDENT "associativity" -> SetAssoc NonA - | IDENT "only"; IDENT "printing" -> SetOnlyPrinting - | IDENT "only"; IDENT "parsing" -> SetOnlyParsing - | IDENT "compat"; s = STRING -> - SetCompatVersion (parse_compat_version s) - | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s]; - s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] -> - begin match s1, s2 with - | { CAst.v = k }, Some s -> SetFormat(k,s) - | s, None -> SetFormat ("text",s) end - | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; - lev = level -> SetItemLevel (x::l,lev) - | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev) - | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None) - | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) - ] ] - ; - syntax_extension_type: - [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference - | IDENT "bigint" -> ETBigint - | IDENT "binder" -> ETBinder true - | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n) - | IDENT "pattern" -> ETPattern (false,None) - | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n) - | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None) - | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n) - | IDENT "closed"; IDENT "binder" -> ETBinder false - ] ] - ; - at_level: - [ [ "at"; n = level -> n ] ] - ; - constr_as_binder_kind: - [ [ "as"; IDENT "ident" -> AsIdent - | "as"; IDENT "pattern" -> AsIdentOrPattern - | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ] - ; -END diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml new file mode 100644 index 00000000..d8c08803 --- /dev/null +++ b/parsing/notation_gram.ml @@ -0,0 +1,43 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map + +let level_of_notation ?(onlyprint=false) ntn = + let (level,onlyprint') = NotationMap.find ntn !notation_level_map in + if onlyprint' && not onlyprint then raise Not_found; + level + +(**********************************************************************) +(* Equality *) + +open Extend + +let parenRelation_eq t1 t2 = match t1, t2 with +| L, L | E, E | Any, Any -> true +| Prec l1, Prec l2 -> Int.equal l1 l2 +| _ -> false + +let production_position_eq pp1 pp2 = match (pp1,pp2) with +| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2 +| InternalProd, InternalProd -> true +| (BorderProd _ | InternalProd), _ -> false + +let production_level_eq l1 l2 = match (l1,l2) with +| NextLevel, NextLevel -> true +| NumLevel n1, NumLevel n2 -> Int.equal n1 n2 +| (NextLevel | NumLevel _), _ -> false + +let constr_entry_key_eq eq v1 v2 = match v1, v2 with +| ETIdent, ETIdent -> true +| ETGlobal, ETGlobal -> true +| ETBigint, ETBigint -> true +| ETBinder b1, ETBinder b2 -> b1 == b2 +| ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) -> + notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 +| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false + +let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) = + let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in + let prod_eq (l1,pp1) (l2,pp2) = + not strict || + (production_level_eq l1 l2 && production_position_eq pp1 pp2) in + notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2 + && List.equal (constr_entry_key_eq prod_eq) u1 u2 + +let level_eq = level_eq_gen false diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli new file mode 100644 index 00000000..f427a607 --- /dev/null +++ b/parsing/notgram_ops.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* level -> bool + +(** {6 Declare and test the level of a (possibly uninterpreted) notation } *) + +val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit +val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 1f29636b..2154f2f8 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,9 +1,9 @@ Tok CLexer +Extend +Notation_gram +Ppextend +Notgram_ops Pcoq -Egramml -Egramcoq G_constr -G_vernac G_prim -G_proofs diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 258c4bb1..eb3e6338 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -17,9 +17,17 @@ let curry f x y = f (x, y) let uncurry f (x,y) = f x y (** Location Utils *) +let ploc_file_of_coq_file = function +| Loc.ToplevelInput -> "" +| Loc.InFile f -> f + let coq_file_of_ploc_file s = if s = "" then Loc.ToplevelInput else Loc.InFile s +let of_coqloc loc = + let open Loc in + Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) "" + let to_coqloc loc = { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc); Loc.line_nb = Ploc.line_nb loc; @@ -78,24 +86,15 @@ module type S = type internal_entry = Tok.t Gramext.g_entry type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list type coq_parsable - val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable + val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit val comment_state : coq_parsable -> ((int * int) * string) list - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a - end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct include Grammar.GMake(CLexer) @@ -104,15 +103,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct type internal_entry = Tok.t Gramext.g_entry type symbol = Tok.t Gramext.g_symbol type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list type coq_parsable = parsable * CLexer.lexer_state ref - let parsable ?(file=Loc.ToplevelInput) c = + let coq_parsable ?(file=Loc.ToplevelInput) c = let state = ref (CLexer.init_lexer_state file) in CLexer.set_lexer_state !state; let a = parsable c in @@ -137,14 +131,25 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct let comment_state (p,state) = CLexer.get_comment_state !state - let entry_print ft x = Entry.print ft x - - (* Not used *) - let srules' = Gramext.srules - let parse_tokens_after_filter = Entry.parse_token +end +module Parsable = +struct + type t = G.coq_parsable + let make = G.coq_parsable + let comment_state = G.comment_state end +module Entry = +struct + + type 'a t = 'a Grammar.GMake(CLexer).Entry.e + + let create = G.Entry.create + let parse = G.entry_parse + let print = G.Entry.print + +end let warning_verbose = Gramext.warning_verbose @@ -208,9 +213,9 @@ let camlp5_verbosity silent f x = (** Grammar extensions *) -(** NB: [extend_statment = - gram_position option * single_extend_statment list] - and [single_extend_statment = +(** NB: [extend_statement = + gram_position option * single_extend_statement list] + and [single_extend_statement = string option * gram_assoc option * production_rule list] and [production_rule = symbol list * action] @@ -237,9 +242,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function | Aentry e -> Symbols.snterm (G.Entry.obj e) | Aentryl (e, n) -> - Symbols.snterml (G.Entry.obj e, string_of_int n) + Symbols.snterml (G.Entry.obj e, n) | Arules rs -> - G.srules' (List.map symbol_of_rules rs) + Gramext.srules (List.map symbol_of_rules rs) and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function | Stop -> fun accu -> accu @@ -264,16 +269,23 @@ let of_coq_extend_statement (pos, st) = type gram_reinit = gram_assoc * gram_position type extend_rule = -| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule + +module EntryCommand = Dyn.Make () +module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end +module EntryDataMap = EntryCommand.Map(EntryData) type ext_kind = | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) + | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind (** The list of extensions *) let camlp5_state = ref [] +let camlp5_entries = ref EntryDataMap.empty + (** Deletion *) let grammar_delete e reinit (pos,rls) = @@ -329,6 +341,7 @@ module Gram = I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil + let gram_extend e ext = grammar_extend e None ext end (** Remove extensions @@ -338,7 +351,7 @@ module Gram = let rec remove_grammars n = if n>0 then - (match !camlp5_state with + match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); @@ -349,21 +362,31 @@ let rec remove_grammars n = camlp5_state := t; remove_grammars n; redo(); - camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state) + camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state + | ByEntry (tag, name, e) :: t -> + G.Unsafe.clear_entry e; + camlp5_state := t; + let EntryData.Ex entries = + try EntryDataMap.find tag !camlp5_entries + with Not_found -> EntryData.Ex String.Map.empty + in + let entries = String.Map.remove name entries in + camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries; + remove_grammars (n - 1) let make_rule r = [None, None, r] (** An entry that checks we reached the end of the input. *) let eoi_entry en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in + let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in let act = Gram.action (fun _ x loc -> x) in uncurry (Gram.extend e) (None, make_rule [symbs, act]); e let map_entry f en = - let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in + let e = Entry.create ((Gram.Entry.name en) ^ "_map") in let symbs = [Symbols.snterm (Gram.Entry.obj en)] in let act = Gram.action (fun x loc -> f x) in uncurry (Gram.extend e) (None, make_rule [symbs, act]); @@ -373,7 +396,7 @@ let map_entry f en = (use eoi_entry) *) let parse_string f x = - let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) + let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm) type gram_universe = string @@ -387,7 +410,6 @@ let create_universe u = let uprim = create_universe "prim" let uconstr = create_universe "constr" let utactic = create_universe "tactic" -let uvernac = create_universe "vernac" let get_univ u = if Hashtbl.mem utables u then u @@ -395,14 +417,14 @@ let get_univ u = let new_entry u s = let ename = u ^ ":" ^ s in - let e = Gram.entry_create ename in + let e = Entry.create ename in e let make_gen_entry u s = new_entry u s module GrammarObj = struct - type ('r, _, _) obj = 'r Gram.entry + type ('r, _, _) obj = 'r Entry.t let name = "grammar" let default _ = None end @@ -412,7 +434,7 @@ module Grammar = Register(GrammarObj) let register_grammar = Grammar.register0 let genarg_grammar = Grammar.obj -let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry = +let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t = let e = new_entry u s in let Rawwit t = etyp in let () = Grammar.register0 t e in @@ -424,38 +446,38 @@ module Prim = struct let gec_gen n = make_gen_entry uprim n - (* Entries that can be referred via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Entry.t table *) (* Typically for tactic or vernac extensions *) let preident = gec_gen "preident" let ident = gec_gen "ident" let natural = gec_gen "natural" let integer = gec_gen "integer" - let bigint = Gram.entry_create "Prim.bigint" + let bigint = Entry.create "Prim.bigint" let string = gec_gen "string" - let lstring = Gram.entry_create "Prim.lstring" + let lstring = Entry.create "Prim.lstring" let reference = make_gen_entry uprim "reference" - let by_notation = Gram.entry_create "by_notation" - let smart_global = Gram.entry_create "smart_global" + let by_notation = Entry.create "by_notation" + let smart_global = Entry.create "smart_global" (* parsed like ident but interpreted as a term *) let var = gec_gen "var" - let name = Gram.entry_create "Prim.name" - let identref = Gram.entry_create "Prim.identref" - let univ_decl = Gram.entry_create "Prim.univ_decl" - let ident_decl = Gram.entry_create "Prim.ident_decl" - let pattern_ident = Gram.entry_create "pattern_ident" - let pattern_identref = Gram.entry_create "pattern_identref" + let name = Entry.create "Prim.name" + let identref = Entry.create "Prim.identref" + let univ_decl = Entry.create "Prim.univ_decl" + let ident_decl = Entry.create "Prim.ident_decl" + let pattern_ident = Entry.create "pattern_ident" + let pattern_identref = Entry.create "pattern_identref" (* A synonym of ident - maybe ident will be located one day *) - let base_ident = Gram.entry_create "Prim.base_ident" + let base_ident = Entry.create "Prim.base_ident" - let qualid = Gram.entry_create "Prim.qualid" - let fullyqualid = Gram.entry_create "Prim.fullyqualid" - let dirpath = Gram.entry_create "Prim.dirpath" + let qualid = Entry.create "Prim.qualid" + let fullyqualid = Entry.create "Prim.fullyqualid" + let dirpath = Entry.create "Prim.dirpath" - let ne_string = Gram.entry_create "Prim.ne_string" - let ne_lstring = Gram.entry_create "Prim.ne_lstring" + let ne_string = Entry.create "Prim.ne_string" + let ne_lstring = Entry.create "Prim.ne_lstring" end @@ -463,7 +485,7 @@ module Constr = struct let gec_constr = make_gen_entry uconstr - (* Entries that can be referred via the string -> Gram.entry table *) + (* Entries that can be referred via the string -> Entry.t table *) let constr = gec_constr "constr" let operconstr = gec_constr "operconstr" let constr_eoi = eoi_entry constr @@ -474,67 +496,29 @@ module Constr = let universe_level = make_gen_entry uconstr "universe_level" let sort = make_gen_entry uconstr "sort" let sort_family = make_gen_entry uconstr "sort_family" - let pattern = Gram.entry_create "constr:pattern" + let pattern = Entry.create "constr:pattern" let constr_pattern = gec_constr "constr_pattern" let lconstr_pattern = gec_constr "lconstr_pattern" - let closed_binder = Gram.entry_create "constr:closed_binder" - let binder = Gram.entry_create "constr:binder" - let binders = Gram.entry_create "constr:binders" - let open_binders = Gram.entry_create "constr:open_binders" - let binders_fixannot = Gram.entry_create "constr:binders_fixannot" - let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint" - let record_declaration = Gram.entry_create "constr:record_declaration" - let appl_arg = Gram.entry_create "constr:appl_arg" + let closed_binder = Entry.create "constr:closed_binder" + let binder = Entry.create "constr:binder" + let binders = Entry.create "constr:binders" + let open_binders = Entry.create "constr:open_binders" + let binders_fixannot = Entry.create "constr:binders_fixannot" + let typeclass_constraint = Entry.create "constr:typeclass_constraint" + let record_declaration = Entry.create "constr:record_declaration" + let appl_arg = Entry.create "constr:appl_arg" end module Module = struct - let module_expr = Gram.entry_create "module_expr" - let module_type = Gram.entry_create "module_type" + let module_expr = Entry.create "module_expr" + let module_type = Entry.create "module_type" end -module Vernac_ = - struct - let gec_vernac s = Gram.entry_create ("vernac:" ^ s) - - (* The different kinds of vernacular commands *) - let gallina = gec_vernac "gallina" - let gallina_ext = gec_vernac "gallina_ext" - let command = gec_vernac "command" - let syntax = gec_vernac "syntax_command" - let vernac_control = gec_vernac "Vernac.vernac_control" - let rec_definition = gec_vernac "Vernac.rec_definition" - let red_expr = make_gen_entry utactic "red_expr" - let hint_info = gec_vernac "hint_info" - (* Main vernac entry *) - let main_entry = Gram.entry_create "vernac" - let noedit_mode = gec_vernac "noedit_command" - - let () = - let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in - let act_eoi = Gram.action (fun _ loc -> None) in - let rule = [ - ([ Symbols.stoken Tok.EOI ], act_eoi); - ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac ); - ] in - uncurry (Gram.extend main_entry) (None, make_rule rule) - - let command_entry_ref = ref noedit_mode - let command_entry = - Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm) - - end - -let main_entry = Vernac_.main_entry - -let set_command_entry e = Vernac_.command_entry_ref := e -let get_command_entry () = !Vernac_.command_entry_ref - let epsilon_value f e = let r = Rule (Next (Stop, e), fun x _ -> f x) in let ext = of_coq_extend_statement (None, [None, None, [r]]) in - let entry = G.entry_create "epsilon" in + let entry = Gram.entry_create "epsilon" in let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None @@ -550,59 +534,119 @@ module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) let grammar_interp = ref GrammarInterpMap.empty -let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref [] +type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t + +module EntryInterp = struct type _ t = Ex : ('a, 'b) entry_extension -> ('a * 'b) t end +module EntryInterpMap = EntryCommand.Map(EntryInterp) + +let entry_interp = ref EntryInterpMap.empty + +type grammar_entry = +| GramExt of int * GrammarCommand.t +| EntryExt : int * ('a * 'b) EntryCommand.tag * 'a -> grammar_entry + +let (grammar_stack : (grammar_entry * GramState.t) list ref) = ref [] type 'a grammar_command = 'a GrammarCommand.tag +type ('a, 'b) entry_command = ('a * 'b) EntryCommand.tag let create_grammar_command name interp : _ grammar_command = let obj = GrammarCommand.create name in let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in obj +let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) entry_command = + let obj = EntryCommand.create name in + let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in + obj + let extend_grammar_command tag g = let modify = GrammarInterpMap.find tag !grammar_interp in let grammar_state = match !grammar_stack with | [] -> GramState.empty - | (_, _, st) :: _ -> st + | (_, st) :: _ -> st in let (rules, st) = modify g grammar_state in let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in let () = List.iter iter rules in let nb = List.length rules in - grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack + grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack -let recover_grammar_command (type a) (tag : a grammar_command) : a list = - let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) -> - match GrammarCommand.eq tag tag' with - | None -> None - | Some Refl -> Some v +let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list = + let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in + let grammar_state = match !grammar_stack with + | [] -> GramState.empty + | (_, st) :: _ -> st + in + let (names, st) = modify g grammar_state in + let entries = List.map (fun name -> Gram.entry_create name) names in + let iter name e = + camlp5_state := ByEntry (tag, name, e) :: !camlp5_state; + let EntryData.Ex old = + try EntryDataMap.find tag !camlp5_entries + with Not_found -> EntryData.Ex String.Map.empty + in + let entries = String.Map.add name e old in + camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries in - List.map_filter filter !grammar_stack + let () = List.iter2 iter names entries in + let nb = List.length entries in + let () = grammar_stack := (EntryExt (nb, tag, g), st) :: !grammar_stack in + entries + +let find_custom_entry tag name = + let EntryData.Ex map = EntryDataMap.find tag !camlp5_entries in + String.Map.find name map + +let extend_dyn_grammar (e, _) = match e with +| GramExt (_, (GrammarCommand.Dyn (tag, g))) -> extend_grammar_command tag g +| EntryExt (_, tag, g) -> ignore (extend_entry_command tag g) + +(** Registering extra grammar *) -let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g +type any_entry = AnyEntry : 'a Gram.entry -> any_entry + +let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty -(* Summary functions: the state of the lexer is included in that of the parser. +let register_grammars_by_name name grams = + grammar_names := String.Map.add name grams !grammar_names + +let find_grammars_by_name name = + try String.Map.find name !grammar_names + with Not_found -> + let fold (EntryDataMap.Any (tag, EntryData.Ex map)) accu = + try AnyEntry (String.Map.find name map) :: accu + with Not_found -> accu + in + EntryDataMap.fold fold !camlp5_entries [] + +(** Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing grammar rules. *) -type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.keyword_state +type frozen_t = + (grammar_entry * GramState.t) list * + CLexer.keyword_state -let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ()) +let freeze _ : frozen_t = + (!grammar_stack, CLexer.get_keyword_state ()) (* We compare the current state of the grammar and the state to unfreeze, by computing the longest common suffixes *) let factorize_grams l1 l2 = if l1 == l2 then ([], [], l1) else List.share_tails l1 l2 -let number_of_entries gcl = - List.fold_left (fun n (p,_,_) -> n + p) 0 gcl +let rec number_of_entries accu = function +| [] -> accu +| ((GramExt (p, _) | EntryExt (p, _, _)), _) :: rem -> + number_of_entries (p + accu) rem let unfreeze (grams, lex) = let (undo, redo, common) = factorize_grams !grammar_stack grams in - let n = number_of_entries undo in + let n = number_of_entries 0 undo in remove_grammars n; grammar_stack := common; CLexer.set_keyword_state lex; - List.iter extend_dyn_grammar (List.rev_map pi2 redo) + List.iter extend_dyn_grammar (List.rev redo) (** No need to provide an init function : the grammar state is statically available, and already empty initially, while @@ -635,17 +679,4 @@ let () = Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_red_expr (Vernac_.red_expr); () - -(** Registering extra grammar *) - -type any_entry = AnyEntry : 'a Gram.entry -> any_entry - -let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty - -let register_grammars_by_name name grams = - grammar_names := String.Map.add name grams !grammar_names - -let find_grammars_by_name name = - String.Map.find name !grammar_names diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9f186224..e12ccaa6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -10,85 +10,48 @@ open Names open Extend -open Vernacexpr open Genarg open Constrexpr open Libnames -open Misctypes -open Genredexpr (** The parser of Coq *) +(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE. + We only have it here to work with Camlp5. Handwritten grammar extensions + should use the safe [Pcoq.grammar_extend] function below. *) module Gram : sig include Grammar.S with type te = Tok.t -(* Where Grammar.S is + type 'a entry = 'a Entry.e + [@@ocaml.deprecated "Use [Pcoq.Entry.t]"] -module type S = - sig - type te = 'x; - type parsable = 'x; - value parsable : Stream.t char -> parsable; - value tokens : string -> list (string * int); - value glexer : Plexing.lexer te; - value set_algorithm : parse_algorithm -> unit; - module Entry : - sig - type e 'a = 'y; - value create : string -> e 'a; - value parse : e 'a -> parsable -> 'a; - value parse_token : e 'a -> Stream.t te -> 'a; - value name : e 'a -> string; - value of_parser : string -> (Stream.t te -> 'a) -> e 'a; - value print : Format.formatter -> e 'a -> unit; - external obj : e 'a -> Gramext.g_entry te = "%identity"; - end - ; - module Unsafe : - sig - value gram_reinit : Plexing.lexer te -> unit; - value clear_entry : Entry.e 'a -> unit; - end - ; - value extend : - Entry.e 'a -> option Gramext.position -> - list - (option string * option Gramext.g_assoc * - list (list (Gramext.g_symbol te) * Gramext.g_action)) -> - unit; - value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit; - end + [@@@ocaml.warning "-3"] -*) - - type 'a entry = 'a Entry.e - type internal_entry = Tok.t Gramext.g_entry - type symbol = Tok.t Gramext.g_symbol - type action = Gramext.g_action - type production_rule = symbol list * action - type single_extend_statment = - string option * Gramext.g_assoc option * production_rule list - type extend_statment = - Gramext.position option * single_extend_statment list - - type coq_parsable - - val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable - val action : 'a -> action val entry_create : string -> 'a entry - val entry_parse : 'a entry -> coq_parsable -> 'a - val entry_print : Format.formatter -> 'a entry -> unit + [@@ocaml.deprecated "Use [Pcoq.Entry.create]"] - (* Get comment parsing information from the Lexer *) - val comment_state : coq_parsable -> ((int * int) * string) list + val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit - (* Apparently not used *) - val srules' : production_rule list -> symbol - val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a + [@@@ocaml.warning "+3"] end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e +module Parsable : +sig + type t + val make : ?file:Loc.source -> char Stream.t -> t + (* Get comment parsing information from the Lexer *) + val comment_state : t -> ((int * int) * string) list +end + +module Entry : sig + type 'a t = 'a Grammar.GMake(CLexer).Entry.e + val create : string -> 'a t + val parse : 'a t -> Parsable.t -> 'a + val print : Format.formatter -> 'a t -> unit +end + (** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using @@ -170,106 +133,88 @@ val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit (** Parse a string *) -val parse_string : 'a Gram.entry -> string -> 'a -val eoi_entry : 'a Gram.entry -> 'a Gram.entry -val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry +val parse_string : 'a Entry.t -> string -> 'a +val eoi_entry : 'a Entry.t -> 'a Entry.t +val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t type gram_universe val get_univ : string -> gram_universe +val create_universe : string -> gram_universe + +val new_entry : gram_universe -> string -> 'a Entry.t val uprim : gram_universe val uconstr : gram_universe val utactic : gram_universe -val uvernac : gram_universe -val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit -val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry + +val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit +val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t val create_generic_entry : gram_universe -> string -> - ('a, rlevel) abstract_argument_type -> 'a Gram.entry + ('a, rlevel) abstract_argument_type -> 'a Entry.t module Prim : sig open Names open Libnames - val preident : string Gram.entry - val ident : Id.t Gram.entry - val name : lname Gram.entry - val identref : lident Gram.entry - val univ_decl : universe_decl_expr Gram.entry - val ident_decl : ident_decl Gram.entry - val pattern_ident : Id.t Gram.entry - val pattern_identref : lident Gram.entry - val base_ident : Id.t Gram.entry - val natural : int Gram.entry - val bigint : Constrexpr.raw_natural_number Gram.entry - val integer : int Gram.entry - val string : string Gram.entry - val lstring : lstring Gram.entry - val qualid : qualid CAst.t Gram.entry - val fullyqualid : Id.t list CAst.t Gram.entry - val reference : reference Gram.entry - val by_notation : (string * string option) Gram.entry - val smart_global : reference or_by_notation Gram.entry - val dirpath : DirPath.t Gram.entry - val ne_string : string Gram.entry - val ne_lstring : lstring Gram.entry - val var : lident Gram.entry + val preident : string Entry.t + val ident : Id.t Entry.t + val name : lname Entry.t + val identref : lident Entry.t + val univ_decl : universe_decl_expr Entry.t + val ident_decl : ident_decl Entry.t + val pattern_ident : Id.t Entry.t + val pattern_identref : lident Entry.t + val base_ident : Id.t Entry.t + val natural : int Entry.t + val bigint : Constrexpr.raw_natural_number Entry.t + val integer : int Entry.t + val string : string Entry.t + val lstring : lstring Entry.t + val reference : qualid Entry.t + val qualid : qualid Entry.t + val fullyqualid : Id.t list CAst.t Entry.t + val by_notation : (string * string option) Entry.t + val smart_global : qualid or_by_notation Entry.t + val dirpath : DirPath.t Entry.t + val ne_string : string Entry.t + val ne_lstring : lstring Entry.t + val var : lident Entry.t end module Constr : sig - val constr : constr_expr Gram.entry - val constr_eoi : constr_expr Gram.entry - val lconstr : constr_expr Gram.entry - val binder_constr : constr_expr Gram.entry - val operconstr : constr_expr Gram.entry - val ident : Id.t Gram.entry - val global : reference Gram.entry - val universe_level : glob_level Gram.entry - val sort : glob_sort Gram.entry - val sort_family : Sorts.family Gram.entry - val pattern : cases_pattern_expr Gram.entry - val constr_pattern : constr_expr Gram.entry - val lconstr_pattern : constr_expr Gram.entry - val closed_binder : local_binder_expr list Gram.entry - val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) - val binders : local_binder_expr list Gram.entry (* list of binder *) - val open_binders : local_binder_expr list Gram.entry - val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (lname * bool * constr_expr) Gram.entry - val record_declaration : constr_expr Gram.entry - val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry + val constr : constr_expr Entry.t + val constr_eoi : constr_expr Entry.t + val lconstr : constr_expr Entry.t + val binder_constr : constr_expr Entry.t + val operconstr : constr_expr Entry.t + val ident : Id.t Entry.t + val global : qualid Entry.t + val universe_level : Glob_term.glob_level Entry.t + val sort : Glob_term.glob_sort Entry.t + val sort_family : Sorts.family Entry.t + val pattern : cases_pattern_expr Entry.t + val constr_pattern : constr_expr Entry.t + val lconstr_pattern : constr_expr Entry.t + val closed_binder : local_binder_expr list Entry.t + val binder : local_binder_expr list Entry.t (* closed_binder or variable *) + val binders : local_binder_expr list Entry.t (* list of binder *) + val open_binders : local_binder_expr list Entry.t + val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t + val typeclass_constraint : (lname * bool * constr_expr) Entry.t + val record_declaration : constr_expr Entry.t + val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t end module Module : sig - val module_expr : module_ast Gram.entry - val module_type : module_ast Gram.entry - end - -module Vernac_ : - sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Vernacexpr.hint_info_expr Gram.entry + val module_expr : module_ast Entry.t + val module_type : module_ast Entry.t end -(** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Gram.entry - -(** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Gram.entry -val set_command_entry : vernac_expr Gram.entry -> unit - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) @@ -277,8 +222,8 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option type gram_reinit = gram_assoc * gram_position (** Type of reinitialization data *) -val grammar_extend : 'a Gram.entry -> gram_reinit option -> - 'a Extend.extend_statment -> unit +val grammar_extend : 'a Entry.t -> gram_reinit option -> + 'a Extend.extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) @@ -288,12 +233,14 @@ val grammar_extend : 'a Gram.entry -> gram_reinit option -> module GramState : Store.S (** Auxiliary state of the grammar. Any added data must be marshallable. *) +(** {6 Extension with parsing rules} *) + type 'a grammar_command (** Type of synchronized parsing extensions. The ['a] type should be marshallable. *) type extend_rule = -| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule +| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t (** Grammar extension entry point. Given some ['a] and a current grammar state, @@ -308,12 +255,35 @@ val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_comman val extend_grammar_command : 'a grammar_command -> 'a -> unit (** Extend the grammar of Coq with the given data. *) -val recover_grammar_command : 'a grammar_command -> 'a list -(** Recover the current stack of grammar extensions. *) +(** {6 Extension with parsing entries} *) + +type ('a, 'b) entry_command +(** Type of synchronized entry creation. The ['a] type should be + marshallable. *) + +type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t +(** Entry extension entry point. Given some ['a] and a current grammar state, + such a function must produce the list of entry extensions that will be + created and kept synchronized w.r.t. the summary, together + with a new state. It should be pure. *) + +val create_entry_command : string -> ('a, 'b) entry_extension -> ('a, 'b) entry_command +(** Create a new entry-creating command with the given name. The extension + function is called to generate the new entries for a given data. *) + +val extend_entry_command : ('a, 'b) entry_command -> 'a -> 'b Entry.t list +(** Create new synchronized entries using the provided data. *) + +val find_custom_entry : ('a, 'b) entry_command -> string -> 'b Entry.t +(** Find an entry generated by the synchronized system in the current state. + @raise Not_found if non-existent. *) + +(** {6 Protection w.r.t. backtrack} *) val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) +val of_coqloc : Loc.t -> Ploc.t val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t @@ -322,7 +292,7 @@ val parser_summary_tag : frozen_t Summary.Dyn.tag (** Registering grammars by name *) -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml new file mode 100644 index 00000000..e1f5e201 --- /dev/null +++ b/parsing/ppextend.ml @@ -0,0 +1,77 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* h n + | PpHOVB n -> hov n + | PpHVB n -> hv n + | PpVB n -> v n + +let ppcmd_of_cut = function + | PpFnl -> fnl () + | PpBrk(n1,n2) -> brk(n1,n2) + +type unparsing = + | UnpMetaVar of int * parenRelation + | UnpBinderMetaVar of int * parenRelation + | UnpListMetaVar of int * parenRelation * unparsing list + | UnpBinderListMetaVar of int * bool * unparsing list + | UnpTerminal of string + | UnpBox of ppbox * unparsing Loc.located list + | UnpCut of ppcut + +type unparsing_rule = unparsing list * precedence +type extra_unparsing_rules = (string * string) list +(* Concrete syntax for symbolic-extension table *) +let notation_rules = + Summary.ref ~name:"notation-rules" (NotationMap.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) NotationMap.t) + +let declare_notation_rule ntn ~extra unpl gram = + notation_rules := NotationMap.add ntn (unpl,extra,gram) !notation_rules + +let find_notation_printing_rule ntn = + try pi1 (NotationMap.find ntn !notation_rules) + with Not_found -> anomaly (str "No printing rule found for " ++ pr_notation ntn ++ str ".") +let find_notation_extra_printing_rules ntn = + try pi2 (NotationMap.find ntn !notation_rules) + with Not_found -> [] +let find_notation_parsing_rules ntn = + try pi3 (NotationMap.find ntn !notation_rules) + with Not_found -> anomaly (str "No parsing rule found for " ++ pr_notation ntn ++ str ".") + +let get_defined_notations () = + NotationSet.elements @@ NotationMap.domain !notation_rules + +let add_notation_extra_printing_rule ntn k v = + try + notation_rules := + let p, pp, gr = NotationMap.find ntn !notation_rules in + NotationMap.add ntn (p, (k,v) :: pp, gr) !notation_rules + with Not_found -> + user_err ~hdr:"add_notation_extra_printing_rule" + (str "No such Notation.") diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli new file mode 100644 index 00000000..7eb5967a --- /dev/null +++ b/parsing/ppextend.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Pp.t -> Pp.t + +val ppcmd_of_cut : ppcut -> Pp.t + +(** {6 Printing rules for notations} *) + +(** Declare and look for the printing rule for symbolic notations *) +type unparsing = + | UnpMetaVar of int * parenRelation + | UnpBinderMetaVar of int * parenRelation + | UnpListMetaVar of int * parenRelation * unparsing list + | UnpBinderListMetaVar of int * bool * unparsing list + | UnpTerminal of string + | UnpBox of ppbox * unparsing Loc.located list + | UnpCut of ppcut + +type unparsing_rule = unparsing list * precedence +type extra_unparsing_rules = (string * string) list +val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit +val find_notation_printing_rule : notation -> unparsing_rule +val find_notation_extra_printing_rules : notation -> extra_unparsing_rules +val find_notation_parsing_rules : notation -> notation_grammar +val add_notation_extra_printing_rule : notation -> string -> string -> unit + +(** Returns notations with defined parsing/printing rules *) +val get_defined_notations : unit -> notation list -- cgit v1.2.3