* http://helm.cs.unibo.it/
*)
-module Ast = CicNotationPt
+(* $Id$ *)
type direction = [ `LeftToRight | `RightToLeft ]
-type loc = Ast.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 reduction =
- [ `Normalize
+type 'lazy_term reduction =
+ [ `Demodulate
+ | `Normalize
| `Reduce
| `Simpl
- | `Unfold of CicNotationPt.term option
+ | `Unfold of 'lazy_term option
| `Whd ]
type ('term, 'lazy_term, 'reduction, 'ident) tactic =
| 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 *)
-
-type metadata =
- | Dependency of string (* baseuri without trailing slash *)
- | Baseuri of string
-
-let compare_metadata = Pervasives.compare
-
-let eq_metadata = (=)
-
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 3
+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 * Ast.term * Gramext.g_assoc *
- int * Ast.term
- (* direction, l1 pattern, associativity, precedence, l2 pattern *)
- | Interpretation of loc *
- string * (string * Ast.argument_pattern list) *
- Ast.cic_appl_pattern
- (* description (i.e. id), symbol, arg pattern, appl pattern *)
-
- | Metadata of loc * metadata
-
- (* 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
-
-let reash_cmd_uris =
- let reash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in
- function
- | Default (loc, name, uris) ->
- let uris = List.map reash_uri uris in
- Default (loc, name, uris)
- | Interpretation (loc, dsc, args, cic_appl_pattern) ->
- let rec aux =
- function
- | CicNotationPt.UriPattern uri ->
- CicNotationPt.UriPattern (reash_uri uri)
- | CicNotationPt.ApplPattern args ->
- CicNotationPt.ApplPattern (List.map aux args)
- | CicNotationPt.VarPattern _
- | CicNotationPt.ImplicitPattern as pat -> pat
- in
- let appl_pattern = aux cic_appl_pattern in
- Interpretation (loc, dsc, args, appl_pattern)
- | cmd -> cmd
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
-