From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Apr 2008 13:44:16 +0000 (+0000)
Subject: get_checked_fix -> get_checked_fixes
X-Git-Tag: make_still_working~5334
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ddad84e0daa6e9552168f7a8ecb101e23c33476;p=helm.git

get_checked_fix -> get_checked_fixes
---

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 1076adbf5..cca0e5cdf 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -68,13 +68,12 @@ let get_checked_fix_or_cofix b = function
   | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))->
       (match get_checked_obj uri with
       | _,height,_,_, NCic.Fixpoint (is_fix,funcs,att) when is_fix = b ->
-         let rlv, name, _, ty, bo = List.nth funcs fixno in
-         rlv, name, bo, ty, att, height
+         funcs, att, height
       | _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
   | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
 ;;
-let get_checked_fix r = get_checked_fix_or_cofix true r;;
-let get_checked_cofix r = get_checked_fix_or_cofix false r;;
+let get_checked_fixes r = get_checked_fix_or_cofix true r;;
+let get_checked_cofixes r = get_checked_fix_or_cofix false r;;
 
 let get_indty_leftno = function 
   | NReference.Ref (_, uri, NReference.Ind _) 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 6f224d527..07bd1b51c 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -39,13 +39,13 @@ val get_checked_indtys:
   NReference.reference -> 
     bool * int * NCic.inductiveType list * NCic.i_attr * int
 
-val get_checked_fix:
+val get_checked_fixes:
   NReference.reference -> 
-   NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int
+   NCic.inductiveFun list * NCic.f_attr * int
 
-val get_checked_cofix:
+val get_checked_cofixes:
   NReference.reference -> 
-   NCic.relevance * string * NCic.term * NCic.term * NCic.f_attr * int
+   NCic.inductiveFun list * NCic.f_attr * int
 
 val get_indty_leftno: NReference.reference -> int
 
diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index defd12e29..db19c9c96 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -421,8 +421,8 @@ module Reduction(RS : Strategy) =
          let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
          if delta > height then config else aux (0, [], body, s) 
      | (_, _, NCic.Const (NReference.Ref 
-               (_,_,NReference.Fix (_,recindex)) as refer),s) as config ->
-        let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in
+               (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
+        let fixes,_, height = NCicEnvironment.get_checked_fixes refer in
         if delta > height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
@@ -435,13 +435,15 @@ module Reduction(RS : Strategy) =
                let new_s =
                  replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
                in
+               let _,_,_,_,body = List.nth fixes fixno in
                aux (0, [], body, new_s)
            | _ -> config)
      | (_, _, NCic.Const _, _) as config -> config
      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
         let decofix = function
-          | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix _)as refer),s)->
-             let _,_,body,_,_,_ = NCicEnvironment.get_checked_cofix refer in
+          | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
+             let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in
+             let _,_,_,_,body = List.nth cofixes c in
              reduce ~delta:0 ~subst context (0,[],body,s)
           | config -> config
         in
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 26e2163ea..690cd5900 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -889,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")))
@@ -910,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 ->