positivity check fixed

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 464186f2e0d1cdf91798761326cc524637733bdb..17380336797d23b58f8a012794e6cd46232c169e 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -238,28 +238,35 @@ let rec weakly_positive ~subst context n nn uri te =
   (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy _ = function
     | C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))))::_) 
-        when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl) 
+        when NUri.eq uri' uri -> 
+          let _, rargs = HExtlib.split_nth lno tl in
+          if rargs = [] then dummy else C.Appl (dummy :: rargs)
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
-  match R.whd context te with
-   | C.Const (Ref.Ref (uri',Ref.Ind _))
-   | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind _)))::_) 
-      when NUri.eq uri' uri -> true
-   | C.Prod (name,source,dest) when
-      does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
-       (* dummy abstraction, so we behave as in the anonimous case *)
-       strictly_positive ~subst context n nn
-        (subst_inductive_type_with_dummy () source) &&
-       weakly_positive ~subst ((name,C.Decl source)::context)
-        (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) ->
-       does_not_occur ~subst context n nn
-        (subst_inductive_type_with_dummy () source)&&
-       weakly_positive ~subst ((name,C.Decl source)::context)
-        (n + 1) (nn + 1) uri dest
-   | _ ->
-     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+  (* this function has the same semantics of are_all_occurrences_positive
+     but the i-th context entry role is played by dummy and some checks
+     are skipped because we already know that are_all_occurrences_positive
+     of uri in te. *)
+  let rec aux context n nn te =
+    match R.whd context te with
+     | t when t = dummy -> true
+     | C.Appl (te::rargs) when te = dummy ->
+        List.for_all (does_not_occur ~subst context n nn) rargs
+     | C.Prod (name,source,dest) when
+        does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
+         (* dummy abstraction, so we behave as in the anonimous case *)
+         strictly_positive ~subst context n nn source &&
+         weakly_positive ~subst ((name,C.Decl source)::context)
+          (n + 1) (nn + 1) uri dest
+     | C.Prod (name,source,dest) ->
+         does_not_occur ~subst context n nn source &&
+         weakly_positive ~subst ((name,C.Decl source)::context)
+          (n + 1) (nn + 1) uri dest
+     | _ ->
+       raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+   in
+     aux context n nn (subst_inductive_type_with_dummy () te)
 
 and strictly_positive ~subst context n nn te =
   match R.whd context te with
@@ -1058,7 +1065,7 @@ and get_relevance ~subst context t args =
    let rec aux context ty = function
      | [] -> [] 
      | arg::tl -> match R.whd ~subst context ty with
-       | C.Prod (name,so,de) -> 
+       | C.Prod (_,so,de) -> 
            let sort = typeof ~subst ~metasenv:[] context so in
            let new_ty = S.subst ~avoid_beta_redexes:true arg de in
            (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[]
@@ -1148,35 +1155,6 @@ let typecheck_subst ~metasenv subst =
     ) [] subst)
 ;;
 
-let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ();;
-(*  let shift e (k, context) = k+1,e::context in
-  let rec aux (evil, context as k) () t =
-    match R.whd ~subst context t with
-    | C.Rel i when i = evil -> (*
-        raise (TypeCheckerFailure (lazy (Printf.sprintf
-         "Argument %s declared as irrelevante is used in a relevant position" 
-           (PP.ppterm ~subst ~metasenv ~context (C.Rel i))))) *) ()
-    | C.Meta _ -> ()
-    | C.Lambda (name,so,tgt) -> 
-        (* checking so is not needed since the implicit version of CC
-         * has untyped lambdas (curry style), see Barras and Bernardo  *)
-        aux (shift (name,C.Decl so) k) () tgt 
-    | C.Appl (C.Const ref::args) -> 
-         let relevance = NCicEnvironment.get_relevance ref in
-         HExtlib.list_iter_default2 
-           (fun t -> function false -> () | _ -> aux k () t)
-           args true relevance
-    | C.Match (_, _, _, []) -> ()
-    | C.Match (ref, _, t, [p]) -> 
-        aux k () p;
-        let _,lno,itl,_,_ = E.get_checked_indtys ref in
-        let _,_,_,cl = List.hd itl in
-        let _,_,c = List.hd cl in
-        if not (is_non_informative lno c) then aux k () t
-    | C.Match (_, _, t, pl) -> List.iter (aux k ()) (t::pl)
-    | t -> U.fold shift k aux () t
-  in 
-    aux (1, context) () *)
 
 let typecheck_obj (uri,_height,metasenv,subst,kind) =
  (* height is not checked since it is only used to implement an optimization *)