type fold_kind = [ `Left | `Right ]
type location = Lexing.position * Lexing.position
+(* cut and past from CicAst.loc_of_floc *)
+let loc_of_floc = function
+ | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
+ (loc_begin, loc_end)
+
type term_attribute =
[ `Loc of location (* source file location *)
(* Syntax pattern extensions *)
+ | Literal of literal
| Layout of layout_pattern
| Magic of magic_term
| Variable of pattern_variable
-and capture_variable = Cic.name * term option (* name, type *)
+ (* name, type. First component must be Ident or Variable (FreshVar _) *)
+and capture_variable = term * term option
+
and meta_subst = term option
and subst = string * term
and case_pattern = string * capture_variable list
| Below of term * term
| Above of term * term
| Frac of term * term
+ | Over of term * term
| Atop of term * term
-(* | Array of term * literal option * literal option
+(* | array of term * literal option * literal option
|+ column separator, row separator +| *)
| Sqrt of term
| Root of term * term (* argument, index *)
(* level 2 variables *)
| FreshVar of string
+type argument_pattern =
+ | IdentArg of int * string (* eta-depth, name *)
+
+type cic_appl_pattern =
+ | UriPattern of string
+ | VarPattern of string
+ | 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
+