From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 19 Jun 2008 17:39:53 +0000 (+0000)
Subject: notation fixed to be NON associative by default
X-Git-Tag: make_still_working~5010
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7af476a04e008ec5a7d1eaf096a4e6ce62aef6cf;p=helm.git

notation fixed to be NON associative by default
---

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 698539207..2d03762ae 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -264,12 +264,9 @@ let check_l1_pattern level1_pattern level associativity =
           raise (Parse_error ("Variables can not be declared with a " ^ 
             "precedence in an associative notation"))
        (* avoid camlp5 divergence due to non-Sself recursion at the same level *)
-    | Ast.TermVar (s,Some l) when l=level -> 
-        incr variables; 
-        Ast.TermVar (s,None) 
-       (* avoid camlp5 divergence due to non-Sself left recursion *)
-    | Ast.TermVar (s,Some _) when !symbols = 0 && !variables = 0 -> 
-          raise (Parse_error "Left recursive rule with precedence not allowed")
+    | Ast.TermVar (s,Some l) when l <= level && !variables=0 && !symbols=0 -> 
+          raise (Parse_error ("Left recursive rule with precedence not greater " ^
+            "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
     | Ast.TermVar _ as t -> incr variables; t
     | Ast.IdentVar _ as t -> t
     | Ast.Ascription _ -> assert false (* TODO *)
@@ -295,7 +292,7 @@ let extend (CL1P (level1_pattern,precedence)) action =
       [ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
         Some (Gramext.Level level),
         [ None,
-          Some (*Gramext.NonA*) Gramext.LeftA,
+          Some (*Gramext.NonA*) Gramext.NonA,
           [ p_atoms, 
             (make_action
               (fun (env: CicNotationEnv.t) (loc: Ast.location) ->
@@ -355,7 +352,7 @@ let _ =
       | i when i < first -> acc
       | i ->
           aux
-            ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.LeftA, dummy_prod)
+            ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod)
              :: acc)
             (i - 1)
     in
@@ -628,7 +625,7 @@ EXTEND
     ];
   term: LEVEL "70N"
     [
-      [ p1 = term; p2 = term ->
+      [ p1 = term; p2 = term LEVEL "71N" ->
           let rec aux = function
             | Ast.Appl (hd :: tl)
             | Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 89dba2987..85edd595c 100644
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -98,17 +98,16 @@ let pp_ast0 t k =
   let rec aux =
     function
     | Ast.Appl ts ->
-        let rec aux_args pos =
+        let rec aux_args level =
           function
           | [] -> []
           | [ last ] ->
-              let last = k last in
-              [ last ]
+              [ Ast.AttributedTerm (`Level level,k last) ]
           | hd :: tl ->
-              (k hd) :: aux_args `Inner tl
+              (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl
         in
         add_level_info Ast.apply_prec 
-          (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts)))
+          (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts)))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         add_level_info Ast.binder_prec
           (hvbox false true