positivity check fixed, a MutInd not applied (but with an exp-named-subst)

[helm.git] / helm / software / components / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index c23555494f803e279be20f54bf85c51b94c4d244..2855367002ef063677589e455b143d5727453ffa 100644 (file)
--- 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)
@@ -391,13 +391,8 @@ and weakly_positive context n nn uri te =
 *)
      C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
-   | C.Prod (C.Anonymous,source,dest) ->
-      strictly_positive context n nn
-       (subst_inductive_type_with_dummy_mutind source) &&
-       weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
    | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive context n nn
         (subst_inductive_type_with_dummy_mutind source) &&
@@ -437,7 +432,9 @@ and strictly_positive context n nn te =
        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
+   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) 
+   | (C.MutInd (uri,i,exp_named_subst)) as t -> 
+      let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
       let (ok,paramsno,ity,cl,name) =
        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
@@ -508,14 +505,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
         raise (TypeCheckerFailure
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           UriManager.string_of_uri uri)))
-   | C.Prod (C.Anonymous,source,dest) ->
-       let b = strictly_positive context n nn source in
-       b &&
-       are_all_occurrences_positive
-        ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
    | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
+      does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
       (* dummy abstraction, so we behave as in the anonimous case *)
       strictly_positive context n nn source &&
        are_all_occurrences_positive
@@ -801,7 +792,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 +843,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 +925,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 +997,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 +1050,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 +1365,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
@@ -1646,6 +1638,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
    | C.LetIn (n,s,ty,t) ->
       (* only to check if s is well-typed *)
       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
+      let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
       let b,ugraph1 =
        R.are_convertible ~subst ~metasenv context ty ty' ugraph1
       in 
@@ -2001,7 +1994,7 @@ end;
        let (_,ty,_) = List.nth fl i in
         ty,ugraph2
 
- and check_exp_named_subst ~logger ~subst context ugraph =
+ and check_exp_named_subst ~logger ~subst context =
    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
      match l with
         [] -> ugraph
@@ -2027,7 +2020,7 @@ end;
                 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
-     check_exp_named_subst_aux ~logger [] ugraph 
+     check_exp_named_subst_aux ~logger []
        
  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
   let module C = Cic in
@@ -2202,6 +2195,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 +2299,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);;