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 1076adbf5126b2ee480dff495103a30b9808683f..cca0e5cdf55868a9e38c411710f0a51e3295afa4 100644 (file)
--- 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 6f224d5273920710bfc14d47be5994878fa79065..07bd1b51c0e373499034da555569670f128bf4ce 100644 (file)
--- 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 defd12e292c0836dd15afb2331b070c0bac0c9f8..db19c9c9617dd13d237c99bb941daa19ed351d87 100644 (file)
--- 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 26e2163ea91f611b0ca10f6bff274607d8c18055..690cd59005f8334a9789b58d4e019102cd64786f 100644 (file)
--- 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 ->