summaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pattern.ml')
-rw-r--r--pretyping/pattern.ml160
1 files changed, 66 insertions, 94 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f58a12c6..390b884c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: pattern.ml,v 1.24.2.2 2004/11/26 17:51:52 herbelin Exp $ *)
+(* $Id: pattern.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
open Util
open Names
@@ -17,18 +17,13 @@ open Rawterm
open Environ
open Nametab
open Pp
+open Mod_subst
(* Metavariables *)
type patvar_map = (patvar * constr) list
-let patvar_of_int n =
- let p = if !Options.v7 & not (Options.do_translate ()) then "?" else "X"
- in
- Names.id_of_string (p ^ string_of_int n)
let pr_patvar = pr_id
-let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n)
-
(* Patterns *)
type constr_pattern =
@@ -62,57 +57,6 @@ let rec occur_meta_pattern = function
| PMeta _ | PSoApp _ -> true
| PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
-let rec subst_pattern subst pat = match pat with
- | PRef ref ->
- let ref' = subst_global subst ref in
- if ref' == ref then pat else
- PRef ref'
- | PVar _
- | PEvar _
- | PRel _ -> pat
- | PApp (f,args) ->
- let f' = subst_pattern subst f in
- let args' = array_smartmap (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
- if args' == args then pat else
- PSoApp (i,args')
- | PLambda (name,c1,c2) ->
- let c1' = subst_pattern subst c1 in
- let c2' = subst_pattern subst c2 in
- if c1' == c1 && c2' == c2 then pat else
- PLambda (name,c1',c2')
- | PProd (name,c1,c2) ->
- let c1' = subst_pattern subst c1 in
- let c2' = subst_pattern subst c2 in
- if c1' == c1 && c2' == c2 then pat else
- PProd (name,c1',c2')
- | PLetIn (name,c1,c2) ->
- let c1' = subst_pattern subst c1 in
- let c2' = subst_pattern subst c2 in
- if c1' == c1 && c2' == c2 then pat else
- PLetIn (name,c1',c2')
- | PSort _
- | PMeta _ -> pat
- | PCase (cs,typ, c, branches) ->
- let typ' = option_smartmap (subst_pattern subst) typ in
- let c' = subst_pattern subst c in
- let branches' = array_smartmap (subst_pattern subst) branches in
- if typ' == typ && c' == c && branches' == branches then pat else
- PCase(cs,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'
-
type constr_label =
| ConstNode of constant
| IndNode of inductive
@@ -121,33 +65,14 @@ type constr_label =
exception BoundPattern;;
-let label_of_ref = function
- | ConstRef sp -> ConstNode sp
- | IndRef sp -> IndNode sp
- | ConstructRef sp -> CstrNode sp
- | VarRef id -> VarNode id
-
-let ref_of_label = function
- | ConstNode sp -> ConstRef sp
- | IndNode sp -> IndRef sp
- | CstrNode sp -> ConstructRef sp
- | VarNode id -> VarRef id
-
-let subst_label subst cstl =
- let ref = ref_of_label cstl in
- let ref' = subst_global subst ref in
- if ref' == ref then cstl else
- label_of_ref ref'
-
-
let rec head_pattern_bound t =
match t with
| PProd (_,_,b) -> head_pattern_bound b
| PLetIn (_,_,b) -> head_pattern_bound b
| PApp (c,args) -> head_pattern_bound c
| PCase (_,p,c,br) -> head_pattern_bound c
- | PRef r -> label_of_ref r
- | PVar id -> VarNode id
+ | PRef r -> r
+ | PVar id -> VarRef id
| PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _
-> raise BoundPattern
(* Perhaps they were arguments, but we don't beta-reduce *)
@@ -155,10 +80,10 @@ let rec head_pattern_bound t =
| PCoFix _ -> anomaly "head_pattern_bound: not a type"
let head_of_constr_reference c = match kind_of_term c with
- | Const sp -> ConstNode sp
- | Construct sp -> CstrNode sp
- | Ind sp -> IndNode sp
- | Var id -> VarNode id
+ | Const sp -> ConstRef sp
+ | Construct sp -> ConstructRef sp
+ | Ind sp -> IndRef sp
+ | Var id -> VarRef id
| _ -> anomaly "Not a rigid reference"
let rec pattern_of_constr t =
@@ -168,7 +93,7 @@ let rec pattern_of_constr t =
| Var id -> PVar id
| Sort (Prop c) -> PSort (RProp c)
| Sort (Type _) -> PSort (RType None)
- | Cast (c,_) -> pattern_of_constr c
+ | Cast (c,_,_) -> pattern_of_constr c
| LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
| Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b)
| Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
@@ -198,9 +123,61 @@ let rec inst lvar = function
(* Non recursive *)
| (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x
(* Bound to terms *)
- | (PFix _ | PCoFix _ as r) ->
+ | (PFix _ | PCoFix _) ->
error ("Not instantiable pattern")
+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 t
+ | PVar _
+ | PEvar _
+ | PRel _ -> pat
+ | PApp (f,args) ->
+ let f' = subst_pattern subst f in
+ let args' = array_smartmap (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
+ if args' == args then pat else
+ PSoApp (i,args')
+ | PLambda (name,c1,c2) ->
+ let c1' = subst_pattern subst c1 in
+ let c2' = subst_pattern subst c2 in
+ if c1' == c1 && c2' == c2 then pat else
+ PLambda (name,c1',c2')
+ | PProd (name,c1,c2) ->
+ let c1' = subst_pattern subst c1 in
+ let c2' = subst_pattern subst c2 in
+ if c1' == c1 && c2' == c2 then pat else
+ PProd (name,c1',c2')
+ | PLetIn (name,c1,c2) ->
+ let c1' = subst_pattern subst c1 in
+ let c2' = subst_pattern subst c2 in
+ if c1' == c1 && c2' == c2 then pat else
+ PLetIn (name,c1',c2')
+ | PSort _
+ | PMeta _ -> pat
+ | PCase (cs,typ, c, branches) ->
+ let typ' = option_smartmap (subst_pattern subst) typ in
+ let c' = subst_pattern subst c in
+ let branches' = array_smartmap (subst_pattern subst) branches in
+ if typ' == typ && c' == c && branches' == branches then pat else
+ PCase(cs,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 instantiate_pattern = inst
let rec pat_of_raw metas vars = function
@@ -230,30 +207,25 @@ let rec pat_of_raw metas vars = function
PSort s
| RHole _ ->
PMeta None
- | RCast (_,c,t) ->
+ | RCast (_,c,_,t) ->
Options.if_verbose
Pp.warning "Cast not taken into account in constr pattern";
pat_of_raw metas vars c
- | ROrderedCase (_,st,po,c,br,_) ->
- PCase ((None,st),option_app (pat_of_raw metas vars) po,
- pat_of_raw metas vars c,
- Array.map (pat_of_raw metas vars) br)
| 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,(po,_),[c,_],brs) ->
+ | RCases (loc,None,[c,_],brs) ->
let sp =
match brs with
| (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
| _ -> None in
- (* When po disappears: switch to rtn type *)
- PCase ((sp,Term.RegularStyle),option_app (pat_of_raw metas vars) po,
+ 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))
| r ->
let loc = loc_of_rawconstr r in
- user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern")
+ user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
and pat_of_raw_branch loc metas vars ind brs i =
let bri = List.filter
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 22:36:52 +0000