X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=62dc951aaa54deb58cc3fe0dc36dfa5e142a4fac;hb=278d9954e80f952f7cde793e33e01bacce1cd40c;hp=48d8b2ea925450736c9be0d60288c351df233751;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 48d8b2ea9..62dc951aa 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -217,13 +217,16 @@ and does_not_occur context n nn te =
        does_not_occur context n nn te && does_not_occur context n nn ty
     | C.Prod (name,so,dest) ->
        does_not_occur context n nn so &&
-        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+         dest
     | C.Lambda (name,so,dest) ->
        does_not_occur context n nn so &&
-        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+         dest
     | C.LetIn (name,so,dest) ->
        does_not_occur context n nn so &&
-        does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
+        does_not_occur ((Some (name,(C.Def (so,None))))::context)
+         (n + 1) (nn + 1) dest
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
     | C.Var (_,exp_named_subst)
@@ -403,7 +406,8 @@ and strictly_positive context n nn te =
           (fun x i ->
             i &&
              weakly_positive
-              ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
+              ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+              x
           ) cl' true
    | t -> does_not_occur context n nn t
 
@@ -672,7 +676,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (name,so,ta) ->
       check_is_really_smaller_arg context n nn kl x safes so &&
-       check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
+       check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
         (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 *)
@@ -689,7 +693,8 @@ and check_is_really_smaller_arg context n nn kl x safes te =
             match CicEnvironment.get_obj uri with
                C.InductiveDefinition (tl,_,paramsno) ->
                 let tys =
-                 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
+                 List.map
+                  (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
                 in
                  let (_,isinductive,_,cl) = List.nth tl i in
                   let cl' =
@@ -727,7 +732,8 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
-                  List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+                  List.map (fun (n,_,ty,_) ->
+                   Some(Cic.Name n,(Cic.Decl ty))) tl
                  in
                   let cl' =
                    List.map
@@ -801,7 +807,8 @@ and guarded_by_destructors context n nn kl x safes =
    | C.Rel n ->
       (match List.nth context (n-1) with
           Some (_,C.Decl _) -> true
-        | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
+        | Some (_,C.Def (bo,_)) ->
+           guarded_by_destructors context n nn kl x safes bo
 	| None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
       )
    | C.Meta _
@@ -820,7 +827,7 @@ and guarded_by_destructors context n nn kl x safes =
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (name,so,ta) ->
       guarded_by_destructors context n nn kl x safes so &&
-       guarded_by_destructors ((Some (name,(C.Def so)))::context)
+       guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
         (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
@@ -850,7 +857,8 @@ and guarded_by_destructors context n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
-                  List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+                  List.map (fun (n,_,ty,_) ->
+                   Some(Cic.Name n,(Cic.Decl ty))) tl
                  in
                   let cl' =
                    List.map
@@ -892,7 +900,8 @@ and guarded_by_destructors context n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
-                  List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+                  List.map
+                   (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
                  in
                   let cl' =
                    List.map
@@ -1058,8 +1067,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
                 [] -> true
               | he::tl ->
                  analyse_branch context so he &&
-                  analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
-                   de tl
+                  analyse_instantiated_type
+                   ((Some (name,(C.Decl so)))::context) de tl
             end
          | C.Lambda _
          | C.LetIn _ ->
@@ -1147,7 +1156,7 @@ and guarded_by_constructors 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.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i && does_not_occur context n nn ty &&
@@ -1293,9 +1302,10 @@ and check_metasenv_consistency metasenv context canonical_context l =
         [] -> []
       | (Some (n,C.Decl t))::tl ->
          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
-      | (Some (n,C.Def t))::tl ->
-         (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+      | (Some (n,C.Def (t,None)))::tl ->
+         (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
       | None::tl -> None::(aux (i+1) tl)
+      | (Some (n,C.Def (_,Some _)))::_ -> assert false
     in
      aux 1 canonical_context
    in
@@ -1304,7 +1314,7 @@ and check_metasenv_consistency metasenv context canonical_context l =
        let res =
         match (t,ct) with
            _,None -> true
-         | Some t,Some (_,C.Def ct) ->
+         | 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
@@ -1325,8 +1335,11 @@ and type_of_aux' metasenv context t =
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t
-          | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
-	  | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
+          | Some (_,C.Def (_,Some ty)) -> S.lift n ty
+          | Some (_,C.Def (bo,None)) ->
+             prerr_endline "##### CASO DA INVESTIGARE E CAPIRE" ;
+             type_of_aux context (S.lift n bo)
+	        | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
         with
          _ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term"))
        )
@@ -1363,7 +1376,7 @@ and type_of_aux' metasenv context t =
           C.Prod (n,s,type2)
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
-      let _ = type_of_aux context s in
+      let ty = type_of_aux context s in
        (* The type of a LetIn is a LetIn. Extremely slow since the computed
           LetIn is later reduced and maybe also re-checked.
        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
@@ -1377,7 +1390,7 @@ and type_of_aux' metasenv context t =
        (* One-step LetIn reduction. Even faster than the previous solution.
           Moreover the inferred type is closer to the expected one. *)
        (CicSubstitution.subst s
-        (type_of_aux ((Some (n,(C.Def s)))::context) t))
+        (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux context he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in