From dec50888f98015c937283acc14e2ffceccc04a11 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 1 Jul 2002 11:34:24 +0000 Subject: [PATCH] mathQL modified, stderr corrected to stdout im mathql_interpreter, new lavel assignment procedure in mQueryGenerator (uses degrees), textual interface for mQueryGenerator added --- helm/gTopLevel/gTopLevel.ml | 6 +- helm/gTopLevel/mQueryGenerator.ml | 86 ++++++++++++++-------- helm/gTopLevel/mQueryGenerator.mli | 12 ++- helm/gTopLevel/topLevel/.depend | 0 helm/gTopLevel/topLevel/Makefile | 47 ++++++++++++ helm/gTopLevel/topLevel/Readme | 15 ++++ helm/gTopLevel/topLevel/topLevel.ml | 65 ++++++++++++++++ helm/ocaml/mathql/mQueryTParser.mly | 2 +- helm/ocaml/mathql/mQueryUtil.ml | 48 +++++------- helm/ocaml/mathql/mQueryUtil.mli | 16 ++-- helm/ocaml/mathql/mathQL.ml | 11 +-- helm/ocaml/mathql_interpreter/diff.ml | 4 +- helm/ocaml/mathql_interpreter/intersect.ml | 4 +- helm/ocaml/mathql_interpreter/mqint.ml | 11 +-- helm/ocaml/mathql_interpreter/select.ml | 14 +++- helm/ocaml/mathql_interpreter/sortedby.ml | 4 +- helm/ocaml/mathql_interpreter/union.ml | 4 +- 17 files changed, 250 insertions(+), 99 deletions(-) create mode 100644 helm/gTopLevel/topLevel/.depend create mode 100644 helm/gTopLevel/topLevel/Makefile create mode 100644 helm/gTopLevel/topLevel/Readme create mode 100644 helm/gTopLevel/topLevel/topLevel.ml diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index d052040c5..85e9b5ebc 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -151,7 +151,7 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = (*CSC: We save the innertypes to disk so that we can retrieve them in the *) (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) (*CSC: local. *) - Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ; + Xml.pp xmlinnertypes (Some "/home/fguidi/innertypes") ; let output = applyStylesheets input mml_styles mml_args in output ;; @@ -1093,10 +1093,10 @@ let backward rendering_window () = match !ProofEngine.goal with | None -> "" | Some metano -> - let (_,_,ty) = + let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - MQueryGenerator.backward ty level + MQueryGenerator.backward metasenv ey ty level in output_html outputhtml result diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index 217f4d4d3..e08847c8f 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -12,15 +12,18 @@ let par () = "

" (* CIC term inspecting functions *) +let env = ref [] (* metasemv *) +let cont = ref [] (* context *) + let ie_out (r, b, v) = let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in - res (pos ^ str_uref r) ^ nl () + res (pos ^ str_uref r) ^ nl () (* FG: si puo' usare xp_str_uref se si vuole xpointer *) let rec il_out = function | [] -> "" | head :: tail -> ie_out head ^ il_out tail -let ie_struri (u, b, v) = str_uref u +let ie_str_uri (u, b, v) = xp_str_uref u let rec il_restrict level = function | [] -> [] @@ -36,61 +39,78 @@ let rec ie_insert ie = function | head :: tail -> head :: if ie_eq head ie then tail else ie_insert ie tail -let inspect_uri main l uri tc v = +let degree t = + let u0 = CicTypeChecker.type_of_aux' !env !cont t in + let u = CicReduction.whd !cont u0 in + let rec deg = function + | Sort _ -> 1 + | Cast (uu, _) -> deg uu + | Prod (_, _, tt) -> deg tt + | _ -> 2 + in deg u + +let inspect_uri main l uri tc v term = + let d = degree term in let fi = match tc with | t0 :: c0 :: _ -> [t0 + 1; c0] | t0 :: _ -> [t0 + 1] | [] -> [] - in ie_insert ((uri, fi), main, v) l + in ie_insert ((uri, fi), main, 2 * v + d - 1) l -let rec inspect_term main l v = function - | Rel i -> l - | Meta (i, _) -> l - | Sort s -> l +let rec inspect_term main l v term = + match term with + | Rel _ -> l + | Meta (_, _) -> l + | Sort _ -> l | Implicit -> l - | Var u -> inspect_uri main l u [] v - | Const (u, i) -> inspect_uri main l u [] v - | MutInd (u, i, t) -> inspect_uri main l u [t] v - | MutConstruct (u, i, t, c) -> inspect_uri main l u [t; c] v + | Var u -> inspect_uri main l u [] v term + | Const (u, _) -> inspect_uri main l u [] v term + | MutInd (u, _, t) -> inspect_uri main l u [t] v term + | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term | Cast (uu, _) -> - (*CSC: Cast modified so that it behaves exactly as if no Cast was there *) inspect_term main l v uu - | Prod (n, uu, tt) -> + | Prod (_, uu, tt) -> let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Lambda (n, uu, tt) -> + inspect_term main luu (v + 1) tt + | Lambda (_, uu, tt) -> let luu = inspect_term false l (v + 1) uu in inspect_term false luu (v + 1) tt - | LetIn (n, uu, tt) -> + | LetIn (_, uu, tt) -> let luu = inspect_term false l (v + 1) uu in inspect_term false luu (v + 1) tt | Appl m -> inspect_list main l true v m - | MutCase (u, i, t, tt, uu, m) -> - let lu = inspect_uri main l u [t] (v + 1) in + | MutCase (u, _, t, tt, uu, m) -> + let lu = inspect_uri main l u [t] (v + 1) term in let ltt = inspect_term false lu (v + 1) tt in let luu = inspect_term false ltt (v + 1) uu in inspect_list main luu false (v + 1) m - | Fix (i, m) -> inspect_ind l (v + 1) m - | CoFix (i, m) -> inspect_coind l (v + 1) m + | Fix (_, m) -> inspect_ind l (v + 1) m + | CoFix (_, m) -> inspect_coind l (v + 1) m and inspect_list main l head v = function | [] -> l | tt :: m -> - let ltt = inspect_term main l (if head then v else v+1) tt in + let ltt = inspect_term main l (if head then v else v + 1) tt in inspect_list false ltt false v m and inspect_ind l v = function | [] -> l - | (n, i, tt, uu) :: m -> + | (_, _, tt, uu) :: m -> let ltt = inspect_term false l v tt in let luu = inspect_term false ltt v uu in inspect_ind luu v m and inspect_coind l v = function | [] -> l - | (n, tt, uu) :: m -> + | (_, tt, uu) :: m -> let ltt = inspect_term false l v tt in let luu = inspect_term false ltt v uu in inspect_coind luu v m -let inspect t = inspect_term true [] 0 t +let rec inspect_backbone = function + | Cast (uu, _) -> inspect_backbone uu + | Prod (_, _, tt) -> inspect_backbone tt + | LetIn (_, uu, tt) -> inspect_backbone tt + | t -> inspect_term true [] 0 t + +let inspect t = inspect_backbone t (* query building functions *) @@ -104,12 +124,12 @@ let build_select (r, b, v) n = let svar = "str" ^ string_of_int n in let mqs = if b then MQMConclusion else MQConclusion in MQSelect (rvar, - MQUse (MQReference [str_uref r], svar), + MQUse (MQReference [xp_str_uref r], svar), MQIs (MQStringSVar svar, mqs) ) let rec build_inter n = function - | [] -> MQPattern [(None, [MQBSS], [MQFSS])] + | [] -> MQPattern (None, [MQBSS], [MQFSS]) | [ie] -> build_select ie n | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) @@ -118,7 +138,7 @@ let restrict_universe query = [] -> query (* no constraints ===> the universe is the library *) | l -> let universe = - MQReference (List.map ie_struri l) + MQReference (List.map ie_str_uri l) in MQLetIn ( "universe", universe, @@ -155,7 +175,7 @@ let locate s = (i.e. no fragment identifier at all) *) MQList (MQSelect ("ref", - MQPattern [(Some "cic", [MQBSS ; MQBC ".con|.ind"],[])], + MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]), MQIs (MQFunc (MQName, "ref"), MQCons s ) @@ -164,7 +184,13 @@ let locate s = in build_result query -let backward t level = +let levels e c t level = + env := e; cont := c; + let il = inspect t in + par () ^ il_out il ^ nl () + +let backward e c t level = + env := e; cont := c; let il = inspect t in let query = build_inter 0 (il_restrict level il) in let query' = restrict_universe query il in diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli index 2d07f4ec4..a07019688 100644 --- a/helm/gTopLevel/mQueryGenerator.mli +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -33,10 +33,14 @@ (* *) (******************************************************************************) -val init : unit -> unit (* INIT database function *) +val levels : Cic.metasenv -> Cic.context -> Cic.term -> int -> string + (* level assignment testing function *) -val close : unit -> unit (* CLOSE database function *) +val init : unit -> unit (* INIT database function *) -val locate : string -> string (* LOCATE query building function *) +val close : unit -> unit (* CLOSE database function *) -val backward : Cic.term -> int -> string (* BACKWARD query building function *) +val locate : string -> string (* LOCATE query building function *) + +val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> string + (* BACKWARD query building function *) diff --git a/helm/gTopLevel/topLevel/.depend b/helm/gTopLevel/topLevel/.depend new file mode 100644 index 000000000..e69de29bb diff --git a/helm/gTopLevel/topLevel/Makefile b/helm/gTopLevel/topLevel/Makefile new file mode 100644 index 000000000..e0af8f6ed --- /dev/null +++ b/helm/gTopLevel/topLevel/Makefile @@ -0,0 +1,47 @@ +BIN_DIR = /usr/local/bin +REQUIRES = helm-cic_textual_parser helm-cic_proof_checking helm-mathql helm-mathql_interpreter +PREDICATES = +OCAMLOPTIONS = -I .. -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) + +all: topLevel +opt: topLevel.opt + +DEPOBJS = topLevel.ml + +TOPLEVELOBJS = ../mQueryGenerator.cmo topLevel.cmo + +depend: + $(OCAMLDEP) $(DEPOBJS) > .depend + +topLevel: $(TOPLEVELOBJS) $(LIBRARIES) + $(OCAMLC) -linkpkg -o topLevel $(TOPLEVELOBJS) + +topLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -linkpkg -o topLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: $(LIBRARIES) + $(OCAMLC) -c $< +.mli.cmi: $(LIBRARIES) + $(OCAMLC) -c $< +.ml.cmx: $(LIBRARIES_OPT) + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[iox] *.o topLevel topLevel.opt + +install: + cp topLevel topLevel.opt $(BIN_DIR) + +uninstall: + rm -f $(BIN_DIR)/topLevel $(BIN_DIR)/topLevel.opt + +.PHONY: install uninstall clean + +include .depend diff --git a/helm/gTopLevel/topLevel/Readme b/helm/gTopLevel/topLevel/Readme new file mode 100644 index 000000000..a59bba799 --- /dev/null +++ b/helm/gTopLevel/topLevel/Readme @@ -0,0 +1,15 @@ +uso del tool topLevel + +Il tool e` un interfaccia testuale per mQueryGenerator che prende dati +dallo stdin e restituisce l'output su stdout in formato html. +L'input puo' contenere piu' di un termine CIC (usare ; per separare). + +Sintassi: topLevel + +Opzioni : -locate : invocazione do Locate + -backward : invocazione di Backward + -show : mostra solo i termini CIC nell'input + -test : mostra l'attribuzione dei livelli per + la backward, ma non la esegue + +le opzioni si possono anche scrivere -l -b -s e -t \ No newline at end of file diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml new file mode 100644 index 000000000..216639399 --- /dev/null +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -0,0 +1,65 @@ +let get_terms () = + let terms = ref [] in + let lexbuf = Lexing.from_channel stdin in + try + while true do + match CicTextualParser.main CicTextualLexer.token lexbuf with + | None -> () + | Some expr -> terms := expr :: ! terms + done; + ! terms + with + CicTextualParser0.Eof -> ! terms + +let locate name = + print_endline (MQueryGenerator.locate name); + flush stdout + +let rec display = function + | [] -> () + | term :: tail -> + display tail; + print_endline ("? " ^ CicPp.ppterm term ^ "

"); + flush stdout + +let rec levels level = function + | [] -> () + | term :: tail -> + levels level tail; + print_endline ("? " ^ CicPp.ppterm term ^ "

"); + print_endline (MQueryGenerator.levels [] [] term level); + flush stdout + +let rec backward level = function + | [] -> () + | term :: tail -> + backward level tail; + print_endline ("? " ^ CicPp.ppterm term ^ "

"); + print_endline (MQueryGenerator.backward [] [] term level); + flush stdout + +let parse_args () = + let rec parse = function + | [] -> () + | ("-l"|"-locate") :: arg :: rem -> + locate arg; parse rem + | ("-d"|"-display") :: rem -> + display (get_terms ()) + | ("-t"|"-test") :: arg :: rem -> + levels (int_of_string arg) (get_terms ()) + | ("-b"|"-backward") :: arg :: rem -> + backward (int_of_string arg) (get_terms ()) + | _ :: rem -> parse rem + in + parse (List.tl (Array.to_list Sys.argv)) + +let _ = + CicCooking.init () ; + Logger.log_callback := + (Logger.log_to_html + ~print_and_flush:(function s -> print_string s ; flush stdout)) ; + MQueryGenerator.init (); + parse_args (); + MQueryGenerator.close (); + exit 0 +;; diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly index 0b375fcfe..9bfcd4e0c 100644 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ b/helm/ocaml/mathql/mQueryTParser.mly @@ -106,7 +106,7 @@ | LPR boole RPR { $2 } ; rlist: - | PATT REF { MQPattern [$2] } + | PATT REF { MQPattern $2 } | rlist UNION rlist { MQUnion ($1, $3) } | rlist INTER rlist { MQIntersect ($1, $3) } | USE rlist POS svar { MQUse ($2, $4) } diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml index cb60eff62..0cf8ebe08 100644 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ b/helm/ocaml/mathql/mQueryUtil.ml @@ -44,6 +44,11 @@ let str_btoken = function | MQBS -> "*" | MQBSS -> "**" +let str_ftoken = function + | MQFC i -> string_of_int i + | MQFS -> "*" + | MQFSS -> "**" + let str_prot = function | Some s -> s | None -> "*" @@ -52,36 +57,23 @@ let rec str_body = function | [] -> "" | head :: tail -> str_btoken head ^ str_body tail -let str_frag l = - match l with - [] -> "" - | l -> - let str_ftokens = - List.fold_left - (fun i t -> - i ^ - match t with - MQFC i -> "/" ^ string_of_int i - | MQFS -> "/*" - | MQFSS -> "/**" - ) "" l - in - "#xpointer(1" ^ str_ftokens ^ ")" -;; +let str_frag xpointer f l = + let sfi = List.fold_left (fun l0 t0 -> l0 ^ "/" ^ f t0) "" l in + if sfi = "" then "" else + if xpointer then "#xpointer(1" ^ sfi ^ ")" else + "#1" ^ sfi let str_tref (p, b, i) = - str_prot p ^ ":/" ^ str_body b ^ str_frag i -;; + str_prot p ^ ":/" ^ str_body b ^ str_frag false str_ftoken i + +let xp_str_tref (p, b, i) = + str_prot p ^ ":/" ^ str_body b ^ str_frag true str_ftoken i let str_uref (u, i) = - UriManager.string_of_uri u ^ - match i with - [] -> "" - | l -> - "#xpointer(1" ^ - List.fold_left (fun i n -> i ^ "/" ^ string_of_int n) "" l ^ - ")" -;; + UriManager.string_of_uri u ^ str_frag false string_of_int i + +let xp_str_uref (u, i) = + UriManager.string_of_uri u ^ str_frag true string_of_int i (* raw HTML representation *) @@ -115,7 +107,6 @@ let out_lvar s = sep "%" ^ sym s let out_tref r = pat (str_tref r) - let rec out_sequence f = function | [] -> sep "." | [s] -> f s @@ -171,7 +162,7 @@ and out_list = function key "select" ^ out_rvar r ^ sub "in" ^ out_list l ^ sub "where" ^ out_bool b | MQUse (l, v) -> key "use" ^ out_list l ^ sub "position" ^ out_svar v | MQUsedBy (l, v) -> key "usedby" ^ out_list l ^ sub "position" ^ out_svar v - | MQPattern p -> key "pattern" ^ out_sequence out_tref p + | MQPattern p -> key "pattern" ^ out_tref p | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ sub "union" ^ out_list l2 ^ sep ")" | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ sub "intersect" ^ out_list l2 ^ sep ")" | MQDiff (l1, l2) -> sep "(" ^ out_list l1 ^ sub "diff" ^ out_list l2 ^ sep ")" @@ -180,7 +171,6 @@ and out_list = function | MQListLVar v -> out_lvar v | MQLetIn (v, l1, l2) -> key "let" ^ out_lvar v ^ sub "be" ^ out_list l1 ^ sub "in" ^ out_list l2 | MQReference s -> key "reference" ^ out_sequence str s - | MQMinimize l -> key "minimize" ^ out_list l let out_query = function | MQList l -> out_list l diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli index 94126555b..0e62e4a13 100644 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ b/helm/ocaml/mathql/mQueryUtil.mli @@ -33,14 +33,18 @@ (* *) (******************************************************************************) -val str_uref : MathQL.mquref -> string (* string linearization of a UriManager reference *) +val str_uref : MathQL.mquref -> string (* string linearization of a UriMan. reference *) -val str_tref : MathQL.mqtref -> string (* string linearization of a tokenized reference *) +val str_tref : MathQL.mqtref -> string (* string linearization of a tokenized reference *) -val out_query : MathQL.mquery -> string (* HTML representation of a query *) +val xp_str_uref : MathQL.mquref -> string (* string linearization of a UriMan. reference *) -val out_result : MathQL.mqresult -> string (* HTML representation of a query result *) +val xp_str_tref : MathQL.mqtref -> string (* string linearization of a tokenized reference *) -val tref_uref : MathQL.mquref -> MathQL.mqtref (* "tref of uref" conversion *) +val out_query : MathQL.mquery -> string (* HTML representation of a query *) -val parse_text : in_channel -> MathQL.mquery (* textual parsing of a query *) +val out_result : MathQL.mqresult -> string (* HTML representation of a query result *) + +val tref_uref : MathQL.mquref -> MathQL.mqtref (* "tref of uref" conversion *) + +val parse_text : in_channel -> MathQL.mquery (* textual parsing of a query *) diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml index 82ab6f9da..d18ebbc92 100644 --- a/helm/ocaml/mathql/mathQL.ml +++ b/helm/ocaml/mathql/mathQL.ml @@ -67,8 +67,6 @@ type mquref = UriManager.uri * (int list) (* uri, fragment identifier *) type mqtref = mqpt * (mqbt list) * (mqft list) (* tokenized pattern reference *) -type mqref = string (* format for references (helper) *) - type mqfunc = | MQName (* Name *) | MQTheory (* theory *) @@ -115,8 +113,8 @@ type mqbool = | MQSubset of mqlist * mqlist (* the two lists denote two sets, the 1st subset of the 2nd *) and mqlist = - | MQReference of mqref list (* reference list *) - | MQPattern of mqtref list (* pattern list *) + | MQReference of string list (* reference list *) + | MQPattern of mqtref (* pattern *) | MQListLVar of mqlvar (* lvar *) | MQListRVar of mqrvar (* rvar *) | MQSelect of mqrvar * mqlist * mqbool (* rvar, list, boolean *) @@ -127,8 +125,7 @@ and mqlist = | MQSortedBy of mqlist * mqorder * mqfunc (* ordering *) | MQDiff of mqlist * mqlist (* set difference *) | MQLetIn of mqlvar * mqlist * mqlist (* explicit lvar assignment *) - | MQMinimize of mqlist (* list minimization *) - + type mquery = | MQList of mqlist @@ -136,4 +133,4 @@ type mquery = (* main type is mqresult *) type mqresult = - | MQRefs of mqref list + | MQRefs of string list diff --git a/helm/ocaml/mathql_interpreter/diff.ml b/helm/ocaml/mathql_interpreter/diff.ml index b32468e40..e2eea1bc1 100644 --- a/helm/ocaml/mathql_interpreter/diff.ml +++ b/helm/ocaml/mathql_interpreter/diff.ml @@ -75,10 +75,10 @@ let diff_ex l1 l2 = let ll1 = string_of_int (List.length l1) in let ll2 = string_of_int (List.length l2) in let diff = string_of_float (after -. before) in - prerr_endline + print_endline ("DIFF(" ^ ll1 ^ ", " ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ ": " ^ diff ^ "s") ; - flush stderr ; + flush stdout ; res ;; diff --git a/helm/ocaml/mathql_interpreter/intersect.ml b/helm/ocaml/mathql_interpreter/intersect.ml index 4152a280d..bf0d05c2c 100644 --- a/helm/ocaml/mathql_interpreter/intersect.ml +++ b/helm/ocaml/mathql_interpreter/intersect.ml @@ -119,9 +119,9 @@ let intersect_ex l1 l2 = let ll1 = string_of_int (List.length l1) in let ll2 = string_of_int (List.length l2) in let diff = string_of_float (after -. before) in - prerr_endline + print_endline ("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ ": " ^ diff ^ "s") ; - flush stderr ; + flush stdout ; res ;; diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml index 5fbfc86c6..cf453c6f6 100644 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -92,13 +92,6 @@ let get_prop_id prop = else List.assoc prop (match !prop_pool with Some l -> l | _ -> assert false) ;; -(* automatically performes the union of a given list of patterns *) -let rec pattern_list_ex = function - | [] -> [] - | [(apreamble, apattern, afragid)] -> pattern_ex (apreamble, apattern, afragid) - | (apreamble, apattern, afragid) :: tail -> - union_ex (pattern_ex (apreamble, apattern, afragid)) (pattern_list_ex tail) - (* execute_ex env q *) (* [env] is the attributed uri environment in which the query [q] *) (* must be evaluated *) @@ -112,8 +105,8 @@ let rec execute_ex env = use_ex (execute_ex env alist) asvar (get_prop_id "refObj") (* "F" (*"refObj"*) *) | MQUse (alist, asvar) -> use_ex (execute_ex env alist) asvar (get_prop_id "backPointer") (* "B" (*"backPointer"*) *) - | MQPattern l -> - pattern_list_ex l + | MQPattern (apreamble, apattern, afragid) -> + pattern_ex (apreamble, apattern, afragid) | MQUnion (l1, l2) -> union_ex (execute_ex env l1) (execute_ex env l2) | MQDiff (l1, l2) -> diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml index c9680f6c3..c25ea2625 100644 --- a/helm/ocaml/mathql_interpreter/select.ml +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -92,7 +92,12 @@ let rec is_good env = in let ul1 = set_of_result (None,!execute env q1) in let ul2 = set_of_result (None,!execute env q2) in -prerr_endline ("MQSETEQUAL(" ^ string_of_int (List.length (!execute env q1)) ^ ">" ^ string_of_int (List.length ul1) ^ "," ^ string_of_int (List.length (!execute env q2)) ^ ">" ^ string_of_int (List.length ul2) ^ ")") ; flush stderr ; + print_endline ("MQSETEQUAL(" ^ + string_of_int (List.length (!execute env q1)) ^ ">" ^ + string_of_int (List.length ul1) ^ "," ^ + string_of_int (List.length (!execute env q2)) ^ ">" ^ + string_of_int (List.length ul2) ^ ")") ; + flush stdout ; (try List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2 with @@ -110,7 +115,12 @@ prerr_endline ("MQSETEQUAL(" ^ string_of_int (List.length (!execute env q1)) ^ " in let ul1 = set_of_result (None,!execute env q1) in let ul2 = set_of_result (None,!execute env q2) in -prerr_endline ("MQSUBSET(" ^ string_of_int (List.length (!execute env q1)) ^ ">" ^ string_of_int (List.length ul1) ^ "," ^ string_of_int (List.length (!execute env q2)) ^ ">" ^ string_of_int (List.length ul2) ^ ")") ; flush stderr ; + print_endline ("MQSUBSET(" ^ + string_of_int (List.length (!execute env q1)) ^ ">" ^ + string_of_int (List.length ul1) ^ "," ^ + string_of_int (List.length (!execute env q2)) ^ ">" ^ + string_of_int (List.length ul2) ^ ")") ; + flush stdout ; let rec is_subset s1 s2 = match s1,s2 with [],_ -> true diff --git a/helm/ocaml/mathql_interpreter/sortedby.ml b/helm/ocaml/mathql_interpreter/sortedby.ml index d468ae2fc..177cf3c03 100644 --- a/helm/ocaml/mathql_interpreter/sortedby.ml +++ b/helm/ocaml/mathql_interpreter/sortedby.ml @@ -53,10 +53,10 @@ let sortedby_ex alist order afunc = let after = Unix.time () and ll1 = string_of_int (List.length alist) in let diff = string_of_float (after -. before) in - prerr_endline + print_endline ("SORTEDBY(" ^ ll1 ^ ") = " ^ string_of_int (List.length res) ^ ": " ^ diff ^ "s") ; - flush stderr ; + flush stdout ; res ;; diff --git a/helm/ocaml/mathql_interpreter/union.ml b/helm/ocaml/mathql_interpreter/union.ml index 2e83b7a7d..c8e46cd0b 100644 --- a/helm/ocaml/mathql_interpreter/union.ml +++ b/helm/ocaml/mathql_interpreter/union.ml @@ -133,7 +133,7 @@ let union_ex l1 l2 = let ll1 = string_of_int (List.length l1) in let ll2 = string_of_int (List.length l2) in let diff = string_of_float (after -. before) in - prerr_endline ("UNION(" ^ ll1 ^ "," ^ ll2 ^ "): " ^ diff ^ "s") ; - flush stderr ; + print_endline ("UNION(" ^ ll1 ^ "," ^ ll2 ^ "): " ^ diff ^ "s") ; + flush stdout ; res ;; -- 2.39.2