- metasenv is now checked

- the last commit introduced a bug: the debrujin function was called on
  the type of a constructor _before_ removing the left parameters. Fixed.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index ce52754702d9c77ac3318480548210e2d2b7f621..57bc5e2ad3698be43ae6a93e77d45b0273d100bb 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -138,11 +138,17 @@ let rec type_of_constant uri =
            (* only to check that ty is well-typed *)
            let _ = type_of ty in ()
          | C.CurrentProof (_,conjs,te,ty,_) ->
-             (*CSC: bisogna controllare anche il metasenv!!! *)
-             let _ = type_of_aux' conjs [] ty in
-              if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
-              then
-               raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
+             let _ =
+              List.fold_left
+               (fun metasenv ((_,context,ty) as conj) ->
+                 ignore (type_of_aux' metasenv context ty) ;
+                 metasenv @ [conj]
+               ) [] conjs
+             in
+              let _ = type_of_aux' conjs [] ty in
+               if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
+               then
+                raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
@@ -635,7 +641,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, ty, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -648,9 +654,9 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                pl true
             else
               List.fold_right
-               (fun (p,(_,te,c)) i ->
+               (fun (p,(_,c)) i ->
                  let rl' =
-                  let debrujinedte = debrujin_constructor uri len te in
+                  let debrujinedte = debrujin_constructor uri len c in
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
@@ -670,7 +676,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, ty, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -685,9 +691,9 @@ and check_is_really_smaller_arg context n nn kl x safes te =
               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
               (*CSC: sugli argomenti di una applicazione                      *)
               List.fold_right
-               (fun (p,(_,te,c)) i ->
+               (fun (p,(_,c)) i ->
                  let rl' =
-                  let debrujinedte = debrujin_constructor uri len te in
+                  let debrujinedte = debrujin_constructor uri len c in
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =
@@ -791,7 +797,7 @@ and guarded_by_destructors context n nn kl x safes =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, ty, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -809,9 +815,9 @@ and guarded_by_destructors context n nn kl x safes =
              guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
-               (fun (p,(_,te,c)) i ->
+               (fun (p,(_,c)) i ->
                  let rl' =
-                  let debrujinedte = debrujin_constructor uri len te in
+                  let debrujinedte = debrujin_constructor uri len c in
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
@@ -831,7 +837,7 @@ and guarded_by_destructors context n nn kl x safes =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, ty, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -853,9 +859,9 @@ and guarded_by_destructors context n nn kl x safes =
                  i && guarded_by_destructors context n nn kl x safes t)
                tl true &&
               List.fold_right
-               (fun (p,(_,te,c)) i ->
+               (fun (p,(_,c)) i ->
                  let rl' =
-                  let debrujinedte = debrujin_constructor uri len te in
+                  let debrujinedte = debrujin_constructor uri len c in
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e, safes',n',nn',x',context') =