Abst removed from the DTD.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2e8b5585f5190c6d2110ef8fab6a576b39f7b614..b539508a1212f10672a08f46691e486be41ba97e 100644 (file)
--- 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
@@ -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