get_check_fix and cofix unified, bug regarding debruijnation of constructors types...

the constructor typs are debruinated wrt some inductive type uri an not wrt
their own, thus a wrong context was created. guarded by constructors ported from the old kernel.

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 1e2cd913e8074a70226b3b067f20840ba6a7ba35..5199dc20f5347372a66c423bc6463aacb37da6a4 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -64,16 +64,14 @@ let get_checked_indtys = function
   | _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
 ;;
 
-let get_checked_fix_or_cofix b = function
+let get_checked_fixes_or_cofixes = 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 ->
+      | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
          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_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 07bd1b51c0e373499034da555569670f128bf4ce..deb7380f63767698e199152943d26f7aff7a6006 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -39,11 +39,7 @@ val get_checked_indtys:
   NReference.reference -> 
     bool * int * NCic.inductiveType list * NCic.i_attr * int
 
-val get_checked_fixes:
-  NReference.reference -> 
-   NCic.inductiveFun list * NCic.f_attr * int
-
-val get_checked_cofixes:
+val get_checked_fixes_or_cofixes:
   NReference.reference -> 
    NCic.inductiveFun list * NCic.f_attr * int
 

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 118bc6911ad9e1149a66887b871074fd85a5ac07..46a81d6205417451d5ed611a35f4cf75f2d52e86 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -401,7 +401,7 @@ module Reduction(RS : Strategy) =
          if delta > height then config else aux (0, [], body, s) 
      | (_, _, NCic.Const (NReference.Ref 
                (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
-        let fixes,_, height = NCicEnvironment.get_checked_fixes refer in
+        let fixes,_, height = NCicEnvironment.get_checked_fixes_or_cofixes refer in
         if delta > height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
@@ -421,7 +421,7 @@ module Reduction(RS : Strategy) =
      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
         let decofix = function
           | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
-             let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in
+             let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
              let _,_,_,_,body = List.nth cofixes c in
              reduce ~delta:0 ~subst context (0,[],body,s)
           | config -> config

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 739bfa6f92f5e0a4ba6fd46750245400824b2ce5..ec70116a211d6594149d2abe0b7ca36fb9e5a25f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -196,7 +196,6 @@ let rec instantiate_parameters params c =
   | t,l -> raise (AssertFailure (lazy "1"))
 ;;
 
-(* specialized only constructors, arities are left untouched *)
 let specialize_inductive_type_constrs ~subst context ty_term =
   match R.whd ~subst context ty_term with
   | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref)  
@@ -204,27 +203,24 @@ let specialize_inductive_type_constrs ~subst context ty_term =
       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
       let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
       let left_args,_ = HExtlib.split_nth leftno args in
-      let itl =
-        List.map (fun (rel, name, arity, cl) ->
-          rel, name, arity,
-            List.map (fun (rel, name, ty) -> 
-              rel, name, instantiate_parameters left_args ty)
-              cl)
-          itl
-      in
-        is_ind, leftno, itl, attrs, i
+      let _,_,_,cl = List.nth itl i in
+      List.map 
+        (fun (rel,name,ty) -> rel, name, instantiate_parameters left_args ty) cl
   | _ -> assert false
 ;;
 
-let fix_lefts_in_constrs ~subst r_uri r_len context ty_term =
-  assert false; (* BUG, ask enrico *)
-  let _,_,itl,_,i = specialize_inductive_type_constrs ~subst context ty_term in
-  let _,_,_,cl = List.nth itl i in  
-  let cl =
-    List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl 
+let specialize_and_abstract_constrs ~subst r_uri r_len context ty_term =
+  let cl = specialize_inductive_type_constrs ~subst context ty_term in
+  let len = List.length context in
+  let context_dcl = 
+    match E.get_checked_obj r_uri with
+    | _,_,_,_, NCic.Inductive (_,_,tys,_) -> 
+        context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys
+    | _ -> assert false
   in
-  (* since arities are closed they are not lifted *)
-  List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl
+  context_dcl,
+  List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl,
+  len, len + r_len
 ;;
 
 exception DoesOccur;;
@@ -773,7 +769,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
   | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) ->
       if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args
       then
-      let fl,_,_ = E.get_checked_fixes r in
+      let fl,_,_ = E.get_checked_fixes_or_cofixes r in
       let ctx_tys, bos = 
         List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl)
       in
@@ -826,10 +822,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
         if not isinductive then recursor aux k t
         else
          let ty = typeof ~subst ~metasenv context term in
-         let itl_ctx,dcl = fix_lefts_in_constrs ~subst r_uri r_len context ty in
+         let dc_ctx, dcl, start, stop = 
+           specialize_and_abstract_constrs ~subst r_uri r_len context ty in
          let args = match t with C.Appl (_::tl) -> tl | _ -> [] in
-         let dc_ctx = context @ itl_ctx in
-         let start, stop = List.length context, List.length context + r_len in
          aux k outtype; 
          List.iter (aux k) args; 
          List.iter2
@@ -849,7 +844,7 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
   try aux (context, recfuns, 1) t
   with NotGuarded s -> raise (TypeCheckerFailure s)
 
-and guarded_by_constructors ~subst ~metasenv context t indURI indlen =
+and guarded_by_constructors ~subst ~metasenv context t indURI indlen nn =
  let rec aux context n nn h te =
   match R.whd ~subst context te with
    | C.Rel m when m > n && m <= nn -> h
@@ -865,16 +860,17 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen =
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       h && List.for_all (does_not_occur ~subst context n nn) tl
    | C.Const (Ref.Ref (_,_,Ref.Con _)) -> true
-   | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (i,j)) as ref) :: tl) as t ->
+   | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (_,j)) as ref) :: tl) as t ->
       let _, paramsno, _, _, _ = E.get_checked_indtys ref in
       let ty_t = typeof ~subst ~metasenv context t in
-      let tys, cl = fix_lefts_in_constrs ~subst indURI indlen context ty_t in
-      let len_ctx = List.length context in
-      let len_tys = List.length tys in
-      let context_c = context @ tys in
-      let _,c = List.nth cl (j-1) in
-      let rec_params = 
-        recursive_args ~subst ~metasenv context_c len_ctx (len_ctx+len_tys) c in
+      let dc_ctx, dcl, start, stop = 
+        specialize_and_abstract_constrs ~subst indURI indlen context ty_t in
+      let _, dc = List.nth dcl (j-1) in
+(*
+        prerr_endline (PP.ppterm ~subst ~metasenv ~context:dc_ctx dc);
+        prerr_endline (PP.ppcontext ~subst ~metasenv dc_ctx);
+ *)
+      let rec_params = recursive_args ~subst ~metasenv dc_ctx start stop dc in
       let rec analyse_instantiated_type rec_spec args =
        match rec_spec, args with
        | h::rec_spec, he::args -> 
@@ -894,20 +890,21 @@ and guarded_by_constructors ~subst ~metasenv context t indURI indlen =
        does_not_occur ~subst context n nn out &&
        does_not_occur ~subst context n nn te &&
        List.for_all (aux context n nn h) pl
-   | C.Const (Ref.Ref (_,_,(Ref.Fix _| Ref.CoFix _)) as ref)
-   | C.Appl(C.Const (Ref.Ref(_,_,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t ->
+   | C.Const (Ref.Ref (_,u,(Ref.Fix _| Ref.CoFix _)) as ref)
+   | C.Appl(C.Const (Ref.Ref(_,u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t ->
       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
-      let fl,_,_ = E.get_checked_fixes ref in 
+      let fl,_,_ = E.get_checked_fixes_or_cofixes ref in 
+      let len = List.length fl in
       let tys = List.map (fun (_,n,_,ty,_) -> n, C.Decl ty) fl in
       List.for_all (does_not_occur ~subst context n nn) tl &&
       List.for_all
-       (fun (_,_,_,ty,bo) ->
-          aux (context@tys) n nn h (debruijn indURI indlen context bo))
+       (fun (_,_,_,_,bo) ->
+          aux (context@tys) n nn h (debruijn u len context bo))
        fl
    | C.Const _
    | C.Appl _ as t -> does_not_occur ~subst context n nn t
  in
-   aux context 0 indlen false t
+   aux context 0 nn false t
                                                                       
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
@@ -938,9 +935,9 @@ and is_really_smaller
     is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
  | C.Appl (he::_) ->
     is_really_smaller r_uri r_len ~subst ~metasenv k he
- | C.Appl _
  | C.Rel _ 
  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
+ | C.Appl [] 
  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
  | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
@@ -952,9 +949,8 @@ and is_really_smaller
           List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl
         else
           let ty = typeof ~subst ~metasenv context term in
-          let itl_ctx,dcl= fix_lefts_in_constrs ~subst r_uri r_len context ty in
-          let start, stop = List.length context, List.length context + r_len in
-          let dc_ctx = context @ itl_ctx in
+          let dc_ctx, dcl, start, stop = 
+            specialize_and_abstract_constrs ~subst r_uri r_len context ty in
           List.for_all2
            (fun p (_,dc) -> 
              let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in
@@ -968,8 +964,8 @@ and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
   | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) 
   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
-     let isinductive, _, _, _, _ = E.get_checked_indtys ref in
-     if isinductive then None else (Some uri)
+     let isinductive, _, itl, _, _ = E.get_checked_indtys ref in
+     if isinductive then None else (Some (uri,List.length itl))
   | C.Prod (n,so,de) ->
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
@@ -1015,13 +1011,14 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
    | C.Inductive (is_ind, leftno, tyl, _) -> 
        check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
    | C.Fixpoint (inductive,fl,_) ->
-      let types, kl, len =
+      let types, kl =
         List.fold_left
-         (fun (types,kl,len) (_,name,k,ty,_) ->
+         (fun (types,kl) (_,name,k,ty,_) ->
            let _ = typeof ~subst ~metasenv [] ty in
-            ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
-         ) ([],[],0) fl
+            ((name,C.Decl ty)::types, k::kl)
+         ) ([],[]) fl
       in
+      let len = List.length types in
       let dfl, kl =   
         List.split (List.map2 
           (fun (_,_,_,_,bo) rno -> 
@@ -1031,7 +1028,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
       in
       List.iter2 (fun (_,name,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
-       if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty))
+       if not (R.are_convertible ~subst ~metasenv types ty_bo ty)
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
        else
         if inductive then begin
@@ -1056,15 +1053,15 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
         end else
          match returns_a_coinductive ~subst [] ty with
           | None ->
-              raise (TypeCheckerFailure
-                (lazy "CoFix: does not return a coinductive type"))
-          | Some uri ->
-              (* guarded by constructors conditions C{f,M} *)
-              if not 
-                (guarded_by_constructors ~subst ~metasenv types bo uri len)
-              then
-                raise (TypeCheckerFailure
-                 (lazy "CoFix: not guarded by constructors"))
+             raise (TypeCheckerFailure
+               (lazy "CoFix: does not return a coinductive type"))
+          | Some (r_uri, r_len) ->
+             (* guarded by constructors conditions C{f,M} *)
+             if not 
+             (guarded_by_constructors ~subst ~metasenv types bo r_uri r_len len)
+             then
+               raise (TypeCheckerFailure
+                (lazy "CoFix: not guarded by constructors"))
         ) fl dfl
 
 let typecheck_obj = check_obj_well_typed;;