X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=f2c0ebbcc5d44555932c0fd715db21ddfe1622be;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=6789c4dff8213acdf53d18aef9b286c0bd46744f;hpb=ed9af5a10b66343f817a1f9eac3add29e4b2baae;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 6789c4dff..f2c0ebbcc 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -64,7 +64,9 @@ let debrujin_constructor uri number_of_types =
         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
-    | C.Meta _ -> assert false
+    | C.Meta (i,l) ->
+       let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
+        C.Meta (i,l)
     | C.Sort _
     | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
@@ -765,6 +767,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
                pl true
             else
+             let pl_and_cl =
+              try
+               List.combine pl cl
+              with
+               Invalid_argument _ ->
+                raise (TypeCheckerFailure "not enough patterns")
+             in
               List.fold_right
                (fun (p,(_,c)) i ->
                  let rl' =
@@ -776,7 +785,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                   in
                    i &&
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -804,6 +813,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
                pl true
             else
+             let pl_and_cl =
+              try
+               List.combine pl cl
+              with
+               Invalid_argument _ ->
+                raise (TypeCheckerFailure "not enough patterns")
+             in
               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
               (*CSC: sugli argomenti di una applicazione                      *)
               List.fold_right
@@ -817,7 +833,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                   in
                    i &&
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | _ ->
           List.fold_right
            (fun p i ->
@@ -938,6 +954,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                  i && guarded_by_destructors context n nn kl x safes p)
                pl true
             else
+             let pl_and_cl =
+              try
+               List.combine pl cl
+              with
+               Invalid_argument _ ->
+                raise (TypeCheckerFailure "not enough patterns")
+             in
              guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
@@ -948,7 +971,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                   in
                    i &&
                    guarded_by_destructors context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -979,6 +1002,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                  i && guarded_by_destructors context n nn kl x safes p)
                pl true
             else
+             let pl_and_cl =
+              try
+               List.combine pl cl
+              with
+               Invalid_argument _ ->
+                raise (TypeCheckerFailure "not enough patterns")
+             in
              guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
@@ -996,7 +1026,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                   in
                    i &&
                    guarded_by_destructors context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | _ ->
           guarded_by_destructors context n nn kl x safes outtype &&
            guarded_by_destructors context n nn kl x safes term &&
@@ -1297,21 +1327,19 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
 	 false,ugraph1
        else
          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
-           C.Sort C.Prop -> true,ugraph1
-         | (C.Sort C.Set | C.Sort C.CProp) ->
-             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-	       match o with
-               C.InductiveDefinition (itl,_,_,_) ->
-                   let (_,_,_,cl) = List.nth itl i in
-                   (* is a singleton definition? *)
-                   List.length cl = 1,ugraph1
-             | _ ->
-                 raise (TypeCheckerFailure
-			  ("Unknown mutual inductive definition:" ^
-			   UriManager.string_of_uri uri))
-             )
-         | _ -> false,ugraph1
-         )
+              C.Sort C.Prop -> true,ugraph1
+           | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
+               (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 match o with
+                    C.InductiveDefinition (itl,_,_,_) ->
+                     let (_,_,_,cl) = List.nth itl i in
+                     (* is a singleton definition or the empty proposition? *)
+                     (List.length cl = 1 || List.length cl = 0),ugraph1
+                  | _ ->
+                   raise (TypeCheckerFailure
+                    ("Unknown mutual inductive definition:" ^
+                       UriManager.string_of_uri uri)))
+           | _ -> false,ugraph1)
    | ((C.Sort C.Set, C.Prod (name,so,ta)) 
    | (C.Sort C.CProp, C.Prod (name,so,ta)))
      when not need_dummy ->
@@ -1766,12 +1794,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           if not branches_ok then
            raise
             (TypeCheckerFailure "Case analysys: wrong branch type");
-          let arguments =
+          let arguments' =
            if not need_dummy then outtype::arguments@[term]
            else outtype::arguments in
           let outtype =
-           if arguments = [] then outtype
-           else CicReduction.head_beta_reduce (C.Appl arguments)
+           if need_dummy && arguments = [] then outtype
+           else CicReduction.head_beta_reduce (C.Appl arguments')
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->
@@ -2031,13 +2059,67 @@ in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
 *)
 ;;
 
-let typecheck uri ugraph =
+let typecheck_obj0 ~logger uri ugraph =
+ let module C = Cic in
+  function
+     C.Constant (_,Some te,ty,_,_) ->
+      let _,ugraph = type_of ~logger ty ugraph in
+      let ty_te,ugraph = type_of ~logger te ugraph in
+      let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
+       if not b then
+         raise (TypeCheckerFailure
+          ("the type of the body is not the one expected"))
+       else
+        ugraph
+   | C.Constant (_,None,ty,_,_) ->
+      (* only to check that ty is well-typed *)
+      let _,ugraph = type_of ~logger ty ugraph in
+       ugraph
+   | C.CurrentProof (_,conjs,te,ty,_,_) ->
+      let _,ugraph =
+       List.fold_left
+        (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
+          let _,ugraph = 
+           type_of_aux' ~logger metasenv context ty ugraph 
+          in
+           metasenv @ [conj],ugraph
+        ) ([],ugraph) conjs
+      in
+       let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+       let type_of_te,ugraph = 
+        type_of_aux' ~logger conjs [] te ugraph
+       in
+       let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
+        if not b then
+          raise (TypeCheckerFailure (sprintf
+           "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
+           (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
+        else
+         ugraph
+   | C.Variable (_,bo,ty,_,_) ->
+      (* only to check that ty is well-typed *)
+      let _,ugraph = type_of ~logger ty ugraph in
+       (match bo with
+           None -> ugraph
+         | Some bo ->
+            let ty_bo,ugraph = type_of ~logger bo ugraph in
+  	    let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
+             if not b then
+              raise (TypeCheckerFailure
+               ("the body is not the one expected"))
+             else
+              ugraph
+            )
+   | (C.InductiveDefinition _ as obj) ->
+      check_mutual_inductive_defs ~logger uri obj ugraph
+
+let typecheck uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
  let logger = new CicLogger.logger in
    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
-   match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+   match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
      CicEnvironment.CheckedObj (cobj,ugraph') -> 
        (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
        cobj,ugraph'
@@ -2045,60 +2127,7 @@ let typecheck uri ugraph =
       (* let's typecheck the uncooked object *)
       logger#log (`Start_type_checking uri) ;
       (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
-      let ugraph1 = 
-	(match uobj with
-         C.Constant (_,Some te,ty,_,_) ->
-           let _,ugraph1 = type_of ~logger ty ugraph in
-	   let ty_te,ugraph2 = type_of ~logger te ugraph1 in
-           let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
-           if not b then
-              raise (TypeCheckerFailure
-                ("Unknown constant:" ^ U.string_of_uri uri))
-           else
-	      ugraph3
-        | C.Constant (_,None,ty,_,_) ->
-          (* only to check that ty is well-typed *)
-          let _,ugraph1 = type_of ~logger ty ugraph in
-	  ugraph1
-        | C.CurrentProof (_,conjs,te,ty,_,_) ->
-           let _,ugraph1 =
-            List.fold_left
-             (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
-               let _,ugraph1 = 
-		 type_of_aux' ~logger metasenv context ty ugraph 
-	       in
-               metasenv @ [conj],ugraph1
-             ) ([],ugraph) conjs
-           in
-            let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
-            let type_of_te,ugraph3 = 
-	      type_of_aux' ~logger conjs [] te ugraph2 
-	    in
-            let b,ugraph4 = R.are_convertible [] type_of_te ty ugraph3 in
-	    if not b then
-               raise (TypeCheckerFailure (sprintf
-                "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
-                (U.string_of_uri uri) (CicPp.ppterm type_of_te)
-                (CicPp.ppterm ty)))
-	    else
-	      ugraph4
-        | C.Variable (_,bo,ty,_,_) ->
-           (* only to check that ty is well-typed *)
-           let _,ugraph1 = type_of ~logger ty ugraph in
-            (match bo with
-                None -> ugraph1
-              | Some bo ->
-	         let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in
-	      	 let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in
-		 if not b then
-                   raise (TypeCheckerFailure
-                     ("Unknown variable:" ^ U.string_of_uri uri))
-		 else
-		   ugraph3
-            )
-        | C.InductiveDefinition _ ->
-           check_mutual_inductive_defs ~logger uri uobj ugraph
-      ) in
+      let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
 	try
 	  CicEnvironment.set_type_checking_info uri;
 	  logger#log (`Type_checking_completed uri);
@@ -2114,16 +2143,20 @@ let typecheck uri ugraph =
 	    *)
 	    Invalid_argument s -> 
 	      (*debug_print s;*)
-	      uobj,ugraph1
+	      uobj,ugraph
 ;;
 
+let typecheck_obj ~logger uri obj =
+ let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
+ let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
+  CicEnvironment.add_type_checked_obj uri (obj,ugraph)
+
 (** wrappers which instantiate fresh loggers *)
 
 let type_of_aux' ?(subst = []) metasenv context t ugraph =
   let logger = new CicLogger.logger in
   type_of_aux' ~logger ~subst metasenv context t ugraph
 
-let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
-  let logger = new CicLogger.logger in
-  typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno)
-
+let typecheck_obj uri obj =
+ let logger = new CicLogger.logger in
+ typecheck_obj ~logger uri obj