let max_precedence = 100
let default_precedence = 50
+let let_in_prec = 10
+let binder_prec = 20
+let apply_prec = 70
+let simple_prec = 90
+
+let let_in_assoc = Gramext.NonA
+let binder_assoc = Gramext.RightA
+let apply_assoc = Gramext.LeftA
+let simple_assoc = Gramext.NonA
+
let level1_pattern = Grammar.Entry.create grammar "level1_pattern"
let level2_pattern = Grammar.Entry.create grammar "level2_pattern"
let level3_term = Grammar.Entry.create grammar "level3_term"
[NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
@ aux p1
| Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
- | Break -> []
+(* | Break -> [] *)
| Box (_, pl) -> List.flatten (List.map aux pl)
and aux_magic magic =
match magic with
(** {2 Grammar} *)
-let boxify = function
- | [ a ] -> a
- | l -> Layout (Box (H, l))
-
let fold_binder binder pt_names body =
let fold_cluster binder terms ty body =
List.fold_right
| SYMBOL "\\ROOT"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
return_term loc (Layout (Root (arg, index)));
| SYMBOL "\\HBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
- return_term loc (Layout (Box (H, p)))
+ return_term loc (Layout (Box ((H, false, false), p)))
| SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
- return_term loc (Layout (Box (V, p)))
- | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
+ return_term loc (Layout (Box ((V, false, false), p)))
+ | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+ return_term loc (Layout (Box ((HV, false, false), p)))
+ | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+ return_term loc (Layout (Box ((HOV, false, false), p)))
+(* | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *)
+(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
| DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
- return_term loc (boxify p)
+ return_term loc (CicNotationUtil.boxify p)
| p = SELF; SYMBOL "\\AS"; id = IDENT ->
return_term loc (Variable (Ascription (p, id)))
]
]
];
level3_term: [
- [ u = URI -> UriPattern u
+ [ u = URI -> UriPattern (UriManager.uri_of_string u)
| id = IDENT -> VarPattern id
| SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
(match terms with