From: Enrico Tassi 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