From 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 20 May 2018 22:23:02 +0200 Subject: [api] [parsing] Move Egram* to `vernac/` The extension mechanism is specific to metasyntax and vernacinterp, thus it makes sense to place them next to each other. We also fix the META entry for the `grammar` camlp5 plugin. --- parsing/egramcoq.ml | 483 -------------------------------------------------- parsing/egramcoq.mli | 19 -- parsing/egramml.ml | 84 --------- parsing/egramml.mli | 33 ---- parsing/parsing.mllib | 2 - 5 files changed, 621 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 (limited to 'parsing') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml deleted file mode 100644 index 5f63d21c4..000000000 --- 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 e15add10f..000000000 --- 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 90cd7d10b..000000000 --- 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 31aa1a989..000000000 --- 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/parsing.mllib b/parsing/parsing.mllib index 103e1188a..e5a0a31cc 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -3,8 +3,6 @@ CLexer Extend Vernacexpr Pcoq -Egramml -Egramcoq G_constr G_vernac G_prim -- cgit v1.2.3