New reduction strategy: the new reduction strategy behaves as the previous

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c0e90a5c6a20157284bf9de115611da4bef94bf6..b57ad4e78876b1192d31a33ec195bd2cf4411b75 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/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 ->
@@ -772,7 +780,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
           C.Rel m when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -784,9 +792,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -809,7 +822,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -818,7 +831,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -830,9 +843,14 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -857,7 +875,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -876,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 ->
@@ -889,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 ->
@@ -952,7 +980,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match CicReduction.whd ~subst context term with
           C.Rel m when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -968,9 +996,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                       let debrujinedty = debrujin_constructor uri len ty in
                        (id, snd (split_prods ~subst tys paramsno ty),
                         snd (split_prods ~subst tys paramsno debrujinedty)
-                       )) cl
+                       )) cl in
+                   let lefts =
+                    match tl with
+                       [] -> assert false
+                     | (_,_,ty,_)::_ ->
+                        fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys,len,isinductive,paramsno,cl')
+                    (tys@lefts,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -996,7 +1029,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
                (fun (p,(_,c,brujinedc)) i ->
-                 let rl' = recursive_args tys 0 len brujinedc in
+                 let rl' = recursive_args lefts_and_tys 0 len brujinedc in
                   let (e,safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
@@ -1004,7 +1037,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                    guarded_by_destructors ~subst context' n' nn' kl x' safes' e
                ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
-           let (tys,len,isinductive,paramsno,cl) =
+           let (lefts_and_tys,len,isinductive,paramsno,cl) =
            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
                C.InductiveDefinition (tl,_,paramsno,_) ->
@@ -1016,9 +1049,14 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods ~subst tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl in
+                  let lefts =
+                   match tl with
+                      [] -> assert false
+                    | (_,_,ty,_)::_ ->
+                       fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys,List.length tl,isinductive,paramsno,cl')
+                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1050,7 +1088,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                (fun (p,(_,c)) i ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
-                   recursive_args tys 0 len debrujinedte
+                   recursive_args lefts_and_tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
@@ -1071,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 ->
@@ -1084,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 ->
@@ -1237,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 &&
@@ -1278,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 &&
@@ -1289,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 &&
@@ -1523,11 +1589,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_gt t' t ugraph in
-         (C.Sort (C.Type t')),ugraph1
-      (* TASSI: CONSTRAINTS *)
+       (try
+         let ugraph1 = CicUniv.add_gt t' t ugraph in
+           (C.Sort (C.Type t')),ugraph1
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
-    | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+    | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
     | C.Cast (te,ty) as t ->
        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
@@ -1812,16 +1880,14 @@ end;
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->
-      let types_times_kl,ugraph1 =
-       (* WAS: list rev list map *)
+      let types,kl,ugraph1,len =
         List.fold_left
-          (fun (l,ugraph) (n,k,ty,_) ->
+          (fun (types,kl,ugraph,len) (n,k,ty,_) ->
             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
-            ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
-         ) ([],ugraph) fl
+             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+              k::kl,ugraph1,len+1)
+         ) ([],[],ugraph,0) fl
       in
-      let (types,kl) = List.split types_times_kl in
-      let len = List.length types in
       let ugraph2 = 
        List.fold_left
           (fun ugraph (name,x,ty,bo) ->
@@ -1855,15 +1921,15 @@ end;
       let (_,_,ty,_) = List.nth fl i in
        ty,ugraph2
    | C.CoFix (i,fl) ->
-       let types,ugraph1 =
+       let types,ugraph1,len =
         List.fold_left
-          (fun (l,ugraph) (n,ty,_) -> 
+          (fun (l,ugraph,len) (n,ty,_) -> 
               let _,ugraph1 = 
                type_of_aux ~logger context ty ugraph in 
-               (Some (C.Name n,(C.Decl ty))::l,ugraph1)
-          ) ([],ugraph) fl
+               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
+                 ugraph1,len+1)
+          ) ([],ugraph,0) fl
        in
-       let len = List.length types in
        let ugraph2 = 
         List.fold_left
            (fun ugraph (_,ty,bo) ->
@@ -1943,9 +2009,12 @@ end;
     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
        let t' = CicUniv.fresh() in
-       let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-       let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-       C.Sort (C.Type t'),ugraph2
+        (try
+         let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+         let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+          C.Sort (C.Type t'),ugraph2
+        with
+         CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
     | (C.Sort _,C.Sort (C.Type t1)) -> 
         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)