X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FmQueryGenerator.ml;h=dd8b00ae327aeb0248acc88a92024046320b7051;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=7e0dd9c965ba8aeb4ddef341ad9f6a60a6cada5c;hpb=f148b4ddc2333650e49436ff6693d1ad1847f8fb;p=helm.git diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 7e0dd9c96..dd8b00ae3 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -35,7 +35,7 @@ module U = MQGUtil let locate s = let query = M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) ) - in M.StatQuery query + in query let unreferred target_pattern source_pattern = let query = @@ -46,7 +46,7 @@ let unreferred target_pattern source_pattern = M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern)) )) - in M.StatQuery query + in query let compose cl = let letin = ref [] in @@ -81,7 +81,13 @@ let compose cl = M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const "")) in let property_only n cl = - let cll = List.map (cons true) cl in + let rec build = function + | [] -> [] + | c :: tl -> + let r = (cons true) c in + if r = [] then build tl else r :: build tl + in + let cll = build cl in M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) in let rec aux = function @@ -108,8 +114,8 @@ let compose cl = | [head] -> (f head) | head :: tail -> let t = (iter f g tail) in g (f head) t in - prerr_endline "(** Compose: received constraints **)"; - U.mathql_of_specs prerr_string cl; flush stderr; + (* prerr_endline "(** Compose: received constraints **)"; + U.mathql_of_specs prerr_string cl; flush stderr; *) aux cl; let must_query = if ! must = [] then @@ -137,7 +143,7 @@ let compose cl = let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in iter f (fun x y z -> x (y z)) ! letin in - M.StatQuery (letin_query (select_query must_query)) + letin_query (select_query must_query) (* high-level functions ****************************************************) @@ -181,4 +187,3 @@ let query_of_constraints u (musts_obj, musts_rel, musts_sort) in let univ = match u with None -> [] | Some l -> [T.Universe l] in compose (must @ only @ univ) -