From 6b2a56097a596638d2b297bd78534b2e7506e206 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 6 Nov 2014 11:11:33 +0100 Subject: Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels) by hopefully computing the right position where to reinit an empty level. Also removing obsolete comment. --- parsing/pcoq.ml4 | 42 ++++++++++++++++++------------------------ 1 file changed, 18 insertions(+), 24 deletions(-) (limited to 'parsing/pcoq.ml4') diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 64a705c2c..f290d903d 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -135,10 +135,13 @@ open Gramtypes In [single_extend_statement], first two parameters are name and assoc iff a level is created *) +(** Type of reinitialization data *) +type gram_reinit = gram_assoc * gram_position + type ext_kind = | ByGrammar of grammar_object G.entry - * gram_assoc option (** for reinitialization if ever needed *) + * gram_reinit option (** for reinitialization if ever needed *) * G.extend_statment | ByEXTEND of (unit -> unit) * (unit -> unit) @@ -146,28 +149,18 @@ type ext_kind = let camlp4_state = ref [] -(** Deletion - - Caveat: deletion is not the converse of extension: when an - empty level is extended, deletion removes the level instead - of keeping it empty. This has an effect on the empty levels 8, - 99 and 200. We didn't find a good solution to this problem - (e.g. using G.extend to know if the level exists results in a - printed error message as side effect). As a consequence an - extension at 99 or 8 (and for pattern 200 too) inside a section - corrupts the parser. *) +(** Deletion *) let grammar_delete e reinit (pos,rls) = List.iter (fun (n,ass,lev) -> List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) (List.rev rls); - if reinit != None then + match reinit with + | Some (a,ext) -> let lev = match pos with Some (Level n) -> n | _ -> assert false in - let pos = match lev with - | "200" -> First - | _ -> After (string_of_int (int_of_string lev + 1)) in - maybe_uncurry (G.extend e) (Some pos, [Some lev,reinit,[]]) + maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]]) + | None -> () (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -211,7 +204,8 @@ let rec remove_grammars n = (match !camlp4_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") | ByGrammar(g,reinit,ext)::t -> - grammar_delete g (Option.map of_coq_assoc reinit) ext; + let f (a,b) = (of_coq_assoc a, of_coq_position b) in + grammar_delete g (Option.map f reinit) ext; camlp4_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> @@ -494,6 +488,10 @@ let error_level_assoc p current expected = 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 @@ -507,7 +505,8 @@ let find_position_gen forpat ensure assoc lev = | (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'; (p,a',false)::l) + 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 @@ -523,12 +522,7 @@ let find_position_gen forpat ensure assoc lev = begin match !init with | None -> (* Create the entry *) - let ext = match !after with - | None -> Some Extend.First - | _ -> - Some (Extend.After (constr_level (Option.get !after))) - in - ext, Some assoc, Some (constr_level n), None + 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 -- cgit v1.2.3