X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=eb9d376f2aea3841eae4f0a96236bd5b690fceb9;hb=26b754bcd3763fd7624637adab0635edefa1168f;hp=c23555494f803e279be20f54bf85c51b94c4d244;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c23555494..eb9d376f2 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -252,14 +252,14 @@ and does_not_occur ?(subst=[]) context n nn te =
          Failure _ -> assert false)
     | C.Sort _
     | C.Implicit _ -> true
-    | C.Meta (_,l) ->
+    | C.Meta (mno,l) ->
        List.fold_right
         (fun x i ->
           match x with
              None -> i
            | 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
+         let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in
           does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
         with
          CicUtil.Subst_not_found _ -> true)
@@ -801,7 +801,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -852,7 +852,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -934,10 +934,10 @@ and guarded_by_destructors ~subst context n nn kl x safes =
   function
      C.Rel m when m > n && m <= nn -> false
    | C.Rel m ->
-      (match List.nth context (n-1) with
+      (match List.nth context (m-1) with
           Some (_,C.Decl _) -> true
         | Some (_,C.Def (bo,_)) ->
-           guarded_by_destructors ~subst context m nn kl x safes
+           guarded_by_destructors ~subst context n nn kl x safes
             (CicSubstitution.lift m bo)
         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
@@ -1006,7 +1006,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                      | (_,_,ty,_)::_ ->
                         fst (split_prods ~subst [] paramsno ty)
                    in
-                    (tys@lefts,len,isinductive,paramsno,cl')
+                    (lefts@tys,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1059,7 +1059,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                     | (_,_,ty,_)::_ ->
                        fst (split_prods ~subst [] paramsno ty)
                   in
-                   (tys@lefts,List.length tl,isinductive,paramsno,cl')
+                   (lefts@tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
                   (lazy ("Unknown mutual inductive definition:" ^
@@ -1374,11 +1374,12 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   let arity1 = CicReduction.whd ~subst context arity1 in
   let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
    match arity1, CicReduction.whd ~subst context arity2 with
-     (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
+     (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) ->
        let b,ugraph1 =
         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
        if b then
-	 check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+	 check_allowed_sort_elimination ~subst ~metasenv ~logger 
+           ((Some (name,C.Decl so1))::context) uri i
           need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
           ugraph1
        else
@@ -2202,6 +2203,9 @@ let typecheck_obj0 ~logger uri ugraph =
       let _,ugraph = type_of ~logger ty ugraph in
        ugraph
    | C.CurrentProof (_,conjs,te,ty,_,_) ->
+      (* this block is broken since the metasenv should 
+       * be topologically sorted before typing metas *)
+      ignore(assert false);
       let _,ugraph =
        List.fold_left
         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
@@ -2303,3 +2307,6 @@ let check_allowed_sort_elimination uri i s1 s2 =
   ~logger:(new CicLogger.logger) [] uri i true
   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
   CicUniv.empty_ugraph)
+;;
+
+Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;