let loc_of_floc = function
| { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
(loc_begin, loc_end)
+let fail floc msg =
+ let (x, y) = loc_of_floc floc in
+ failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
type term_attribute =
[ `Loc of location (* source file location *)
| `Level of int * Gramext.g_assoc (* precedence, associativity *)
| `XmlAttrs of (string option * string * string) list
(* list of XML attributes: namespace, name, value *)
+ | `Raw of string (* unparsed version *)
]
type literal =
| Binder of binder_kind * capture_variable * term (* kind, name, body *)
| Case of term * string option * term option * (case_pattern * term) list
(* what to match, inductive type, out type, <pattern,action> list *)
+ | Cast of term * term
| LetIn of capture_variable * term * term (* name, body, where *)
| LetRec of induction_kind * (capture_variable * term * int) list * term
(* (name, body, decreasing argument) list, where *)
| Root of term * term (* argument, index *)
| Break
| Box of box_spec * term list
+ | Group of term list
and magic_term =
(* level 1 magics *)
type cic_appl_pattern =
| UriPattern of UriManager.uri
| VarPattern of string
+ | ImplicitPattern
| ApplPattern of cic_appl_pattern list
-type phrase = (* TODO hackish: replace with TacticAst.statement or similar *)
- | Print of term
- | Notation of term * Gramext.g_assoc option * int option * term
- (* level 1 pattern, associativity, precedence, level 2 pattern *)
- | Interpretation of (string * argument_pattern list) * cic_appl_pattern
- | Render of UriManager.uri
- | Dump (* dump grammar *)
+(** {2 Standard precedences} *)
+
+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