* 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 option
| Type of UriManager.uri * int
type 'lazy_term reduction =
- [ `Normalize
+ [ `Demodulate
+ | `Normalize
| `Reduce
| `Simpl
| `Unfold of 'lazy_term option
| 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 = 5
| 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 * UriManager.uri * bool (* add composites *)
- | Alias of loc * alias_spec
- (** parameters, name, type, fields *)
| 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
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
-