commit of galax mathql interpreter

[helm.git] / helm / ocaml / mathql_interpreter_galax / test_select2.ml

diff --git a/helm/ocaml/mathql_interpreter_galax/test_select2.ml b/helm/ocaml/mathql_interpreter_galax/test_select2.ml
new file mode 100644 (file)
index 0000000..12cc1fc
--- /dev/null
+++ b/helm/ocaml/mathql_interpreter_galax/test_select2.ml
@@ -0,0 +1,55 @@
+
+
+(*
+ 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 "CC_Props"; MQBD; MQBSS],
+                     []
+                   ),
+                   "$s0"
+                  ),
+      (*WHERE *) MQIs
+                  (
+                  MQStringSVar "$s0",
+                  MQConclusion
+                  )
+     )
+
+    )
+   ) 
+   with MQRefs l -> l
+  );
+
+
+
+;;
+
+
+
+
+
+
+
+
+