From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- parsing/egramcoq.ml | 163 +++++++++++++++++++++++++++------------------------- 1 file changed, 84 insertions(+), 79 deletions(-) (limited to 'parsing/egramcoq.ml') diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a292c746..5f63d21c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -1,16 +1,17 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* str "left" | Extend.RightA -> str "right" | Extend.NonA -> str "non" in - errorlabstrm "" + 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.") @@ -80,10 +82,6 @@ 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 -> @@ -148,11 +146,11 @@ let find_position accu forpat assoc level = (**************************************************************************) (* - * --- Note on the mapping of grammar productions to camlp4 actions --- + * --- 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 camlp4 conventions): + * 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, @@ -176,8 +174,8 @@ let find_position accu forpat assoc level = (**********************************************************************) (* Binding constr entry keys to entries *) -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function +(* 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 @@ -209,7 +207,7 @@ let adjust_level assoc from = function (* 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) -> + | (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)) -> @@ -230,14 +228,14 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = -| TTName : ('self, Name.t Loc.located) entry +| TTName : ('self, Misctypes.lname) entry | TTReference : ('self, reference) entry -| TTBigint : ('self, Bigint.bigint) entry -| TTBinder : ('self, local_binder list) 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 -| TTBinderListT : ('self, local_binder list) entry -| TTBinderListF : Tok.t list -> ('self, local_binder list 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 @@ -262,9 +260,11 @@ 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) +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 @@ -291,40 +291,34 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as 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) +| 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 -| TTBinder -> Aentry Constr.binder -| TTBinderListT -> Aentry Constr.open_binders +| TTOpenBinderList -> 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) - -let cases_pattern_expr_of_name (loc,na) = match na with - | Anonymous -> CPatAtom (loc,None) - | Name id -> CPatAtom (loc,Some (Ident (loc,id))) +| 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 : (local_binder list * bool) list; + binders : cases_pattern_expr list; + binderlists : local_binder_expr list list; } let push_constr subst v = { subst with constrs = v :: subst.constrs } @@ -334,21 +328,25 @@ match e with | TTConstr _ -> push_constr subst v | TTName -> begin match forpat with - | ForConstr -> push_constr subst (constr_expr_of_name v) + | ForConstr -> { subst with binders = cases_pattern_expr_of_name v :: subst.binders } | 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 } +| 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 (CPrim (Loc.ghost, Numeral v)) - | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v)) + | 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 (CRef (v, None)) - | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v)) + | 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 } @@ -359,7 +357,7 @@ type (_, _) 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 +| TyMark : int * bool * int * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule type 'r gen_eval = Loc.t -> 'r env -> 'r @@ -373,18 +371,27 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s 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) -> +| TyMark (n, b, p, 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 + 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 +| TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) | TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) @@ -403,9 +410,9 @@ let make_ty_rule assoc from forpat prods = 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 -> + | GramConstrListMark (n, b, p) :: rem -> let AnyTyRule r = make_ty_rule rem in - AnyTyRule (TyMark (n, b, r)) + AnyTyRule (TyMark (n, b, p, r)) in make_ty_rule (List.rev prods) @@ -430,16 +437,14 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = 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) + let env = (env.constrs, env.constrlists, env.binders, env.binderlists) in + CAst.make ~loc @@ CNotation (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, []) + CAst.make ~loc @@ CPatNotation (notation, env, []) let extend_constr state forpat ng = - let n = ng.notgram_level in + 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 = @@ -450,7 +455,7 @@ let extend_constr state forpat ng = 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 = [] } 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 @@ -460,7 +465,7 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () -let extend_constr_notation (_, ng) state = +let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> default_constr_levels | Some lev -> lev @@ -472,7 +477,7 @@ let extend_constr_notation (_, ng) state = let state = GramState.set state constr_levels levels in (r @ r', state) -let constr_grammar : (Notation.level * notation_grammar) grammar_command = +let constr_grammar : one_notation_grammar grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) +let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn -- cgit v1.2.3