+type checked_l1_pattern = CL1P of CicNotationPt.term * int
+
+let check_l1_pattern level1_pattern level associativity =
+ let variables = ref 0 in
+ let symbols = ref 0 in
+ let rec aux = function
+ | Ast.AttributedTerm (att, t) -> Ast.AttributedTerm (att,aux t)
+ | Ast.Literal _ as l -> incr symbols; l
+ | Ast.Layout l -> Ast.Layout (aux_layout l)
+ | Ast.Magic m -> Ast.Magic (aux_magic m)
+ | Ast.Variable v -> Ast.Variable (aux_variable v)
+ | t -> assert false
+ and aux_layout = function
+ | Ast.Sub (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2)
+ | Ast.Sup (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sup (p1, p2)
+ | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
+ | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
+ | Ast.Frac (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
+ | Ast.Atop (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
+ | Ast.Over (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
+ | Ast.Root (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
+ | Ast.Sqrt p -> Ast.Sqrt (aux p)
+ | Ast.Break as t -> t
+ | Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
+ | Ast.Group pl -> Ast.Group (List.map aux pl)
+ and aux_magic magic =
+ match magic with
+ | Ast.Opt p -> Ast.Opt (aux p)
+ | Ast.List0 (p, x) -> Ast.List0 (aux p, x)
+ | Ast.List1 (p, x) -> Ast.List1 (aux p, x)
+ | _ -> assert false
+ and aux_variable =
+ function
+ | Ast.NumVar _ as t -> t
+ | Ast.TermVar (s,None) when associativity <> Gramext.NonA ->
+ incr variables;
+ if !variables > 2 then
+ raise (Parse_error ("Exactly 2 variables must be specified in an "^
+ "associative notation"));
+ (match !variables, associativity with
+ | 1,Gramext.LeftA -> Ast.TermVar (s, None) (*Ast.TermVar (s, Some
+ (level-1)) *)
+ | 1,Gramext.RightA -> Ast.TermVar (s, None)
+ | 2,Gramext.LeftA ->Ast.TermVar (s, None)
+ | 2,Gramext.RightA -> Ast.TermVar (s, Some (level-1))
+ | _ -> assert false)
+ | Ast.TermVar (s,Some _) when associativity <> Gramext.NonA ->
+ 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 && !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 *)
+ | Ast.FreshVar _ -> assert false
+ in
+ if associativity <> Gramext.NonA && level = min_precedence then
+ raise (Parse_error ("You can not specify an associative notation " ^
+ "at level "^string_of_int min_precedence ^ "; increase it"));
+ let cp = CL1P (aux level1_pattern, level) in
+ if !variables <> 2 && associativity <> Gramext.NonA then
+ raise (Parse_error ("Exactly 2 variables must be specified in an "^
+ "associative notation"));
+ cp
+;;
+
+let extend (CL1P (level1_pattern,precedence)) action =