.cvsignore added

[helm.git] / helm / interface / cicTypeChecker.ml

diff --git a/helm/interface/cicTypeChecker.ml b/helm/interface/cicTypeChecker.ml
index 63433937b39bafec7166e0567dc9d763bc3014bd..de9f46bfe174f9e5caad0d8fe13ef5410c3a0c11 100644 (file)
--- a/helm/interface/cicTypeChecker.ml
+++ b/helm/interface/cicTypeChecker.ml
@@ -14,7 +14,7 @@ let debug t env =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG",
+   CicPp.ppobj (C.Variable ("DEBUG", None,
     C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0),
     C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0),
     C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0),
@@ -93,12 +93,19 @@ let rec cooked_type_of_constant uri cookingsno =
 and type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
+ let module U = UriManager in
   (* 0 because a variable is never cooked => no partial cooking at one level *)
   match CicCache.is_type_checked uri 0 with
-     CicCache.CheckedObj (C.Variable (_,ty)) -> ty
-   | CicCache.UncheckedObj (C.Variable (_,ty)) ->
+     CicCache.CheckedObj (C.Variable (_,_,ty)) -> ty
+   | CicCache.UncheckedObj (C.Variable (_,bo,ty)) ->
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
+       (match bo with
+           None -> ()
+         | Some bo ->
+            if not (R.are_convertible (type_of bo) ty) then
+             raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
+       ) ;
        CicCache.set_type_checking_info uri ;
        ty
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
@@ -120,6 +127,8 @@ and does_not_occur n nn te =
        does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
     | C.Lambda (_,so,dest) ->
        does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
+    | C.LetIn (_,so,dest) ->
+       does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur n nn x) l true
     | C.Const _
@@ -394,6 +403,7 @@ and recursive_args n nn te =
    | C.Prod (_,so,de) ->
       (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
    | C.Lambda _ -> raise Impossible (* due to type-checking *)
+   | C.LetIn _ -> raise NotImplemented
    | C.Appl _ -> []
    | C.Const _
    | C.Abst _ -> raise Impossible
@@ -466,6 +476,10 @@ and check_is_really_smaller_arg n nn kl x safes te =
       check_is_really_smaller_arg n nn kl x safes so &&
        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta
+   | C.LetIn (_,so,ta) ->
+      check_is_really_smaller_arg n nn kl x safes so &&
+       check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
+        (List.map (fun x -> x + 1) safes) ta
    | C.Appl (he::_) ->
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
       (*CSC: solo perche' non abbiamo trovato controesempi            *)
@@ -594,6 +608,10 @@ and guarded_by_destructors n nn kl x safes =
       guarded_by_destructors n nn kl x safes so &&
        guarded_by_destructors (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta
+   | C.LetIn (_,so,ta) ->
+      guarded_by_destructors n nn kl x safes so &&
+       guarded_by_destructors (n+1) (nn+1) kl (x+1)
+        (List.map (fun x -> x + 1) safes) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       let k = List.nth kl (m - n - 1) in
        if not (List.length tl > k) then false
@@ -742,6 +760,9 @@ and guarded_by_constructors n nn h =
    | C.Lambda (_,so,de) ->
       does_not_occur n nn so &&
        guarded_by_constructors (n + 1) (nn + 1) h de
+   | C.LetIn (_,so,de) ->
+      does_not_occur n nn so &&
+       guarded_by_constructors (n + 1) (nn + 1) h de
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       h = 1 &&
        List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
@@ -971,6 +992,10 @@ and type_of t =
          (* only to check if the product is well-typed *)
          let _ = sort_of_prod (sort1,sort2) in
           C.Prod (n,s,type2)
+   | C.LetIn (n,s,t) ->
+       let type1 = type_of_aux env s in
+       let type2 = type_of_aux (type1::env) t in
+        type2
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux env he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
@@ -1189,10 +1214,15 @@ let typecheck uri =
             debug (type_of te) [] ;
             if not (R.are_convertible (type_of te) ty) then
              raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
-        | C.Variable (_,ty) ->
+        | C.Variable (_,bo,ty) ->
            (* only to check that ty is well-typed *)
-           (*CSC [] wrong *)
-           let _ = type_of ty in ()
+           let _ = type_of ty in
+            (match bo with
+                None -> ()
+              | Some bo ->
+                 if not (R.are_convertible (type_of bo) ty) then
+                  raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
+            )
         | C.InductiveDefinition _ ->
            cooked_mutual_inductive_defs uri uobj
       ) ;