let symbol_table = Hashtbl.create 503;;
(* eq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "eq",
- None, Some "cic:/Coq/Init/Logic/eq.ind"))
+ None, Some HelmLibraryObjects.Logic.eq_SURI))
:: List.map acic2cexpr (List.tl args)));;
-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_Type/eqT.ind"))
- :: List.map acic2cexpr (List.tl args)));;
-
(* and *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "and",
- None, Some "cic:/Coq/Init/Logic/and.ind"))
+ None, Some HelmLibraryObjects.Logic.and_SURI))
:: List.map acic2cexpr args));;
(* or *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "or",
- None, Some "cic:/Coq/Init/Logic/or.ind"))
+ None, Some HelmLibraryObjects.Logic.or_SURI))
:: List.map acic2cexpr args));;
(* iff *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "iff",
- None, Some "cic:/Coq/Init/Logic/iff.con"))
+ None, Some HelmLibraryObjects.Logic.iff_SURI))
:: List.map acic2cexpr args));;
(* not *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "not",
- None, Some "cic:/Coq/Init/Logic/not.con"))
+ None, Some HelmLibraryObjects.Logic.not_SURI))
:: List.map acic2cexpr args));;
(* Rinv *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "inv",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con"))
+ None, Some HelmLibraryObjects.Reals.rinv_SURI))
:: List.map acic2cexpr args));;
(* Ropp *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "opp",
- None, Some "cic:/Coq/Reals/Rdefinitions/Ropp.con"))
+ None, Some HelmLibraryObjects.Reals.ropp_SURI))
:: List.map acic2cexpr args));;
(* exists *)
-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)] ->
- Binder
- (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t)
- | _ -> raise Not_found);;
-
-Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
(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#xpointer(1/1)"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
- None, Some "cic:/Coq/Init/Peano/le.ind"))
+ None, Some HelmLibraryObjects.Peano.le_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "leq",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con"))
+ None, Some HelmLibraryObjects.Reals.rle_SURI))
:: List.map acic2cexpr args));;
(* lt *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "lt",
- None, Some "cic:/Coq/Init/Peano/lt.con"))
+ None, Some HelmLibraryObjects.Peano.lt_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "lt",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con"))
+ None, Some HelmLibraryObjects.Reals.rlt_SURI))
:: List.map acic2cexpr args));;
(* geq *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "geq",
- None, Some "cic:/Coq/Init/Peano/ge.con"))
+ None, Some HelmLibraryObjects.Peano.ge_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "geq",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con"))
+ None, Some HelmLibraryObjects.Reals.rge_SURI))
:: List.map acic2cexpr args));;
(* gt *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "gt",
- None, Some "cic:/Coq/Init/Peano/gt.con"))
+ None, Some HelmLibraryObjects.Peano.gt_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "gt",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con"))
+ None, Some HelmLibraryObjects.Reals.rgt_SURI))
:: List.map acic2cexpr args));;
(* plus *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/Init/Peano/plus.con"))
+ None, Some HelmLibraryObjects.Peano.plus_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con"))
+ None, Some HelmLibraryObjects.BinInt.zplus_SURI))
:: 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"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
(fun aid sid args acic2cexpr ->
let appl () =
Appl
(Some aid, (Symbol (Some sid, "plus",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con"))
+ None, Some HelmLibraryObjects.Reals.rplus_SURI))
:: List.map acic2cexpr args)
in
let rec aux acc = function
| [ Cic.AConst (nid, uri, []); n] when
- UriManager.eq uri r1_uri ->
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
(match n with
- | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
+ | Cic.AConst (_, uri, []) when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
Num (Some aid, string_of_int (acc + 2))
| Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
- UriManager.eq uri rplus_uri ->
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
aux (acc + 1) args
| _ -> appl ())
| _ -> appl ()
(* zero and one *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
(fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
(fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;;
(* times *)
-Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "times",
- None, Some "cic:/Coq/Init/Peano/mult.con"))
+ None, Some HelmLibraryObjects.Peano.mult_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "times",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con"))
+ None, Some HelmLibraryObjects.Reals.rmult_SURI))
:: List.map acic2cexpr args));;
(* minus *)
-Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "minus",
- None, Some "cic:/Coq/Arith/Minus/mult.con"))
+ None, Some HelmLibraryObjects.Peano.minus_SURI))
:: List.map acic2cexpr args));;
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "minus",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con"))
+ None, Some HelmLibraryObjects.Reals.rminus_SURI))
:: List.map acic2cexpr args));;
(* div *)
-Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con"
+Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI
(fun aid sid args acic2cexpr ->
Appl
(Some aid, (Symbol (Some sid, "div",
- None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con"))
+ None, Some HelmLibraryObjects.Reals.rdiv_SURI))
:: List.map acic2cexpr args));;
function
Cic.Prop -> "Prop"
| Cic.Set -> "Set"
- | Cic.Type -> "Type"
+ | Cic.Type _ -> "Type" (* TASSI *)
| Cic.CProp -> "Type"
;;
let get_constructors uri i =
let inductive_types =
- (match CicEnvironment.get_obj uri with
- Cic.Constant _ -> assert false
- | Cic.Variable _ -> assert false
- | Cic.CurrentProof _ -> assert false
- | Cic.InductiveDefinition (l,_,_) -> l
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
+ Cic.Constant _ -> assert false
+ | Cic.Variable _ -> assert false
+ | Cic.CurrentProof _ -> assert false
+ | Cic.InductiveDefinition (l,_,_) -> l
) in
let (_,_,_,constructors) = List.nth inductive_types i in
constructors
make_subst subst, Some uri_str)::List.map acic2cexpr tl))
| C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
let inductive_types =
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false
make_subst subst, Some (UriManager.string_of_uri uri)))
| C.AMutInd (id,uri,i,subst) ->
let inductive_types =
- (match CicEnvironment.get_obj uri with
+ (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
| Cic.CurrentProof _ -> assert false
projects / helm.git / blobdiff