diff options
| author | Maxime Dénès | 2020-02-03 18:19:42 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-06 11:22:43 +0200 |
| commit | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch) | |
| tree | fbad060c3c2e29e81751dea414c898b5cb0fa22d /pretyping/evarconv.ml | |
| parent | cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff) | |
Primitive persistent arrays
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0206d4e70d..6880383a31 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -130,7 +130,7 @@ let flex_kind_of_term flags env evd c sk = | Evar ev -> if is_frozen flags ev then Rigid else Flexible ev - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ -> Rigid + | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false @@ -212,7 +212,7 @@ let occur_rigidly flags env evd (evk,_) t = (match aux c with | Rigid b -> Rigid b | _ -> Reducible) - | Meta _ | Fix _ | CoFix _ | Int _ | Float _ -> Reducible + | Meta _ | Fix _ | CoFix _ | Int _ | Float _ | Array _ -> Reducible in match aux t with | Rigid b -> b @@ -898,7 +898,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty only if necessary) or the second argument is potentially usable as a canonical projection or canonical value *) let rec is_unnamed (hd, args) = match EConstr.kind i hd with - | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _) -> + | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _|Array _) -> Stack.not_purely_applicative args | (CoFix _|Meta _|Rel _)-> true | Evar _ -> Stack.not_purely_applicative args @@ -1019,7 +1019,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | Ind _, Ind _ | Construct _, Construct _ | Int _, Int _ - | Float _, Float _ -> + | Float _, Float _ + | Array _, Array _ -> rigids env evd sk1 term1 sk2 term2 | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *) @@ -1064,9 +1065,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end - | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Evar _ | Lambda _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Array _ | Evar _ | Lambda _), _ -> UnifFailure (evd,NotSameHead) - | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) -> + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Array _ | Evar _ | Lambda _) -> UnifFailure (evd,NotSameHead) | Case _, _ -> UnifFailure (evd,NotSameHead) | Proj _, _ -> UnifFailure (evd,NotSameHead) |