]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_interpreter_galax/test_select.ml
This commit was manufactured by cvs2svn to create branch 'scripts'.
[helm.git] / helm / ocaml / mathql_interpreter_galax / test_select.ml
diff --git a/helm/ocaml/mathql_interpreter_galax/test_select.ml b/helm/ocaml/mathql_interpreter_galax/test_select.ml
deleted file mode 100755 (executable)
index 9893352..0000000
+++ /dev/null
@@ -1,55 +0,0 @@
-
-
-(*
- select uri0
-  in use pattern "cic:/Coq/Reals/Rdefinitions/Rlt.con" position $s0
-  where $s0 is mainconclusion
-*)
-
-
-
-open Mathql_semantics;;
-open MathQL;;
-
-(* stampa tutti i documenti che fanno match con un pattern di input *)
-List.iter
- (function atturi -> print_endline ("output: " ^ atturi))
-  (match Mqint2.execute
-    (MQList
-      (MQSelect
-     (
-      (*SELECT*) "uri0",
-      (*  IN  *) MQUse
-                  (
-                  MQPattern
-                   (
-                    Some "cic",
-                    [MQBD; MQBC"Algebra"; MQBD; MQBC "Basics"; MQBD; MQBSS],
-                     []
-                   ),
-                   "$s0"
-                  ),
-      (*WHERE *) MQIs
-                  (
-                  MQStringSVar "$s0",
-                  MQConclusion
-                  )
-     )
-
-    )
-   ) 
-   with MQRefs l -> l
-  );
-
-
-
-;;
-
-
-
-
-
-
-
-