summaryrefslogtreecommitdiff
path: root/pretyping/patternops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/patternops.ml')
-rw-r--r--pretyping/patternops.ml169
1 files changed, 108 insertions, 61 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c9925087..3c1c4700 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -15,11 +15,9 @@ open Globnames
open Nameops
open Term
open Constr
-open Vars
open Glob_term
open Pp
open Mod_subst
-open Misctypes
open Decl_kinds
open Pattern
open Environ
@@ -31,7 +29,7 @@ let case_info_pattern_eq i1 i2 =
i1.cip_extensible == i2.cip_extensible
let rec constr_pattern_eq p1 p2 = match p1, p2 with
-| PRef r1, PRef r2 -> eq_gr r1 r2
+| PRef r1, PRef r2 -> GlobRef.equal r1 r2
| PVar v1, PVar v2 -> Id.equal v1 v2
| PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
Evar.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
@@ -48,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
| PIf (t1, l1, r1), PIf (t2, l2, r2) ->
constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
@@ -57,10 +55,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
constr_pattern_eq p1 p2 &&
constr_pattern_eq r1 r2 &&
List.equal pattern_eq l1 l2
-| PFix f1, PFix f2 ->
- fixpoint_eq f1 f2
-| PCoFix f1, PCoFix f2 ->
- cofixpoint_eq f1 f2
+| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) ->
+ Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2
+| PCoFix (i1,f1), PCoFix (i2,f2) ->
+ Int.equal i1 i2 && rec_declaration_eq f1 f2
| PProj (p1, t1), PProj (p2, t2) ->
Projection.equal p1 p2 && constr_pattern_eq t1 t2
| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
@@ -71,19 +69,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
and pattern_eq (i1, j1, p1) (i2, j2, p2) =
Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
-and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
- Int.equal i1 i2 &&
- Array.equal Int.equal arg1 arg2 &&
- rec_declaration_eq r1 r2
-
-and cofixpoint_eq (i1, r1) (i2, r2) =
- Int.equal i1 i2 &&
- rec_declaration_eq r1 r2
-
and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
Array.equal Name.equal n1 n2 &&
- Array.equal Constr.equal c1 c2 &&
- Array.equal Constr.equal r1 r2
+ Array.equal constr_pattern_eq c1 c2 &&
+ Array.equal constr_pattern_eq r1 r2
let rec occur_meta_pattern = function
| PApp (f,args) ->
@@ -123,8 +112,10 @@ let rec occurn_pattern n = function
| PMeta _ | PSoApp _ -> true
| PEvar (_,args) -> Array.exists (occurn_pattern n) args
| PVar _ | PRef _ | PSort _ -> false
- | PFix fix -> not (noccurn n (mkFix fix))
- | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+ | PFix (_,(_,tl,bl)) ->
+ Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
+ | PCoFix (_,(_,tl,bl)) ->
+ Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
let noccurn_pattern n c = not (occurn_pattern n c)
@@ -139,8 +130,7 @@ let rec head_pattern_bound t =
| PCase (_,p,c,br) -> head_pattern_bound c
| PRef r -> r
| PVar id -> VarRef id
- | PProj (p,c) -> ConstRef (Projection.constant p)
- | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _
+ | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _
-> raise BoundPattern
(* Perhaps they were arguments, but we don't beta-reduce *)
| PLambda _ -> raise BoundPattern
@@ -160,8 +150,8 @@ let pattern_of_constr env sigma t =
| Rel n -> PRel n
| Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
| Var id -> PVar id
- | Sort (Prop Null) -> PSort GProp
- | Sort (Prop Pos) -> PSort GSet
+ | Sort Prop -> PSort GProp
+ | Sort Set -> PSort GSet
| Sort (Type _) -> PSort (GType [])
| Cast (c,_,_) -> pattern_of_constr env c
| LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
@@ -193,7 +183,7 @@ let pattern_of_constr env sigma t =
| Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
(* These are the two evar kinds used for existing goals *)
(* see Proofview.mark_in_evm *)
- if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
+ if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev)
else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
| Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
@@ -210,8 +200,16 @@ let pattern_of_constr env sigma t =
in
PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
Array.to_list (Array.mapi branch_of_constr br))
- | Fix f -> PFix f
- | CoFix f -> PCoFix f in
+ | Fix (lni,(lna,tl,bl)) ->
+ let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+ let env' = Array.fold_left2 push env lna tl in
+ PFix (lni,(lna,Array.map (pattern_of_constr env) tl,
+ Array.map (pattern_of_constr env') bl))
+ | CoFix (ln,(lna,tl,bl)) ->
+ let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+ let env' = Array.fold_left2 push env lna tl in
+ PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl,
+ Array.map (pattern_of_constr env') bl)) in
pattern_of_constr env t
(* To process patterns, we need a translation without typing at all. *)
@@ -226,10 +224,14 @@ let map_pattern_with_binders g f l = function
| PCase (ci,po,p,pl) ->
PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
| PProj (p,pc) -> PProj (p, f l pc)
+ | PFix (lni,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl))
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
(* Non recursive *)
- | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _
- (* Bound to terms *)
- | PFix _ | PCoFix _ as x) -> x
+ | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x
let error_instantiate_pattern id l =
let is = match l with
@@ -263,15 +265,12 @@ let instantiate_pattern env sigma lvar c =
error_instantiate_pattern id (List.subtract Id.equal ctx vars)
with Not_found (* Map.find failed *) ->
x)
- | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
| c ->
map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
aux [] 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 (fun _ -> succ) (liftn_pattern k) n c
let lift_pattern k = liftn_pattern k 1
@@ -279,25 +278,26 @@ let lift_pattern k = liftn_pattern k 1
let rec subst_pattern subst pat =
match pat with
| PRef ref ->
- let ref',t = subst_global subst ref in
- if ref' == ref then pat else
- pattern_of_constr (Global.env()) Evd.empty t
+ let ref',t = subst_global subst ref in
+ if ref' == ref then pat else
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ pattern_of_constr env evd t
| PVar _
| PEvar _
| PRel _ -> pat
| PProj (p,c) ->
- let p' = Projection.map (fun p ->
- destConstRef (fst (subst_global subst (ConstRef p)))) p in
+ let p' = Projection.map (subst_mind subst) p in
let c' = subst_pattern subst c in
if p' == p && c' == c then pat else
PProj(p',c')
| PApp (f,args) ->
let f' = subst_pattern subst f in
- let args' = Array.smartmap (subst_pattern subst) args in
+ let args' = Array.Smart.map (subst_pattern subst) args in
if f' == f && args' == args then pat else
PApp (f',args')
| PSoApp (i,args) ->
- let args' = List.smartmap (subst_pattern subst) args in
+ let args' = List.Smart.map (subst_pattern subst) args in
if args' == args then pat else
PSoApp (i,args')
| PLambda (name,c1,c2) ->
@@ -312,7 +312,7 @@ let rec subst_pattern subst pat =
PProd (name,c1',c2')
| PLetIn (name,c1,t,c2) ->
let c1' = subst_pattern subst c1 in
- let t' = Option.smartmap (subst_pattern subst) t in
+ let t' = Option.Smart.map (subst_pattern subst) t in
let c2' = subst_pattern subst c2 in
if c1' == c1 && t' == t && c2' == c2 then pat else
PLetIn (name,c1',t',c2')
@@ -326,7 +326,7 @@ let rec subst_pattern subst pat =
PIf (c',c1',c2')
| PCase (cip,typ,c,branches) ->
let ind = cip.cip_ind in
- let ind' = Option.smartmap (subst_ind subst) ind in
+ let ind' = Option.Smart.map (subst_ind subst) ind in
let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
let typ' = subst_pattern subst typ in
let c' = subst_pattern subst c in
@@ -334,23 +334,39 @@ let rec subst_pattern subst pat =
let c' = subst_pattern subst c in
if c' == c then br else (i,n,c')
in
- let branches' = List.smartmap subst_branch branches in
+ let branches' = List.Smart.map subst_branch branches in
if cip' == cip && typ' == typ && c' == c && branches' == branches
then pat
else PCase(cip', typ', c', branches')
- | PFix fixpoint ->
- let cstr = mkFix fixpoint in
- let fixpoint' = destFix (subst_mps subst cstr) in
- if fixpoint' == fixpoint then pat else
- PFix fixpoint'
- | PCoFix cofixpoint ->
- let cstr = mkCoFix cofixpoint in
- let cofixpoint' = destCoFix (subst_mps subst cstr) in
- if cofixpoint' == cofixpoint then pat else
- PCoFix cofixpoint'
-
-let mkPLambda na b = PLambda(na,PMeta None,b)
-let rev_it_mkPLambda = List.fold_right mkPLambda
+ | PFix (lni,(lna,tl,bl)) ->
+ let tl' = Array.Smart.map (subst_pattern subst) tl in
+ let bl' = Array.Smart.map (subst_pattern subst) bl in
+ if bl' == bl && tl' == tl then pat
+ else PFix (lni,(lna,tl',bl'))
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let tl' = Array.Smart.map (subst_pattern subst) tl in
+ let bl' = Array.Smart.map (subst_pattern subst) bl in
+ if bl' == bl && tl' == tl then pat
+ else PCoFix (ln,(lna,tl',bl'))
+
+let mkPLetIn na b t c = PLetIn(na,b,t,c)
+let mkPProd na t u = PProd(na,t,u)
+let mkPLambda na t b = PLambda(na,t,b)
+let mkPLambdaUntyped na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped
+
+let mkPProd_or_LetIn (na,_,bo,t) c =
+ match bo with
+ | None -> mkPProd na t c
+ | Some b -> mkPLetIn na b (Some t) c
+
+let mkPLambda_or_LetIn (na,_,bo,t) c =
+ match bo with
+ | None -> mkPLambda na t c
+ | Some b -> mkPLetIn na b (Some t) c
+
+let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c)
+let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c)
let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp
@@ -400,7 +416,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
pat_of_raw metas vars b1,pat_of_raw metas vars b2)
| GLetTuple (nal,(_,None),b,c) ->
let mkGLambda na c = DAst.make ?loc @@
- GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+ GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
let c = List.fold_right mkGLambda nal c in
let cip =
{ cip_style = LetStyle;
@@ -429,7 +445,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
let pred = match p,indnames with
| Some p, Some {CAst.v=(_,nal)} ->
let nvars = na :: List.rev nal @ vars in
- rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
+ rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p))
| None, _ -> PMeta None
| Some p, None ->
match DAst.get p with
@@ -448,9 +464,40 @@ 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)
- | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+ | GRec (GFix (ln,n), ids, decls, tl, cl) ->
+ if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
+ err ?loc (Pp.str "\"struct\" annotation is expected.")
+ else
+ let ln = Array.map (fst %> Option.get) ln in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+ let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+ let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+ let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+ let names = Array.map (fun id -> Name id) ids in
+ PFix ((ln,n), (names, tl, cl))
+
+ | GRec (GCoFix n, ids, decls, tl, cl) ->
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+ let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+ let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+ let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+ let names = Array.map (fun id -> Name id) ids in
+ PCoFix (n, (names, tl, cl))
+
+ | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
err ?loc (Pp.str "Non supported pattern."))
+and pat_of_glob_in_context metas vars decls c =
+ let rec aux acc vars = function
+ | (na,bk,b,t) :: decls ->
+ let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in
+ aux (decl::acc) (na::vars) decls
+ | [] ->
+ acc, pat_of_raw metas vars c
+ in aux [] vars decls
+
and pats_of_glob_branches loc metas vars ind brs =
let get_arg p = match DAst.get p with
| PatVar na ->
@@ -475,7 +522,7 @@ and pats_of_glob_branches loc metas vars ind brs =
(str "No unique branch for " ++ int j ++ str"-th constructor.");
let lna = List.map get_arg lv in
let vars' = List.rev lna @ vars in
- let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
+ let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in
let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
ext, ((j-1, tags, pat) :: pats)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 03:20:56 +0000