From 981fc313f34918b7e0ac2fe449c0d947a13d20f5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 28 Nov 2002 23:12:40 +0000 Subject: Affinement de la gestion des niveaux toujours; type ETBigint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3334 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/egrammar.ml | 84 ++++++++++++++++++++++++++------------------------ parsing/extend.ml | 17 +++++----- parsing/extend.mli | 2 +- toplevel/metasyntax.ml | 36 ++++++++++------------ 4 files changed, 69 insertions(+), 70 deletions(-) diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index a7cfcc591e..f294f70799 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -37,49 +37,46 @@ let (grammar_state : all_grammar_command list ref) = ref [] (**************************************************************************) -let canonise_assoc = function - | None -> Gramext.LeftA (* camlp4 rule *) - | Some Gramext.NonA -> Gramext.RightA - | Some a -> a - let assoc_level = function | Gramext.LeftA -> "L" | _ -> "" -let constr_level assoc = function - | 8 -> assert (assoc <> Some Gramext.LeftA); "top" - | n -> (string_of_int n)^(assoc_level (canonise_assoc assoc)) +let constr_level = function + | 8,assoc -> assert (assoc <> Gramext.LeftA); "top" + | n,assoc -> (string_of_int n)^(assoc_level assoc) let constr_prod_level = function | 8 -> "top" | n -> string_of_int n let numeric_levels = - ref [8,Some Gramext.RightA; 1,Some Gramext.RightA; 0,Some Gramext.RightA] + ref [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA] (* 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 *) -exception Found of Gramext.g_assoc option +exception Found of Gramext.g_assoc + +open Ppextend -let eq_assoc a b = match (canonise_assoc a, canonise_assoc b) with - | Gramext.LeftA, Gramext.LeftA -> true - | Gramext.LeftA, _ -> false - | _, Gramext.LeftA -> false +let admissible_assoc = function + | Gramext.LeftA, (Gramext.RightA | Gramext.NonA) -> false + | Gramext.RightA, Gramext.LeftA -> false | _ -> true - -let find_position assoc = function - | None -> None, Some (canonise_assoc assoc) + +let find_position other assoc = function + | None -> None, (if other then assoc else None), None | Some n -> - if n = 8 & canonise_assoc assoc = Gramext.LeftA then + let assoc = out_some assoc in + if n = 8 & assoc = Gramext.LeftA then error "Left associativity not allowed at level 8"; - let after = ref (8,Some Gramext.RightA) in + let after = ref (8,Gramext.RightA) in let rec add_level q = function | (p,_ as pa)::l when p > n -> pa :: add_level pa l | (p,a as pa)::l as l' when p = n -> - if eq_assoc a assoc then raise (Found a); + if admissible_assoc (a,assoc) then raise (Found a); (* Maybe this was (p,Left) and p occurs a second time *) - if canonise_assoc a = Gramext.LeftA then + if a = Gramext.LeftA then match l with | (p,a)::_ as l' when p = n -> raise (Found a) | _ -> after := pa; (n,assoc)::l' @@ -90,12 +87,14 @@ let find_position assoc = function after := q; (n,assoc)::l in try - numeric_levels := add_level (8,Some Gramext.RightA) !numeric_levels; - Some (Gramext.After (constr_level (snd !after) (fst !after))), - Some (canonise_assoc assoc) + (* Create the entry *) + numeric_levels := add_level (8,Gramext.RightA) !numeric_levels; + Some (Gramext.After (constr_level !after)), + Some assoc, Some (constr_level (n,assoc)) with - Found a -> Some (Gramext.Level (constr_level a n)), - Some (canonise_assoc a) + Found a -> + (* Just inherit the existing associativity and name (None) *) + Some (Gramext.Level (constr_level (n,a))), None, None (* Interpretation of the right hand side of grammar rules *) @@ -147,6 +146,9 @@ let make_act f pil = | Some (p, ETIdent) :: tl -> (* non-terminal *) Gramext.action (fun (v:identifier) -> make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) + | Some (p, ETBigint) :: tl -> (* non-terminal *) + Gramext.action (fun (v:Bignat.bigint) -> + make ((p,CNumeral (dummy_loc,v)) :: env) tl) | Some (p, ETPattern) :: tl -> failwith "Unexpected entry of type cases pattern" in make [] (List.rev pil) @@ -160,7 +162,10 @@ let make_cases_pattern_act f pil = | Some (p, ETPattern) :: tl -> (* non-terminal *) Gramext.action (fun v -> make ((p,v) :: env) tl) | Some (p, ETReference) :: tl -> (* non-terminal *) - Gramext.action (fun v -> make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl) + Gramext.action (fun v -> make ((p,CPatAtom(dummy_loc,Some v)) :: env) + tl) + | Some (p, ETBigint) :: tl -> (* non-terminal *) + Gramext.action (fun v -> make ((p,CPatNumeral(dummy_loc,v)) :: env) tl) | Some (p, (ETIdent | ETConstr _ | ETOther _)) :: tl -> error "ident and constr entry not admitted in patterns cases syntax extensions" in make [] (List.rev pil) @@ -210,17 +215,17 @@ let make_rule univ assoc etyp rule = (* Rules of a level are entered in reverse order, so that the first rules are applied before the last ones *) -let extend_entry univ (te, etyp, pos, name, ass, rls) = +let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) = let rules = List.rev (List.map (make_rule univ ass etyp) rls) in - grammar_extend te pos [(name, ass, rules)] + grammar_extend te pos [(name, p4ass, rules)] (* Defines new entries. If the entry already exists, check its type *) let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} = let typ = explicitize_entry (fst univ) n in let e,lev = get_constr_entry typ in - let pos,ass = find_position ass lev in - let name = option_app (constr_level ass) lev in - (e,typ,pos,name,ass,rls) + let other = match typ with ETOther _ -> true | _ -> false in + let pos,p4ass,name = find_position other ass lev in + (e,typ,pos,name,ass,p4ass,rls) (* Add a bunch of grammar rules. Does not check if it is well formed *) let extend_grammar_rules gram = @@ -248,27 +253,24 @@ let make_gen_act f pil = Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) -let extend_constr entry pos (level,assoc) make_act pt = +let extend_constr entry (level,assoc) make_act pt = let univ = get_univ "constr" in let pil = List.map (symbol_of_prod_item univ assoc) pt in let (symbs,ntl) = List.split pil in let act = make_act ntl in - grammar_extend entry pos [(level, assoc, [symbs, act])] + let pos,p4assoc,name = find_position false assoc level in + grammar_extend entry pos [(name, p4assoc, [symbs, act])] let extend_constr_notation (n,assoc,ntn,rule) = let mkact loc env = CNotation (loc,ntn,env) in let (e,level) = get_constr_entry (ETConstr (n,())) in - let pos,assoc = find_position assoc level in - extend_constr e pos (option_app (constr_level assoc) level,assoc) - (make_act mkact) rule + extend_constr e (level,assoc) (make_act mkact) rule let extend_constr_delimiters (sc,rule,pat_rule) = let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in - extend_constr Constr.constr (Some (Gramext.Level "0")) - (None,None) - (make_act mkact) rule; + extend_constr Constr.constr (Some 0,Some Gramext.NonA) (make_act mkact) rule; let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in - extend_constr Constr.pattern None (None,None) + extend_constr Constr.pattern (None,None) (make_cases_pattern_act mkact) pat_rule (* These grammars are not a removable *) diff --git a/parsing/extend.ml b/parsing/extend.ml index ae3561c1f9..c7ea8737fa 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -25,7 +25,7 @@ type production_position = | InternalProd type 'pos constr_entry_key = - | ETIdent | ETReference + | ETIdent | ETReference | ETBigint | ETConstr of (int * 'pos) | ETPattern | ETOther of string * string @@ -158,6 +158,7 @@ let rename_command_entry nt = let explicitize_prod_entry pos univ nt = if univ = "prim" & nt = "var" then ETIdent else + if univ = "prim" & nt = "bigint" then ETBigint else if univ <> "constr" then ETOther (univ,nt) else match nt with | "constr0" -> ETConstr (0,pos) @@ -238,18 +239,18 @@ let border = function | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a | _ -> None -let clever_assoc = function +let clever_assoc ass = function | [g] when g.gr_production <> [] -> (match border g.gr_production, border (List.rev g.gr_production) with - Some RightA, Some LeftA -> Some NonA - | a, b when a=b -> a - | Some LeftA, Some RightA -> Some LeftA (* since LR *) - | _ -> None) - | _ -> None + | Some LeftA, Some RightA -> ass (* Untractable; we cheat *) + | Some LeftA, _ -> Some LeftA + | _, Some RightA -> Some RightA + | _ -> Some NonA) + | _ -> ass let gram_entry univ (nt, ass, rl) = let l = List.map (gram_rule (univ,nt)) rl in - let ass = if ass = None then clever_assoc l else ass in + let ass = clever_assoc ass l in { ge_name = nt; gl_assoc = ass; gl_rules = l } diff --git a/parsing/extend.mli b/parsing/extend.mli index 705fc88185..12d2ecc620 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -26,7 +26,7 @@ type production_position = | InternalProd type 'pos constr_entry_key = - | ETIdent | ETReference + | ETIdent | ETReference | ETBigint | ETConstr of (int * 'pos) | ETPattern | ETOther of string * string diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 0862c792de..e527fafd8c 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -327,7 +327,7 @@ let string_of_assoc = function | Some(Gramext.LeftA) | None -> "LEFTA" | Some(Gramext.NonA) -> "NONA" -let make_symbolic assoc n symbols etyps = +let make_symbolic n symbols etyps = (n,List.map assoc_of_type etyps), (String.concat " " (List.flatten (List.map string_of_symbol symbols))) @@ -446,6 +446,7 @@ let interp_syntax_modifiers = let rec interp assoc level etyps = function | [] -> let n = match level with None -> 1 | Some n -> n in + let assoc = match assoc with None -> Some Gramext.NonA | a -> a in (assoc,n,etyps,!onlyparsing) | SetEntryType (s,typ) :: l -> let id = id_of_string s in @@ -486,25 +487,20 @@ let set_entry_type etyps (x,typ) = let assoc = if left then Gramext.LeftA else Gramext.RightA in ETConstr (n,BorderProd (left,Some assoc)) | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd) - | (ETPattern | ETIdent | ETOther _ | ETReference as t), _ -> t + | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t with Not_found -> ETConstr typ in (x,typ) -let collapse_assoc_left = function - | None | Some Gramext.LeftA -> Some Gramext.NonA - | a -> a +let border = function + | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a + | _ -> None -let collapse_assoc_right = function - | Some Gramext.RightA -> Some Gramext.NonA - | a -> a - -let is_border = function - | (_,ETConstr(_,BorderProd _)) :: _ -> true - | _ -> false - -let adjust_associativity typs assoc = - let assoc = if is_border typs then assoc else collapse_assoc_left assoc in - if is_border (List.rev typs) then assoc else collapse_assoc_right assoc +let recompute_assoc typs = + match border typs, border (List.rev typs) with + | Some Gramext.LeftA, Some Gramext.RightA -> assert false + | Some Gramext.LeftA, _ -> Some Gramext.LeftA + | _, Some Gramext.RightA -> Some Gramext.RightA + | _ -> Some Gramext.NonA let add_syntax_extension df modifiers = let (assoc,n,etyps,onlyparse) = interp_syntax_modifiers modifiers in @@ -513,8 +509,8 @@ let add_syntax_extension df modifiers = (n,BorderProd(true,assoc)) (10,InternalProd) (n,BorderProd(false,assoc)) [] (split df) in let typs = List.map (set_entry_type etyps) typs in - let assoc = adjust_associativity typs assoc in - let (prec,notation) = make_symbolic assoc n symbs typs in + let assoc = recompute_assoc typs in + let (prec,notation) = make_symbolic n symbs typs in let gram_rule = make_grammar_rule n assoc typs symbs notation in let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbs) in Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule)) @@ -596,9 +592,9 @@ let add_notation_in_scope df a modifiers sc toks = let etyps = merge_entry_types etyps' etyps in *) let typs = List.map (set_entry_type etyps) typs in - let assoc = adjust_associativity typs assoc in + let assoc = recompute_assoc typs in (* Declare the parsing and printing rules if not already done *) - let (prec,notation) = make_symbolic assoc n symbols typs in + let (prec,notation) = make_symbolic n symbols typs in let gram_rule = make_grammar_rule n assoc typs symbols notation in let pp_rule = if onlyparse then None else Some (make_pp_rule typs symbols) in Lib.add_anonymous_leaf (inSyntaxExtension(prec,notation,gram_rule,pp_rule)); -- cgit v1.2.3