diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/compat.ml4 | 71 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 644 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 16 | ||||
| -rw-r--r-- | parsing/entry.ml | 30 | ||||
| -rw-r--r-- | parsing/entry.mli | 23 | ||||
| -rw-r--r-- | parsing/parsing.mllib | 1 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 539 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 88 |
8 files changed, 613 insertions, 799 deletions
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 310a44149a..2b67693d28 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -21,17 +21,11 @@ end exception Exc_located = Ploc.Exc IFDEF CAMLP5_6_00 THEN -let ploc_make_loc fname lnb pos bpep = Ploc.make_loc fname lnb pos bpep "" let ploc_file_name = Ploc.file_name ELSE -let ploc_make_loc fname lnb pos bpep = Ploc.make lnb pos bpep let ploc_file_name _ = "" END -let of_coqloc loc = - let (fname, lnb, pos, bp, ep) = Loc.represent loc in - ploc_make_loc fname lnb pos (bp,ep) - let to_coqloc loc = Loc.create (ploc_file_name loc) (Ploc.line_nb loc) (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc) @@ -44,10 +38,6 @@ module CompatLoc = Camlp4.PreCast.Loc exception Exc_located = CompatLoc.Exc_located -let of_coqloc loc = - let (fname, lnb, pos, bp, ep) = Loc.represent loc in - CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false) - let to_coqloc loc = Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc) (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc) @@ -65,6 +55,7 @@ IFDEF CAMLP5 THEN module PcamlSig = struct end module Token = Token +module CompatGramext = struct include Gramext type assoc = g_assoc end ELSE @@ -73,68 +64,10 @@ module Ast = Camlp4.PreCast.Ast module Pcaml = Camlp4.PreCast.Syntax module MLast = Ast module Token = struct exception Error of string end +module CompatGramext = Camlp4.Sig.Grammar END - -(** Grammar auxiliary types *) - -IFDEF CAMLP5 THEN - -let to_coq_assoc = function -| Gramext.RightA -> Extend.RightA -| Gramext.LeftA -> Extend.LeftA -| Gramext.NonA -> Extend.NonA - -let of_coq_assoc = function -| Extend.RightA -> Gramext.RightA -| Extend.LeftA -> Gramext.LeftA -| Extend.NonA -> Gramext.NonA - -let of_coq_position = function -| Extend.First -> Gramext.First -| Extend.Last -> Gramext.Last -| Extend.Before s -> Gramext.Before s -| Extend.After s -> Gramext.After s -| Extend.Level s -> Gramext.Level s - -let to_coq_position = function -| Gramext.First -> Extend.First -| Gramext.Last -> Extend.Last -| Gramext.Before s -> Extend.Before s -| Gramext.After s -> Extend.After s -| Gramext.Level s -> Extend.Level s -| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *) - -ELSE - -let to_coq_assoc = function -| PcamlSig.Grammar.RightA -> Extend.RightA -| PcamlSig.Grammar.LeftA -> Extend.LeftA -| PcamlSig.Grammar.NonA -> Extend.NonA - -let of_coq_assoc = function -| Extend.RightA -> PcamlSig.Grammar.RightA -| Extend.LeftA -> PcamlSig.Grammar.LeftA -| Extend.NonA -> PcamlSig.Grammar.NonA - -let of_coq_position = function -| Extend.First -> PcamlSig.Grammar.First -| Extend.Last -> PcamlSig.Grammar.Last -| Extend.Before s -> PcamlSig.Grammar.Before s -| Extend.After s -> PcamlSig.Grammar.After s -| Extend.Level s -> PcamlSig.Grammar.Level s - -let to_coq_position = function -| PcamlSig.Grammar.First -> Extend.First -| PcamlSig.Grammar.Last -> Extend.Last -| PcamlSig.Grammar.Before s -> Extend.Before s -| PcamlSig.Grammar.After s -> Extend.After s -| PcamlSig.Grammar.Level s -> Extend.Level s - -END - - (** Signature of CLexer *) IFDEF CAMLP5 THEN diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index eff666c9c4..21a9afa293 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Errors open Util open Pcoq @@ -16,6 +15,136 @@ open Notation_term open Libnames open Names +(**********************************************************************) +(* This determines (depending on the associativity of the current + level and on the expected associativity) if a reference to constr_n is + a reference to the current level (to be translated into "SELF" on the + left border and into "constr LEVEL n" elsewhere), to the level below + (to be translated into "NEXT") or to an below wrt associativity (to be + translated in camlp4 into "constr" without level) or to another level + (to be translated into "constr LEVEL n") + + The boolean is true if the entry was existing _and_ empty; this to + circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the + converse of the extension mechanism *) + +let constr_level = string_of_int + +let default_levels = + [200,Extend.RightA,false; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 10,Extend.RightA,false; + 9,Extend.RightA,false; + 8,Extend.RightA,true; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_pattern_levels = + [200,Extend.RightA,true; + 100,Extend.RightA,false; + 99,Extend.RightA,true; + 11,Extend.LeftA,false; + 10,Extend.RightA,false; + 1,Extend.LeftA,false; + 0,Extend.RightA,false] + +let default_constr_levels = (default_levels, default_pattern_levels) + +(* At a same level, LeftA takes precedence over RightA and NoneA *) +(* In case, several associativity exists for a level, we make two levels, *) +(* first LeftA, then RightA and NoneA together *) + +let admissible_assoc = function + | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> 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 + errorlabstrm "" + (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) + +type gram_level = + gram_position option * gram_assoc option * string option * + (** for reinitialization: *) gram_reinit option + +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 camlp4 actions --- @@ -43,6 +172,146 @@ open Names (**********************************************************************) (** Declare Notations grammar rules *) +(**********************************************************************) +(* Binding constr entry keys to entries *) + +(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp4_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 (camlp4_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, Name.t Loc.located) entry +| TTReference : ('self, reference) entry +| TTBigint : ('self, Bigint.bigint) entry +| TTBinder : ('self, local_binder list) entry +| TTConstr : prod_info * 'r target -> ('r, 'r) entry +| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry +| TTBinderListT : ('self, local_binder list) entry +| TTBinderListF : Tok.t list -> ('self, local_binder 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 tkl = + let rec mkrule : Tok.t list -> unit rules = function + | [] -> Rules ({ norec_rule = Stop }, ignore) + | 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) +| TTBinderListF [] -> Alist1 (Aentry Constr.binder) +| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) +| TTName -> Aentry Prim.name +| TTBinder -> Aentry Constr.binder +| TTBinderListT -> Aentry Constr.open_binders +| TTBigint -> Aentry Prim.bigint +| TTReference -> Aentry Constr.global + +let interp_entry forpat e = match e with +| ETName -> TTAny TTName +| ETReference -> TTAny TTReference +| ETBigint -> TTAny TTBigint +| ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") +| ETBinder false -> TTAny TTBinder +| ETConstr p -> TTAny (TTConstr (p, forpat)) +| ETPattern -> assert false (** not used *) +| ETOther _ -> assert false (** not used *) +| ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETBinderList (true, []) -> TTAny TTBinderListT +| ETBinderList (true, _) -> assert false +| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) + let constr_expr_of_name (loc,na) = match na with | Anonymous -> CHole (loc,None,Misctypes.IntroAnonymous,None) | Name id -> CRef (Ident (loc,id), None) @@ -58,140 +327,122 @@ type grammar_constr_prod_item = (* tells action rule to make a list of the n previous parsed items; concat with last parsed list if true *) -let make_constr_action - (f : Loc.t -> constr_notation_substitution -> constr_expr) pil = - let rec make (constrs,constrlists,binders as fullsubst) = function - | [] -> - Gram.action (fun (loc:CompatLoc.t) -> f (!@loc) fullsubst) - | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> - (* parse a non-binding item *) - Gram.action (fun _ -> make fullsubst tl) - | GramConstrNonTerminal (typ, Some _) :: tl -> - (* parse a binding non-terminal *) - (match typ with - | (ETConstr _| ETOther _) -> - Gram.action (fun (v:constr_expr) -> - make (v :: constrs, constrlists, binders) tl) - | ETReference -> - Gram.action (fun (v:reference) -> - make (CRef (v,None) :: constrs, constrlists, binders) tl) - | ETName -> - Gram.action (fun (na:Loc.t * Name.t) -> - make (constr_expr_of_name na :: constrs, constrlists, binders) tl) - | ETBigint -> - Gram.action (fun (v:Bigint.bigint) -> - make (CPrim(Loc.ghost,Numeral v) :: constrs, constrlists, binders) tl) - | ETConstrList (_,n) -> - Gram.action (fun (v:constr_expr list) -> - make (constrs, v::constrlists, binders) tl) - | ETBinder _ | ETBinderList (true,_) -> - Gram.action (fun (v:local_binder list) -> - make (constrs, constrlists, v::binders) tl) - | ETBinderList (false,_) -> - Gram.action (fun (v:local_binder list list) -> - make (constrs, constrlists, List.flatten v::binders) tl) - | ETPattern -> - failwith "Unexpected entry of type cases pattern") - | GramConstrListMark (n,b) :: tl -> - (* Rebuild expansions of ConstrList *) - let heads,constrs = List.chop n constrs in - let constrlists = - if b then (heads@List.hd constrlists)::List.tl constrlists - else heads::constrlists - in make (constrs, constrlists, binders) tl - in - make ([],[],[]) (List.rev pil) - -let check_cases_pattern_env loc (env,envlist,hasbinders) = - if hasbinders then Topconstr.error_invalid_pattern_notation loc - else (env,envlist) - -let make_cases_pattern_action - (f : Loc.t -> cases_pattern_notation_substitution -> cases_pattern_expr) pil = - let rec make (env,envlist,hasbinders as fullenv) = function - | [] -> - Gram.action - (fun (loc:CompatLoc.t) -> - let loc = !@loc in - f loc (check_cases_pattern_env loc fullenv)) - | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl -> - (* parse a non-binding item *) - Gram.action (fun _ -> make fullenv tl) - | GramConstrNonTerminal (typ, Some _) :: tl -> - (* parse a binding non-terminal *) - (match typ with - | ETConstr _ -> (* pattern non-terminal *) - Gram.action (fun (v:cases_pattern_expr) -> - make (v::env, envlist, hasbinders) tl) - | ETReference -> - Gram.action (fun (v:reference) -> - make (CPatAtom (Loc.ghost,Some v) :: env, envlist, hasbinders) tl) - | ETName -> - Gram.action (fun (na:Loc.t * Name.t) -> - make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl) - | ETBigint -> - Gram.action (fun (v:Bigint.bigint) -> - make (CPatPrim (Loc.ghost,Numeral v) :: env, envlist, hasbinders) tl) - | ETConstrList (_,_) -> - Gram.action (fun (vl:cases_pattern_expr list) -> - make (env, vl :: envlist, hasbinders) tl) - | ETBinder _ | ETBinderList (true,_) -> - Gram.action (fun (v:local_binder list) -> - make (env, envlist, hasbinders) tl) - | ETBinderList (false,_) -> - Gram.action (fun (v:local_binder list list) -> - make (env, envlist, true) tl) - | (ETPattern | ETOther _) -> - anomaly (Pp.str "Unexpected entry of type cases pattern or other")) - | GramConstrListMark (n,b) :: tl -> - (* Rebuild expansions of ConstrList *) - let heads,env = List.chop n env in - if b then - make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl - else - make (env,heads::envlist,hasbinders) tl +type 'r env = { + constrs : 'r list; + constrlists : 'r list list; + binders : (local_binder list * bool) 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 -> push_constr subst (constr_expr_of_name v) + | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) + end +| TTBinder -> { subst with binders = (v, true) :: subst.binders } +| TTBinderListT -> { subst with binders = (v, true) :: subst.binders } +| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } +| TTBigint -> + begin match forpat with + | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v)) + | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v)) + end +| TTReference -> + begin match forpat with + | ForConstr -> push_constr subst (CRef (v, None)) + | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, 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 * ('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, rem) -> + fun f env -> + let heads, constrs = List.chop n env.constrs in + let constrlists = + if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists + else heads :: env.constrlists + 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) :: rem -> + let AnyTyRule r = make_ty_rule rem in + AnyTyRule (TyMark (n, b, r)) in - make ([],[],false) (List.rev pil) - -let rec make_constr_prod_item assoc from forpat = function - | GramConstrTerminal tok :: l -> - gram_token_of_token tok :: make_constr_prod_item assoc from forpat l - | GramConstrNonTerminal (nt, ovar) :: l -> - symbol_of_constr_prod_entry_key assoc from forpat nt - :: make_constr_prod_item assoc from forpat l - | GramConstrListMark _ :: l -> - make_constr_prod_item assoc from forpat l - | [] -> - [] + 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 grammar_extend Constr.pattern reinit empty - else grammar_extend Constr.operconstr reinit empty - -let pure_sublevels level symbs = - let filter s = - try - let i = level_of_snterml s in - begin match level with - | Some j when Int.equal i j -> None - | _ -> Some i - end - with Failure _ -> None - in - List.map_filter filter symbs - -let extend_constr (entry,level) (n,assoc) mkact forpat rules = - List.fold_left (fun nb pt -> - let symbs = make_constr_prod_item assoc n forpat pt in - let pure_sublevels = pure_sublevels level symbs in - let needed_levels = register_empty_levels forpat pure_sublevels in - let pos,p4assoc,name,reinit = find_position forpat assoc level in - let nb_decls = List.length needed_levels + 1 in - List.iter (prepare_empty_levels forpat) needed_levels; - unsafe_grammar_extend entry reinit (Option.map of_coq_position pos, - [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]); - nb_decls) 0 rules + 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, List.map fst env.binders) in + CNotation (loc, notation , env) +| ForPattern -> fun notation loc env -> + let invalid = List.exists (fun (_, b) -> not b) env.binders in + let () = if invalid then Topconstr.error_invalid_pattern_notation loc in + let env = (env.constrs, env.constrlists) in + CPatNotation (loc, notation, env, []) type notation_grammar = { notgram_level : int; @@ -201,106 +452,51 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -let extend_constr_constr_notation ng = - let level = ng.notgram_level in - let mkact loc env = CNotation (loc, ng.notgram_notation, env) in - let e = interp_constr_entry_key false level in - let ext = (ETConstr (level, ()), ng.notgram_assoc) in - extend_constr e ext (make_constr_action mkact) false ng.notgram_prods - -let extend_constr_pat_notation ng = - let level = ng.notgram_level in - let mkact loc env = CPatNotation (loc, ng.notgram_notation, env, []) in - let e = interp_constr_entry_key true level in - let ext = ETConstr (level, ()), ng.notgram_assoc in - extend_constr e ext (make_cases_pattern_action mkact) true ng.notgram_prods - -let extend_constr_notation (_, ng) = - (* Add the notation in constr *) - let nb = extend_constr_constr_notation ng in - (* Add the notation in cases_pattern *) - let nb' = extend_constr_pat_notation ng in - nb + nb' - -module GrammarCommand = Dyn.Make(struct end) -module GrammarInterp = struct type 'a t = 'a -> int end -module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) - -let grammar_interp = ref GrammarInterpMap.empty - -let (grammar_state : (int * GrammarCommand.t) list ref) = ref [] - -type 'a grammar_command = 'a GrammarCommand.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 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 nb_decls = List.length needed_levels + 1 in + let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in + let empty = { constrs = []; constrlists = []; binders = [] } 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 extend_grammar tag g = - let nb = GrammarInterpMap.find tag !grammar_interp g in - grammar_state := (nb, GrammarCommand.Dyn (tag, g)) :: !grammar_state +let constr_levels = GramState.field () -let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar tag g +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 : (Notation.level * notation_grammar) GrammarCommand.tag = +let constr_grammar : (Notation.level * notation_grammar) grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar constr_grammar (pr, ntn) +let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) let recover_constr_grammar ntn prec = - let filter (_, gram) : notation_grammar option = match gram with - | GrammarCommand.Dyn (tag, obj) -> - match GrammarCommand.eq tag constr_grammar with - | None -> None - | Some Refl -> - let (prec', ng) = obj in - if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng - else None + let filter (prec', ng) = + if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng + else None in - match List.map_filter filter !grammar_state with + match List.map_filter filter (recover_grammar_command constr_grammar) with | [x] -> x | _ -> assert false - -(* 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) list * CLexer.frozen_t - -let freeze _ : frozen_t = (!grammar_state, CLexer.freeze ()) - -(* 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 unfreeze (grams, lex) = - let (undo, redo, common) = factorize_grams !grammar_state grams in - let n = number_of_entries undo in - remove_grammars n; - remove_levels n; - grammar_state := common; - CLexer.unfreeze lex; - List.iter extend_dyn_grammar (List.rev_map snd redo) - -(** No need to provide an init function : the grammar state is - statically available, and already empty initially, while - the lexer state should not be resetted, since it contains - keywords declared in g_*.ml4 *) - -let _ = - Summary.declare_summary "GRAMMAR_LEXER" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = Summary.nop } - -let with_grammar_rule_protection f x = - let fs = freeze false in - try let a = f x in unfreeze fs; a - with reraise -> - let reraise = Errors.push reraise in - let () = unfreeze fs in - iraise reraise diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 6ec1066260..1fe06a29df 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -36,20 +36,6 @@ type notation_grammar = { notgram_typs : notation_var_internalization_type list; } -(** {5 Extending the parser with Summary-synchronized commands} *) - -type 'a grammar_command -(** Type of synchronized parsing extensions. The ['a] type should be - marshallable. *) - -val create_grammar_command : string -> ('a -> int) -> 'a grammar_command -(** Create a new grammar-modifying command with the given name. The function - should modify the parser state and return the number of grammar extensions - performed. *) - -val extend_grammar : 'a grammar_command -> 'a -> unit -(** Extend the grammar of Coq with the given data. *) - (** {5 Adding notations} *) val extend_constr_grammar : Notation.level -> notation_grammar -> unit @@ -58,5 +44,3 @@ val extend_constr_grammar : Notation.level -> notation_grammar -> unit val recover_constr_grammar : notation -> Notation.level -> notation_grammar (** For a declared grammar, returns the rule + the ordered entry types of variables in the rule (for use in the interpretation) *) - -val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b diff --git a/parsing/entry.ml b/parsing/entry.ml deleted file mode 100644 index b7c6c23fa6..0000000000 --- a/parsing/entry.ml +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Errors -open Util - -type 'a t = string - -(** Entries are registered with a unique name *) - -let entries = ref String.Set.empty - -let create name = - let () = - if String.Set.mem name !entries then - anomaly (Pp.str ("Entry " ^ name ^ " already defined")) - in - let () = entries := String.Set.add name !entries in - name - -let unsafe_of_name name = - assert (String.Set.mem name !entries); - name - -let repr s = s diff --git a/parsing/entry.mli b/parsing/entry.mli deleted file mode 100644 index 4c73fe2049..0000000000 --- a/parsing/entry.mli +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Typed grammar entries *) - -type 'a t -(** Typed grammar entries. We need to defined them here so that they are - marshallable and defined before the Pcoq.Gram module. They are basically - unique names. They should be kept synchronized with the {!Pcoq} entries. *) - -val create : string -> 'a t -(** Create an entry. They should be synchronized with the entries defined in - {!Pcoq}. *) - -(** {5 Meta-programming} *) - -val repr : 'a t -> string -val unsafe_of_name : string -> 'a t diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index b052b6ee6d..0e1c79c91b 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,7 +1,6 @@ Tok Compat CLexer -Entry Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 6dcf76da8c..efb89cd6e1 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -19,10 +19,19 @@ module G = GrammarMake (CLexer) let warning_verbose = Compat.warning_verbose -module Symbols = GramextMake(G) +let of_coq_assoc = function +| Extend.RightA -> CompatGramext.RightA +| Extend.LeftA -> CompatGramext.LeftA +| Extend.NonA -> CompatGramext.NonA + +let of_coq_position = function +| Extend.First -> CompatGramext.First +| Extend.Last -> CompatGramext.Last +| Extend.Before s -> CompatGramext.Before s +| Extend.After s -> CompatGramext.After s +| Extend.Level s -> CompatGramext.Level s -let gram_token_of_token = Symbols.stoken -let gram_token_of_string s = gram_token_of_token (CLexer.terminal s) +module Symbols = GramextMake(G) let camlp4_verbosity silent f x = let a = !warning_verbose in @@ -32,26 +41,6 @@ let camlp4_verbosity silent f x = let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x - -(** [grammar_object] is the superclass of all grammar entries *) - -module type Gramobj = -sig - type grammar_object - val weaken_entry : 'a G.entry -> grammar_object G.entry -end - -module Gramobj : Gramobj = -struct - type grammar_object = Obj.t - let weaken_entry e = Obj.magic e -end - -(** Grammar entries with associated types *) - -type grammar_object = Gramobj.grammar_object -let weaken_entry x = Gramobj.weaken_entry x - (** Grammar extensions *) (** NB: [extend_statment = @@ -63,14 +52,57 @@ let weaken_entry x = Gramobj.weaken_entry x In [single_extend_statement], first two parameters are name and assoc iff a level is created *) +(** Binding general entry keys to symbol *) + +let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function +| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc)) +| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) + +let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function + | Atoken t -> Symbols.stoken t + | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) + | Aself -> Symbols.sself + | Anext -> Symbols.snext + | Aentry e -> + Symbols.snterm (G.Entry.obj e) + | Aentryl (e, n) -> + Symbols.snterml (G.Entry.obj e, string_of_int n) + | Arules rs -> + G.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 +| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) + +and symbol_of_rules : type a. a Extend.rules -> _ = function +| Rules (r, act) -> + let symb = symbol_of_rule r.norec_rule [] in + let act = of_coq_action r.norec_rule act in + (symb, act) + +let of_coq_production_rule : type a. a Extend.production_rule -> _ = function +| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) + +let of_coq_single_extend_statement (lvl, assoc, rule) = + (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) + +let of_coq_extend_statement (pos, st) = + (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) + (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position +type extend_rule = +| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule + type ext_kind = - | ByGrammar of - grammar_object G.entry - * gram_reinit option (** for reinitialization if ever needed *) - * G.extend_statment + | ByGrammar of extend_rule | ByEXTEND of (unit -> unit) * (unit -> unit) (** The list of extensions *) @@ -86,13 +118,28 @@ let grammar_delete e reinit (pos,rls) = (List.rev rls); match reinit with | Some (a,ext) -> - let lev = match Option.map Compat.to_coq_position pos with - | Some (Level n) -> n + let a = of_coq_assoc a in + let ext = of_coq_position ext in + let lev = match pos with + | Some (CompatGramext.Level n) -> n | _ -> assert false in maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) | None -> () +(** Extension *) + +let grammar_extend e reinit ext = + let ext = of_coq_extend_statement ext in + let undo () = grammar_delete e reinit ext in + let redo () = camlp4_verbose (maybe_uncurry (G.extend e)) ext in + camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + redo () + +let grammar_extend_sync e reinit ext = + camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; + camlp4_verbose (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext) + (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -119,12 +166,6 @@ module Gram = G.delete_rule e pil end -(** This extension command is used by the Grammar constr *) - -let unsafe_grammar_extend e reinit ext = - camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state; - camlp4_verbose (maybe_uncurry (G.extend e)) ext - (** Remove extensions [n] is the number of extended entries (not the number of Grammar commands!) @@ -134,9 +175,8 @@ let rec remove_grammars n = if n>0 then (match !camlp4_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") - | ByGrammar(g,reinit,ext)::t -> - let f (a,b) = (of_coq_assoc a, of_coq_position b) in - grammar_delete g (Option.map f reinit) ext; + | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> + grammar_delete g reinit (of_coq_extend_statement ext); camlp4_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -188,21 +228,9 @@ let get_univ u = if Hashtbl.mem utables u then u else raise Not_found -(** A table associating grammar to entries *) -let gtable : Obj.t Gram.entry String.Map.t ref = ref String.Map.empty - -let get_grammar (e : 'a Entry.t) : 'a Gram.entry = - Obj.magic (String.Map.find (Entry.repr e) !gtable) - -let set_grammar (e : 'a Entry.t) (g : 'a Gram.entry) = - assert (not (String.Map.mem (Entry.repr e) !gtable)); - gtable := String.Map.add (Entry.repr e) (Obj.magic g) !gtable - let new_entry u s = let ename = u ^ ":" ^ s in - let entry = Entry.create ename in let e = Gram.entry_create ename in - let () = set_grammar entry e in e let make_gen_entry u s = new_entry u s @@ -374,344 +402,97 @@ let main_entry = Vernac_.main_entry let set_command_entry e = Vernac_.command_entry_ref := e let get_command_entry () = !Vernac_.command_entry_ref -(**********************************************************************) -(* This determines (depending on the associativity of the current - level and on the expected associativity) if a reference to constr_n is - a reference to the current level (to be translated into "SELF" on the - left border and into "constr LEVEL n" elsewhere), to the level below - (to be translated into "NEXT") or to an below wrt associativity (to be - translated in camlp4 into "constr" without level) or to another level - (to be translated into "constr LEVEL n") - - The boolean is true if the entry was existing _and_ empty; this to - circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the - converse of the extension mechanism *) - -let constr_level = string_of_int - -let default_levels = - [200,Extend.RightA,false; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 10,Extend.RightA,false; - 9,Extend.RightA,false; - 8,Extend.RightA,true; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let default_pattern_levels = - [200,Extend.RightA,true; - 100,Extend.RightA,false; - 99,Extend.RightA,true; - 11,Extend.LeftA,false; - 10,Extend.RightA,false; - 1,Extend.LeftA,false; - 0,Extend.RightA,false] - -let level_stack = - ref [(default_levels, default_pattern_levels)] - -(* At a same level, LeftA takes precedence over RightA and NoneA *) -(* In case, several associativity exists for a level, we make two levels, *) -(* first LeftA, then RightA and NoneA together *) - -let admissible_assoc = function - | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> 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 pr_assoc = function - | Extend.LeftA -> str "left" - | Extend.RightA -> str "right" - | Extend.NonA -> str "non" in - errorlabstrm "" - (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 forpat ensure assoc lev = - let ccurrent,pcurrent as current = List.hd !level_stack in - match lev with - | None -> - level_stack := current :: !level_stack; - 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 = - if forpat then (ccurrent, add_level None pcurrent) - else (add_level None ccurrent, pcurrent) in - level_stack := updated:: !level_stack; - let assoc = create_assoc assoc in - begin match !init with - | None -> - (* Create the entry *) - Some (create_pos !after), Some assoc, Some (constr_level n), None - | _ -> - (* The reinit flag has been updated *) - Some (Extend.Level (constr_level n)), None, None, !init - end - with - (* Nothing has changed *) - Exit -> - level_stack := current :: !level_stack; - (* Just inherit the existing associativity and name (None) *) - Some (Extend.Level (constr_level n)), None, None, None - -let remove_levels n = - level_stack := List.skipn n !level_stack - -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 forpat levels = - let filter n = - try - let levels = (if forpat then snd else fst) (List.hd !level_stack) in - if not (list_mem_assoc_triple n levels) then - Some (find_position_gen forpat true None (Some n)) - else None - with Failure _ -> None - in - List.map_filter filter levels - -let find_position forpat assoc level = - find_position_gen forpat false assoc level - -(* Synchronise the stack of level updates *) -let synchronize_level_positions () = - let _ = find_position true None None in () - -(**********************************************************************) -(* Binding constr entry keys to entries *) - -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function - | Some Extend.NonA | Some Extend.RightA -> Extend.RightA - | None | Some Extend.LeftA -> Extend.LeftA - -let assoc_eq al ar = match al, ar with -| Extend.NonA, Extend.NonA -| Extend.RightA, Extend.RightA -| Extend.LeftA, Extend.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 (Extend.NonA|Extend.LeftA))) -> - Some None - (* If RightA on the right-hand side, set to the explicit (current) level *) - | (NumLevel n,BorderProd (Right,Some Extend.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 Extend.NonA)) -> None - (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_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 - | Extend.LeftA -> Some (Some (n, true)) - | _ -> Some None - end - (* None means NEXT *) - | (NextLevel,_) -> Some None -(* Compute production name elsewhere *) - | (NumLevel n,InternalProd) -> - match from with - | ETConstr (p,()) when Int.equal p (n + 1) -> Some None - | ETConstr (p,()) -> Some (Some (n, Int.equal n p)) - | _ -> Some (Some (n,false)) - -let compute_entry adjust forpat = function - | ETConstr (n,q) -> - (if forpat then weaken_entry Constr.pattern - else weaken_entry Constr.operconstr), - adjust (n,q), false - | ETName -> weaken_entry Prim.name, None, false - | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") - | ETBinder false -> weaken_entry Constr.binder, None, false - | ETBinderList (true,tkl) -> - let () = match tkl with [] -> () | _ -> assert false in - weaken_entry Constr.open_binders, None, false - | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.") - | ETBigint -> weaken_entry Prim.bigint, None, false - | ETReference -> weaken_entry Constr.global, None, false - | ETPattern -> weaken_entry Constr.pattern, None, false - | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") - | ETOther (u,n) -> assert false - -(* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key forpat level = - if level = 200 && not forpat then weaken_entry Constr.binder_constr, None - else if forpat then weaken_entry Constr.pattern, Some level - else weaken_entry Constr.operconstr, Some level - -(* This computes the name to give to a production knowing the name and - associativity of the level where it must be added *) -let interp_constr_prod_entry_key ass from forpat en = - compute_entry (adjust_level ass from) forpat en - -(**********************************************************************) -(* Binding constr entry keys to symbols *) - -let is_self from e = - match from, e with - ETConstr(n,()), ETConstr(NumLevel n', - BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false - | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> Int.equal n n' - | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint - | ETPattern, ETPattern) -> true - | ETOther(s1,s2), ETOther(s1',s2') -> - String.equal s1 s1' && String.equal s2 s2' - | _ -> false - -let is_binder_level from e = - match from, e with - ETConstr(200,()), - ETConstr(NumLevel 200,(BorderProd(Right,_)|InternalProd)) -> true - | _ -> false - -let make_sep_rules tkl = - Gram.srules' - [List.map gram_token_of_token tkl, - List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl - (Gram.action (fun loc -> ()))] - -let rec symbol_of_constr_prod_entry_key assoc from forpat typ = - if is_binder_level from typ then - if forpat then - Symbols.snterml (Gram.Entry.obj Constr.pattern,"200") - else - Symbols.snterml (Gram.Entry.obj Constr.operconstr,"200") - else if is_self from typ then - Symbols.sself - else - match typ with - | ETConstrList (typ',[]) -> - Symbols.slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) - | ETConstrList (typ',tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - make_sep_rules tkl) - | ETBinderList (false,[]) -> - Symbols.slist1 - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) - | ETBinderList (false,tkl) -> - Symbols.slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), - make_sep_rules tkl) - - | _ -> - match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> Symbols.snterm (Gram.Entry.obj eobj) - | (eobj,Some None,_) -> Symbols.snext - | (eobj,Some (Some (lev,cur)),_) -> - Symbols.snterml (Gram.Entry.obj eobj,constr_level lev) - -(** Binding general entry keys to symbol *) - -let tuplify l = - List.fold_left (fun accu x -> Obj.repr (x, accu)) (Obj.repr ()) l - -let rec adj : type a b c. (a, b, Loc.t -> Loc.t * c) adj -> _ = function -| Adj0 -> Obj.magic (fun accu f loc -> f (Obj.repr (to_coqloc loc, tuplify accu))) -| AdjS e -> Obj.magic (fun accu f x -> adj e (x :: accu) f) - -let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function - | Atoken t -> Symbols.stoken t - | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) - | Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s, gram_token_of_string sep) - | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) - | Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s, gram_token_of_string sep) - | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) - | Aself -> Symbols.sself - | Anext -> Symbols.snext - | Aentry e -> - let e = get_grammar e in - Symbols.snterm (Gram.Entry.obj (weaken_entry e)) - | Aentryl (e, n) -> - let e = get_grammar e in - Symbols.snterml (Gram.Entry.obj (weaken_entry e), string_of_int n) - | Arules rs -> Gram.srules' (symbol_of_rules rs [] (fun x -> I0 x)) - -and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function -| Stop -> fun accu -> accu -| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) +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 () = maybe_uncurry (G.extend entry) ext in + try Some (parse_string entry "") with _ -> None -and symbol_of_rules : type a. a Extend.rules -> _ = function -| Rule0 -> fun accu _ -> accu -| RuleS (r, e, rs) -> fun accu f -> - let symb = symbol_of_rule r [] in - let act = adj e [] f in - symbol_of_rules rs ((symb, act) :: accu) (fun x -> IS (f x)) +(** Synchronized grammar extensions *) -let level_of_snterml e = int_of_string (Symbols.snterml_level e) +module GramState = Store.Make(struct end) -let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> Gram.action = function -| Stop -> fun f -> Gram.action (fun loc -> f (to_coqloc loc)) -| Next (r, _) -> fun f -> Gram.action (fun x -> of_coq_action r (f x)) +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t -let of_coq_production_rule : type a. a Extend.production_rule -> _ = function -| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) +module GrammarCommand = Dyn.Make(struct end) +module GrammarInterp = struct type 'a t = 'a grammar_extension end +module GrammarInterpMap = GrammarCommand.Map(GrammarInterp) -let of_coq_single_extend_statement (lvl, assoc, rule) = - (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) +let grammar_interp = ref GrammarInterpMap.empty -let of_coq_extend_statement (pos, st) = - (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) - -let grammar_extend e reinit ext = - let ext = of_coq_extend_statement ext in - unsafe_grammar_extend e reinit ext +let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref [] -let name_of_entry e = Entry.unsafe_of_name (Gram.Entry.name e) +type 'a grammar_command = 'a GrammarCommand.tag -let list_entry_names () = [] +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 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 () = maybe_uncurry (Gram.extend entry) ext in - try Some (parse_string entry "") with _ -> None +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 + 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 + +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 + in + List.map_filter filter !grammar_stack + +let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g + +(* 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.frozen_t + +let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ()) + +(* 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 unfreeze (grams, lex) = + let (undo, redo, common) = factorize_grams !grammar_stack grams in + let n = number_of_entries undo in + remove_grammars n; + grammar_stack := common; + CLexer.unfreeze lex; + List.iter extend_dyn_grammar (List.rev_map pi2 redo) + +(** No need to provide an init function : the grammar state is + statically available, and already empty initially, while + the lexer state should not be resetted, since it contains + keywords declared in g_*.ml4 *) + +let _ = + Summary.declare_summary "GRAMMAR_LEXER" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = Summary.nop } + +let with_grammar_rule_protection f x = + let fs = freeze false in + try let a = f x in unfreeze fs; a + with reraise -> + let reraise = Errors.push reraise in + let () = unfreeze fs in + iraise reraise (** Registering grammar of generic arguments *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index d320520015..319ca256e1 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -19,7 +19,7 @@ open Genredexpr (** The parser of Coq *) -module Gram : Compat.GrammarSig +module Gram : module type of Compat.GrammarMake(CLexer) (** The parser of Coq is built from three kinds of rule declarations: @@ -96,36 +96,6 @@ module Gram : Compat.GrammarSig *) -val gram_token_of_token : Tok.t -> Gram.symbol -val gram_token_of_string : string -> Gram.symbol - -(** The superclass of all grammar entries *) -type grammar_object - -(** Type of reinitialization data *) -type gram_reinit = gram_assoc * gram_position - -(** General entry keys *) - -(** This intermediate abstract representation of entries can - both be reified into mlexpr for the ML extensions and - dynamically interpreted as entries for the Coq level extensions -*) - -(** Add one extension at some camlp4 position of some camlp4 entry *) -val unsafe_grammar_extend : - grammar_object Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - Gram.extend_statment -> unit - -val grammar_extend : - 'a Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - 'a Extend.extend_statment -> unit - -(** Remove the last n extensions *) -val remove_grammars : int -> unit - (** Temporary activate camlp4 verbosity *) val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit @@ -145,7 +115,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry @@ -251,40 +220,45 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry val get_command_entry : unit -> vernac_expr Gram.entry val set_command_entry : vernac_expr Gram.entry -> unit -(** Mapping formal entries into concrete ones *) - -(** Binding constr entry keys to entries and symbols *) +val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option -val interp_constr_entry_key : bool (** true for cases_pattern *) -> - int -> grammar_object Gram.entry * int option +(** {5 Extending the parser without synchronization} *) -val symbol_of_constr_prod_entry_key : gram_assoc option -> - constr_entry_key -> bool -> constr_prod_entry_key -> - Gram.symbol +type gram_reinit = gram_assoc * gram_position +(** Type of reinitialization data *) -val name_of_entry : 'a Gram.entry -> 'a Entry.t +val grammar_extend : 'a Gram.entry -> gram_reinit option -> + 'a Extend.extend_statment -> unit +(** Extend the grammar of Coq, without synchronizing it with the bactracking + mechanism. This means that grammar extensions defined this way will survive + an undo. *) -val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option +(** {5 Extending the parser with summary-synchronized commands} *) -(** Binding general entry keys to symbols *) +module GramState : Store.S +(** Auxilliary state of the grammar. Any added data must be marshallable. *) -(** Recover the list of all known tactic notation entries. *) -val list_entry_names : unit -> (string * argument_type) list +type 'a grammar_command +(** Type of synchronized parsing extensions. The ['a] type should be + marshallable. *) -(** Registering/resetting the level of a constr entry *) +type extend_rule = +| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule -val find_position : - bool (** true if for creation in pattern entry; false if in constr entry *) -> - Extend.gram_assoc option -> int option -> - Extend.gram_position option * Extend.gram_assoc option * string option * - (** for reinitialization: *) gram_reinit option +type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t +(** Grammar extension entry point. Given some ['a] and a current grammar state, + such a function must produce the list of grammar extensions that will be + applied in the same order and kept synchronized w.r.t. the summary, together + with a new state. It should be pure. *) -val synchronize_level_positions : unit -> unit +val create_grammar_command : string -> 'a grammar_extension -> 'a grammar_command +(** Create a new grammar-modifying command with the given name. The extension + function is called to generate the rules for a given data. *) -val register_empty_levels : bool -> int list -> - (Extend.gram_position option * Extend.gram_assoc option * - string option * gram_reinit option) list +val extend_grammar_command : 'a grammar_command -> 'a -> unit +(** Extend the grammar of Coq with the given data. *) -val remove_levels : int -> unit +val recover_grammar_command : 'a grammar_command -> 'a list +(** Recover the current stack of grammar extensions. *) -val level_of_snterml : Gram.symbol -> int +val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b |