X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fwhelp%2FfwdQueries.ml;h=5453c544e5202f010faa923d0e0d18905cbfdf04;hb=4573f1fecaf83f4706f39702555d5319d132477b;hp=1f4e508fc032f7534d82e32b44a706b6a199ccac;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/whelp/fwdQueries.ml b/helm/software/components/whelp/fwdQueries.ml index 1f4e508fc..5453c544e 100644 --- a/helm/software/components/whelp/fwdQueries.ml +++ b/helm/software/components/whelp/fwdQueries.ml @@ -89,10 +89,10 @@ let fwd_simpl ~dbd t = let from = "genLemma" in let where = Printf.sprintf "h_outer = \"%s\"" - (HMysql.escape (UriManager.string_of_uri outer)) in + (HSql.escape HSql.Library dbd (UriManager.string_of_uri outer)) in let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in - let result = HMysql.exec dbd query in - let lemmas = HMysql.map ~f:(map inners) result in + let result = HSql.exec HSql.Library dbd query in + let lemmas = HSql.map ~f:(map inners) result in let ranked = List.fold_left rank [] lemmas in let ordered = List.rev (List.fast_sort compare ranked) in filter_map_n filter 0 ordered @@ -104,12 +104,12 @@ let decomposables ~dbd = | None -> None | Some str -> match CicUtil.term_of_uri (UriManager.uri_of_string str) with - | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno) + | Cic.MutInd (uri, typeno, _) -> Some (uri, Some typeno) + | Cic.Const (uri, _) -> Some (uri, None) | _ -> raise (UriManager.IllFormedUri str) in let select, from = "source", "decomposables" in let query = Printf.sprintf "SELECT %s FROM %s" select from in - let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in + let decomposables = HSql.map ~f:map (HSql.exec HSql.Library dbd query) in filter_map_n (fun _ x -> x) 0 decomposables -