]> matita.cs.unibo.it Git - helm.git/commitdiff
guarded_by_destructors on steroids
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 10:17:34 +0000 (10:17 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 10:17:34 +0000 (10:17 +0000)
  when Fix/i args and some args are not guarded
  1) fixed params in interval 0..i are checked for bewing just passed around
  2) the fix is unfolded, debruijned, fixed arguments substituted,
     not fixed arguments pushed and checked for guardednes
  3) a new function with relative fixed arguments (not to be checked again)
     is added to k
  4) the resulting term is applied to the remaining arguments

  testcase: cic:/Suresnes/MiniC/MiniC/State/sizeOfType.con

helm/software/components/ng_kernel/nCicTypeChecker.ml

index 60c9ab6170e7679e8270dacd106111bff8739be7..63b7765a5fc54bee614df84ddf11a4b254c7ace0 100644 (file)
@@ -22,14 +22,71 @@ 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 ->
+      let lefts, _ = HExtlib.split_nth j args in
+      List.map (fun ((b,x),i) -> b && x = NCic.Rel (k+(j-i))) 
+        (HExtlib.list_mapi (fun x i -> x,i) (List.combine acc lefts))
+  | 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,29 +958,46 @@ 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 = 
-(*
-   prerr_endline ("GB: " ^ NCicPp.ppterm ~metasenv ~subst ~context t
-     ^ "        " ^ String.concat "," (List.map (fun i -> NCicPp.ppterm ~metasenv ~subst ~context (C.Rel i)) safes));
- *)
+ let rec aux (context, recfuns, x as k) t = 
   let t = R.whd ~delta:max_int ~subst context t in
+(*
+   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 List.mem_assoc m recfuns -> 
+  | 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.Def (bo,_) -> aux k (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
+  | 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 ^ 
@@ -936,38 +1010,39 @@ 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.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.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) ->
+    when List.exists (fun t->try aux k t;false with NotGuarded _->true) args ->
       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
+        (* cerco i parametri fissi solo fino a j, un po aleatorio *)
+      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 = 
+        (* potrebbe anche aggiungere un arg di cui fa push alle safe *)
+        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
@@ -978,18 +1053,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'
+    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)
 
 (*
@@ -1036,12 +1109,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)
@@ -1049,19 +1118,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 =
@@ -1072,10 +1135,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::_) ->
@@ -1105,7 +1168,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
@@ -1175,15 +1238,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")))
@@ -1219,7 +1288,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;;