aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/eConstr.ml22
-rw-r--r--engine/eConstr.mli7
-rw-r--r--engine/evd.ml2
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/termops.ml42
-rw-r--r--engine/termops.mli4
-rw-r--r--kernel/constr.ml83
-rw-r--r--kernel/constr.mli86
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/nativecode.ml12
-rw-r--r--kernel/nativevalues.ml28
11 files changed, 261 insertions, 29 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 3dc1933a14..2913645c1c 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -259,7 +259,17 @@ let decompose_prod_n_assum sigma n c =
let existential_type = Evd.existential_type
-let map sigma f c = match kind sigma c with
+let map_under_context f n c =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr (Constr.map_under_context f n (unsafe_to_constr c))
+let map_branches f ci br =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
+let map_return_predicate f ci p =
+ let f c = unsafe_to_constr (f (of_constr c)) in
+ of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+
+let map_gen userview sigma f c = match kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c
| Cast (b,k,t) ->
@@ -296,6 +306,12 @@ let map sigma f c = match kind sigma c with
let l' = Array.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
+ | Case (ci,p,b,bl) when userview ->
+ let b' = f b in
+ let p' = map_return_predicate f ci p in
+ let bl' = map_branches f ci bl in
+ if b'==b && p'==p && bl'==bl then c
+ else mkCase (ci, p', b', bl')
| Case (ci,p,b,bl) ->
let b' = f b in
let p' = f p in
@@ -313,6 +329,9 @@ let map sigma f c = match kind sigma c with
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
+let map_user_view = map_gen true
+let map = map_gen false
+
let map_with_binders sigma g f l c0 = match kind sigma c0 with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c0
@@ -794,6 +813,7 @@ struct
let to_sorts = ESorts.unsafe_to_sorts
let to_instance = EInstance.unsafe_to_instance
let to_constr = unsafe_to_constr
+let to_constr_array = unsafe_to_constr_array
let to_rel_decl = unsafe_to_rel_decl
let to_named_decl = unsafe_to_named_decl
let to_named_context =
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index ecb36615f3..f897448557 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -224,7 +224,11 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
(** {6 Iterators} *)
val map : Evd.evar_map -> (t -> t) -> t -> t
+val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
+val map_under_context : (t -> t) -> int -> t -> t
+val map_branches : (t -> t) -> case_info -> t array -> t array
+val map_return_predicate : (t -> t) -> case_info -> t -> t
val iter : Evd.evar_map -> (t -> unit) -> t -> unit
val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
@@ -315,6 +319,9 @@ sig
val to_constr : t -> Constr.t
(** Physical identity. Does not care for defined evars. *)
+ val to_constr_array : t array -> Constr.t array
+ (** Physical identity. Does not care for defined evars. *)
+
val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
(** Physical identity. Does not care for defined evars. *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 9f976b57dd..d7b03a84f1 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1267,7 +1267,9 @@ module MiniEConstr = struct
let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
let of_kind = Constr.of_kind
let of_constr c = c
+ let of_constr_array v = v
let unsafe_to_constr c = c
+ let unsafe_to_constr_array v = v
let unsafe_eq = Refl
let to_constr ?(abort_on_undefined_evars=true) sigma c =
diff --git a/engine/evd.mli b/engine/evd.mli
index db2bd4eedf..1a5614988d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -657,10 +657,12 @@ module MiniEConstr : sig
val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
+ val of_constr_array : Constr.t array -> t array
val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
val unsafe_to_constr : t -> Constr.t
+ val unsafe_to_constr_array : t array -> Constr.t array
val unsafe_eq : (t, Constr.t) eq
diff --git a/engine/termops.ml b/engine/termops.ml
index e4c8ae66bc..156d1370e3 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -715,10 +715,26 @@ let map_constr_with_binders_left_to_right sigma g f l c =
then c
else mkCoFix (ln,(lna,tl',bl'))
+let map_under_context_with_full_binders sigma g f l n d =
+ let open EConstr in
+ let f l c = Unsafe.to_constr (f l (of_constr c)) in
+ let g d l = g (of_rel_decl d) l in
+ let d = EConstr.Unsafe.to_constr (EConstr.whd_evar sigma d) in
+ EConstr.of_constr (Constr.map_under_context_with_full_binders g f l n d)
+
+let map_branches_with_full_binders sigma g f l ci bl =
+ let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+ let bl' = Array.map2 (map_under_context_with_full_binders sigma g f l) tags bl in
+ if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_full_binders sigma g f l ci p =
+ let n = List.length ci.ci_pp_info.ind_tags in
+ let p' = map_under_context_with_full_binders sigma g f l n p in
+ if p' == p then p else p'
+
(* strong *)
-let map_constr_with_full_binders sigma g f l cstr =
+let map_constr_with_full_binders_gen userview sigma g f l cstr =
let open EConstr in
- let open RelDecl in
match EConstr.kind sigma cstr with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> cstr
@@ -728,16 +744,16 @@ let map_constr_with_full_binders sigma g f l cstr =
if c==c' && t==t' then cstr else mkCast (c', k, t')
| Prod (na,t,c) ->
let t' = f l t in
- let c' = f (g (LocalAssum (na, t)) l) c in
+ let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in
if t==t' && c==c' then cstr else mkProd (na, t', c')
| Lambda (na,t,c) ->
let t' = f l t in
- let c' = f (g (LocalAssum (na, t)) l) c in
+ let c' = f (g (RelDecl.LocalAssum (na, t)) l) c in
if t==t' && c==c' then cstr else mkLambda (na, t', c')
| LetIn (na,b,t,c) ->
let b' = f l b in
let t' = f l t in
- let c' = f (g (LocalDef (na, b, t)) l) c in
+ let c' = f (g (RelDecl.LocalDef (na, b, t)) l) c in
if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
| App (c,al) ->
let c' = f l c in
@@ -749,6 +765,12 @@ let map_constr_with_full_binders sigma g f l cstr =
| Evar (e,al) ->
let al' = Array.map (f l) al in
if Array.for_all2 (==) al al' then cstr else mkEvar (e, al')
+ | Case (ci,p,c,bl) when userview ->
+ let p' = map_return_predicate_with_full_binders sigma g f l ci p in
+ let c' = f l c in
+ let bl' = map_branches_with_full_binders sigma g f l ci bl in
+ if p==p' && c==c' && bl'==bl then cstr else
+ mkCase (ci, p', c', bl')
| Case (ci,p,c,bl) ->
let p' = f l p in
let c' = f l c in
@@ -758,7 +780,7 @@ let map_constr_with_full_binders sigma g f l cstr =
| Fix (ln,(lna,tl,bl)) ->
let tl' = Array.map (f l) tl in
let l' =
- Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
+ Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
@@ -766,12 +788,18 @@ let map_constr_with_full_binders sigma g f l cstr =
| CoFix(ln,(lna,tl,bl)) ->
let tl' = Array.map (f l) tl in
let l' =
- Array.fold_left2 (fun l na t -> g (LocalAssum (na, t)) l) l lna tl in
+ Array.fold_left2 (fun l na t -> g (RelDecl.LocalAssum (na, t)) l) l lna tl in
let bl' = Array.map (f l') bl in
if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
then cstr
else mkCoFix (ln,(lna,tl',bl'))
+let map_constr_with_full_binders sigma g f =
+ map_constr_with_full_binders_gen false sigma g f
+
+let map_constr_with_full_binders_user_view sigma g f =
+ map_constr_with_full_binders_gen true sigma g f
+
(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
right according to the usual representation of the constructions as
diff --git a/engine/termops.mli b/engine/termops.mli
index 80988989f1..b967bb6abb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -63,6 +63,10 @@ val map_constr_with_full_binders :
Evd.evar_map ->
(rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
+val map_constr_with_full_binders_user_view :
+ Evd.evar_map ->
+ (rel_declaration -> 'a -> 'a) ->
+ ('a -> constr -> constr) -> 'a -> constr -> constr
(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 9bf743152f..c73fe7fbde 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -503,7 +503,79 @@ let fold_constr_with_binders g f n acc c =
not recursive and the order with which subterms are processed is
not specified *)
-let map f c = match kind c with
+let rec map_under_context f n d =
+ if n = 0 then f d else
+ match kind d with
+ | LetIn (na,b,t,c) ->
+ let b' = f b in
+ let t' = f t in
+ let c' = map_under_context f (n-1) c in
+ if b' == b && t' == t && c' == c then d
+ else mkLetIn (na,b',t',c')
+ | Lambda (na,t,b) ->
+ let t' = f t in
+ let b' = map_under_context f (n-1) b in
+ if t' == t && b' == b then d
+ else mkLambda (na,t',b')
+ | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
+
+let map_branches f ci bl =
+ let nl = Array.map List.length ci.ci_pp_info.cstr_tags in
+ let bl' = Array.map2 (map_under_context f) nl bl in
+ if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate f ci p =
+ map_under_context f (List.length ci.ci_pp_info.ind_tags) p
+
+let rec map_under_context_with_binders g f l n d =
+ if n = 0 then f l d else
+ match kind d with
+ | LetIn (na,b,t,c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = map_under_context_with_binders g f (g l) (n-1) c in
+ if b' == b && t' == t && c' == c then d
+ else mkLetIn (na,b',t',c')
+ | Lambda (na,t,b) ->
+ let t' = f l t in
+ let b' = map_under_context_with_binders g f (g l) (n-1) b in
+ if t' == t && b' == b then d
+ else mkLambda (na,t',b')
+ | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
+
+let map_branches_with_binders g f l ci bl =
+ let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+ let bl' = Array.map2 (map_under_context_with_binders g f l) tags bl in
+ if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_binders g f l ci p =
+ map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p
+
+let rec map_under_context_with_full_binders g f l n d =
+ if n = 0 then f l d else
+ match kind d with
+ | LetIn (na,b,t,c) ->
+ let b' = f l b in
+ let t' = f l t in
+ let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in
+ if b' == b && t' == t && c' == c then d
+ else mkLetIn (na,b',t',c')
+ | Lambda (na,t,b) ->
+ let t' = f l t in
+ let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in
+ if t' == t && b' == b then d
+ else mkLambda (na,t',b')
+ | _ -> CErrors.anomaly (Pp.str "Ill-formed context")
+
+let map_branches_with_full_binders g f l ci bl =
+ let tags = Array.map List.length ci.ci_pp_info.cstr_tags in
+ let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in
+ if Array.for_all2 (==) bl' bl then bl else bl'
+
+let map_return_predicate_with_full_binders g f l ci p =
+ map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p
+
+let map_gen userview f c = match kind c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> c
| Cast (b,k,t) ->
@@ -540,6 +612,12 @@ let map f c = match kind c with
let l' = Array.Smart.map f l in
if l'==l then c
else mkEvar (e, l')
+ | Case (ci,p,b,bl) when userview ->
+ let b' = f b in
+ let p' = map_return_predicate f ci p in
+ let bl' = map_branches f ci bl in
+ if b'==b && p'==p && bl'==bl then c
+ else mkCase (ci, p', b', bl')
| Case (ci,p,b,bl) ->
let b' = f b in
let p' = f p in
@@ -557,6 +635,9 @@ let map f c = match kind c with
if tl'==tl && bl'==bl then c
else mkCoFix (ln,(lna,tl',bl'))
+let map_user_view = map_gen true
+let map = map_gen false
+
(* Like {!map} but with an accumulator. *)
let fold_map f accu c = match kind c with
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 70acf19328..9cc044316b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -381,6 +381,85 @@ type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
+(** {6 Functionals working on expressions canonically abstracted over
+ a local context (possibly with let-ins)} *)
+
+(** [map_under_context f l c] maps [f] on the immediate subterms of a
+ term abstracted over a context of length [n] (local definitions
+ are counted) *)
+
+val map_under_context : (constr -> constr) -> int -> constr -> constr
+
+(** [map_branches f br] maps [f] on the immediate subterms of an array
+ of "match" branches [br] in canonical eta-let-expanded form; it is
+ not recursive and the order with which subterms are processed is
+ not specified; it preserves sharing; the immediate subterms are the
+ types and possibly terms occurring in the context of each branch as
+ well as the body of each branch *)
+
+val map_branches : (constr -> constr) -> case_info -> constr array -> constr array
+
+(** [map_return_predicate f p] maps [f] on the immediate subterms of a
+ return predicate of a "match" in canonical eta-let-expanded form;
+ it is not recursive and the order with which subterms are processed
+ is not specified; it preserves sharing; the immediate subterms are
+ the types and possibly terms occurring in the context of each
+ branch as well as the body of the predicate *)
+
+val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr
+
+(** [map_under_context_with_binders g f n l c] maps [f] on the
+ immediate subterms of a term abstracted over a context of length
+ [n] (local definitions are counted); it preserves sharing; it
+ carries an extra data [n] (typically a lift index) which is
+ processed by [g] (which typically add 1 to [n]) at each binder
+ traversal *)
+
+val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
+
+(** [map_branches_with_binders f br] maps [f] on the immediate
+ subterms of an array of "match" branches [br] in canonical
+ eta-let-expanded form; it carries an extra data [n] (typically a
+ lift index) which is processed by [g] (which typically adds 1 to
+ [n]) at each binder traversal; it is not recursive and the order
+ with which subterms are processed is not specified; it preserves
+ sharing; the immediate subterms are the types and possibly terms
+ occurring in the context of the branch as well as the body of the
+ branch *)
+
+val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
+
+(** [map_return_predicate_with_binders f p] maps [f] on the immediate
+ subterms of a return predicate of a "match" in canonical
+ eta-let-expanded form; it carries an extra data [n] (typically a
+ lift index) which is processed by [g] (which typically adds 1 to
+ [n]) at each binder traversal; it is not recursive and the order
+ with which subterms are processed is not specified; it preserves
+ sharing; the immediate subterms are the types and possibly terms
+ occurring in the context of each branch as well as the body of the
+ predicate *)
+
+val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
+
+(** [map_under_context_with_full_binders g f n l c] is similar to
+ [map_under_context_with_binders] except that [g] takes also a full
+ binder as argument and that only the number of binders (and not
+ their signature) is required *)
+
+val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr
+
+(** [map_branches_with_full_binders g f l br] is equivalent to
+ [map_branches_with_binders] but using
+ [map_under_context_with_full_binders] *)
+
+val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array
+
+(** [map_return_predicate_with_full_binders g f l p] is equivalent to
+ [map_return_predicate_with_binders] but using
+ [map_under_context_with_full_binders] *)
+
+val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr
+
(** {6 Functionals working on the immediate subterm of a construction } *)
(** [fold f acc c] folds [f] on the immediate subterms of [c]
@@ -395,6 +474,13 @@ val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
val map : (constr -> constr) -> constr -> constr
+(** [map_user_view f c] maps [f] on the immediate subterms of [c]; it
+ differs from [map f c] in that the typing context and body of the
+ return predicate and of the branches of a [match] are considered as
+ immediate subterm of a [match] *)
+
+val map_user_view : (constr -> constr) -> constr -> constr
+
(** Like {!map}, but also has an additional accumulator. *)
val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4d13a5fcb8..1d2f22b006 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -932,7 +932,7 @@ let check_one_fix renv recpos trees def =
let case_spec = branches_specif renv
(lazy_subterm_specif renv [] c_0) ci in
let stack' = push_stack_closures renv l stack in
- let stack' = filter_stack_domain renv.env p stack' in
+ let stack' = filter_stack_domain renv.env p stack' in
Array.iteri (fun k br' ->
let stack_br = push_stack_args case_spec.(k) stack' in
check_rec_call renv stack_br br') lrest
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ad10c86945..eed25a4ca4 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -632,6 +632,14 @@ let mkMLapp f args =
| MLapp(f,args') -> MLapp(f,Array.append args' args)
| _ -> MLapp(f,args)
+let mkForceCofix prefix ind arg =
+ let name = fresh_lname Anonymous in
+ MLlet (name, arg,
+ MLif (
+ MLisaccu (prefix, ind, MLlocal name),
+ MLapp (MLprimitive Force_cofix, [|MLlocal name|]),
+ MLlocal name))
+
let empty_params = [||]
let decompose_MLlam c =
@@ -1143,7 +1151,7 @@ let ml_of_instance instance u =
let arg = ml_of_lam env l a in
let force =
if annot.asw_finite then arg
- else MLapp(MLprimitive Force_cofix, [|arg|]) in
+ else mkForceCofix annot.asw_prefix annot.asw_ind arg in
mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
| Lif(t,bt,bf) ->
MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
@@ -1999,7 +2007,7 @@ let compile_mind mb mind stack =
let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
- let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
+ let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in
let gn = Gproj ("", ind, proj_arg) in
Glet (gn, mkMLlam [|c_uid|] code) :: acc
in
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 3bf23f1468..93e74af845 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -154,10 +154,6 @@ let args_of_accu (k:accumulator) =
let acc = (get_accu k).acc_arg in
(Obj.magic (Array.of_list acc) : t array)
-let is_accu x =
- let o = Obj.repr x in
- Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
-
let mk_fix_accu rec_pos pos types bodies =
mk_accu (Afix(types,bodies,rec_pos, pos))
@@ -172,19 +168,17 @@ let upd_cofix (cofix :t) (cofix_fun : t) =
| _ -> assert false
let force_cofix (cofix : t) =
- if is_accu cofix then
- let accu = (Obj.magic cofix : accumulator) in
- let atom = atom_of_accu accu in
- match atom with
- | Acofix(typ,norm,pos,f) ->
- let args = args_of_accu accu in
- let f = Array.fold_right (fun arg f -> f arg) args f in
- let v = f (Obj.magic ()) in
- set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
- v
- | Acofixe(_,_,_,v) -> v
- | _ -> cofix
- else cofix
+ let accu = (Obj.magic cofix : accumulator) in
+ let atom = atom_of_accu accu in
+ match atom with
+ | Acofix(typ,norm,pos,f) ->
+ let args = args_of_accu accu in
+ let f = Array.fold_right (fun arg f -> f arg) args f in
+ let v = f (Obj.magic ()) in
+ set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
+ v
+ | Acofixe(_,_,_,v) -> v
+ | _ -> cofix
let mk_const tag = Obj.magic tag
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:59:52 +0000