Symbol of string option * string * subst option * string option
(* h:xref, name, subst, definitionURL *)
| LocalVar of (string option) * string (* h:xref, name *)
- | Meta of string option * string (* h:xref, name *)
+ | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
| Num of string option * string (* h:xref, value *)
| Appl of string option * cexpr list (* h:xref, args *)
| Binder of string option * string * decl * cexpr
def = string * cexpr (* name, body *)
and
subst = (UriManager.uri * cexpr) list
+and
+ meta_subst = cexpr option list
;;
(* NOTATION *)
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
- None, Some "cic:/Coq/Init/Logic/eqT.ind"))
+ None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
:: List.map acic2cexpr (List.tl args)));;
(* and *)
None, Some "cic:/Coq/Init/Logic/not.con"))
:: List.map acic2cexpr args));;
+(* Rinv *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "inv",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+ :: List.map acic2cexpr args));;
+
+(* Ropp *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "opp",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+ :: List.map acic2cexpr args));;
+
(* exists *)
Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
None, Some "cic:/Coq/Arith/Minus/mult.con"))
:: List.map acic2cexpr args));;
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con"
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "minus",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
+ :: List.map acic2cexpr args));;
+
+(* div *)
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
+ (fun aid sid args acic2cexpr ->
+ Appl
+ (Some aid, (Symbol (Some sid, "div",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
+ :: List.map acic2cexpr args));;
+
| C.AVar (id,uri,subst) ->
Symbol (Some id, UriManager.name_of_uri uri,
make_subst subst, Some (UriManager.string_of_uri uri))
- | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
+ | C.AMeta (id,n,l) ->
+ let l' =
+ List.rev_map
+ (function
+ None -> None
+ | Some t -> Some (acic2cexpr t)
+ ) l
+ in
+ Meta (Some id,("?" ^ (string_of_int n)),l')
| C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
| C.AImplicit _ -> raise NotImplemented
| C.AProd (id,n,s,t) ->