]
type literal =
- [ `Symbol of string
- | `Keyword of string
- | `Number of string
+ [ `Symbol of string * (string option * string option)
+ | `Keyword of string * (string option * string option)
+ | `Number of string * (string option * string option)
]
type case_indtype = string * href option
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 6
+let magic = 8
type term =
(* CIC AST *)
| LetIn of term capture_variable * term * term (* name, body, where *)
| LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term
(* (params, name, body, decreasing arg) list, where *)
- | Ident of string * subst list option
- (* literal, substitutions.
- * Some [] -> user has given an empty explicit substitution list
- * None -> user has given no explicit substitution list *)
+ | Ident of string * [ `Ambiguous | `Uri of string | `Rel ]
+ (* literal, disambiguation info (can be ambiguous, a disambiguated uri,
+ * or an identifier to be converted in a Rel)
+ * case `Uri is also used for literal uris
+ * the parser fills the name of the identifier using the final part of the
+ * uri
+ *)
| Implicit of [`Vector | `JustOne | `Tagged of string]
| Meta of int * meta_subst list
- | Num of string * int (* literal, instance *)
+ | Num of string * (string option * string) option
+ (* literal, (uri, interpretation name) *)
| Sort of sort_kind
- | Symbol of string * int (* canonical name, instance *)
-
+ (* XXX: symbols used to be packed with their instance number, probably for
+ * disambiguation purposes; hopefully we won't need this info any more *)
+ | Symbol of string * (string option * string) option
+ (* canonical name, (uri, interpretation name) *)
| UserInput (* place holder for user input, used by MatitaConsole, not to be
used elsewhere *)
- | Uri of string * subst list option (* as Ident, for long names *)
| NRef of NReference.reference
| NCic of NCic.term
(* Syntax pattern extensions *)
-
- | Literal of literal
+ (* string option = optional name of an Ast.Symbol occurring in the level 2
+ * term, which is associated to this literal *)
+ | Literal of (string option * literal)
| Layout of layout_pattern
| Magic of magic_term
| Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
(** left parameters, name, type, fields *)
+let name_of_obj = function
+ | Theorem (_,n,_,_,_) | Record (_,n,_,_)
+ | Inductive (_,(n,_,_,_)::_) -> n
+ | _ -> (* empty inductive block *) assert false
+;;
+
+let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
+
+let map_pattern f = function
+ | Pattern (s,h,vl) -> Pattern (s,h,List.map (map_variable f) vl)
+ | p -> p
+;;
+
+let map f = function
+ | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+ | Appl tl -> Appl (List.map f tl)
+ | Binder (k,n,body) -> Binder (k,map_variable f n,f body)
+ | Case (t,ity,oty,pl) ->
+ let pl' = List.map (fun (p,u) -> map_pattern f p, f u) pl in
+ Case (f t,ity,HExtlib.map_option f oty,pl')
+ | Cast (u,v) -> Cast (f u,f v)
+ | LetIn (n,u,v) -> LetIn (n,f u,f v)
+ | LetRec (ik,l,t) ->
+ let l' = List.map (fun (vl,v,u,n) ->
+ (List.map (map_variable f) vl,
+ map_variable f v,
+ f u,
+ n)) l
+ in LetRec (ik,l',f t)
+ | t -> t
+;;
+
(** {2 Standard precedences} *)
let let_in_prec = 10
let apply_prec = 70
let simple_prec = 90
+(* sequents *)
+
+type context_entry =
+ Decl of term
+ | Def of term * term
+
+type sequent = int * context * term
+and context = (string * context_entry) list