aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/term.ml4
-rw-r--r--kernel/term.mli1
-rw-r--r--pretyping/clenv.ml40
-rw-r--r--pretyping/evd.ml9
-rw-r--r--pretyping/evd.mli5
-rw-r--r--pretyping/reductionops.ml51
-rw-r--r--pretyping/unification.ml14
7 files changed, 83 insertions, 41 deletions
diff --git a/kernel/term.ml b/kernel/term.ml
index 3386f45f51..5f9a3ff93d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -388,7 +388,9 @@ let destApplication = destApp
let isApp c = match kind_of_term c with App _ -> true | _ -> false
-let isProd c = match kind_of_term c with | Prod(_) -> true | _ -> false
+let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
+
+let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
(* Destructs a constant *)
let destConst c = match kind_of_term c with
diff --git a/kernel/term.mli b/kernel/term.mli
index 4133ca8920..fcae3341e4 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -234,6 +234,7 @@ val isMeta : constr -> bool
val isSort : constr -> bool
val isCast : constr -> bool
val isApp : constr -> bool
+val isLambda : constr -> bool
val isProd : constr -> bool
val isConst : constr -> bool
val isConstruct : constr -> bool
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 96facdef2a..cfecbf3191 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -383,6 +383,32 @@ let error_already_defined b =
anomalylabstrm ""
(str "Position " ++ int n ++ str" already defined")
+let rec similar_type_shapes t u =
+ let t,_ = decompose_app t and u,_ = decompose_app u in
+ match kind_of_term t, kind_of_term u with
+ | Prod (_,t1,t2), Prod (_,u1,u2) -> similar_type_shapes t2 u2
+ | Const cst, Const cst' -> cst = cst'
+ | Var id, Var id' -> id = id'
+ | Ind ind, Ind ind' -> ind = ind'
+ | Rel n, Rel n' -> n = n'
+ | Sort s, Sort s' -> family_of_sort s = family_of_sort s'
+ | Case (_,_,c,_), Case (_,_,c',_) -> similar_type_shapes c c'
+ | _ -> false
+
+let clenv_unify_similar_types clenv t u =
+ if similar_type_shapes t u then
+ try Processed, clenv_unify true CUMUL t u clenv
+ with e when precatchable_exception e -> Coercible t, clenv
+ else Coercible t, clenv
+
+let clenv_assign_binding clenv k (sigma,c) =
+ let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
+ let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
+ let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
+ let status,clenv'' = clenv_unify_similar_types clenv' c_typ k_typ in
+(* let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*)
+ { clenv'' with evd = meta_assign k (c,status) clenv''.evd }
+
let clenv_match_args bl clenv =
if bl = [] then
clenv
@@ -390,25 +416,15 @@ let clenv_match_args bl clenv =
let mvs = clenv_independent clenv in
check_bindings bl;
List.fold_left
- (fun clenv (loc,b,(sigma,c)) ->
+ (fun clenv (loc,b,(sigma,c as sc)) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
else error_already_defined b
else
- let c_typ = nf_betaiota (clenv_get_type_of clenv c) in
- let c_typ = clenv_hnf_constr clenv c_typ in
- let clenv = { clenv with evd = evar_merge clenv.evd sigma} in
- {clenv with evd = meta_assign k (c,Coercible c_typ) clenv.evd})
+ clenv_assign_binding clenv k sc)
clenv bl
-let clenv_assign_binding clenv k (sigma,c) =
- let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
- let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
- let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
- let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
- { clenv' with evd = meta_assign k (c',Coercible c_typ) evd }
-
let clenv_constrain_last_binding c clenv =
let all_mvs = collect_metas clenv.templval.rebus in
let k =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ebd635b807..7b5690e2cc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -335,7 +335,8 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
*)
type instance_status =
- IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
+ | IsSuperType | IsSubType
+ | ConvUpToEta of int | Coercible of types | Processed
(* Clausal environments *)
@@ -538,13 +539,13 @@ let meta_merge evd1 evd2 =
type metabinding = metavariable * constr * instance_status
-let retract_defined_metas evd =
+let retract_coercible_metas evd =
let mc,ml =
Metamap.fold (fun n v (mc,ml) ->
match v with
- | Clval (na,(b,s),typ) ->
+ | Clval (na,(b,s),typ) when s <> Processed ->
(n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml
- | Cltyp _ as v ->
+ | v ->
mc, Metamap.add n v ml)
evd.metas ([],Metamap.empty) in
mc, { evd with metas = ml }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 784e066b71..b6ffd02c12 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -112,7 +112,8 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
*)
type instance_status =
- IsSuperType | IsSubType | ConvUpToEta of int | Coercible of types
+ | IsSuperType | IsSubType
+ | ConvUpToEta of int | Coercible of types | Processed
type clbinding =
| Cltyp of name * constr freelisted
@@ -180,7 +181,7 @@ val metas_of : evar_defs -> metamap
type metabinding = metavariable * constr * instance_status
-val retract_defined_metas : evar_defs -> metabinding list * evar_defs
+val retract_coercible_metas : evar_defs -> metabinding list * evar_defs
val subst_defined_metas : metabinding list -> constr -> constr option
(**********************************************************)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3e9b08beb4..7f05b1cbfa 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -882,28 +882,49 @@ let nf_meta env c = meta_instance env (mk_freelisted c)
(* Instantiate metas that create beta/iota redexes *)
-let meta_reducible_instance env b =
- let s =
- List.map (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+let meta_value evd mv =
+ let rec valrec mv =
+ try
+ let b,_ = meta_fvalue evd mv in
+ instance
+ (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
+ b.rebus
+ with Anomaly _ | Not_found ->
+ mkMeta mv
in
+ valrec mv
+
+let meta_reducible_instance evd b =
+ let fm = Metaset.elements b.freemetas in
+ let s = List.fold_left (fun l mv ->
+ try let g,s = meta_fvalue evd mv in (mv,(g.rebus,s))::l
+ with Anomaly _ | Not_found -> l) [] fm in
let rec irec u =
let u = whd_betaiota u in
match kind_of_term u with
| Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
- let bl' = Array.map irec bl in
- let p' = irec p in
let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
- let g = List.assoc m s in
- (match kind_of_term g with
- | Construct _ -> whd_betaiota (mkCase (ci,p',g,bl'))
- | _ -> mkCase (ci,p',c,bl'))
+ (match
+ try
+ let g,s = List.assoc m s in
+ if isConstruct g or s = Processed then Some g else None
+ with Not_found -> None
+ with
+ | Some g -> irec (mkCase (ci,p,g,bl))
+ | None -> mkCase (ci,irec p,c,Array.map irec bl))
| App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
- let l' = Array.map irec l in
let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
- let g = List.assoc m s in
- (match kind_of_term g with
- | Lambda _ -> beta_appvect g l'
- | _ -> mkApp (f,l'))
+ (match
+ try
+ let g,s = List.assoc m s in
+ if isLambda g or s = Processed then Some g else None
+ with Not_found -> None
+ with
+ | Some g -> irec (mkApp (g,l))
+ | None -> mkApp (f,Array.map irec l))
+ | Meta m ->
+ (try let g,s = List.assoc m s in if s = Processed then irec g else u
+ with Not_found -> u)
| _ -> map_constr irec u
in
- if s = [] then b.rebus else irec b.rebus
+ if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e296737f25..bd6fb5ad88 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -65,7 +65,7 @@ let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
let opp_status = function
| IsSuperType -> IsSubType
| IsSubType -> IsSuperType
- | ConvUpToEta _ | Coercible _ as x -> x
+ | ConvUpToEta _ | Coercible _ | Processed as x -> x
let extract_instance_status = function
| Cumul -> (IsSubType,IsSuperType)
@@ -231,13 +231,13 @@ let merge_instances env sigma mod_delta st1 st2 c1 c2 =
| (ConvUpToEta n1, ConvUpToEta n2) ->
let side = left (* arbitrary choice, but agrees with compatibility *) in
unify_with_eta side mod_delta env sigma n1 n2 c1 c2
- | ((IsSubType | ConvUpToEta _ | Coercible _ as oppst1),
- (IsSubType | ConvUpToEta _ | Coercible _)) ->
+ | ((IsSubType | ConvUpToEta _ | Coercible _ | Processed as oppst1),
+ (IsSubType | ConvUpToEta _ | Coercible _ | Processed)) ->
let res = unify_0 env sigma Cumul mod_delta c2 c1 in
if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
else (st2=IsSubType, ConvUpToEta 0, res)
- | ((IsSuperType | ConvUpToEta _ | Coercible _ as oppst1),
- (IsSuperType | ConvUpToEta _ | Coercible _)) ->
+ | ((IsSuperType | ConvUpToEta _ | Coercible _ | Processed as oppst1),
+ (IsSuperType | ConvUpToEta _ | Coercible _ | Processed)) ->
let res = unify_0 env sigma Cumul mod_delta c1 c2 in
if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
else (st2=IsSuperType, ConvUpToEta 0, res)
@@ -379,7 +379,7 @@ let w_merge env with_types mod_delta metas evars evd =
else
begin
let evd,n =
- if with_types (* or occur_meta mvty *) then
+ if with_types & status <> Processed then
let sigma = evars_of evd in
let metas = metas_of evd in
let mvty = Typing.meta_type evd mv in
@@ -439,7 +439,7 @@ let w_merge env with_types mod_delta metas evars evd =
types of metavars are unifiable with the types of their instances *)
let w_unify_core_0 env with_types cv_pb mod_delta m n evd =
- let (mc1,evd') = retract_defined_metas evd in
+ let (mc1,evd') = retract_coercible_metas evd in
let (mc2,ec) =
unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in
w_merge env with_types mod_delta mc2 ec evd'
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 18:30:40 +0000