X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=4b00edd05b2878ccea79ea6712540c2cfaf7db2a;hb=fcdc755773839176c7206b579b6dd1ff665ed8f5;hp=334ab86224bbd37b9d4b3345c1cb53696d8b6314;hpb=9c2f11b475fe7a62a3e7213efeacba2378cdfc96;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 334ab8622..4b00edd05 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -417,29 +417,30 @@ let does_not_occur ~subst context n nn t =
 (*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!*)
-  let dummy_mutind = C.Implicit `Hole in
+  let dummy = C.Sort (C.Type ~-1) in
   (*CSC: mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_mutind _ = function
-    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind
-    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri ->
-       dummy_mutind
-    | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind t
+  let rec subst_inductive_type_with_dummy _ = function
+    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+        when NUri.eq uri' uri -> dummy
+    | 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.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_mutind () source) &&
-         weakly_positive ~subst ((name,C.Decl source)::context)
-         (n + 1) (nn + 1) uri dest
+        (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_mutind () source)&&
-         weakly_positive ~subst ((name,C.Decl source)::context)
-         (n + 1) (nn + 1) uri dest
+        (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"))
 
@@ -888,7 +889,8 @@ and eat_lambdas ~subst ~metasenv context n te =
 
 and guarded_by_destructors ~subst ~metasenv context recfuns t = 
  let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
- let rec aux (context, recfuns, x, safes as k) = function
+ let rec aux (context, recfuns, x, safes as k) t = 
+  match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*)
   | C.Rel m as t when List.mem_assoc m recfuns -> 
       raise (NotGuarded (lazy 
         (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around")))
@@ -909,6 +911,14 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
          raise (NotGuarded (lazy 
            (NCicPp.ppterm ~context ~subst ~metasenv rec_arg ^ " not smaller")));
        List.iter (aux k) tl
+       (*
+  | C.Appl (C.Const ((Ref.Ref (_,_,Ref.Fix (i,j))) as r)::args) ->
+      List.iter (aux k) args;
+      let fixes,_,_ = E.get_checked_fixes r in
+      let _,_,_,_,bo = List.nth fixes i in
+      let bo_wout_lam, context = eat_lambdas ~subst ~metasenv context j in
+      (* debruijna body..... *) assert false
+*)
   | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when List.mem m safes || m = x ->
@@ -1003,17 +1013,12 @@ and split_prods ~subst context n te =
 and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
  match R.whd ~subst context te with
  | C.Rel m when List.mem m safes -> true
- | C.Rel _ -> false
- | C.LetIn _ -> raise (AssertFailure (lazy "letin after whd"))
- | C.Sort _ | C.Implicit _ | C.Prod _ | C.Lambda _ 
- | C.Const (Ref.Ref (_,_,(Ref.Decl | Ref.Def | Ref.Ind _ | Ref.CoFix _))) ->
-    raise (AssertFailure (lazy "not a constructor"))
- | C.Appl ([]|[_]) -> raise (AssertFailure (lazy "empty/unary appl"))
+ | C.Lambda (name, s, t) ->
+     is_really_smaller ~subst ~metasenv (shift_k (name, C.Decl s) k) t
  | C.Appl (he::_) ->
-    (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
-    (*CSC: solo perche' non abbiamo trovato controesempi            *)
-    (*TASSI: da capire soprattutto se he è un altro fix che non ha ridotto...*)
-    is_really_smaller ~subst ~metasenv k he
+     is_really_smaller ~subst ~metasenv k he
+ | C.Appl _
+ | C.Rel _ 
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
    (*| C.Fix (_, fl) ->
@@ -1034,9 +1039,7 @@ and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
             is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true*)
- | C.Meta _ -> 
-     true (* XXX if this check is repeated when the user completes the
-             definition *)
+ | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
     (match term with
     | C.Rel m | C.Appl (C.Rel m :: _ ) when List.mem m safes || m = x ->
@@ -1052,6 +1055,7 @@ and is_really_smaller ~subst ~metasenv (context, recfuns, x, safes as k) te =
              is_really_smaller ~subst ~metasenv k e)
            pl cl
     | _ -> List.for_all (is_really_smaller ~subst ~metasenv k) pl)
+ | _ -> assert false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with