parameter sintax added to axiom statement

[helm.git] / helm / software / components / metadata / metadataConstraints.ml

diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index a4267c5fc6825faa3ccd11da33dc7e8d00a789ce..3e8ac2f7250c3aa29ec3bffa835589c0711fe365 100644 (file)
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -28,6 +28,9 @@
 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
 
@@ -165,7 +168,7 @@ let exec dbtype ~(dbd:HSql.dbd) ?rating (n,from,where) =
             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 -> 
@@ -269,8 +272,9 @@ and inspect_conclusion n t =
        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) ->
@@ -308,7 +312,7 @@ let rec inspect_term n t =
        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
@@ -377,18 +381,28 @@ and signature_concl =
     | 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 _
@@ -398,7 +412,7 @@ and signature_concl =
 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) ->
@@ -641,25 +655,25 @@ let sigmatch ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
    | 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
@@ -667,7 +681,7 @@ let sigmatch ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
         (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 *)