Several instances of the same bug fixed at once: when processing a Fix,

before adding the types to the context (to process the bodies), the types
must be lifted. The simplify tactic is still not working propertly.

diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml
index d8392f6206ab745e2647a75286e30745e481e18a..98b14298274542288534df848c3bedf4303fa78d 100644 (file)
--- a/components/cic_acic/cic2acic.ml
+++ b/components/cic_acic/cic2acic.ml
@@ -353,8 +353,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
              let fresh_idrefs =
               List.map (function _ -> gen_id seed) funs in
              let new_idrefs = List.rev fresh_idrefs @ idrefs in
-             let tys =
-              List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+             let tys,_ =
+               List.fold_left
+                 (fun (types,len) (n,_,ty,_) ->
+                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                     len+1)
+                ) ([],0) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
@@ -370,8 +374,12 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
              let fresh_idrefs =
               List.map (function _ -> gen_id seed) funs in
              let new_idrefs = List.rev fresh_idrefs @ idrefs in
-             let tys =
-              List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
+             let tys,_ =
+               List.fold_left
+                 (fun (types,len) (n,ty,_) ->
+                    (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                     len+1)
+                ) ([],0) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = `Prop then
@@ -687,9 +695,12 @@ let plain_acic_term_of_cic_term =
       C.AMutCase (fresh_id, uri, tyno, aux context outty,
        aux context term, List.map (aux context) patterns)
    | C.Fix (funno, funs) ->
-      let tys =
-       List.map
-        (fun (name,_,ty,_) -> mk_fresh_id (), Some (C.Name name, C.Decl ty)) funs
+      let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+            (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+              len+1
+         ) ([],0) funs
       in
        C.AFix (fresh_id, funno,
         List.map2
@@ -698,9 +709,12 @@ let plain_acic_term_of_cic_term =
          ) tys funs
       )
    | C.CoFix (funno, funs) ->
-      let tys =
-       List.map (fun (name,ty,_) ->
-        mk_fresh_id (),Some (C.Name name, C.Decl ty)) funs
+      let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+            (mk_fresh_id (),(Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))))::types,
+              len+1
+         ) ([],0) funs
       in
        C.ACoFix (fresh_id, funno,
         List.map2

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index 576721be3542c1b67a098c05f0fbbadede1e2f85..bfba135cf992cb6c44c9cba58364f9f42e9c3f61 100644 (file)
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -973,8 +973,12 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-            let tys =
-              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,_,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+               ) ([],0) fl1
             in
             if i1 = i2 then
              List.fold_right2
@@ -992,9 +996,13 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+               ) ([],0) fl1
+            in
             if i1 = i2 then
               List.fold_right2
               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->

diff --git a/components/cic_proof_checking/cicTypeChecker.ml b/components/cic_proof_checking/cicTypeChecker.ml
index 5dc42548953c9bf231372f94486a14c2153bba0a..b57ad4e78876b1192d31a33ec195bd2cf4411b75 100644 (file)
--- a/components/cic_proof_checking/cicTypeChecker.ml
+++ b/components/cic_proof_checking/cicTypeChecker.ml
@@ -292,8 +292,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
         in
          List.fold_right
           (fun (_,_,ty,bo) i ->
@@ -304,8 +308,12 @@ and does_not_occur ?(subst=[]) context n nn te =
        let len = List.length fl in
         let n_plus_len = n + len in
         let nn_plus_len = nn + len in
-        let tys =
-         List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+        let tys,_ =
+         List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
         in
          List.fold_right
           (fun (_,ty,bo) i ->
@@ -886,7 +894,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -899,7 +912,12 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -1091,7 +1109,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,_,ty,bo) i ->
@@ -1104,7 +1127,12 @@ and guarded_by_destructors ~subst context n nn kl x safes =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        and x_plus_len = x + len
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        and safes' = List.map (fun x -> x + len) safes in
         List.fold_right
          (fun (_,ty,bo) i ->
@@ -1257,7 +1285,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
         let n_plus_len = n + len
         and nn_plus_len = nn + len
         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+        and tys,_ =
+          List.fold_left
+            (fun (types,len) (n,ty,_) ->
+               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+           ) ([],0) fl
+        in
          List.fold_right
           (fun (_,ty,bo) i ->
             i && does_not_occur ~subst context n nn ty &&
@@ -1298,7 +1332,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
+       in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i && does_not_occur ~subst context n nn ty &&
@@ -1309,7 +1349,13 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+       and tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
+       in
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur ~subst context n nn ty &&
@@ -1835,7 +1881,6 @@ end;
            outtype,ugraph5
    | C.Fix (i,fl) ->
       let types,kl,ugraph1,len =
-       (* WAS: list rev list map *)
         List.fold_left
           (fun (types,kl,ugraph,len) (n,k,ty,_) ->
             let _,ugraph1 = type_of_aux ~logger context ty ugraph in

diff --git a/components/cic_proof_checking/freshNamesGenerator.ml b/components/cic_proof_checking/freshNamesGenerator.ml
index 3cfda02dff123a649bf51005ed6a0c01647c275d..73b75ce18e7257e876a0d316d934fd95db15350d 100755 (executable)
--- a/components/cic_proof_checking/freshNamesGenerator.ml
+++ b/components/cic_proof_checking/freshNamesGenerator.ml
@@ -193,9 +193,13 @@ let rec mk_fresh_names ~subst metasenv context t =
        let pl' = List.map (mk_fresh_names ~subst metasenv context) pl in
        Cic.MutCase (sp, i, outty', t', pl')
     | Cic.Fix (i, fl) -> 
-        let tys = List.map 
-           (fun (n,_,ty,_) -> 
-             Some (Cic.Name n,(Cic.Decl ty))) fl in
+        let tys,_ =
+          List.fold_left
+            (fun (types,len) (n,_,ty,_) ->
+               (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+           ) ([],0) fl
+        in
        let fl' = List.map 
            (fun (n,i,ty,bo) -> 
              let ty' = mk_fresh_names ~subst metasenv context ty in
@@ -203,9 +207,13 @@ let rec mk_fresh_names ~subst metasenv context t =
              (n,i,ty',bo')) fl in
        Cic.Fix (i, fl') 
     | Cic.CoFix (i, fl) ->
-       let tys = List.map 
-           (fun (n,_,ty) -> 
-             Some (Cic.Name n,(Cic.Decl ty))) fl in
+        let tys,_ =
+          List.fold_left
+            (fun (types,len) (n,ty,_) ->
+               (Some (Cic.Name n,(Cic.Decl (CicSubstitution.lift len ty)))::types,
+                len+1)
+           ) ([],0) fl
+        in
        let fl' = List.map 
            (fun (n,ty,bo) -> 
              let ty' = mk_fresh_names ~subst metasenv context ty in

diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml
index 1b5922d1d28f8f0af33c462f55ea1d07d21faa18..f72ec4679842b9888bed5b07b9e92bc48fd50b28 100644 (file)
--- a/components/tactics/proofEngineReduction.ml
+++ b/components/tactics/proofEngineReduction.ml
@@ -587,8 +587,12 @@ let reduce context =
              if l = [] then res else C.Appl (res::l)
        )
     | C.Fix (i,fl) ->
-       let tys =
-        List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,_,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        in
         let t' () =
          let fl' =
@@ -625,8 +629,12 @@ let reduce context =
              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
            )
     | C.CoFix (i,fl) ->
-       let tys =
-        List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        in
         let t' =
          let fl' =
@@ -819,8 +827,12 @@ let simpl context =
              if l = [] then res else C.Appl (res::l)
        )
     | C.Fix (i,fl) ->
-       let tys =
-        List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+         List.fold_left
+           (fun (types,len) (n,_,ty,_) ->
+              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+               len+1)
+          ) ([],0) fl
        in
         let t' () =
          let fl' =
@@ -857,8 +869,12 @@ let simpl context =
              | None -> if l = [] then t' () else C.Appl ((t' ())::l)
            )
     | C.CoFix (i,fl) ->
-       let tys =
-        List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       let tys,_ =
+        List.fold_left
+          (fun (types,len) (n,ty,_) ->
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              len+1)
+         ) ([],0) fl
        in
         let t' =
          let fl' =