Missing check in positivity implemented: we did not check uniformity for

left parameters in contravariant position.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 56119fce7c3ead8eed15d7521b2adf1b1ae48890..8124afcc4ae9115f708800b1c68845597ce9ca8b 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -138,8 +138,6 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
          (PP.ppterm ~subst ~metasenv ~context t2))))
 ;;
 
-(* REMINDER: eat_prods was here *)
-
 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 let rec instantiate_parameters params c =
@@ -226,16 +224,32 @@ let rec eat_or_subst_lambdas
   | (_, te, _, _) -> te, k
 ;;
 
+let check_homogeneous_call ~subst context indparamsno n uri reduct tl =
+ let last =
+  List.fold_left
+   (fun k x ->
+     if k = 0 then 0
+     else
+      match R.whd context x with
+      | C.Rel m when m = n - (indparamsno - k) -> k - 1
+      | _ -> raise (TypeCheckerFailure (lazy 
+         ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
+         string_of_int indparamsno ^ " fixed) is not homogeneous in "^
+         "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct))))
+   indparamsno tl
+ in
+  if last <> 0 then
+   raise (TypeCheckerFailure
+    (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+     NUri.string_of_uri uri)))
+;;
 
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
-(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
-(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
-(*CSC strictly_positive                                                  *)
-(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
-let rec weakly_positive ~subst context n nn uri te =
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+(* Inductive types being checked for positivity have *)
+(* indexes x s.t. n < x <= nn.                       *)
+let rec weakly_positive ~subst context n nn uri indparamsno posuri te =
+  (*CSC: Not very nice. *)
   let dummy = C.Sort C.Prop in
-  (*CSC: mettere in cicSubstitution *)
+  (*CSC: to be moved 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,lno))))::tl) 
@@ -256,27 +270,27 @@ let rec weakly_positive ~subst context n nn uri te =
      | 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
+         strictly_positive ~subst context n nn indparamsno posuri source &&
+         aux ((name,C.Decl source)::context) (n + 1) (nn + 1) 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
+         aux ((name,C.Decl source)::context) (n + 1) (nn + 1) 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 =
+and strictly_positive ~subst context n nn indparamsno posuri te =
   match R.whd context te with
    | t when does_not_occur ~subst context n nn t -> true
-   | C.Rel _ -> true
+   | C.Rel _ when indparamsno = 0 -> true
+   | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
+      check_homogeneous_call ~subst context indparamsno n posuri reduct tl;
+      List.for_all (does_not_occur ~subst context n nn) tl
    | C.Prod (name,so,ta) ->
       does_not_occur ~subst context n nn so &&
-       strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
-   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      List.for_all (does_not_occur ~subst context n nn) tl
+       strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1)
+        indparamsno posuri ta
    | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
@@ -289,32 +303,16 @@ and strictly_positive ~subst context n nn te =
       ok &&
       List.for_all (does_not_occur ~subst context n nn) arguments &&
       List.for_all 
-       (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl
+       (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1)
+         uri indparamsno posuri) cl
    | _ -> false
        
 (* the inductive type indexes are s.t. n < x <= nn *)
 and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
   match R.whd context te with
   |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
-      let last =
-       List.fold_left
-        (fun k x ->
-          if k = 0 then 0
-          else
-           match R.whd context x with
-           | C.Rel m when m = n - (indparamsno - k) -> k - 1
-           | _ -> raise (TypeCheckerFailure (lazy 
-              ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
-              string_of_int indparamsno ^ " fixed) is not homogeneous in "^
-              "appl:\n"^ PP.ppterm ~context ~subst ~metasenv:[] reduct))))
-        indparamsno tl
-      in
-       if last = 0 then
-        List.for_all (does_not_occur ~subst context n nn) tl
-       else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
-          NUri.string_of_uri uri)))
+      check_homogeneous_call ~subst context indparamsno n uri reduct tl;
+      List.for_all (does_not_occur ~subst context n nn) tl
   | C.Rel m when m = i ->
       if indparamsno = 0 then
        true
@@ -324,7 +322,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
           NUri.string_of_uri uri)))
   | C.Prod (name,source,dest) when
       does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
-      strictly_positive ~subst context n nn source &&
+      strictly_positive ~subst context n nn indparamsno uri source &&
        are_all_occurrences_positive ~subst 
         ((name,C.Decl source)::context) uri indparamsno
         (i+1) (n + 1) (nn + 1) dest
@@ -335,7 +333,6 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
        are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
         uri indparamsno (i+1) (n + 1) (nn + 1) dest
    | _ ->
-prerr_endline ("MM: " ^ NCicPp.ppterm ~subst ~metasenv:[] ~context te);
      raise
       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
         (NUri.string_of_uri uri))))
@@ -946,7 +943,7 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
          ("Too many args for constructor: " ^ String.concat " "
          (List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args))))
       in
-      let left, args = HExtlib.split_nth paramsno tl in
+      let _, args = HExtlib.split_nth paramsno tl in
       analyse_instantiated_type rec_params args
    | C.Appl ((C.Match (_,out,te,pl))::_) 
    | C.Match (_,out,te,pl) as t ->