X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=11d68b78c052d0d653bb2b73372c3afd160d2dee;hb=ba64642ca7771cd9cc7b9f73476c8f608ffeeda5;hp=2e8b5585f5190c6d2110ef8fab6a576b39f7b614;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2e8b5585f..11d68b78c 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -75,6 +75,7 @@ let rec cooked_type_of_constant uri cookingsno =
            (* 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
@@ -141,7 +142,6 @@ and does_not_occur context n nn te =
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
     | C.Const _
-    | C.Abst _
     | C.MutInd _
     | C.MutConstruct _ -> true
     | C.MutCase (_,_,_,out,te,pl) ->
@@ -444,8 +444,7 @@ and recursive_args context n nn te =
    | C.Lambda _
    | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
    | C.Appl _ -> []
-   | C.Const _
-   | C.Abst _ -> raise (Impossible 5)
+   | C.Const _ -> raise (Impossible 5)
    | C.MutInd _
    | C.MutConstruct _
    | C.MutCase _
@@ -537,7 +536,6 @@ and check_is_really_smaller_arg context n nn kl x safes te =
       check_is_really_smaller_arg context n nn kl x safes he
    | C.Appl [] -> raise (Impossible 11)
    | C.Const _
-   | C.Abst _
    | C.MutInd _ -> raise (Impossible 12)
    | C.MutConstruct _ -> false
    | C.MutCase (uri,_,i,outtype,term,pl) ->
@@ -697,7 +695,6 @@ and guarded_by_destructors context n nn kl x safes =
        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
        tl true
    | C.Const _
-   | C.Abst _
    | C.MutInd _
    | C.MutConstruct _ -> true
    | C.MutCase (uri,_,i,outtype,term,pl) ->
@@ -885,8 +882,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
             guarded_by_constructors context n nn true te tl coInductiveTypeURI
          | C.Appl _ ->
             does_not_occur context n nn te
-         | C.Const _
-         | C.Abst _ -> raise (Impossible 26)
+         | C.Const _ -> raise (Impossible 26)
          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
             guarded_by_constructors context n nn true te [] coInductiveTypeURI
          | C.MutInd _ ->
@@ -920,8 +916,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
          | C.Appl _ -> 
             List.fold_left
              (fun i x -> i && does_not_occur context n nn x) true l
-         | C.Const _
-         | C.Abst _ -> raise (Impossible 31)
+         | C.Const _ -> raise (Impossible 31)
          | C.MutInd _ ->
             List.fold_left
              (fun i x -> i && does_not_occur context n nn x) true l
@@ -980,7 +975,6 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
    | C.Const _ -> true
-   | C.Abst _
    | C.MutInd _ -> assert false
    | C.MutConstruct _ -> true
    | C.MutCase (_,_,_,out,te,pl) ->
@@ -1110,10 +1104,14 @@ and type_of_branch context argsno need_dummy outtype term constype =
        else
         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
    | C.Prod (name,so,de) ->
-      C.Prod (C.Anonimous,so,type_of_branch
-       ((Some (name,(C.Decl so)))::context) argsno need_dummy
-       (CicSubstitution.lift 1 outtype)
-       (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
+      let term' =
+       match CicSubstitution.lift 1 term with
+          C.Appl l -> C.Appl (l@[C.Rel 1])
+        | t -> C.Appl [t ; C.Rel 1]
+      in
+       C.Prod (C.Anonimous,so,type_of_branch
+        ((Some (name,(C.Decl so)))::context) argsno need_dummy
+        (CicSubstitution.lift 1 outtype) term' de)
   | _ -> raise (Impossible 20)
 
 (* check_metasenv_consistency checks that the "canonical" context of a
@@ -1136,19 +1134,19 @@ and check_metasenv_consistency metasenv context canonical_context l =
     in
      aux 1 canonical_context
    in
-  List.iter2 
-    (fun t ct -> 
-      let res =
-       match (t,ct) with
-          _,None -> true
-        | Some t,Some (_,C.Def ct) ->
-           R.are_convertible context t ct
-        | Some t,Some (_,C.Decl ct) ->
-           R.are_convertible context (type_of_aux' metasenv context t) ct
-        | _, _  -> false
-      in
-       if not res then raise MetasenvInconsistency
-    ) l lifted_canonical_context 
+    List.iter2 
+     (fun t ct -> 
+       let res =
+        match (t,ct) with
+           _,None -> true
+         | Some t,Some (_,C.Def ct) ->
+            R.are_convertible context t ct
+         | Some t,Some (_,C.Decl ct) ->
+            R.are_convertible context (type_of_aux' metasenv context t) ct
+         | _, _  -> false
+       in
+        if not res then raise MetasenvInconsistency
+     ) l lifted_canonical_context 
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 and type_of_aux' metasenv context t =
@@ -1209,7 +1207,6 @@ and type_of_aux' metasenv context t =
       let cty = cooked_type_of_constant uri cookingsno in
        decr fdebug ;
        cty
-   | C.Abst _ -> raise (Impossible 22)
    | C.MutInd (uri,cookingsno,i) ->
       incr fdebug ;
       let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
@@ -1493,7 +1490,7 @@ let typecheck uri =
           (* only to check that ty is well-typed *)
           let _ = type_of ty in ()
         | C.CurrentProof (_,conjs,te,ty) ->
-	    (*CSC [] wrong *)
+            (*CSC: bisogna controllare anche il metasenv!!! *)
             let _ = type_of_aux' conjs [] ty in
              debug (type_of_aux' conjs [] te) [] ;
              if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then