From f6c7ba13084782457d1a41c1e8d573479b105fa0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 4 Dec 2002 22:45:00 +0000 Subject: Correction divers bugs d'affichage; explicitation du niveau de grammaire quand mentionn explicitement par l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3377 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/pcoq.ml4 | 33 +++++++++++----------- parsing/pcoq.mli | 2 ++ parsing/ppconstr.ml | 4 +-- toplevel/metasyntax.ml | 74 ++++++++++++++++++++++++-------------------------- 4 files changed, 57 insertions(+), 56 deletions(-) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 72eb7dca1..96b358402 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -122,14 +122,17 @@ module Gram = end +let camlp4_verbosity silent f x = + let a = !Gramext.warning_verbose in + Gramext.warning_verbose := silent; + f x; + Gramext.warning_verbose := a + (* This extension command is used by the Grammar constr *) let grammar_extend te pos rls = camlp4_state := ByGrammar (Gramobj.weaken_entry te,pos,rls) :: !camlp4_state; - let a = !Gramext.warning_verbose in - Gramext.warning_verbose := Options.is_verbose (); - G.extend te pos rls; - Gramext.warning_verbose := a + camlp4_verbosity (Options.is_verbose ()) (G.extend te pos) rls (* n is the number of extended entries (not the number of Grammar commands!) to remove. *) @@ -503,22 +506,20 @@ let camlp4_assoc = function | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA | None | Some Gramext.LeftA -> Gramext.LeftA -(* Official Coq convention *) -let coq_assoc = function - | None -> Gramext.LeftA - | Some a -> a - let adjust_level assoc = function - (* If no associativity constraints, adopt the current one *) + (* If NonA on the right-hand side, set to NEXT *) | (n,BorderProd (false,Some Gramext.NonA)) -> Some None - | (n,BorderProd (_,Some Gramext.NonA)) -> None - (* Otherwise, deal with the current one *) - | (n,BorderProd (_,a)) when coq_assoc a = camlp4_assoc assoc -> None - | (n,BorderProd (left,a)) -> - let a = coq_assoc a in + (* If NonA on the left-hand side, adopt the current assoc ?? *) + | (n,BorderProd (true,Some Gramext.NonA)) -> None + (* Associativity is None means force the level *) + | (n,BorderProd (_,None)) -> Some (Some n) + (* If the expected assoc is the current one, SELF on both sides *) + | (n,BorderProd (_,Some a)) when a = camlp4_assoc assoc -> None + (* Otherwise, force the level, n or n-1, according to expected assoc *) + | (n,BorderProd (left,Some a)) -> if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA) then Some (Some n) else Some (Some (n-1)) - | (8,InternalProd) -> None +(* | (8,InternalProd) -> None (* Or (Some 8) for factorization ? *)*) | (n,InternalProd) -> Some (Some n) let compute_entry allow_create adjust = function diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7409a9e80..4ea1c4e5b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -46,6 +46,8 @@ val grammar_extend : val remove_grammars : int -> unit +val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit + (* Parse a string *) val parse_string : 'a Gram.Entry.e -> string -> 'a diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index a8dd7b8aa..d38259768 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -103,7 +103,7 @@ let pr_notation pr s env = prlist (print_hunk pr env) unpl, level let pr_delimiters key strm = - let left = "`"^key^":" and right = "`" in + let left = "'"^key^":" and right = "'" in let lspace = if is_letter (left.[String.length left -1]) then str " " else mt () in let rspace = @@ -386,6 +386,7 @@ let gentermpr gt = with s -> wrap_exception s (* [at_top] means ids of env must be avoided in bound variables *) + let gentermpr_core at_top env t = gentermpr (Termast.ast_of_constr at_top env t) @@ -394,4 +395,3 @@ let gentermpr_core at_top env t = pr_constr (Constrextern.extern_constr at_top env t) *) - diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e37d0d664..7313ed7bd 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -258,10 +258,9 @@ type symbol = | Break of int let prec_assoc = function - | Some(Gramext.RightA) -> (L,E) - | Some(Gramext.LeftA) -> (E,L) - | Some(Gramext.NonA) -> (L,L) - | None -> (L,L) (* NONA by default *) + | Gramext.RightA -> (L,E) + | Gramext.LeftA -> (E,L) + | Gramext.NonA -> (L,L) let level_rule (n,p) = if p = E then n else max (n-1) 0 @@ -270,49 +269,50 @@ let meta_pattern m = Pmeta(m,Tany) open Symbols -type white_status = NextMaybeLetter | NoSpace | AddBrk of int +type white_status = Juxtapose | Separate of int let add_break l = function - | AddBrk n -> UNP_BRK (n,1) :: l + | Separate n -> UNP_BRK (n,1) :: l | _ -> l let precedence_of_entry_type = function - | ETConstr (n,BorderProd (left,a)) -> + | ETConstr (n,BorderProd (left,None)) -> (n,Prec n) + | ETConstr (n,BorderProd (left,Some a)) -> (n, let (lp,rp) = prec_assoc a in if left then lp else rp) | ETConstr (n,InternalProd) -> (n,E) | _ -> 0,E +(* x = y |-> x brk = y (breaks before any symbol) *) +(* x =S y |-> x spc =S spc y (protect from confusion; each side for symmetry)*) +(* + { |-> + { may breaks reversibility without space but oth. not elegant *) +(* x y |-> x spc y *) + (* For old ast printer *) let make_hunks_ast symbols etyps from = let (_,l) = List.fold_right (fun it (ws,l) -> match it with | NonTerminal m -> - let (_,lp) = precedence_of_entry_type (List.assoc m etyps) in + let (n,lp) = precedence_of_entry_type (List.assoc m etyps) in let u = PH (meta_pattern (string_of_id m), None, lp) in let l' = u :: (add_break l ws) in -(* - ((if from = 10 (* lconstr *) then AddBrk 1 else NextMaybeLetter), l') -*) - (AddBrk 1, l') + (Separate 1, l') | Terminal s -> -(* - let l' = add_break l ws in -*) - let l' = l in - if from = 10 (* lconstr *) then (AddBrk 1, RO s :: l') - else - let n = if is_letter (s.[0]) then 1 else 0 in - let s = - if (ws = NextMaybeLetter or ws = AddBrk 1) - & is_letter (s.[String.length s -1]) - then s^" " - else s - in - (AddBrk n, RO s :: l') + let n,(s,l) = + if + is_letter (s.[0]) or + is_letter (s.[String.length s -1]) or + is_digit (s.[String.length s -1]) + then + (* We want spaces around both sides *) + Separate 1, + if ws = Separate 0 then s^" ",l else s,add_break l ws + else + Juxtapose, (s,l) in + (n, RO s :: l) | Break n -> - (NoSpace, UNP_BRK (n,1) :: l)) - symbols (NoSpace,[]) + (Juxtapose, UNP_BRK (n,1) :: l)) + symbols (Juxtapose,[]) in l let make_hunks etyps symbols = @@ -325,21 +325,21 @@ let make_hunks etyps symbols = let prec = precedence_of_entry_type (List.nth typs (i-1)) in let u = UnpMetaVar (i ,prec) in let l' = match ws with - | AddBrk n -> UnpCut (PpBrk(n,1)) :: u :: l + | Separate n -> UnpCut (PpBrk(n,1)) :: u :: l | _ -> u :: l in - (NextMaybeLetter, l') + (Separate 1, l') | Terminal s -> let n = if is_letter (s.[0]) then 1 else 0 in let s = - if (ws = NextMaybeLetter or ws = AddBrk 1) + if (ws = Separate 1) & is_letter (s.[String.length s -1]) then s^" " else s in - (AddBrk n, UnpTerminal s :: l) + (Separate n, UnpTerminal s :: l) | Break n -> - (NoSpace, UnpCut (PpBrk (n,1)) :: l)) - symbols (NextMaybeLetter,[]) + (Juxtapose, UnpCut (PpBrk (n,1)) :: l)) + symbols (Juxtapose,[]) in l let string_of_prec (n,p) = @@ -526,9 +526,7 @@ let set_entry_type etyps (x,typ) = let typ = try match List.assoc x etyps, typ with | ETConstr (n,()), (_,BorderProd (left,_)) -> - (* We set an associativity telling not to change the level *) - let assoc = if left then Gramext.LeftA else Gramext.RightA in - ETConstr (n,BorderProd (left,Some assoc)) + ETConstr (n,BorderProd (left,None)) | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd) | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t with Not_found -> ETConstr typ @@ -576,7 +574,7 @@ let open_notation i (_,(oldse,prec,ntn,scope,pat,onlyparse,df)) = if not b then Symbols.declare_notation_interpretation ntn scope pat prec df; if not b & not onlyparse then - Symbols.declare_uninterpretation (NotationRule (ntn,scope)) pat + Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat end let cache_notation o = -- cgit v1.2.3