aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/closure.ml119
-rw-r--r--checker/closure.mli5
-rw-r--r--checker/reduction.ml30
3 files changed, 53 insertions, 101 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index 35c16d2ab..a8b2b30f8 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -279,11 +279,12 @@ and fterm =
| FProj of constant * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCases of case_info * fconstr * fconstr * fconstr array
+ | FCase of case_info * fconstr * fconstr * fconstr array
+ | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (name * constr) list * constr * fconstr subs
| FProd of name * fconstr * fconstr
| FLetIn of name * fconstr * fconstr * constr * fconstr subs
- | FEvar of existential_key * fconstr array
+ | FEvar of existential_key * fconstr array (* why diff from kernel/closure? *)
| FLIFT of int * fconstr
| FCLOS of constr * fconstr subs
| FLOCKED
@@ -306,6 +307,7 @@ let update v1 (no,t) =
type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
+ | ZcaseT of case_info * constr * constr array * fconstr subs
| Zproj of int * int * constant
| Zfix of fconstr * stack
| Zshift of int
@@ -373,77 +375,7 @@ let zupdate m s =
Zupdate(m)::s'
else s
-(* Closure optimization: *)
-let rec compact_constr (lg, subs as s) c k =
- match c with
- Rel i ->
- if i < k then c,s else
- (try Rel (k + lg - List.index Int.equal (i-k+1) subs), (lg,subs)
- with Not_found -> Rel (k+lg), (lg+1, (i-k+1)::subs))
- | (Sort _|Var _|Meta _|Ind _|Const _|Construct _) -> c,s
- | Evar(ev,v) ->
- let (v',s) = compact_vect s v k in
- if v==v' then c,s else Evar(ev,v'),s
- | Cast(a,ck,b) ->
- let (a',s) = compact_constr s a k in
- let (b',s) = compact_constr s b k in
- if a==a' && b==b' then c,s else Cast(a', ck, b'), s
- | App(f,v) ->
- let (f',s) = compact_constr s f k in
- let (v',s) = compact_vect s v k in
- if f==f' && v==v' then c,s else App(f',v'), s
- | Proj (p, t) ->
- let (t', s) = compact_constr s t k in
- if t' == t then c,s else Proj(p,t'), s
- | Lambda(n,a,b) ->
- let (a',s) = compact_constr s a k in
- let (b',s) = compact_constr s b (k+1) in
- if a==a' && b==b' then c,s else Lambda(n,a',b'), s
- | Prod(n,a,b) ->
- let (a',s) = compact_constr s a k in
- let (b',s) = compact_constr s b (k+1) in
- if a==a' && b==b' then c,s else Prod(n,a',b'), s
- | LetIn(n,a,ty,b) ->
- let (a',s) = compact_constr s a k in
- let (ty',s) = compact_constr s ty k in
- let (b',s) = compact_constr s b (k+1) in
- if a==a' && ty==ty' && b==b' then c,s else LetIn(n,a',ty',b'), s
- | Fix(fi,(na,ty,bd)) ->
- let (ty',s) = compact_vect s ty k in
- let (bd',s) = compact_vect s bd (k+Array.length ty) in
- if ty==ty' && bd==bd' then c,s else Fix(fi,(na,ty',bd')), s
- | CoFix(i,(na,ty,bd)) ->
- let (ty',s) = compact_vect s ty k in
- let (bd',s) = compact_vect s bd (k+Array.length ty) in
- if ty==ty' && bd==bd' then c,s else CoFix(i,(na,ty',bd')), s
- | Case(ci,p,a,br) ->
- let (p',s) = compact_constr s p k in
- let (a',s) = compact_constr s a k in
- let (br',s) = compact_vect s br k in
- if p==p' && a==a' && br==br' then c,s else Case(ci,p',a',br'),s
-and compact_vect s v k = compact_v [] s v k (Array.length v - 1)
-and compact_v acc s v k i =
- if i < 0 then
- let v' = Array.of_list acc in
- if Array.for_all2 (==) v v' then v,s else v',s
- else
- let (a',s') = compact_constr s v.(i) k in
- compact_v (a'::acc) s' v k (i-1)
-
-(* Computes the minimal environment of a closure.
- Idea: if the subs is not identity, the term will have to be
- reallocated entirely (to propagate the substitution). So,
- computing the set of free variables does not change the
- complexity. *)
-let optimise_closure env c =
- if is_subs_id env then (env,c) else
- let (c',(_,s)) = compact_constr (0,[]) c 1 in
- let env' =
- Array.map (fun i -> clos_rel env i) (Array.of_list s) in
- (subs_cons (env', subs_id 0),c')
-
let mk_lambda env t =
- let (env,t) = optimise_closure env t in
let (rvars,t') = decompose_lam t in
FLambda(List.length rvars, List.rev rvars, t', env)
@@ -487,9 +419,7 @@ let mk_clos_deep clos_fun env t =
{ norm = Red;
term = FProj (p, clos_fun env c) }
| Case (ci,p,c,v) ->
- { norm = Red;
- term = FCases (ci, clos_fun env p, clos_fun env c,
- Array.map (clos_fun env) v) }
+ { norm = Red; term = FCaseT (ci, p, clos_fun env c, v, env) }
| Fix fx ->
{ norm = Cstr; term = FFix (fx, env) }
| CoFix cfx ->
@@ -520,10 +450,13 @@ let rec to_constr constr_fun lfts v =
| FFlex (ConstKey op) -> Const op
| FInd op -> Ind op
| FConstruct op -> Construct op
- | FCases (ci,p,c,ve) ->
+ | FCase (ci,p,c,ve) ->
Case (ci, constr_fun lfts p,
constr_fun lfts c,
Array.map (constr_fun lfts) ve)
+ | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *)
+ to_constr constr_fun lfts
+ {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)}
| FFix ((op,(lna,tys,bds)),e) ->
let n = Array.length bds in
let ftys = Array.map (mk_clos e) tys in
@@ -573,6 +506,8 @@ let term_of_fconstr =
| FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
| FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
compose_lam (List.rev tys) f
+ | FCaseT(ci,p,c,b,env) when is_subs_id env && is_lift_id lfts ->
+ Case(ci,p,term_of_fconstr_lift lfts c,b)
| FFix(fx,e) when is_subs_id e && is_lift_id lfts -> Fix fx
| FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> CoFix cfx
| _ -> to_constr term_of_fconstr_lift lfts v in
@@ -592,7 +527,10 @@ let rec zip m stk =
| [] -> m
| Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
| Zcase(ci,p,br)::s ->
- let t = FCases(ci, p, m, br) in
+ let t = FCase(ci, p, m, br) in
+ zip {norm=neutr m.norm; term=t} s
+ | ZcaseT(ci,p,br,e)::s ->
+ let t = FCaseT(ci, p, m, br, e) in
zip {norm=neutr m.norm; term=t} s
| Zproj (i,j,cst) :: s ->
zip {norm=neutr m.norm; term=FProj (cst,m)} s
@@ -672,7 +610,8 @@ let rec get_args n tys f e stk =
(* Eta expansion: add a reference to implicit surrounding lambda at end of stack *)
let rec eta_expand_stack = function
- | (Zapp _ | Zfix _ | Zcase _ | Zshift _ | Zupdate _ | Zproj _ as e) :: s ->
+ | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _
+ | Zshift _ | Zupdate _ as e) :: s ->
e :: eta_expand_stack s
| [] ->
[Zshift 1; Zapp [|{norm=Norm; term= FRel 1}|]]
@@ -790,7 +729,8 @@ let rec knh info m stk =
| FCLOS(t,e) -> knht info e t (zupdate m stk)
| FLOCKED -> assert false
| FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
- | FCases(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
+ | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk)
+ | FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk)
| FFix(((ri,n),(_,_,_)),_) ->
(match get_nth_arg m ri.(n) stk with
(Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -814,12 +754,11 @@ and knht info e t stk =
match t with
| App(a,b) ->
knht info e a (append_stack (mk_clos_vect e b) stk)
- | Case(ci,p,t,br) ->
- knht info e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk)
- | Fix _ -> knh info (mk_clos2 e t) stk
+ | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk)
+ | Fix _ -> knh info (mk_clos2 e t) stk (* laziness *)
| Cast(a,_,_) -> knht info e a stk
| Rel n -> knh info (clos_rel e n) stk
- | Proj (p,c) -> knh info (mk_clos2 e t) stk
+ | Proj (p,c) -> knh info (mk_clos2 e t) stk (* laziness *)
| (Lambda _|Prod _|Construct _|CoFix _|Ind _|
LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
(mk_clos2 e t, stk)
@@ -852,19 +791,23 @@ let rec knr info m stk =
assert (ci.ci_npar>=0);
let rargs = drop_parameters depth ci.ci_npar args in
kni info br.(c-1) (rargs@s)
- | (_, cargs, Zfix(fx,par)::s) ->
+ | (depth, args, ZcaseT(ci,_,br,env)::s) ->
+ assert (ci.ci_npar>=0);
+ let rargs = drop_parameters depth ci.ci_npar args in
+ knit info env br.(c-1) (rargs@s)
+ | (_, cargs, Zfix(fx,par)::s) ->
let rarg = fapp_stack(m,cargs) in
let stk' = par @ append_stack [|rarg|] s in
let (fxe,fxbd) = contract_fix_vect fx.term in
knit info fxe fxbd stk'
- | (depth, args, Zproj (n, m, cst)::s) ->
+ | (depth, args, Zproj (n, m, cst)::s) ->
let rargs = drop_parameters depth n args in
let rarg = project_nth_arg m rargs in
- kni info rarg s
- | (_,args,s) -> (m,args@s))
+ kni info rarg s
+ | (_,args,s) -> (m,args@s))
| FCoFix _ when red_set info.i_flags fIOTA ->
(match strip_update_shift_app m stk with
- (_, args, ((Zcase _::_) as stk')) ->
+ (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
let (fxe,fxbd) = contract_fix_vect m.term in
knit info fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
diff --git a/checker/closure.mli b/checker/closure.mli
index 03970fc9f..4bb2a88c0 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -98,7 +98,8 @@ type fterm =
| FProj of constant * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
- | FCases of case_info * fconstr * fconstr * fconstr array
+ | FCase of case_info * fconstr * fconstr * fconstr array
+ | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (name * constr) list * constr * fconstr subs
| FProd of name * fconstr * fconstr
| FLetIn of name * fconstr * fconstr * constr * fconstr subs
@@ -115,6 +116,7 @@ type fterm =
type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
+ | ZcaseT of case_info * constr * constr array * fconstr subs
| Zproj of int * int * constant
| Zfix of fconstr * stack
| Zshift of int
@@ -180,6 +182,5 @@ val kni: clos_infos -> fconstr -> stack -> fconstr * stack
val knr: clos_infos -> fconstr -> stack -> fconstr * stack
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
-val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
(* End of cbn debug section i*)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index aa9639e55..e333b67c3 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -42,7 +42,8 @@ let compare_stack_shape stk1 stk2 =
| (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
| (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
Int.equal bal 0 && compare_rec 0 s1 s2
- | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
+ | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1,
+ (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) ->
bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -75,6 +76,8 @@ let pure_stack lfts stk =
| (Zfix(fx,a),(l,pstk)) ->
let (lfx,pa) = pure_rec l a in
(l, Zlfix((lfx,fx),pa)::pstk)
+ | (ZcaseT(ci,p,br,env),(l,pstk)) ->
+ (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk)
| (Zcase(ci,p,br),(l,pstk)) ->
(l,Zlcase(ci,l,p,br)::pstk)) in
snd (pure_rec lfts stk)
@@ -176,6 +179,7 @@ let rec no_arg_available = function
| Zapp v :: stk -> Array.length v = 0 && no_arg_available stk
| Zproj _ :: _ -> true
| Zcase _ :: _ -> true
+ | ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
let rec no_nth_arg_available n = function
@@ -188,6 +192,7 @@ let rec no_nth_arg_available n = function
else false
| Zproj _ :: _ -> true
| Zcase _ :: _ -> true
+ | ZcaseT _ :: _ -> true
| Zfix _ :: _ -> true
let rec no_case_available = function
@@ -197,11 +202,12 @@ let rec no_case_available = function
| Zapp _ :: stk -> no_case_available stk
| Zproj (_,_,_) :: _ -> false
| Zcase _ :: _ -> false
+ | ZcaseT _ :: _ -> false
| Zfix _ :: _ -> true
let in_whnf (t,stk) =
match fterm_of t with
- | (FLetIn _ | FCases _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
+ | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false
| FLambda _ -> no_arg_available stk
| FConstruct _ -> no_case_available stk
| FCoFix _ -> no_case_available stk
@@ -414,8 +420,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
- | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
- | (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
+ | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
+ | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
| (FLOCKED,_) | (_,FLOCKED) ) -> assert false
(* In all other cases, terms are not convertible *)
@@ -430,21 +436,23 @@ and convert_stacks univ infos lft1 lft2 stk1 stk2 =
and convert_vect univ infos lft1 lft2 v1 v2 =
Array.iter2 (fun t1 t2 -> ccnv univ CONV infos lft1 lft2 t1 t2) v1 v2
-let clos_fconv cv_pb env t1 t2 =
- let infos = create_clos_infos betaiotazeta env in
+let clos_fconv cv_pb eager_delta env t1 t2 =
+ let infos =
+ create_clos_infos
+ (if eager_delta then betadeltaiota else betaiotazeta) env in
let univ = universes env in
ccnv univ cv_pb infos el_id el_id (inject t1) (inject t2)
-let fconv cv_pb env t1 t2 =
+let fconv cv_pb eager_delta env t1 t2 =
if eq_constr t1 t2 then ()
- else clos_fconv cv_pb env t1 t2
+ else clos_fconv cv_pb eager_delta env t1 t2
-let conv = fconv CONV
-let conv_leq = fconv CUMUL
+let conv = fconv CONV false
+let conv_leq = fconv CUMUL false
(* option for conversion : no compilation for the checker *)
-let vm_conv = fconv
+let vm_conv cv_pb = fconv cv_pb true
(********************************************************************)
(* Special-Purpose Reduction *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:05:59 +0000