X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=531705a3c2d40abf7d2699291e683b5da0b2e70f;hb=4e3d7b4b47f66f0745333bfd4efcb27b4528f4c3;hp=951f68dbd84b28043a100fe3c72c114d4f5927a7;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 951f68dbd..531705a3c 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -240,12 +240,16 @@ and type_of_variable ~logger uri ugraph =
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
-   (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
-   (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
-   (*CSC: universi                                                    *)
-   match CicReduction.whd ~subst context te with
+   match te with
       C.Rel m when m > n && m <= nn -> false
-    | C.Rel _
+    | C.Rel m ->
+       (try
+         (match List.nth context (m-1) with
+             Some (_,C.Def (bo,_)) ->
+              does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
+           | _ -> true)
+        with
+         Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
     | C.Meta (_,l) ->
@@ -253,7 +257,12 @@ and does_not_occur ?(subst=[]) context n nn te =
         (fun x i ->
           match x with
              None -> i
-           | Some x -> i && does_not_occur ~subst context n nn x) l true
+           | Some x -> i && does_not_occur ~subst context n nn x) l true &&
+       (try
+         let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
+          does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
+        with
+         CicUtil.Subst_not_found _ -> true)
     | C.Cast (te,ty) ->
        does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
     | C.Prod (name,so,dest) ->
@@ -1384,10 +1393,10 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype =
           C.Appl l -> C.Appl (l@[C.Rel 1])
         | t -> C.Appl [t ; C.Rel 1]
       in
-       C.Prod (C.Anonymous,so,type_of_branch ~subst
+       C.Prod (name,so,type_of_branch ~subst
         ((Some (name,(C.Decl so)))::context) argsno need_dummy
         (CicSubstitution.lift 1 outtype) term' de)
-  | _ -> raise (AssertFailure (lazy "20"))
+   | _ -> raise (AssertFailure (lazy "20"))
 
 (* check_metasenv_consistency checks that the "canonical" context of a
 metavariable is consitent - up to relocation via the relocation list l -
@@ -1472,7 +1481,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           | None -> raise 
 	      (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
         with
-        _ ->
+        Failure _ ->
           raise (TypeCheckerFailure (lazy "unbound variable"))
        )
     | C.Var (uri,exp_named_subst) ->
@@ -1560,7 +1569,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 type_of_aux ~logger 
 	   ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 
        in
-       (CicSubstitution.subst s ty1),ugraph2
+       (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
    | C.Appl (he::tl) when List.length tl > 0 ->
        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
        let tlbody_and_type,ugraph2 = 
@@ -1763,6 +1772,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		R.are_convertible 
 		  ~subst ~metasenv context ty_p ty_branch ugraph3 
 	      in 
+(* Debugging code
+if not b1 then
+begin
+prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
+prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
+prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
+prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
+end;
+*)
 	      if not b1 then
 		debug_print (lazy
 		  ("#### " ^ CicPp.ppterm ty_p ^ 
@@ -1945,7 +1963,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		    begin
 		      CicReduction.fdebug := -1 ;
 		      eat_prods ~subst context 
-			(CicSubstitution.subst hete t) tl ugraph1
+			(CicSubstitution.subst ~avoid_beta_redexes:true hete t)
+                         tl ugraph1
 			(*TASSI: not sure *)
 		    end
 		  else
@@ -2147,9 +2166,12 @@ let typecheck_obj ~logger uri obj =
 
 (** wrappers which instantiate fresh loggers *)
 
+let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
+
 let type_of_aux' ?(subst = []) metasenv context t ugraph =
   let logger = new CicLogger.logger in
-  type_of_aux' ~logger ~subst metasenv context t ugraph
+  profiler.HExtlib.profile 
+    (type_of_aux' ~logger ~subst metasenv context t) ugraph
 
 let typecheck_obj uri obj =
  let logger = new CicLogger.logger in