From 0541d7039eb3ac663597059413b2d9a889d6b0b5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 12 Feb 2004 12:27:19 +0000 Subject: Décomposition automatique des règles d'analyse syntaxique pour les notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A*{B}+{C}" en présence d'une notation "_ * { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A|P}" etc. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/metasyntax.ml | 88 +++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 69 insertions(+), 19 deletions(-) (limited to 'toplevel/metasyntax.ml') diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a50339c6e..3d773a7da 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -576,9 +576,6 @@ let string_of_assoc = function | Some(Gramext.LeftA) | None -> "LEFTA" | Some(Gramext.NonA) -> "NONA" -let make_symbolic n symbols etyps = - ((n,List.map (assoc_of_type n) etyps), make_notation_key symbols) - let is_not_small_constr = function ETConstr _ -> true | ETOther("constr","binder_constr") -> true @@ -633,6 +630,14 @@ let recompute_assoc typs = | _, Some Gramext.RightA -> Some Gramext.RightA | _ -> None +let rec expand_squash = function + | Term ("","{") :: NonTerm (ProdPrimitive (ETConstr _), n) :: Term ("","}") + :: l -> + NonTerm (ProdPrimitive (ETConstr (NextLevel,InternalProd)),n) + :: expand_squash l + | a :: l -> a :: expand_squash l + | [] -> [] + let make_grammar_rule n typs symbols ntn perm = let assoc = recompute_assoc typs in let prod = make_production typs symbols in @@ -858,6 +863,35 @@ let find_precedence lev etyps symbols = if lev = None then error "Cannot determine the level"; out_some lev +let check_curly_brackets_notation_exists () = + try let _ = Symbols.level_of_notation "{ _ }" in () + with Not_found -> + error "Notations involving patterns of the form \"{ _ }\" are treated \n\ +specially and require that the notation \"{ _ }\" is already reserved" + +(* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *) +let remove_curly_brackets l = + let rec next = function + | Break _ :: l -> next l + | l -> l in + let rec aux deb = function + | [] -> [] + | Terminal "{" as t1 :: l -> + (match next l with + | NonTerminal _ as x :: l' as l0 -> + (match next l' with + | Terminal "}" as t2 :: l'' as l1 -> + if l <> l0 or l' <> l1 then + warning "Skipping spaces inside curly brackets"; + if deb & l'' = [] then [t1;x;t2] else begin + check_curly_brackets_notation_exists (); + x :: aux false l'' + end + | l1 -> t1 :: x :: aux false l1) + | l0 -> t1 :: aux false l0) + | x :: l -> x :: aux false l + in aux true l + let compute_syntax_data forv7 (df,modifiers) = let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in (* Notation defaults to NONA *) @@ -865,6 +899,8 @@ let compute_syntax_data forv7 (df,modifiers) = let toks = split_notation_string df in let innerlevel = NumLevel (if forv7 then 10 else 200) in let (vars,symbols) = analyse_notation_tokens toks in + let symbols = remove_curly_brackets symbols in + let notation = make_notation_key symbols in check_rule_reversibility symbols; let n = if !Options.v7 then find_precedence_v7 n etyps symbols @@ -877,24 +913,25 @@ let compute_syntax_data forv7 (df,modifiers) = symbols in (* To globalize... *) let typs = List.map (set_entry_type etyps) typs in - let (prec,notation) = make_symbolic n symbols typs in - ((onlyparse,vars,notation),prec,(n,typs,symbols,fmt),(Lib.library_dp(),df)) + let ppdata = (n,typs,symbols,fmt) in + let prec = (n,List.map (assoc_of_type n) typs) in + ((onlyparse,vars,notation),prec,ppdata,(Lib.library_dp(),df)) let add_syntax_extension local mv mv8 = let data8 = option_app (compute_syntax_data false) mv8 in let data = option_app (compute_syntax_data !Options.v7) mv in let prec,gram_rule = match data with - | None -> None, None - | Some ((_,_,notation),prec,(n,typs,symbols,_),_) -> - Some prec, Some (make_grammar_rule n typs symbols notation None) in + | None -> None, None + | Some ((_,_,notation),prec,(n,typs,symbols,_),_) -> + Some prec, Some (make_grammar_rule n typs symbols notation None) in match data, data8 with - | None, None -> (* Nothing to do: V8Notation while not translating *) () - | _, Some d | Some d, None -> - let ((_,_,notation),ppprec,ppdata,_) = d in - let notation = match data with Some ((_,_,ntn),_,_,_) -> ntn | _ -> notation in - let pp_rule = make_pp_rule ppdata in - Lib.add_anonymous_leaf - (inSyntaxExtension (local,(prec,ppprec),notation,gram_rule,pp_rule)) + | None, None -> (* Nothing to do: V8Notation while not translating *) () + | _, Some d | Some d, None -> + let ((_,_,ntn),ppprec,ppdata,_) = d in + let ntn' = match data with Some ((_,_,ntn),_,_,_) -> ntn | _ -> ntn in + let pp_rule = make_pp_rule ppdata in + Lib.add_anonymous_leaf + (inSyntaxExtension (local,(prec,ppprec),ntn',gram_rule,pp_rule)) (**********************************************************************) (* Distfix, Infix, Symbols *) @@ -977,6 +1014,18 @@ let mk_permut vars7 vars8 = (fun v8 subs -> list_index v8 vars7 - 1 :: subs) vars8 []) +let contract_notation ntn = + let rec aux ntn i = + if i <= String.length ntn - 5 then + let ntn' = + if String.sub ntn i 5 = "{ _ }" then + String.sub ntn 0 i ^ "_" ^ + String.sub ntn (i+5) (String.length ntn -i-5) + else ntn in + aux ntn' (i+1) + else ntn in + aux ntn 0 + let add_notation_in_scope local df c mods omodv8 scope toks = let ((onlyparse,vars,notation),prec,(n,typs,symbols,_ as ppdata),df') = compute_syntax_data !Options.v7 (df,mods) in @@ -997,8 +1046,9 @@ let add_notation_in_scope local df c mods omodv8 scope toks = | _ -> (* means the rule already exists: recover it *) try - let _, oldprec8 = Symbols.level_of_notation notation in - let rule,_ = Symbols.find_notation_printing_rule notation in + let ntn = contract_notation notation in + let _, oldprec8 = Symbols.level_of_notation ntn in + let rule,_ = Symbols.find_notation_printing_rule ntn in notation,vars,oldprec8,rule with Not_found -> error "No known parsing rule for this notation in V8" in @@ -1025,7 +1075,7 @@ let level_rule (n,p) = if p = E then n else max (n-1) 0 let check_notation_existence notation = try - let a,_ = Symbols.level_of_notation notation in + let a,_ = Symbols.level_of_notation (contract_notation notation) in if a = None then raise Not_found with Not_found -> error "Parsing rule for this notation has to be previously declared" @@ -1033,7 +1083,7 @@ let check_notation_existence notation = let build_old_pp_rule notation scope symbs (r,vars) = let prec = try - let a,_ = Symbols.level_of_notation notation in + let a,_ = Symbols.level_of_notation (contract_notation notation) in if a = None then raise Not_found else out_some a with Not_found -> error "Parsing rule for this notation has to be previously declared" in -- cgit v1.2.3