added testlibrary script

diff --git a/helm/gTopLevel/.cvsignore b/helm/gTopLevel/.cvsignore
index 61337747a60239f3e0a8668c12ce9e1e01521bf9..f578d2072da83a80f73b120fce5841cf1c2ed3ad 100644 (file)
--- a/helm/gTopLevel/.cvsignore
+++ b/helm/gTopLevel/.cvsignore
@@ -1,6 +1,7 @@
 *.cm[iox]
 gTopLevel gTopLevel.opt
 regtest regtest.opt
+testlibrary
 styles stylesheets meta_stylesheets
 chosenTermEditor.ml
 chosenTransformer.ml

diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index ec10354a78bb2217da342dc32cd8d5b2245f5769..54a2f1d1660d48d405f75bba3064a32fde5c2427 100644 (file)
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -1,8 +1,8 @@
 BIN_DIR = /usr/local/bin
 REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \
            gdome2-xslt helm-mathql_interpreter helm-mathql_generator \
-                          helm-tactics hbugs-client mathml-editor helm-cic_transformations \
-           helm-cic_textual_parser2
+          helm-tactics hbugs-client mathml-editor helm-cic_transformations \
+           helm-cic_textual_parser2 helm-cic_cache
 PREDICATES = "gnome,init,glade"
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
 OCAMLFIND = ocamlfind
@@ -29,11 +29,13 @@ INTERFACE_FILES = \
 
 DEPOBJS = \
        $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \
-       gTopLevel.ml regtest.ml batchParser.ml batchParser.mli
+       gTopLevel.ml regtest.ml testlibrary.ml batchParser.ml batchParser.mli
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo
 REGTESTOBJS = \
        $(INTERFACE_FILES:%.mli=%.cmo) batchParser.cmo regtest.cmo
+TESTLIBOBJS = \
+       $(INTERFACE_FILES:%.mli=%.cmo) testlibrary.cmo
 
 $(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES)
 $(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT)
@@ -55,6 +57,8 @@ gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES)
 gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
        $(OCAMLOPT) -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx)
 
+testlibrary: $(TESTLIBOBJS) $(LIBRARIES)
+       $(OCAMLC) -linkpkg -o $@ $(TESTLIBOBJS)
 regtest: $(REGTESTOBJS) $(LIBRARIES)
        $(OCAMLC) -linkpkg -o $@ $(REGTESTOBJS)
 regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(LIBRARIES)

diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml
new file mode 100644 (file)
index 0000000..bdc07e9
--- /dev/null
+++ b/helm/gTopLevel/testlibrary.ml
@@ -0,0 +1,76 @@
+
+let mqi_debug_fun = ignore
+let mqi_flags = []
+let mqi_handle = MQIConn.init mqi_flags mqi_debug_fun
+
+let verbose = false
+
+exception Failure of string
+let fail msg = raise (Failure msg)
+
+module DisambiguateCallbacks =
+ struct
+  let output_html ?(append_NL = true) msg =
+    if verbose then
+      (if append_NL then print_string else print_endline)
+        (Ui_logger.string_of_html_msg msg)
+
+  let interactive_user_uri_choice
+   ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id =
+     List.filter
+      (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+
+  let interactive_interpretation_choice _ = fail "Multiple interpretations"
+  let input_or_locate_uri ~title = fail "Unknown identifier"
+ end
+
+module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks)
+
+let debug_print s = prerr_endline ("^^^^^^ " ^ s)
+
+let main () =
+  let uri = UriManager.uri_of_string (Sys.argv.(1)) in
+  let obj = CicCache.get_obj uri in
+  let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
+    Cic2acic.acic_object_of_cic_object obj
+  in
+  let ids_to_uris = Hashtbl.create 1023 in
+  let round_trip annterm =
+    debug_print "(1) acic -> ast";
+    let (ast, _) =
+      Acic2Ast.ast_of_acic ids_to_inner_sorts ids_to_uris annterm
+    in
+    debug_print ("ast: " ^ CicAstPp.pp_term ast);
+    let (_, _, term) =
+      Disambiguate'.disambiguate_term mqi_handle [] [] ast
+        DisambiguateTypes.Environment.empty
+    in
+    debug_print ("term: " ^ CicPp.ppterm term)
+  in
+  match annobj with
+  | Cic.AConstant (_, _, _, None, ty, _) ->
+      debug_print "Cic.AConstant (ty)";
+      round_trip ty
+  | Cic.AConstant (_, _, _, Some bo, ty, _) ->
+      debug_print "Cic.AConstant (bo)";
+      round_trip bo;
+      debug_print "Cic.AConstant (ty)";
+      round_trip ty
+  | Cic.AVariable (_, _, None, ty, _) ->
+      debug_print "Cic.AVariable (ty)";
+      round_trip ty
+  | Cic.AVariable (_, _, Some bo, ty, _) ->
+      debug_print "Cic.AVariable (bo)";
+      round_trip bo;
+      debug_print "Cic.AVariable (ty)";
+      round_trip ty
+  | Cic.ACurrentProof (_, _, _, _, proof, ty, _) ->
+      debug_print "Cic.ACurrentProof (proof)";
+      round_trip proof;
+      debug_print "Cic.ACurrentProof (ty)";
+      round_trip ty
+  | Cic.AInductiveDefinition _ ->
+      debug_print "AInductiveDefinition: boh ..."
+
+let _ = main ()
+