type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
type induction_kind = [ `Inductive | `CoInductive ]
-type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
type fold_kind = [ `Left | `Right ]
type location = Lexing.position * Lexing.position
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 href = UriManager.uri
+
+type child_pos = [ `None | `Left | `Right | `Inner ]
type term_attribute =
- [ `Loc of location (* source file location *)
- | `IdRef of string (* ACic pointer *)
+ [ `Loc of location (* source file location *)
+ | `IdRef of string (* ACic pointer *)
+ | `Level of int * Gramext.g_assoc (* precedence, associativity *)
+ | `ChildPos of child_pos (* position of l1 pattern variables *)
+ | `XmlAttrs of (string option * string * string) list
+ (* list of XML attributes: namespace, name, value *)
+ | `Raw of string (* unparsed version *)
]
type literal =
| `Number of string
]
+type case_indtype = string * href option
+
+(** To be increased each time the term type below changes, used for "safe"
+ * marshalling *)
+let magic = 1
+
type term =
(* CIC AST *)
| Appl of term list
| Binder of binder_kind * capture_variable * term (* kind, name, body *)
- | Case of term * string option * term option * (case_pattern * term) list
+ | Case of term * case_indtype 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 *)
| Literal of literal
| Layout of layout_pattern
+
| Magic of magic_term
| Variable of pattern_variable
and meta_subst = term option
and subst = string * term
-and case_pattern = string * capture_variable list
+and case_pattern = string * href option * capture_variable list
-and box_kind = H | V
+and box_kind = H | V | HV | HOV
+and box_spec = box_kind * bool * bool (* kind, spacing, indent *)
and layout_pattern =
| Sub of term * term
| Sqrt of term
| Root of term * term (* argument, index *)
| Break
- | Box of box_kind * term list
+ | Box of box_spec * term list
+ | Group of term list
and magic_term =
(* level 1 magics *)
- | List0 of term * literal option
- | List1 of term * literal option
+ | List0 of term * literal option (* pattern, separator *)
+ | List1 of term * literal option (* pattern, separator *)
| Opt of term
(* level 2 magics *)
| Fold of fold_kind * term * string list * term
(* base case pattern, recursive case bound names, recursive case pattern *)
| Default of term * term (* "some" case pattern, "none" case pattern *)
+ | Fail
+ | If of term * term * term (* test, pattern if true, pattern if false *)
and pattern_variable =
(* level 1 and 2 variables *)
| FreshVar of string
type argument_pattern =
- | IdentArg of string
- | EtaArg of string option * argument_pattern (* eta abstraction *)
+ | IdentArg of int * string (* eta-depth, name *)
type cic_appl_pattern =
- | UriPattern of string
- | ArgPattern of argument_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 *)
+(** {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