(* the type cexpr is inspired by OpenMath. A few primitive constructors
have been added, in order to take into account some special features
of functional expressions. Most notably: case, let in, let rec, and
- explicit substitutons *)
+ explicit substitutions *)
type cexpr =
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 *)
let symbol_table = Hashtbl.create 503;;
(* eq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
- None, Some "cic:/Coq/Init/Logic/eq.ind#(/1/0)"))
+ None, Some "cic:/Coq/Init/Logic/eq.ind"))
:: List.map acic2cexpr (List.tl args)));;
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
- None, Some "cic:/Coq/Init/Logic/eqT.ind#(/1/0)"))
+ None, Some "cic:/Coq/Init/Logic_Type/eqT.ind"))
:: List.map acic2cexpr (List.tl args)));;
(* and *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "and",
- None, Some "cic:/Coq/Init/Logic/and.ind#(/1/0)"))
+ None, Some "cic:/Coq/Init/Logic/and.ind"))
:: List.map acic2cexpr args));;
(* or *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "or",
- None, Some "cic:/Coq/Init/Logic/or.ind#(/1/0)"))
+ None, Some "cic:/Coq/Init/Logic/or.ind"))
:: List.map acic2cexpr args));;
(* iff *)
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#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
(Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
| _ -> raise Not_found);;
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
match (List.tl args) with
[Cic.ALambda (_,Cic.Name n,s,t)] ->
| _ -> raise Not_found);;
(* leq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#(/1/0)"
+Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)"
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
- None, Some "cic:/Coq/Init/Peano/le.ind#(/1/0)"))
+ None, Some "cic:/Coq/Init/Peano/le.ind"))
:: List.map acic2cexpr args));;
Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con"
None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
:: List.map acic2cexpr args));;
+let rplus_uri =
+ UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
+let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;;
+let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
+
Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
(fun aid sid args acic2cexpr ->
- Appl
- (Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
- :: List.map acic2cexpr args));;
+ let appl () =
+ Appl
+ (Some aid, (Symbol (Some sid, "plus",
+ None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
+ :: List.map acic2cexpr args)
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when
+ UriManager.eq uri r1_uri ->
+ (match n with
+ | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+ Num (Some aid, string_of_int (acc + 2))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri rplus_uri ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+;;
+
+(* zero and one *)
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
+ (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
+
+Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
+ (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
(* times *)
Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
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));;
+
let string_of_sort =
function
- Cic.Prop -> "Prop"
- | Cic.Set -> "Set"
- | Cic.Type -> "Type"
+ Cic.Prop -> "Prop"
+ | Cic.Set -> "Set"
+ | Cic.Type -> "Type"
+ | Cic.CProp -> "Type"
;;
let get_constructors uri i =
| 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) ->
(try
(let f = Hashtbl.find symbol_table uri_str in
f aid sid tl acic2cexpr)
- with notfound ->
+ with Not_found ->
Appl (Some aid, Symbol (Some sid,UriManager.name_of_uri uri,
make_subst subst, Some uri_str)::List.map acic2cexpr tl))
| C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
) in
let (name,_,_,_) = List.nth inductive_types i in
let uri_str = UriManager.string_of_uri uri in
- let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ ")") in
+ let puri_str =
+ uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" in
(try
(let f = Hashtbl.find symbol_table puri_str in
f aid sid tl acic2cexpr)
- with notfound ->
+ with Not_found ->
Appl (Some aid, Symbol (Some sid, name,
- make_subst subst, Some puri_str)::List.map acic2cexpr tl))
+ make_subst subst, Some uri_str)::List.map acic2cexpr tl))
| C.AAppl (id,li) ->
Appl (Some id, List.map acic2cexpr li)
| C.AConst (id,uri,subst) ->
- Symbol (Some id, UriManager.name_of_uri uri,
- make_subst subst, Some (UriManager.string_of_uri uri))
+ let uri_str = UriManager.string_of_uri uri in
+ (try
+ let f = Hashtbl.find symbol_table uri_str in
+ f "dummy" id [] acic2cexpr
+ with Not_found ->
+ Symbol (Some id, UriManager.name_of_uri uri,
+ make_subst subst, Some (UriManager.string_of_uri uri)))
| C.AMutInd (id,uri,i,subst) ->
let inductive_types =
(match CicEnvironment.get_obj uri with
) in
let (name,_,_,_) = List.nth inductive_types i in
let uri_str = UriManager.string_of_uri uri in
- let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ ")") in
- Symbol (Some id, name, make_subst subst, Some puri_str)
+ Symbol (Some id, name, make_subst subst, Some uri_str)
| C.AMutConstruct (id,uri,i,j,subst) ->
let constructors = get_constructors uri i in
let (name,_) = List.nth constructors (j-1) in
let uri_str = UriManager.string_of_uri uri in
- let puri_str = (uri_str ^ "#(/1/" ^ (string_of_int i) ^ "/" ^ (string_of_int j) ^ ")") in
- Symbol (Some id, name, make_subst subst, Some puri_str)
+ Symbol (Some id, name, make_subst subst, Some uri_str)
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let constructors = get_constructors uri typeno in
let named_patterns =