X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=55a3a6d7f927608c9546abf72dcf5b173516ff0e;hb=c87ca87169e38a22e7bf7a347238597500964285;hp=6dceca87ff375ecadbd8e5d9efcbe6bba044fc52;hpb=3928102abd95778d390e2790fdb7ac2ae3567813;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 6dceca87f..55a3a6d7f 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -22,14 +22,74 @@ let set_logger f = logger := f;;
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
-let shift_k e (c,rf,x,safes) =
-  e::c,List.map (fun (k,v) -> k+1,v) rf,x+1,List.map ((+)1) safes
+type recf_entry = 
+  | Evil of int (* rno *) 
+  | UnfFix of bool list (* fixed arguments *) 
+  | Safe
 ;;
 
-let shift_k_add_1_safe e (c,rf,x,safes) =
-  e::c,List.map (fun (k,v) -> k+1,v) rf,x+1,1::List.map ((+)1) safes
+let is_dangerous i l = 
+  List.exists (function (j,Evil _) when j=i -> true | _ -> false) l
 ;;
 
+let is_unfolded i l = 
+  List.exists (function (j,UnfFix _) when j=i -> true | _ -> false) l
+;;
+
+let is_safe i l =
+  List.exists (function (j,Safe) when j=i -> true | _ -> false) l
+;;
+
+let get_recno i l = 
+  try match List.assoc i l with Evil rno -> rno | _ -> assert false
+  with Not_found -> assert false
+;;
+
+let get_fixed_args i l = 
+  try match List.assoc i l with UnfFix fa -> fa | _ -> assert false
+  with Not_found -> assert false
+;;
+
+let shift_k e (c,rf,x) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1;;
+
+let string_of_recfuns ~subst ~metasenv ~context l = 
+  let pp = NCicPp.ppterm ~subst ~metasenv ~context in
+  let safe, rest = List.partition (function (_,Safe) -> true | _ -> false) l in
+  let dang, unf = List.partition (function (_,UnfFix _) -> false | _->true)rest in
+  "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (NCic.Rel i)) safe) ^
+  "\n\tfix  : "^String.concat "," 
+   (List.map 
+     (function (i,UnfFix l)-> pp(NCic.Rel i)^"/"^String.concat "," (List.map
+       string_of_bool l)
+     | _ ->assert false) unf) ^
+  "\n\trec  : "^String.concat "," 
+   (List.map 
+     (function (i,Evil rno)->pp(NCic.Rel i)^"/"^string_of_int rno
+     | _ -> assert false) dang)
+;;
+
+let fixed_args bo j n nn =
+ let rec aux k acc = function
+  | NCic.Appl (NCic.Rel i::args) when i+k > n && i+k <= nn ->
+      (try 
+        let lefts, _ = HExtlib.split_nth j args in
+        List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i)) 
+          (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts))
+      with Failure "HExtlib.split_nth" -> assert false)
+        (* se sono meno di j, fino a j deduco, dopo false *)
+  | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t    
+ in
+   aux 0 (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bo
+;;
+
+let rec list_iter_default2 f l1 def l2 = 
+  match l1,l2 with
+    | [], _ -> ()
+    | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb 
+    | a::ta, [] -> f a def; list_iter_default2 f ta def [] 
+;;
+
+
 (*
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
@@ -901,27 +961,42 @@ and eat_lambdas ~subst ~metasenv context n te =
   | (n, C.Lambda (name,so,ta)) when n > 0 ->
       eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
    | (n, te) ->
-      raise (AssertFailure (lazy (Printf.sprintf "9 (%d, %s)" n 
+      raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n 
         (NCicPp.ppterm ~subst ~metasenv ~context te))))
 
+and eat_or_subst_lambdas 
+ ~subst ~metasenv n te to_be_subst args (context, recfuns, x as k) 
+=
+  match n, R.whd ~subst context te, to_be_subst, args with
+  | (0, _,_,[]) -> te, k
+  | (0, _,_,_::_) -> C.Appl (te::args), k
+  | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
+      eat_or_subst_lambdas ~subst ~metasenv 
+       (n - 1) (S.subst arg ta) to_be_subst args k
+  | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
+      eat_or_subst_lambdas ~subst ~metasenv 
+       (n - 1) ta to_be_subst args (shift_k (name,(C.Decl so)) k)
+  | (n, te, _, []) -> te, k
+  | (n, te, _, _::_) -> C.Appl (te::args), k
+
 and guarded_by_destructors r_uri r_len ~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) t = 
+ let rec aux (context, recfuns, x as k) t = 
+  let t = R.whd ~delta:max_int ~subst context t in
 (*
-   prerr_endline ("GB: " ^ NCicPp.ppterm ~metasenv ~subst ~context t
-     ^ "        " ^ String.concat "," (List.map (fun i -> NCicPp.ppterm ~metasenv ~subst ~context (C.Rel i)) safes));
- *)
-  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 -> 
+   prerr_endline ("GB:\n" ^ 
+     NCicPp.ppcontext ~subst ~metasenv context^
+     NCicPp.ppterm ~metasenv ~subst ~context t^
+       string_of_recfuns ~subst ~metasenv ~context recfuns);
+*)
+  try
+  match t with
+  | C.Rel m as t when is_dangerous m recfuns -> 
       raise (NotGuarded (lazy 
-        (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around")))
-  | C.Rel m ->
-     (match List.nth context (m-1) with 
-     | _,C.Decl _ -> ()
-     | _,C.Def (bo,_) -> aux (context, recfuns, x, safes) (S.lift m bo))
-  | C.Meta _ -> ()
-  | C.Appl ((C.Rel m)::tl) as t when List.mem_assoc m recfuns ->
-     let rec_no = List.assoc m recfuns in
+        (NCicPp.ppterm ~subst ~metasenv ~context t ^ 
+         " is a partial application of a fix")))
+  | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns ->
+     let rec_no = get_recno m recfuns in
      if not (List.length tl > rec_no) then 
        raise (NotGuarded (lazy 
          (NCicPp.ppterm ~context ~subst ~metasenv t ^ 
@@ -934,38 +1009,46 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
           t) (NCicPp.ppterm ~context ~subst ~metasenv rec_arg)
           (NCicPp.ppcontext ~subst ~metasenv context))));
        List.iter (aux k) tl
-  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,j))) as r)::args) 
-    when List.length args > j 
-     (* TODO: extra check really usueful?? *)      
-    && List.exists (fun (k,_) -> List.exists (fun t -> not (does_not_occur ~subst context k (k+1) t)) args) recfuns
-    && is_really_smaller r_uri r_len ~subst ~metasenv k (List.nth args j) ->
+  | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns ->
+       let fixed_args = get_fixed_args m recfuns in
+       list_iter_default2 (fun x b -> if not b then aux k x) tl false fixed_args
+  | C.Rel m ->
+     (match List.nth context (m-1) with 
+     | _,C.Decl _ -> ()
+     | _,C.Def (bo,_) -> aux k (S.lift m bo))
+  | C.Meta _ -> ()
+  | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,j))) 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 ctx_tys, bos = 
         List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl)
       in
       let bo = List.nth bos i in
-      let bo = debruijn uri (List.length fl) context bo in
-      let args, rest = HExtlib.split_nth j args in  
-      let bo = 
-        (* TODO: here we should check which args are passed around ... *)
-        if j > 0 then R.head_beta_reduce ~upto:j (C.Appl (bo::args)) else bo 
-      in
-      let bo, context_rec = eat_lambdas ~subst ~metasenv context 1 bo in
-      let bo = 
-        if rest = [] then  bo else
-        let rest = List.tl rest in if rest <> [] then C.Appl (bo::rest) else bo
+      let fl_len = List.length fl in
+      let bo = debruijn uri fl_len context bo in
+      let ctx_len = List.length context in
+        (* we may look for fixed params not only up to j ... *)
+      let fa = fixed_args bo j ctx_len (ctx_len + fl_len) in
+      list_iter_default2 (fun x b -> if not b then aux k x) args false fa; 
+      let context = context@ctx_tys in
+      let k = context, recfuns, x in
+      let bo, k = 
+        (* we should enrich k with infos regarding args that are safe but not
+         * fixed *)
+        eat_or_subst_lambdas ~subst ~metasenv j bo fa args k
       in
-      let k = context@ctx_tys, recfuns, x, safes in
-      aux (shift_k_add_1_safe (List.hd context_rec) k) bo
+      let k = context, (List.length context - i,UnfFix fa) :: recfuns, x in
+       aux k bo
   | 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 ->
+     | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
         (* TODO: add CoInd to references so that this call is useless *)
         let isinductive, _, _, _, _ = E.get_checked_indtys ref in
         if not isinductive then recursor aux k t
         else
          let ty = typeof ~subst ~metasenv context term in
-         let itl_ctx,cl = fix_lefts_in_constrs ~subst r_uri r_len context ty in
+         let itl_ctx,dcl = fix_lefts_in_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
@@ -976,11 +1059,16 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
              let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in
              let p, k = get_new_safes ~subst k p rl in
              aux k p) 
-           pl cl
+           pl dcl
      | _ -> recursor aux k t)
   | t -> recursor aux k t
+  with
+   NotGuarded _ as exc ->
+    let t' = R.whd ~delta:0 ~subst context t in
+    if t = t' then raise exc
+    else aux k t'
  in
-  try aux (context, recfuns, 1, []) t
+  try aux (context, recfuns, 1) t
   with NotGuarded s -> raise (TypeCheckerFailure s)
 
 (*
@@ -1027,12 +1115,8 @@ and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
-  | C.Rel _ | C.Appl _ -> []
+  | C.Rel _ | C.Appl _ | C.Const _ -> []
   | C.Prod (name,so,de) ->
-(*
-      prerr_endline ("RA: " ^ NCicPp.ppterm ~subst ~metasenv ~context so
-       ^ " == " ^ string_of_bool (not (does_not_occur ~subst context n nn so)));
- *)
      (not (does_not_occur ~subst context n nn so)) ::
       (recursive_args ~subst ~metasenv 
         ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
@@ -1040,19 +1124,13 @@ and recursive_args ~subst ~metasenv context n nn te =
      raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst
      ~metasenv ~context:[] t)))
 
-and get_new_safes ~subst (context, recfuns, x, safes as k) p rl =
+and get_new_safes ~subst (context, recfuns, x as k) p rl =
   match R.whd ~subst context p, rl with
   | C.Lambda (name,so,ta), b::tl ->
-      let safes = (if b then [0] else []) @ safes in
+      let recfuns = (if b then [0,Safe] else []) @ recfuns in
       get_new_safes ~subst 
-        (shift_k (name,(C.Decl so)) (context, recfuns, x, safes)) ta tl
-  | C.Meta _ as e, _ | e, [] -> 
-(*
-      prerr_endline ("GNS: " ^ String.concat ","
-        (List.map (fun i -> 
-          NCicPp.ppterm ~subst ~metasenv:[] ~context (C.Rel i)) safes));
- *)
-      e, k
+        (shift_k (name,(C.Decl so)) (context, recfuns, x)) ta tl
+  | C.Meta _ as e, _ | e, [] -> e, k
   | _ -> raise (AssertFailure (lazy "Ill formed pattern"))
 
 and split_prods ~subst context n te =
@@ -1063,10 +1141,10 @@ and split_prods ~subst context n te =
   | _ -> raise (AssertFailure (lazy "split_prods"))
 
 and is_really_smaller 
-  r_uri r_len ~subst ~metasenv (context, recfuns, x, safes as k) te 
+  r_uri r_len ~subst ~metasenv (context, recfuns, x as k) te 
 =
  match R.whd ~subst context te with
- | C.Rel m when List.mem m safes -> true
+ | C.Rel m when is_safe m recfuns -> true
  | C.Lambda (name, s, t) ->
     is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
  | C.Appl (he::_) ->
@@ -1096,7 +1174,7 @@ and is_really_smaller
  | 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 ->
+    | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
         (* TODO: add CoInd to references so that this call is useless *)
         let isinductive, _, _, _, _ = E.get_checked_indtys ref in
         if not isinductive then
@@ -1166,15 +1244,21 @@ 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, len =
         List.fold_left
          (fun (types,kl,len) (_,name,k,ty,_) ->
            let _ = typeof ~subst ~metasenv [] ty in
             ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
          ) ([],[],0) fl
       in
-      List.iter (fun (_,name,x,ty,bo) ->
-       let bo = debruijn uri len [] bo in
+      let dfl, kl =   
+        List.split (List.map2 
+          (fun (_,_,_,_,bo) rno -> 
+             let dbo = debruijn uri len [] bo in
+             dbo, Evil rno)
+          fl kl)
+      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))
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
@@ -1210,7 +1294,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
               then
                 raise (TypeCheckerFailure
                  (lazy "CoFix: not guarded by constructors"))
-        ) fl
+        ) fl dfl
 
 let typecheck_obj = check_obj_well_typed;;