X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Ftest_indexing.ml;h=ba6b2ebe062c173735685f50a30f7dab27a2a87c;hb=727d6939c3f3ff1769ac1d11cad11d2e06433295;hp=7391812f3d71b8c6028723edd50f0e1b3ccb219f;hpb=22d39afadb3027477e4a42c315ec10518cbf47ed;p=helm.git diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml index 7391812f3..ba6b2ebe0 100644 --- a/helm/ocaml/paramodulation/test_indexing.ml +++ b/helm/ocaml/paramodulation/test_indexing.ml @@ -1,3 +1,5 @@ +(* $Id$ *) + open Path_indexing (* @@ -210,11 +212,11 @@ let test_refl () = ] ] in let ens = [ - (UriManager.uri_of_string"cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", + (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", + (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", + (UriManager.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", C.Rel 2); ] in let term2 = C.Appl [ @@ -231,10 +233,21 @@ let test_refl () = 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 ();; *) Helm_registry.load_from "../../matita/matita.conf.xml"; -test_refl ();; +(* test_refl ();; *) +test_lib ();;