cicUtil : we added a context to is_sober to check for consistancy

                     of RELS (not implemented yet)
doubleTypeInference: the inferred name of an anonymous lambda must be the name
                     of the expected prod :)
acic2Procedural    : we added a consistancy check that was missing

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index dd59d1f6e5305dfb74b04ea21dd7c035a21f62b1..a6e0667b05de904d64209c177889ea06b3f37daa 100644 (file)
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -202,8 +202,8 @@ let mk_convert st ?name sty ety note =
         [T.Note note]
       else []
    in
-   assert (Ut.is_sober csty); 
-   assert (Ut.is_sober cety);
+   assert (Ut.is_sober st.context csty); 
+   assert (Ut.is_sober st.context cety);
    if Ut.alpha_equivalence csty cety then script else 
    let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
    match name with
@@ -266,11 +266,14 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
         in
         if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
            {st with context = Cn.clear st.context premise}, script name
-        else
+        else begin
+           assert (Ut.is_sober st.context (H.cic ity));
+           let ity = H.acic_bc st.context ity in
            let br1 = [T.Id ""] in
            let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
            let text = "non linear rewrite" in
            st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
+        end
       | _                         -> assert false
 
 let mk_rewrite st dtext where qs tl direction t = 
@@ -305,8 +308,9 @@ and proc_letin st what name v w t =
               | C.AAppl (_, hd :: tl) when is_fwd_rewrite_left hd tl  ->
                  mk_fwd_rewrite st dtext intro tl false v t ity
               | v                                                     ->
+                 assert (Ut.is_sober st.context (H.cic ity));
+                 let ity = H.acic_bc st.context ity in
                  let qs = [proc_proof (next st) v; [T.Id ""]] in
-                 let ity = H.acic_bc st.context ity in
                  st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
            in
            st, C.Decl (H.cic ity), rqv

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 75b7fd2cc8505390ec0ff96cc203d9744fd5b390..8c42aed6131a5348fb542f580eb1422f423d87e8 100644 (file)
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -557,43 +557,44 @@ let alpha_equivalence =
   in
    aux
 
-let is_sober t =
-   let rec sober_term g = function
+let is_sober c t =
+   let rec sober_term c g = function
       | C.Rel _ 
       | C.Sort _  
       | C.Implicit _                    -> g      
       | C.Const (_, xnss) 
       | C.Var (_, xnss) 
       | C.MutConstruct (_, _, _, xnss)
-      | C.MutInd (_, _, xnss)           -> sober_xnss g xnss
-      | C.Meta (_, xss)                 -> sober_xss g xss
+      | C.MutInd (_, _, xnss)           -> sober_xnss c g xnss
+      | C.Meta (_, xss)                 -> sober_xss c g xss
       | C.Lambda (_, v, t)
       | C.Prod (_, v, t)
-      | C.Cast (t, v)                   -> sober_term (sober_term g t) v
-      | C.LetIn (_, v, ty, t)           -> sober_term
-                                            (sober_term (sober_term g t) ty) v
+      | C.Cast (t, v)                   ->
+         sober_term c (sober_term c g t) v
+      | C.LetIn (_, v, ty, t)           ->
+         sober_term c (sober_term c (sober_term c g t) ty) v
       | C.Appl []                       
       | C.Appl [_]                      -> fun b -> false
-      | C.Appl ts                       -> sober_terms g ts
+      | C.Appl ts                       -> sober_terms c g ts
       | C.MutCase (_, _, t, v, ts)      -> 
-         sober_terms (sober_term (sober_term g t) v) ts
-      | C.Fix (_, ifs)                  -> sober_ifs g ifs
-      | C.CoFix (_, cifs)               -> sober_cifs g cifs
-   and sober_terms g = List.fold_left sober_term g
-   and sober_xnss g =
-      let map g (_, t) = sober_term g t in
+         sober_terms c (sober_term c (sober_term c g t) v) ts
+      | C.Fix (_, ifs)                  -> sober_ifs c g ifs
+      | C.CoFix (_, cifs)               -> sober_cifs c g cifs
+   and sober_terms c g = List.fold_left (sober_term c) g
+   and sober_xnss c g =
+      let map g (_, t) = sober_term c g t in
       List.fold_left map g
-   and sober_xss g =
+   and sober_xss c g =
       let map g = function 
          | None   -> g
-        | Some t -> sober_term g t
+        | Some t -> sober_term c g t
       in
       List.fold_left map g
-   and sober_ifs g =
-      let map g (_, _, t, v) = sober_term (sober_term g t) v in
+   and sober_ifs c g =
+      let map g (_, _, t, v) = sober_term c (sober_term c g t) v in
       List.fold_left map g
-   and sober_cifs g =
-      let map g (_, t, v) = sober_term (sober_term g t) v in
+   and sober_cifs c g =
+      let map g (_, t, v) = sober_term c (sober_term c g t) v in
       List.fold_left map g
    in 
-   sober_term (fun b -> b) t true
+   sober_term c (fun b -> b) t true

diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli
index 9977d186465c24e245e4ea404a8ae6bf1c4ca812..54a0a9bea639a2d72a16a03840b0166382c4625e 100644 (file)
--- a/helm/software/components/cic/cicUtil.mli
+++ b/helm/software/components/cic/cicUtil.mli
@@ -70,4 +70,4 @@ val alpha_equivalence: Cic.term -> Cic.term -> bool
 (* FG: Consistency Check 
  * detects applications without arguments
  *)
-val is_sober: Cic.term -> bool
+val is_sober: Cic.context -> Cic.term -> bool

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index 1671b98d25321ca6492f8565715ba99d5ddfedba..7f93716b26c6685e1b3a2c74e3da64fc1b4d95cc 100644 (file)
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -339,17 +339,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
      | C.Lambda (n,s,t) ->
         (* Let's visit all the subterms that will not be visited later *)
          let _ = type_of_aux context s None in 
-         let expected_target_type =
+         let n, expected_target_type =
           match expectedty with
-             None -> None
+           | None -> n, None
            | Some expectedty' ->
-              let ty =
+              let n, ty =
                match R.whd context expectedty' with
-                  C.Prod (_,_,expected_target_type) ->
-                   beta_reduce expected_target_type
+                | C.Prod (n',_,expected_target_type) ->
+                   let xtt = beta_reduce expected_target_type in
+                  if n <> C.Anonymous then n, xtt else n', xtt
                 | _ -> assert false
               in
-               Some ty
+               n, Some ty
          in 
           let type2 =
            type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type