open Path_indexing
-
+(*
let build_equality term =
let module C = Cic in
C.Implicit None, (C.Implicit None, term, C.Rel 1, Utils.Gt), [], []
and t2 = M.apply_subst subst2 term in
Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
;;
+*)
+
+
+let test_refl () =
+ let module C = Cic in
+ let context = [
+ Some (C.Name "H", C.Decl (
+ C.Prod (C.Name "z", C.Rel 3,
+ C.Appl [
+ C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ C.Rel 4; C.Rel 3; C.Rel 1])));
+ Some (C.Name "x", C.Decl (C.Rel 2));
+ Some (C.Name "y", C.Decl (C.Rel 1));
+ Some (C.Name "A", C.Decl (C.Sort C.Set))
+ ]
+ in
+ let term = C.Appl [
+ C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []); C.Rel 4;
+ C.Rel 2;
+ C.Lambda (C.Name "z", C.Rel 4,
+ C.Appl [
+ C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ C.Rel 5; C.Rel 1; C.Rel 3
+ ]);
+ C.Appl [C.MutConstruct
+ (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); (* reflexivity *)
+ C.Rel 4; C.Rel 2];
+ C.Rel 3;
+(* C.Appl [C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []); (\* symmetry *\) *)
+(* C.Rel 4; C.Appl [C.Rel 1; C.Rel 2]] *)
+ C.Appl [
+ C.Const (HelmLibraryObjects.Logic.eq_ind_URI, []);
+ C.Rel 4; C.Rel 3;
+ C.Lambda (C.Name "z", C.Rel 4,
+ C.Appl [
+ C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ C.Rel 5; C.Rel 1; C.Rel 4
+ ]);
+ C.Appl [C.MutConstruct (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+ C.Rel 4; C.Rel 3];
+ C.Rel 2; C.Appl [C.Rel 1; C.Rel 2]
+ ]
+ ] in
+ let ens = [
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var",
+ C.Rel 4);
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var",
+ C.Rel 3);
+ (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var",
+ C.Rel 2);
+ ] in
+ let term2 = C.Appl [
+ C.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens);
+ C.Appl [C.Rel 1; C.Rel 2]
+ ] in
+ let ty, ug =
+ CicTypeChecker.type_of_aux' [] context term CicUniv.empty_ugraph
+ in
+ Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term) (CicPp.ppterm ty);
+ let ty, ug =
+ CicTypeChecker.type_of_aux' [] context term2 CicUniv.empty_ugraph
+ in
+ Printf.printf "OK, %s ha tipo %s\n" (CicPp.ppterm term2) (CicPp.ppterm ty);
+;;
+
+
+let test_lib () =
+ let uri = Sys.argv.(1) in
+ let t = CicUtil.term_of_uri (UriManager.uri_of_string uri) in
+ let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ Printf.printf "Term of %s: %s\n" uri (CicPp.ppterm t);
+ Printf.printf "type: %s\n" (CicPp.ppterm ty);
+;;
(* differing ();; *)
(* next_after ();; *)
(* discrimination_tree_test ();; *)
(* path_indexing_test ();; *)
-test_subst ();;
-
+(* test_subst ();; *)
+Helm_registry.load_from "../../matita/matita.conf.xml";
+(* test_refl ();; *)
+test_lib ();;