let inter = Constr.UriManagerSet.inter set1 set2 in
List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
+(* Profiling code
let at_most =
let profiler = CicUtil.profile "at_most" in
- fun ~dbd ~where uri -> profiler (Constr.at_most ~dbd ~where) uri
+ fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
let sigmatch =
let profiler = CicUtil.profile "sigmatch" in
fun ~dbd ~facts ~where signature ->
- profiler (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+ profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+*) let at_most = Constr.at_most let sigmatch = MetadataConstraints.sigmatch
let filter_uris_forward ~dbd (main, constants) uris =
let main_uris =
| _ -> bag)
s s
+(* Profiling code
let apply_tac_verbose =
let profiler = CicUtil.profile "apply_tac_verbose" in
- fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
+ fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
let sigmatch =
let profiler = CicUtil.profile "sigmatch" in
- fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler (Constr.sigmatch ~dbd ~facts ~where) signature
+ fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
let cmatch' =
let profiler = CicUtil.profile "cmatch'" in
- fun ~dbd ~facts signature -> profiler (Constr.cmatch' ~dbd ~facts) signature
+ fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
+*) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch'
let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
let (_, metasenv, _, _) = proof in
function
Cic.Lambda (n,s,t) ->
let dummy_uri =
- UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in
+ UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
(aux (i+1) (s::types)
(CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
| t -> t,types
when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
let s = UriManager.string_of_uri s in
let len = String.length s in
- let dummy_index = int_of_string (String.sub s 11 (len-11)) in
+ let dummy_index = int_of_string (String.sub s 11 (len-15)) in
let dummy_type = List.nth types dummy_index in
Some (d,dummy_type)
| _::l -> look_for_dummy_main l
(Mysql.escape (UriManager.string_of_uri outer)) in
let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
let result = Mysql.exec dbd query in
- let lemmas = Mysql.map result ~f:(map inners) in
+ let lemmas = Mysql.map ~f:(map inners) result in
let ranked = List.fold_left rank [] lemmas in
let ordered = List.rev (List.fast_sort compare ranked) in
map_filter filter 0 ordered
+
+(* get_decomposables ********************************************************)
+
+let decomposables ~dbd =
+ let map row = match row.(0) with
+ | None -> None
+ | Some str ->
+ match CicUtil.term_of_uri (UriManager.uri_of_string str) with
+ | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno)
+ | _ ->
+ raise (UriManager.IllFormedUri str)
+ in
+ let select, from = "source", "decomposables" in
+ let query = Printf.sprintf "SELECT %s FROM %s" select from in
+ let decomposables = Mysql.map ~f:map (Mysql.exec dbd query) in
+ map_filter (fun _ x -> x) 0 decomposables