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

[helm.git] / helm / software / components / acic_procedural / acic2Procedural.ml

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