aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml45
-rw-r--r--pretyping/matching.ml34
-rw-r--r--pretyping/pattern.ml102
-rw-r--r--pretyping/pattern.mli7
-rw-r--r--test-suite/output/Tactics.out3
-rw-r--r--test-suite/output/Tactics.v9
6 files changed, 152 insertions, 48 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2fe967153f..2cbbfca028 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -873,6 +873,13 @@ let extern_type at_top env t =
(******************************************************************)
(* Main translation function from pattern -> constr_expr *)
+let it_destPLambda n c =
+ let rec aux n nal c =
+ if n=0 then (nal,c) else match c with
+ | PLambda (na,_,c) -> aux (n-1) (na::nal) c
+ | _ -> anomaly "it_destPLambda" in
+ aux n [] c
+
let rec raw_of_pat env = function
| PRef ref -> RRef (loc,ref)
| PVar id -> RVar (loc,id)
@@ -897,20 +904,30 @@ let rec raw_of_pat env = function
RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
| PLambda (na,t,c) ->
RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
- | PCase ((_,cs),typopt,tm,[||]) ->
- if typopt <> None then failwith "TODO: PCase to RCases";
- RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None,
- [raw_of_pat env tm,(Anonymous,None)],[])
- | PCase ((Some ind,cs),typopt,tm,bv) ->
- let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
- let mib,mip = lookup_mind_specif (Global.env()) ind in
- let k = mip.Declarations.mind_nrealargs in
- let nparams = mib.Declarations.mind_nparams in
- let cstrnargs = mip.Declarations.mind_consnrealdecls in
- Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env)
- (fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
- avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv
- | PCase _ -> error "Unsupported case-analysis while printing pattern"
+ | PIf (c,b1,b2) ->
+ RIf (loc, raw_of_pat env c, (Anonymous,None),
+ raw_of_pat env b1, raw_of_pat env b2)
+ | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
+ let nal,b = it_destPLambda n b in
+ RLetTuple (loc,nal,(Anonymous,None),raw_of_pat env tm,raw_of_pat env b)
+ | PCase ((_,cstr_nargs,ind,ind_nargs),p,tm,bv) ->
+ let brs =
+ array_map2_i (fun i n b ->
+ let nal,c = it_destPLambda n b in
+ let mkPatVar na = PatVar (loc,na) in
+ (* ind is None only if no branch and no return type *)
+ let cs = (out_some ind,i+1) in
+ let p = PatCstr (loc,cs,List.map mkPatVar nal,Anonymous) in
+ let ids = map_succeed out_name nal in
+ (loc,ids,[p],raw_of_pat (nal@env) c)) cstr_nargs bv in
+ let decompose_pred n p =
+ let nal,p = it_destPLambda (n+1) p in
+ (List.hd nal, Some (loc,out_some ind,List.tl nal)),
+ Some (raw_of_pat env p) in
+ let indnames,pred =
+ if p = PMeta None then (Anonymous,None),None
+ else decompose_pred (out_some ind_nargs) p in
+ RCases (loc,pred,[raw_of_pat env tm,indnames],Array.to_list brs)
| PFix f -> Detyping.detype false [] env (mkFix f)
| PCoFix c -> Detyping.detype false [] env (mkCoFix c)
| PSort s -> RSort (loc,s)
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 462fe1eb1d..2b0a0ac7b2 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -17,6 +17,7 @@ open Termops
open Reductionops
open Term
open Rawterm
+open Sign
open Environ
open Pattern
(*i*)
@@ -70,6 +71,11 @@ let memb_metavars m n =
let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
+let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
+ match ind with
+ | Some ind -> ind = ci2.ci_ind
+ | None -> cs1 = ci2.ci_cstr_nargs
+
let matches_core convert allow_partial_app pat c =
let rec sorec stk sigma p t =
let cT = strip_outer_cast t in
@@ -79,7 +85,7 @@ let matches_core convert allow_partial_app pat c =
List.map
(function
| PRel n -> n
- | _ -> error "Only bound indices are currently allowed in second order pattern matching")
+ | _ -> error "Only bound indices allowed in second order pattern matching")
args in
let frels = Intset.elements (free_rels cT) in
if list_subset frels relargs then
@@ -150,15 +156,27 @@ let matches_core convert allow_partial_app pat c =
if is_conv env evars c cT then sigma
else raise PatternMatchingFailure
- | PCase (_,_,a1,br1), Case (_,_,a2,br2) ->
- (* On ne teste pas le prédicat *)
- if (Array.length br1) = (Array.length br2) then
- array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2
+ | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
+ let ctx,b2 = decompose_prod_n_assum ci.ci_cstr_nargs.(0) b2 in
+ let ctx',b2' = decompose_prod_n_assum ci.ci_cstr_nargs.(1) b2' in
+ let n = List.length ctx and n' = List.length ctx' in
+ if noccur_between 1 n b2 & noccur_between 1 n' b2' then
+ let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in
+ let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in
+ let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
+ sorec s' (sorec s (sorec stk sigma a1 a2) b1 b2) b1' b2'
else
raise PatternMatchingFailure
- (* À faire *)
- | PFix f0, Fix f1 when f0 = f1 -> sigma
- | PCoFix c0, CoFix c1 when c0 = c1 -> sigma
+
+ | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
+ if same_case_structure ci1 ci2 br1 br2 then
+ array_fold_left2 (sorec stk)
+ (sorec stk (sorec stk sigma a1 a2) p1 p2) br1 br2
+ else
+ raise PatternMatchingFailure
+
+ | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> sigma
+ | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> sigma
| _ -> raise PatternMatchingFailure
in
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 634f0b5915..9029578cd2 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -38,8 +38,9 @@ type constr_pattern =
| PLetIn of name * constr_pattern * constr_pattern
| PSort of rawsort
| PMeta of patvar option
- | PCase of (inductive option * case_style)
- * constr_pattern option * constr_pattern * constr_pattern array
+ | PIf of constr_pattern * constr_pattern * constr_pattern
+ | PCase of (case_style * int array * inductive option * int option)
+ * constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
@@ -49,9 +50,10 @@ let rec occur_meta_pattern = function
| PLambda (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
| PProd (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
| PLetIn (na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c)
- | PCase(_,None,c,br) ->
- (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
- | PCase(_,Some p,c,br) ->
+ | PIf (c,c1,c2) ->
+ (occur_meta_pattern c) or
+ (occur_meta_pattern c1) or (occur_meta_pattern c2)
+ | PCase(_,p,c,br) ->
(occur_meta_pattern p) or
(occur_meta_pattern c) or (array_exists occur_meta_pattern br)
| PMeta _ | PSoApp _ -> true
@@ -70,6 +72,7 @@ let rec head_pattern_bound t =
| PProd (_,_,b) -> head_pattern_bound b
| PLetIn (_,_,b) -> head_pattern_bound b
| PApp (c,args) -> head_pattern_bound c
+ | PIf (c,_,_) -> head_pattern_bound c
| PCase (_,p,c,br) -> head_pattern_bound c
| PRef r -> r
| PVar id -> VarRef id
@@ -103,14 +106,44 @@ let rec pattern_of_constr t =
| Construct sp -> PRef (ConstructRef sp)
| Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
| Case (ci,p,a,br) ->
- PCase ((Some ci.ci_ind,ci.ci_pp_info.style),
- Some (pattern_of_constr p),pattern_of_constr a,
+ let cip = ci.ci_pp_info in
+ PCase ((cip.style,ci.ci_cstr_nargs,Some ci.ci_ind,Some cip.ind_nargs),
+ pattern_of_constr p,pattern_of_constr a,
Array.map pattern_of_constr br)
| Fix f -> PFix f
| CoFix f -> PCoFix f
(* To process patterns, we need a translation without typing at all. *)
+let map_pattern_with_binders g f l = function
+ | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
+ | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
+ | PLambda (n,a,b) -> PLambda (n,f l a,f (g l) b)
+ | PProd (n,a,b) -> PProd (n,f l a,f (g l) b)
+ | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g l) b)
+ | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
+ | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
+ (* Non recursive *)
+ | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _
+ (* Bound to terms *)
+ | PFix _ | PCoFix _ as x) -> x
+
+let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+
+let rec instantiate_pattern lvar = function
+ | PVar id as x -> (try List.assoc id lvar with Not_found -> x)
+ | (PFix _ | PCoFix _) -> error ("Not instantiable pattern")
+ | c -> map_pattern (instantiate_pattern lvar) c
+
+let rec liftn_pattern k n = function
+ | PRel i as x -> if i >= n then PRel (i+k) else x
+ | PFix x -> PFix (destFix (liftn k n (mkFix x)))
+ | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
+ | c -> map_pattern_with_binders succ (liftn_pattern k) n c
+
+let lift_pattern k = liftn_pattern k 1
+
+(*
let rec inst lvar = function
| PVar id as x -> (try List.assoc id lvar with Not_found -> x)
| PApp (p,pl) -> PApp (inst lvar p, Array.map (inst lvar) pl)
@@ -125,6 +158,7 @@ let rec inst lvar = function
(* Bound to terms *)
| (PFix _ | PCoFix _) ->
error ("Not instantiable pattern")
+*)
let rec subst_pattern subst pat = match pat with
| PRef ref ->
@@ -160,12 +194,20 @@ let rec subst_pattern subst pat = match pat with
PLetIn (name,c1',c2')
| PSort _
| PMeta _ -> pat
- | PCase (cs,typ, c, branches) ->
- let typ' = option_smartmap (subst_pattern subst) typ in
+ | PIf (c,c1,c2) ->
+ let c' = subst_pattern subst c in
+ let c1' = subst_pattern subst c1 in
+ let c2' = subst_pattern subst c2 in
+ if c' == c && c1' == c1 && c2' == c2 then pat else
+ PIf (c',c1',c2')
+ | PCase ((a,b,ind,n as cs),typ,c,branches) ->
+ let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in
+ let typ' = subst_pattern subst typ in
let c' = subst_pattern subst c in
let branches' = array_smartmap (subst_pattern subst) branches in
+ let cs' = if ind == ind' then cs else (a,b,ind',n) in
if typ' == typ && c' == c && branches' == branches then pat else
- PCase(cs,typ', c', branches')
+ PCase(cs',typ', c', branches')
| PFix fixpoint ->
let cstr = mkFix fixpoint in
let fixpoint' = destFix (subst_mps subst cstr) in
@@ -177,8 +219,8 @@ let rec subst_pattern subst pat = match pat with
if cofixpoint' == cofixpoint then pat else
PCoFix cofixpoint'
-
-let instantiate_pattern = inst
+let mkPLambda na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambda = List.fold_right mkPLambda
let rec pat_of_raw metas vars = function
| RVar (_,id) ->
@@ -212,17 +254,30 @@ let rec pat_of_raw metas vars = function
Pp.warning "Cast not taken into account in constr pattern";
pat_of_raw metas vars c
| RIf (_,c,(_,None),b1,b2) ->
- PCase ((None,IfStyle),None, pat_of_raw metas vars c,
- [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
- | RCases (loc,None,[c,_],brs) ->
- let sp =
+ PIf (pat_of_raw metas vars c,
+ pat_of_raw metas vars b1,pat_of_raw metas vars b2)
+ | RLetTuple (loc,nal,(_,None),b,c) ->
+ let mkRLambda c na = RLambda (loc,na,RHole (loc,Evd.InternalHole),c) in
+ let c = List.fold_left mkRLambda c nal in
+ PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
+ [|pat_of_raw metas vars c|])
+ | RCases (loc,p,[c,(na,indnames)],brs) ->
+ let pred,ind_nargs, ind = match p,indnames with
+ | Some p, Some (_,ind,nal) ->
+ rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
+ Some (List.length nal),Some ind
+ | _ -> PMeta None, None, None in
+ let ind = match ind with Some _ -> ind | None ->
match brs with
| (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
| _ -> None in
- PCase ((sp,Term.RegularStyle),None,
- pat_of_raw metas vars c,
- Array.init (List.length brs)
- (pat_of_raw_branch loc metas vars sp brs))
+ let cbrs =
+ Array.init (List.length brs) (pat_of_raw_branch loc metas vars ind brs)
+ in
+ let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
+ PCase ((RegularStyle,cstr_nargs,ind,ind_nargs), pred,
+ pat_of_raw metas vars c, brs)
+
| r ->
let loc = loc_of_rawconstr r in
user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
@@ -230,12 +285,12 @@ let rec pat_of_raw metas vars = function
and pat_of_raw_branch loc metas vars ind brs i =
let bri = List.filter
(function
- (_,_,[PatCstr(_,c,lv,_)],_) -> snd c = i+1
+ (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
| (loc,_,_,_) ->
user_err_loc (loc,"pattern_of_rawconstr",
Pp.str "Not supported pattern")) brs in
match bri with
- [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
+ | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
if ind <> None & ind <> Some indsp then
user_err_loc (loc,"pattern_of_rawconstr",
Pp.str "All constructors must be in the same inductive type");
@@ -246,8 +301,7 @@ and pat_of_raw_branch loc metas vars ind brs i =
user_err_loc (loc,"pattern_of_rawconstr",
Pp.str "Not supported pattern")) lv in
let vars' = List.rev lna @ vars in
- List.fold_right (fun na b -> PLambda(na,PMeta None,b)) lna
- (pat_of_raw metas vars' br)
+ List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
| _ -> user_err_loc (loc,"pattern_of_rawconstr",
str "No unique branch for " ++ int (i+1) ++
str"-th constructor")
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 0815f87211..4093f5e110 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -39,8 +39,9 @@ type constr_pattern =
| PLetIn of name * constr_pattern * constr_pattern
| PSort of rawsort
| PMeta of patvar option
- | PCase of (inductive option * case_style)
- * constr_pattern option * constr_pattern * constr_pattern array
+ | PIf of constr_pattern * constr_pattern * constr_pattern
+ | PCase of (case_style * int array * inductive option * int option)
+ * constr_pattern * constr_pattern * constr_pattern array
| PFix of fixpoint
| PCoFix of cofixpoint
@@ -76,3 +77,5 @@ val pattern_of_rawconstr : rawconstr ->
val instantiate_pattern :
(identifier * constr_pattern) list -> constr_pattern -> constr_pattern
+
+val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 71c59e4327..8e8b8059f9 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1 +1,4 @@
intro H; split; [ a H | e H ].
+intros; match goal with
+ | |- context [if ?X then _ else _] => case X
+ end; trivial.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 24a33651cd..8fa9199408 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -7,3 +7,12 @@ Lemma test : True -> True /\ True.
intro H; split; [a H|e H].
Show Script.
Qed.
+
+(* Test printing of match context *)
+(* Used to fail after translator removal (see bug #1070) *)
+
+Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
+Proof.
+intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
+Show Script.
+Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 07:05:23 +0000