diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 9416bff2..825d1af0 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: egrammar.ml 10987 2008-05-26 12:28:36Z herbelin $ *) +(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -114,27 +114,33 @@ let make_constr_prod_item univ assoc from forpat = function let prepare_empty_levels entry (pos,p4assoc,name,reinit) = grammar_extend entry pos reinit [(name, p4assoc, [])] -let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) = +let pure_sublevels level symbs = + map_succeed (function + | Gramext.Snterml (_,n) when Some (int_of_string n) <> level -> + int_of_string n + | _ -> + failwith "") symbs + +let extend_constr (entry,level) (n,assoc) mkact forpat pt = let univ = get_univ "constr" in let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in let (symbs,ntl) = List.split pil in - let needed_levels = register_empty_levels forpat symbs 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 List.iter (prepare_empty_levels entry) needed_levels; grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])] let extend_constr_notation (n,assoc,ntn,rule) = (* Add the notation in constr *) let mkact loc env = CNotation (loc,ntn,List.map snd env) in - let (e,level) = get_constr_entry false (ETConstr (n,())) in - let pos,p4assoc,name,reinit = find_position false assoc level in - extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit) - (make_constr_action mkact) (false,rule); + let e = get_constr_entry false (ETConstr (n,())) in + extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule; (* Add the notation in cases_pattern *) let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in - let (e,level) = get_constr_entry true (ETConstr (n,())) in - let pos,p4assoc,name,reinit = find_position true assoc level in - extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit) - (make_cases_pattern_action mkact) (true,rule) + let e = get_constr_entry true (ETConstr (n,())) in + extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) + true rule (**********************************************************************) (** Making generic actions in type generic_argument *) @@ -228,7 +234,7 @@ let rec interp_entry_name up_level s = try get_entry (get_univ "prim") s with _ -> try get_entry (get_univ "constr") s - with _ -> error ("Unknown entry "^s) + with _ -> error ("Unknown entry "^s^".") in let o = object_of_typed_entry e in let t = type_of_typed_entry e in @@ -248,7 +254,7 @@ let get_tactic_entry n = else if 1<=n && n<5 then weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n)) else - error ("Invalid Tactic Notation level: "^(string_of_int n)) + error ("Invalid Tactic Notation level: "^(string_of_int n)^".") (* Declaration of the tactic grammar rule *) @@ -261,7 +267,7 @@ let add_tactic_entry (key,lev,prods,tac) = let rules = if lev = 0 then begin if not (head_is_ident prods) then - error "Notation for simple tactic must start with an identifier"; + error "Notation for simple tactic must start with an identifier."; let mkact s tac loc l = (TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in make_rule univ (mkact key tac) mkprod prods |