diff options
| author | herbelin | 2004-02-12 12:27:19 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-12 12:27:19 +0000 |
| commit | 0541d7039eb3ac663597059413b2d9a889d6b0b5 (patch) | |
| tree | 2b58e8651d26fbc5e6590233ff3002f2dd33c262 /interp/constrextern.ml | |
| parent | 61de148a1b0c357c54e7fecb9152c1f153552cf3 (diff) | |
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.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 28ab30c057..455b91e4da 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1074,15 +1074,43 @@ let same c d = try check_same_type c d; true with _ -> false let make_current_scopes (scopt,scopes) = option_fold_right push_scope scopt scopes +let has_curly_brackets ntn = + String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or + String.sub ntn (String.length ntn - 6) 6 = " { _ }" or + string_string_contains ntn " { _ } ") + +let expand_curly_brackets make_ntn ntn l = + let ntn' = ref ntn in + let rec expand_ntn = + function + | [] -> [] + | a::l as l' -> + let a' = + try + let i = string_index_from !ntn' 0 "{ _ }" in + ntn' := + String.sub !ntn' 0 i ^ "_" ^ + String.sub !ntn' (i+5) (String.length !ntn' -i-5); + make_ntn "{ _ }" [a] + with Not_found -> a in + a' :: expand_ntn l in + let l = expand_ntn l in + (* side effect *) + make_ntn !ntn' l + let make_notation loc ntn l = - match ntn,l with + if has_curly_brackets ntn + then expand_curly_brackets (fun n l -> CNotation (loc,n,l)) ntn l + else match ntn,l with (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) | "- _", [CNumeral(_,Bignat.POS p)] -> CNotation (loc,ntn,[CNotation(loc,"( _ )",l)]) | _ -> CNotation (loc,ntn,l) let make_pat_notation loc ntn l = - match ntn,l with + if has_curly_brackets ntn + then expand_curly_brackets (fun n l -> CPatNotation (loc,n,l)) ntn l + else match ntn,l with (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *) | "- _", [CPatNumeral(_,Bignat.POS p)] -> CPatNotation (loc,ntn,[CPatNotation(loc,"( _ )",l)]) |