From fbadb3454a52d879edc58a4a09ca46c1e77dce2f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Apr 2008 17:52:04 +0000 Subject: [PATCH] Avoid (whd ~delta:true) during guarded_by_destructors as much as possible. Note: it is better to check again if this commit is fully correct (i.e. w.r.t. the catch-all case in the main "match ... with" of the aux function). --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 6dceca87f..60c9ab617 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -911,7 +911,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns 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)); *) - match R.whd ~subst context t with (* TODO: use ~delta:false as mush as poss*) + let t = R.whd ~delta:max_int ~subst context t in + try + match t with | C.Rel m as t when List.mem_assoc m recfuns -> raise (NotGuarded (lazy (NCicPp.ppterm ~subst ~metasenv ~context t ^ " passed around"))) @@ -979,6 +981,13 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = pl cl | _ -> 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 with NotGuarded s -> raise (TypeCheckerFailure s) -- 2.39.2