open Printf
open MetadataTypes
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
+
let critical_value = 7
let just_factor = 1
and table0.source = hits.source order by hits.no desc")
from where
in
- (* prerr_endline query; *)
+ (* debug_print (lazy query); *)
let result = HSql.exec dbtype dbd query in
HSql.map result
~f:(fun row ->
merge n (inspect_conclusion n s) (inspect_conclusion n t)
| Cic.Lambda (_, s, t) ->
merge n (inspect_conclusion n s) (inspect_conclusion n t)
- | Cic.LetIn (_, s, t) ->
- merge n (inspect_conclusion n s) (inspect_conclusion n t)
+ | Cic.LetIn (_, s, ty, t) ->
+ merge n (inspect_conclusion n s)
+ (merge n (inspect_conclusion n ty) (inspect_conclusion n t))
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
add_root (n-1) u l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
Some uri, SetSet.empty
| Cic.Cast (t, _) -> inspect_term n t
| Cic.Prod (_, _, t) -> inspect_term n t
- | Cic.LetIn (_, _, t) -> inspect_term n t
+ | Cic.LetIn (_, _, _, t) -> inspect_term n t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
let childunion = inspect_children (n-1) l in
Some u, childunion
| Cic.Const (u,exp_named_subst) ->
UriManagerSet.singleton u
| Cic.MutInd (u, t, exp_named_subst) ->
+ let rec projections_of uris =
+ List.flatten
+ (List.map
+ (fun uri ->
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+ projections_of (CicUtil.projections_of_record o uri))
+ uris)
+ in
let uri = UriManager.uri_of_uriref u t None in
- UriManagerSet.singleton uri
+ List.fold_right UriManagerSet.add
+ (projections_of [u]) (UriManagerSet.singleton uri)
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
let uri = UriManager.uri_of_uriref u t (Some c) in
- UriManagerSet.singleton uri
+ UriManagerSet.singleton uri
| Cic.Cast (t, _) -> signature_concl t
| Cic.Prod (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
| Cic.Lambda (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
- | Cic.LetIn (_, s, t) ->
- UriManagerSet.union (signature_concl s) (signature_concl t)
+ | Cic.LetIn (_, s, ty, t) ->
+ UriManagerSet.union (signature_concl s)
+ (UriManagerSet.union (signature_concl ty) (signature_concl t))
| Cic.Appl l -> add l
| Cic.MutCase _
| Cic.Fix _
let rec signature_of = function
| Cic.Cast (t, _) -> signature_of t
| Cic.Prod (_, _, t) -> signature_of t
- | Cic.LetIn (_, _, t) -> signature_of t
+ | Cic.LetIn (_, _, _, t) -> signature_of t
| Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
Some (u, []), add l
| Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
| Some (main, types) -> Some main,types
in
let constants_no = UriManagerSet.cardinal constants in
- (* prerr_endline (("constants_no: ")^(string_of_int constants_no)); *)
+ (* debug_print (lazy (("constants_no: ")^(string_of_int constants_no))); *)
if (constants_no > critical_value) then
let subsets =
let subsets = power_upto just_factor constants in
- (* let _ = prerr_endline (("subsets: ")^
- (string_of_int (List.length subsets))) in *)
+ (* let _ = debug_print (lazy (("subsets: ")^
+ (string_of_int (List.length subsets)))) in *)
let types_no = List.length types in
if types_no > 0 then
List.map (function (n,l) -> (n+types_no,types@l)) subsets
else subsets
in
- prerr_endline ("critical_value exceded..." ^ string_of_int constants_no);
+ debug_print (lazy ("critical_value exceded..." ^ string_of_int constants_no));
let all_constants =
let all = match main with None -> types | Some m -> m::types in
List.fold_right UriManagerSet.add all constants
in
compute_with_only ~dbd ~where main subsets all_constants
else
- (prerr_endline ("all subsets..." ^ string_of_int constants_no);
+ (debug_print (lazy ("all subsets..." ^ string_of_int constants_no));
let subsets =
let subsets = power constants in
let types_no = List.length types in
(0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
else subsets
in
- prerr_endline "fine1";
+ debug_print (lazy "fine1");
compute_exactly ~dbd ~facts ~where main subsets)
(* match query wrappers *)