aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrexpr_ops.ml22
-rw-r--r--interp/notation_ops.ml25
-rw-r--r--kernel/cClosure.ml11
-rw-r--r--kernel/constr.ml45
-rw-r--r--kernel/inductive.ml9
-rw-r--r--kernel/reduction.ml33
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/patternops.ml10
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/unification.ml19
-rw-r--r--tactics/term_dnet.ml32
12 files changed, 159 insertions, 60 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 737e86848..8b78a91b5 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -159,11 +159,8 @@ let rec constr_expr_eq e1 e2 =
Id.equal id1 id2 && List.equal instance_eq c1 c2
| CSort s1, CSort s2 ->
Miscops.glob_sort_eq s1 s2
- | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) ->
- constr_expr_eq a1 a2 &&
- constr_expr_eq b1 b2
- | CCast(a1,CastCoerce), CCast(a2, CastCoerce) ->
- constr_expr_eq a1 a2
+ | CCast(t1,c1), CCast(t2,c2) ->
+ constr_expr_eq t1 t2 && cast_expr_eq c1 c2
| CNotation(n1, s1), CNotation(n2, s2) ->
String.equal n1 n2 &&
constr_notation_substitution_eq s1 s2
@@ -176,7 +173,10 @@ let rec constr_expr_eq e1 e2 =
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
- | _ -> false
+ | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
+ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
+ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
+ | CGeneralization _ | CDelimiters _), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_located explicitation_eq) e1 e2 &&
@@ -232,6 +232,16 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
and instance_eq (x1,c1) (x2,c2) =
Id.equal x1 x2 && constr_expr_eq c1 c2
+and cast_expr_eq c1 c2 = match c1, c2 with
+| CastConv t1, CastConv t2
+| CastVM t1, CastVM t2
+| CastNative t1, CastNative t2 -> constr_expr_eq t1 t2
+| CastCoerce, CastCoerce -> true
+| CastConv _, _
+| CastVM _, _
+| CastNative _, _
+| CastCoerce, _ -> false
+
let constr_loc c = CAst.(c.loc)
let cases_pattern_expr_loc cp = CAst.(cp.loc)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0344dda97..20492e38c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -980,6 +980,19 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
else
bind_termlist_env alp sigma x l
+let match_cast match_fun sigma c1 c2 =
+ match c1, c2 with
+ | CastConv t1, CastConv t2
+ | CastVM t1, CastVM t2
+ | CastNative t1, CastNative t2 ->
+ match_fun sigma t1 t2
+ | CastCoerce, CastCoerce ->
+ sigma
+ | CastConv _, _
+ | CastVM _, _
+ | CastNative _, _
+ | CastCoerce, _ -> raise No_match
+
let does_not_come_from_already_eta_expanded_var glob =
(* This is hack to avoid looping on a rule with rhs of the form *)
(* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
@@ -1125,11 +1138,8 @@ let rec match_ inner u alp metas sigma a1 a2 =
let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
- | GCast(c1,CastConv t1), NCast (c2,CastConv t2)
- | GCast(c1,CastVM t1), NCast (c2,CastVM t2) ->
- match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
- | GCast(c1, CastCoerce), NCast(c2, CastCoerce) ->
- match_in u alp metas sigma c1 c2
+ | GCast(t1, c1), NCast(t2, c2) ->
+ match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
| GSort (GType _), NSort (GType _) when not u -> sigma
| GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
@@ -1157,8 +1167,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
- | (GRec _ | GEvar _), _
- | _,_ -> raise No_match
+ | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
+ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
+ | GCast _), _ -> raise No_match
and match_in u = match_ true u
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index e1b086b75..fa12e5406 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -480,7 +480,8 @@ let rec lft_fconstr n ft =
| FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
| FLIFT(k,m) -> lft_fconstr (n+k) m
| FLOCKED -> assert false
- | _ -> {norm=ft.norm; term=FLIFT(n,ft)}
+ | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _
+ | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(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 =
@@ -958,7 +959,10 @@ let rec knr info m stk =
(match evar_value info.i_cache ev with
Some c -> knit info env c stk
| None -> (m,stk))
- | _ -> (m,stk)
+ | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
+ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
+ | FCLOS _ -> (m, stk)
+
(* Computes the weak head normal form of a term *)
and kni info m stk =
@@ -1034,7 +1038,8 @@ and norm_head info m =
mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
| FProj (p,c) ->
mkProj (p, kl info c)
- | t -> term_of_fconstr m
+ | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
+ | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
(* Initialization and then normalization *)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index be59f9341..5930cfadc 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -674,6 +674,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
| Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2
| Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2
| LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2
+ (* Why do we suddenly make a special case for Cast here? *)
| App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
| _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
| App (c1,l1), App (c2,l2) ->
@@ -691,7 +692,9 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
&& Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
- | _ -> false
+ | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _
+ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _
+ | CoFix _), _ -> false
(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -811,9 +814,6 @@ let always_true _ _ = true
let rec eq_constr_nounivs m n =
(m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n
-(** We only use this function over blocks! *)
-let tag t = Obj.tag (Obj.repr t)
-
let constr_ord_int f t1 t2 =
let (=?) f g i1 i2 j1 j2=
let c = f i1 i2 in
@@ -825,35 +825,50 @@ let constr_ord_int f t1 t2 =
((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2
in
match kind t1, kind t2 with
+ | Cast (c1,_,_), _ -> f c1 t2
+ | _, Cast (c2,_,_) -> f t1 c2
+ (* Why this special case? *)
+ | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
+ | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
| Rel n1, Rel n2 -> Int.compare n1 n2
- | Meta m1, Meta m2 -> Int.compare m1 m2
+ | Rel _, _ -> -1 | _, Rel _ -> 1
| Var id1, Var id2 -> Id.compare id1 id2
+ | Var _, _ -> -1 | _, Var _ -> 1
+ | Meta m1, Meta m2 -> Int.compare m1 m2
+ | Meta _, _ -> -1 | _, Meta _ -> 1
+ | Evar (e1,l1), Evar (e2,l2) ->
+ (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+ | Evar _, _ -> -1 | _, Evar _ -> 1
| Sort s1, Sort s2 -> Sorts.compare s1 s2
- | Cast (c1,_,_), _ -> f c1 t2
- | _, Cast (c2,_,_) -> f t1 c2
+ | Sort _, _ -> -1 | _, Sort _ -> 1
| Prod (_,t1,c1), Prod (_,t2,c2)
| Lambda (_,t1,c1), Lambda (_,t2,c2) ->
(f =? f) t1 t2 c1 c2
+ | Prod _, _ -> -1 | _, Prod _ -> 1
+ | Lambda _, _ -> -1 | _, Lambda _ -> 1
| LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
((f =? f) ==? f) b1 b2 t1 t2 c1 c2
- | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2
- | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2))
+ | LetIn _, _ -> -1 | _, LetIn _ -> 1
| App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
- | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
- | Evar (e1,l1), Evar (e2,l2) ->
- (Evar.compare =? (Array.compare f)) e1 e2 l1 l2
+ | App _, _ -> -1 | _, App _ -> 1
| Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2
+ | Const _, _ -> -1 | _, Const _ -> 1
| Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2
+ | Ind _, _ -> -1 | _, Ind _ -> 1
| Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2
+ | Construct _, _ -> -1 | _, Construct _ -> 1
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
+ | Case _, _ -> -1 | _, Case _ -> 1
| Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
((fix_cmp =? (Array.compare f)) ==? (Array.compare f))
ln1 ln2 tl1 tl2 bl1 bl2
+ | Fix _, _ -> -1 | _, Fix _ -> 1
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
((Int.compare =? (Array.compare f)) ==? (Array.compare f))
ln1 ln2 tl1 tl2 bl1 bl2
- | t1, t2 -> Int.compare (tag t1) (tag t2)
+ | CoFix _, _ -> -1 | _, CoFix _ -> 1
+ | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
let rec compare m n=
constr_ord_int compare m n
@@ -937,7 +952,9 @@ let hasheq t1 t2 =
&& array_eqeq lna1 lna2
&& array_eqeq tl1 tl2
&& array_eqeq bl1 bl2
- | _ -> false
+ | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _
+ | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _
+ | Fix _ | CoFix _), _ -> false
(** Note that the following Make has the side effect of creating
once and for all the table we'll use for hash-consing all constr *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0782ea820..62aa9a2d7 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -809,8 +809,11 @@ let rec subterm_specif renv stack t =
| Dead_code -> Dead_code
| Not_subterm -> Not_subterm)
+ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+ | Construct _ | CoFix _ -> Not_subterm
+
+
(* Other terms are not subterms *)
- | _ -> Not_subterm
and lazy_subterm_specif renv stack t =
lazy (subterm_specif renv stack t)
@@ -1193,8 +1196,8 @@ let check_one_cofix env nbfix def deftype =
| Meta _ -> ()
| Evar _ ->
List.iter (check_rec_call env alreadygrd n tree vlra) args
-
- | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+ | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
+ | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
let ((mind, _),_) = codomain_is_coind env deftype in
let vlra = lookup_subterms env mind in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bf998933e..41d6c05eb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -57,7 +57,9 @@ let compare_stack_shape stk1 stk2 =
Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
- | (_,_) -> false in
+ | [], _ :: _
+ | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false
+ in
compare_rec 0 stk1 stk2
type lft_constr_stack_elt =
@@ -122,14 +124,17 @@ let nf_betaiota env t =
let whd_betaiotazeta env x =
match kind x with
- | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
+ | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> x
| App (c, _) ->
begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
- | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+ | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+ | Case _ | Fix _ | CoFix _ | Proj _ ->
+ whd_val (create_clos_infos betaiotazeta env) (inject x)
end
- | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+ | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
+ whd_val (create_clos_infos betaiotazeta env) (inject x)
let whd_all env t =
match kind t with
@@ -138,9 +143,12 @@ let whd_all env t =
| App (c, _) ->
begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ -> t
- | _ -> whd_val (create_clos_infos all env) (inject t)
+ | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
+ | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
+ whd_val (create_clos_infos all env) (inject t)
end
- | _ -> whd_val (create_clos_infos all env) (inject t)
+ | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
+ whd_val (create_clos_infos all env) (inject t)
let whd_allnolet env t =
match kind t with
@@ -149,9 +157,12 @@ let whd_allnolet env t =
| App (c, _) ->
begin match kind c with
| Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
- | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+ | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
+ | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
+ whd_val (create_clos_infos allnolet env) (inject t)
end
- | _ -> whd_val (create_clos_infos allnolet env) (inject t)
+ | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
+ whd_val (create_clos_infos allnolet env) (inject t)
(********************************************************************)
(* Conversion *)
@@ -578,10 +589,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
| ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
| (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
- | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
+ | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false
- (* In all other cases, terms are not convertible *)
- | _ -> raise NotConvertible
+ | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _
+ | FProd _ | FEvar _), _ -> raise NotConvertible
and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 47e812319..4ae875cd7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -302,7 +302,7 @@ let rec extract_type env db j c args =
if Projection.unfolded p then Tunknown
else extract_type env db j (mkProj (Projection.unfold p, t)) args
| Case _ | Fix _ | CoFix _ -> Tunknown
- | _ -> assert false
+ | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false
(*s Auxiliary function dealing with type application.
Precondition: [r] is a type scheme represented by the signature [s],
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3a9179813..20ef65c88 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -371,7 +371,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
| PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
Array.fold_left2 (sorec ctx env) subst args1 args2
- | _ -> raise PatternMatchingFailure
+ | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
+ | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
+ | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure
in
sorec [] env (Id.Map.empty, Id.Map.empty) pat c
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 4d8c09c50..41e09004c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -59,7 +59,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
fixpoint_eq f1 f2
| PCoFix f1, PCoFix f2 ->
cofixpoint_eq f1 f2
-| _ -> false
+| PProj (p1, t1), PProj (p2, t2) ->
+ Projection.equal p1 p2 && constr_pattern_eq t1 t2
+| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
+ | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
+ | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false
(** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
and pattern_eq (i1, j1, p1) (i2, j2, p2) =
@@ -442,8 +446,8 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
one non-trivial branch. These facts are used in [Constrextern]. *)
PCase (info, pred, pat_of_raw metas vars c, brs)
- | r -> err ?loc (Pp.str "Non supported pattern.")
- )
+ | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+ err ?loc (Pp.str "Non supported pattern."))
and pats_of_glob_branches loc metas vars ind brs =
let get_arg p = match DAst.get p with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 04374c88b..ba0502ca4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1167,7 +1167,8 @@ let local_whd_state_gen flags sigma =
|_ -> s
else s
- | x -> s
+ | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s
+
in
whrec
@@ -1771,8 +1772,8 @@ let meta_reducible_instance evd b =
let is_coerce = match s with CoerceToType -> true | _ -> false in
if not is_coerce then irec g else u
with Not_found -> u)
- | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) ->
- let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in
+ | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
+ let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
(match
try
let g, s = Metamap.find m metas in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a4e2f90d4..84ffab426 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -573,7 +573,9 @@ let is_rigid_head sigma flags t =
| Ind (i,u) -> true
| Construct _ -> true
| Fix _ | CoFix _ -> true
- | _ -> false
+ | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _)
+ | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _)
+ | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *)
let force_eqs c =
Universes.Constraints.fold
@@ -654,7 +656,10 @@ let rec is_neutral env sigma ts t =
| Evar _ | Meta _ -> true
| Case (_, p, c, cl) -> is_neutral env sigma ts c
| Proj (p, c) -> is_neutral env sigma ts c
- | _ -> false
+ | Lambda _ | LetIn _ | Construct _ | CoFix _ -> false
+ | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *)
+ | Fix _ -> false (* This is an approximation *)
+ | App _ -> assert false
let is_eta_constructor_app env sigma ts f l1 term =
match EConstr.kind sigma f with
@@ -1788,7 +1793,9 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
with ex when precatchable_exception ex ->
matchrec c)
- | _ -> user_err Pp.(str "Match_subterm")))
+ | Cast (_, _, _) (* Is this expected? *)
+ | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
+ | Construct _ -> user_err Pp.(str "Match_subterm")))
in
try matchrec cl
with ex when precatchable_exception ex ->
@@ -1854,7 +1861,11 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
| Lambda (_,t,c) ->
bind (matchrec t) (matchrec c)
- | _ -> fail "Match_subterm"))
+ | Cast (_, _, _) -> fail "Match_subterm" (* Is this expected? *)
+
+ | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _
+ | Construct _ -> fail "Match_subterm"))
+
in
let res = matchrec cl [] in
match res with
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 6c8130d79..7567cfa30 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -95,13 +95,20 @@ struct
let compare cmp t1 t2 = match t1, t2 with
| DRel, DRel -> 0
+ | DRel, _ -> -1 | _, DRel -> 1
| DSort, DSort -> 0
+ | DSort, _ -> -1 | _, DSort -> 1
| DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
+ | DRef _, _ -> -1 | _, DRef _ -> 1
+
| DCtx (tl1, tr1), DCtx (tl2, tr2)
| DLambda (tl1, tr1), DLambda (tl2, tr2)
| DApp (tl1, tr1), DApp (tl2, tr2) ->
let c = cmp tl1 tl2 in
if c = 0 then cmp tr1 tr2 else c
+ | DCtx _, _ -> -1 | _, DCtx _ -> 1
+ | DLambda _, _ -> -1 | _, DLambda _ -> 1
+ | DApp _, _ -> -1 | _, DApp _ -> 1
| DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) ->
let c = cmp c1 c2 in
@@ -113,6 +120,7 @@ struct
else c
else c
else c
+ | DCase _, _ -> -1 | _, DCase _ -> 1
| DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) ->
let c = Int.compare j1 j2 in
@@ -124,6 +132,8 @@ struct
else c
else c
else c
+ | DFix _, _ -> -1 | _, DFix _ -> 1
+
| DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) ->
let c = Int.compare i1 i2 in
if c = 0 then
@@ -131,7 +141,18 @@ struct
if c = 0 then Array.compare cmp pl1 pl2
else c
else c
- | _ -> Pervasives.compare t1 t2 (** OK **)
+ | DCoFix _, _ -> -1 | _, DCoFix _ -> 1
+
+ | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) ->
+ let c = cmp t1 t2 in
+ if Int.equal c 0 then
+ let c = Option.compare cmp ot1 ot2 in
+ if Int.equal c 0 then cmp u1 u2
+ else c
+ else c
+ | DCons _, _ -> -1 | _, DCons _ -> 1
+
+ | DNil, DNil -> 0
let fold f acc = function
| (DRel | DNil | DSort | DRef _) -> acc
@@ -174,7 +195,8 @@ struct
Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
- | _ -> assert false
+ | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
+ | DFix _ | DCoFix _ | DCons _), _ -> assert false
let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
let head w = map (fun _ -> ()) w in
@@ -194,11 +216,13 @@ struct
DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
| DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
- | _ -> assert false
+ | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
+ | DFix _ | DCoFix _ | DCons _), _ -> assert false
let terminal = function
| (DRel | DSort | DNil | DRef _) -> true
- | _ -> false
+ | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ ->
+ false
let compare t1 t2 = compare dummy_cmp t1 t2
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:56:29 +0000