From 944f62d08b7d78bcb20dd12ba138891d432b5987 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 May 2018 15:21:10 +0200 Subject: Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works. --- kernel/cClosure.ml | 32 ++++++++++++++++---------------- kernel/constr.ml | 28 ++++++++++++++-------------- kernel/esubst.ml | 2 +- kernel/reduction.ml | 2 +- 4 files changed, 32 insertions(+), 32 deletions(-) (limited to 'kernel') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 08114abc4..435cf0a79 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -482,7 +482,7 @@ let rec lft_fconstr n ft = let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = - if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v + if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v let clos_rel e i = match expand_rel i e with @@ -547,7 +547,7 @@ let mk_clos_vect env v = match v with | [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|] | [|v0; v1; v2; v3|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] -| v -> CArray.Fun1.map mk_clos env v +| v -> Array.Fun1.map mk_clos env v (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct @@ -562,7 +562,7 @@ let mk_clos_deep clos_fun env t = term = FCast (clos_fun env a, k, clos_fun env b)} | App (f,v) -> { norm = Red; - term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) } + term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } | Proj (p,c) -> { norm = Red; term = FProj (p, clos_fun env c) } @@ -605,21 +605,21 @@ let rec to_constr constr_fun lfts v = Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in + let ftys = Array.Fun1.map mk_clos e tys in + let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in let lfts' = el_liftn n lfts in - mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, + Array.Fun1.map constr_fun lfts' fbds)) | FCoFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in - let ftys = CArray.Fun1.map mk_clos e tys in - let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in + let ftys = Array.Fun1.map mk_clos e tys in + let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys, - CArray.Fun1.map constr_fun lfts' fbds)) + mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys, + Array.Fun1.map constr_fun lfts' fbds)) | FApp (f,ve) -> mkApp (constr_fun lfts f, - CArray.Fun1.map constr_fun lfts ve) + Array.Fun1.map constr_fun lfts ve) | FProj (p,c) -> mkProj (p,constr_fun lfts c) @@ -1024,14 +1024,14 @@ and norm_head info tab m = | FProd(na,dom,rng) -> mkProd(na, kl info tab dom, kl info tab rng) | FCoFix((n,(na,tys,bds)),e) -> - let ftys = CArray.Fun1.map mk_clos e tys in + let ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FFix((n,(na,tys,bds)),e) -> - let ftys = CArray.Fun1.map mk_clos e tys in + let ftys = Array.Fun1.map mk_clos e tys in let fbds = - CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in + Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds)) | FEvar((i,args),env) -> mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args) diff --git a/kernel/constr.ml b/kernel/constr.ml index a1779b36d..8f83d6baa 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -468,16 +468,16 @@ let iter_with_binders g f n c = match kind c with | Prod (_,t,c) -> f n t; f (g n) c | Lambda (_,t,c) -> f n t; f (g n) c | LetIn (_,b,t,c) -> f n b; f n t; f (g n) c - | App (c,l) -> f n c; CArray.Fun1.iter f n l - | Evar (_,l) -> CArray.Fun1.iter f n l - | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl + | App (c,l) -> f n c; Array.Fun1.iter f n l + | Evar (_,l) -> Array.Fun1.iter f n l + | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl | Proj (p,c) -> f n c | Fix (_,(_,tl,bl)) -> - CArray.Fun1.iter f n tl; - CArray.Fun1.iter f (iterate g (Array.length tl) n) bl + Array.Fun1.iter f n tl; + Array.Fun1.iter f (iterate g (Array.length tl) n) bl | CoFix (_,(_,tl,bl)) -> - CArray.Fun1.iter f n tl; - CArray.Fun1.iter f (iterate g (Array.length tl) n) bl + Array.Fun1.iter f n tl; + Array.Fun1.iter f (iterate g (Array.length tl) n) bl (* [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is @@ -625,7 +625,7 @@ let map_with_binders g f l c0 = match kind c0 with else mkLetIn (na, b', t', c') | App (c, al) -> let c' = f l c in - let al' = CArray.Fun1.Smart.map f l al in + let al' = Array.Fun1.Smart.map f l al in if c' == c && al' == al then c0 else mkApp (c', al') | Proj (p, t) -> @@ -633,25 +633,25 @@ let map_with_binders g f l c0 = match kind c0 with if t' == t then c0 else mkProj (p, t') | Evar (e, al) -> - let al' = CArray.Fun1.Smart.map f l al in + let al' = Array.Fun1.Smart.map f l al in if al' == al then c0 else mkEvar (e, al') | Case (ci, p, c, bl) -> let p' = f l p in let c' = f l c in - let bl' = CArray.Fun1.Smart.map f l bl in + let bl' = Array.Fun1.Smart.map f l bl in if p' == p && c' == c && bl' == bl then c0 else mkCase (ci, p', c', bl') | Fix (ln, (lna, tl, bl)) -> - let tl' = CArray.Fun1.Smart.map f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.Smart.map f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in if tl' == tl && bl' == bl then c0 else mkFix (ln,(lna,tl',bl')) | CoFix(ln,(lna,tl,bl)) -> - let tl' = CArray.Fun1.Smart.map f l tl in + let tl' = Array.Fun1.Smart.map f l tl in let l' = iterate g (Array.length tl) l in - let bl' = CArray.Fun1.Smart.map f l' bl in + let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) type instance_compare_fn = GlobRef.t -> int -> diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 91cc64523..4b8edf63f 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -140,7 +140,7 @@ let rec comp mk_cl s1 s2 = | ESID _, _ -> s2 | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2) | _, CONS(x,s') -> - CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') + CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') | CONS(x,s), SHIFT(k,s') -> let lg = Array.length x in if k == lg then comp mk_cl s s' diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 81fbd4f5e..38106fbf6 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with | [|c0; c1|] -> [|(l, c0); (l, c1)|] | [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|] | [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|] -| v -> CArray.Fun1.map (fun l t -> (l, t)) l v +| v -> Array.Fun1.map (fun l t -> (l, t)) l v let pure_stack lfts stk = let rec pure_rec lfts stk = -- cgit v1.2.3