]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter_galax/test_select.ml
commit of galax mathql interpreter
[helm.git] / helm / ocaml / mathql_interpreter_galax / test_select.ml
1
2
3 (*
4  select uri0
5   in use pattern "cic:/Coq/Reals/Rdefinitions/Rlt.con" position $s0
6   where $s0 is mainconclusion
7 *)
8
9
10
11 open Mathql_semantics;;
12 open MathQL;;
13
14 (* stampa tutti i documenti che fanno match con un pattern di input *)
15 List.iter
16  (function atturi -> print_endline ("output: " ^ atturi))
17   (match Mqint2.execute
18     (MQList
19       (MQSelect
20      (
21       (*SELECT*) "uri0",
22       (*  IN  *) MQUse
23                   (
24                    MQPattern
25                     (
26                      Some "cic",
27                      [MQBD; MQBC"Algebra"; MQBD; MQBC "Basics"; MQBD; MQBSS],
28                      []
29                     ),
30                    "$s0"
31                   ),
32       (*WHERE *) MQIs
33                   (
34                    MQStringSVar "$s0",
35                    MQConclusion
36                   )
37      )
38
39     )
40    ) 
41    with MQRefs l -> l
42   );
43
44
45
46 ;;
47
48
49
50
51
52
53
54
55