* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
type direction = [ `LeftToRight | `RightToLeft ]
-type loc = CicNotationPt.location
+type loc = Token.flocation
type ('term, 'lazy_term, 'ident) pattern =
- 'lazy_term option * ('ident * 'term) list * 'term
+ 'lazy_term option * ('ident * 'term) list * 'term option
type ('term, 'ident) type_spec =
| Ident of 'ident
| Type of UriManager.uri * int
type 'lazy_term reduction =
- [ `Normalize
+ [ `Demodulate
+ | `Normalize
| `Reduce
| `Simpl
| `Unfold of 'lazy_term option
| IdTac of loc
| Injection of loc * 'term
| Intros of loc * int option * 'ident list
+ | Inversion of loc * 'term
| LApply of loc * int option * 'term list * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
| Search_pat of loc * search_kind * string (* searches with string pattern *)
| Search_term of loc * search_kind * 'term (* searches with term pattern *)
-type alias_spec =
- | Ident_alias of string * string (* identifier, uri *)
- | Symbol_alias of string * int * string (* name, instance no, description *)
- | Number_alias of int * string (* instance no, description *)
-
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 4
+let magic = 5
-type ('term,'obj) command =
+type 'obj command =
| Default of loc * string * UriManager.uri list
| Include of loc * string
| Set of loc * string * string
| Drop of loc
| Qed of loc
- (** name.
- * Name is needed when theorem was started without providing a name
- *)
- | Coercion of loc * 'term * bool (* add composites *)
- | Alias of loc * alias_spec
- (** parameters, name, type, fields *)
+ | Coercion of loc * UriManager.uri * bool (* add composites *)
| Obj of loc * 'obj
- | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
- int * CicNotationPt.term
- (* direction, l1 pattern, associativity, precedence, l2 pattern *)
- | Interpretation of loc *
- string * (string * CicNotationPt.argument_pattern list) *
- CicNotationPt.cic_appl_pattern
- (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
- (* DEBUGGING *)
- | Dump of loc (* dump grammar on stdout *)
- (* DEBUGGING *)
- | Render of loc * UriManager.uri (* render library object *)
-
-(* composed magic: term + command magics. No need to change this value *)
-let magic = magic + 10000 * CicNotationPt.magic
type ('term, 'lazy_term, 'reduction, 'ident) tactical =
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
| _ -> false
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
- | Command of loc * ('term,'obj) command
+ | Command of loc * 'obj command
| Macro of loc * 'term macro
| Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
* ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement =
| Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code
| Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment
-
- (* statements meaningful for matitadep *)
-type dependency =
- | IncludeDep of string
- | BaseuriDep of string
- | UriDep of UriManager.uri
-