aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/matching.ml110
-rw-r--r--pretyping/matching.mli13
-rw-r--r--pretyping/pattern.ml42
-rw-r--r--pretyping/pattern.mli48
-rw-r--r--pretyping/pretyping.ml33
-rw-r--r--pretyping/pretyping.mli21
6 files changed, 197 insertions, 70 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 2c0285ed24..ddfe5dd076 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -46,9 +46,10 @@ type bound_ident_map = (identifier * identifier) list
exception PatternMatchingFailure
-let constrain (n,m) (names,terms as subst) =
+let constrain (n,(ids,m as x)) (names,terms as subst) =
try
- if eq_constr m (List.assoc n terms) then subst
+ let (ids',m') = List.assoc n terms in
+ if ids = ids' && eq_constr m m' then subst
else raise PatternMatchingFailure
with
Not_found ->
@@ -56,7 +57,7 @@ let constrain (n,m) (names,terms as subst) =
Flags.if_verbose Pp.warning
("Collision between bound variable "^string_of_id n^
" and a metavariable of same name.");
- (names,(n,m)::terms)
+ (names,(n,x)::terms)
let add_binders na1 na2 (names,terms as subst) =
match na1, na2 with
@@ -76,7 +77,7 @@ let add_binders na1 na2 (names,terms as subst) =
let build_lambda toabstract stk (m : constr) =
let rec buildrec m p_0 p_1 = match p_0,p_1 with
| (_, []) -> m
- | (n, (na,t)::tl) ->
+ | (n, (_,na,t)::tl) ->
if List.mem n toabstract then
buildrec (mkLambda (na,t,m)) (n+1) tl
else
@@ -96,7 +97,58 @@ let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
| Some ind -> ind = ci2.ci_ind
| None -> cs1 = ci2.ci_cstr_ndecls
-let matches_core convert allow_partial_app pat c =
+let rec list_insert f a = function
+ | [] -> [a]
+ | b::l when f a b -> a::b::l
+ | b::l when a = b -> raise PatternMatchingFailure
+ | b::l -> b :: list_insert f a l
+
+let extract_bound_vars =
+ let rec aux k = function
+ | ([],_) -> []
+ | (n::l,(na1,na2,_)::stk) when k = n ->
+ begin match na1,na2 with
+ | Name id1,Name _ -> list_insert (<) id1 (aux (k+1) (l,stk))
+ | Name _,Anonymous -> anomaly "Unnamed bound variable"
+ | Anonymous,_ -> raise PatternMatchingFailure
+ end
+ | (l,_::stk) -> aux (k+1) (l,stk)
+ | (_,[]) -> assert false
+ in aux 1
+
+let dummy_constr = mkProp
+
+let rec make_renaming ids = function
+ | (Name id,Name _,_)::stk ->
+ let renaming = make_renaming ids stk in
+ (try mkRel (list_index id ids) :: renaming
+ with Not_found -> dummy_constr :: renaming)
+ | (_,_,_)::stk ->
+ dummy_constr :: make_renaming ids stk
+ | [] ->
+ []
+
+let merge_binding allow_bound_rels stk n cT subst =
+ let depth = List.length stk in
+ let c =
+ if depth = 0 then
+ (* Optimization *)
+ ([],cT)
+ else
+ let frels = Intset.elements (free_rels cT) in
+ let frels = List.filter (fun i -> i <= depth) frels in
+ if allow_bound_rels then
+ let frels = Sort.list (<) frels in
+ let canonically_ordered_vars = extract_bound_vars (frels,stk) in
+ let renaming = make_renaming canonically_ordered_vars stk in
+ (canonically_ordered_vars, substl renaming cT)
+ else if frels = [] then
+ ([],lift (-depth) cT)
+ else
+ raise PatternMatchingFailure in
+ constrain (n,c) subst
+
+let matches_core convert allow_partial_app allow_bound_rels pat c =
let conv = match convert with
| None -> eq_constr
| Some (env,sigma) -> is_conv env sigma in
@@ -112,21 +164,11 @@ let matches_core convert allow_partial_app pat c =
args in
let frels = Intset.elements (free_rels cT) in
if list_subset frels relargs then
- constrain (n,build_lambda relargs stk cT) subst
+ constrain (n,([],build_lambda relargs stk cT)) subst
else
raise PatternMatchingFailure
- | PMeta (Some n), m ->
- let depth = List.length stk in
- if depth = 0 then
- (* Optimisation *)
- constrain (n,cT) subst
- else
- let frels = Intset.elements (free_rels cT) in
- if List.for_all (fun i -> i > depth) frels then
- constrain (n,lift (-depth) cT) subst
- else
- raise PatternMatchingFailure
+ | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst
| PMeta None, m -> subst
@@ -151,14 +193,8 @@ let matches_core convert allow_partial_app pat c =
let p = Array.length args2 - Array.length args1 in
if p>=0 then
let args21, args22 = array_chop p args2 in
- let subst =
- let depth = List.length stk in
- let c = mkApp(c2,args21) in
- let frels = Intset.elements (free_rels c) in
- if List.for_all (fun i -> i > depth) frels then
- constrain (n,lift (-depth) c) subst
- else
- raise PatternMatchingFailure in
+ let c = mkApp(c2,args21) in
+ let subst = merge_binding allow_bound_rels stk n c subst in
array_fold_left2 (sorec stk) subst args1 args22
else raise PatternMatchingFailure
@@ -167,15 +203,15 @@ let matches_core convert allow_partial_app pat c =
with Invalid_argument _ -> raise PatternMatchingFailure)
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
- sorec ((na2,c2)::stk)
+ sorec ((na1,na2,c2)::stk)
(add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
- sorec ((na2,c2)::stk)
+ sorec ((na1,na2,c2)::stk)
(add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
- sorec ((na2,t2)::stk)
+ sorec ((na1,na2,t2)::stk)
(add_binders na1 na2 (sorec stk subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
@@ -184,8 +220,10 @@ let matches_core convert allow_partial_app pat c =
let n = rel_context_length ctx in
let n' = rel_context_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 s =
+ List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in
+ let s' =
+ List.fold_left (fun l (na,_,t) -> (Anonymous,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 subst a1 a2) b1 b2) b1' b2'
else
@@ -206,16 +244,20 @@ let matches_core convert allow_partial_app pat c =
let names,terms = sorec [] ([],[]) pat c in
(names,Sort.list (fun (a,_) (b,_) -> a<b) terms)
-let extended_matches = matches_core None true
+let matches_core_closed convert allow_partial_app pat c =
+ let names,subst = matches_core convert allow_partial_app false pat c in
+ (names, List.map (fun (a,(_,b)) -> (a,b)) subst)
+
+let extended_matches = matches_core None true true
-let matches c p = snd (matches_core None true c p)
+let matches c p = snd (matches_core_closed None true c p)
let special_meta = (-1)
(* Tells if it is an authorized occurrence and if the instance is closed *)
let authorized_occ partial_app closed pat c mk_ctx next =
try
- let sigma = matches_core None partial_app pat c in
+ let sigma = matches_core_closed None partial_app pat c in
if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
then next ()
else sigma, mk_ctx (mkMeta special_meta), next
@@ -308,7 +350,7 @@ let is_matching_appsubterm ?(closed=true) pat c =
with PatternMatchingFailure -> false
let matches_conv env sigma c p =
- snd (matches_core (Some (env,sigma)) false c p)
+ snd (matches_core_closed (Some (env,sigma)) false c p)
let is_matching_conv env sigma pat n =
try let _ = matches_conv env sigma pat n in true
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 95314054e5..eb9c8fc8c6 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -6,18 +6,25 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+(** This module implements pattern-matching on terms *)
+
open Names
open Term
open Environ
open Pattern
open Termops
-(** {6 This modules implements pattern-matching on terms } *)
-
+(** [PatternMatchingFailure] is the exception raised when pattern
+ matching fails *)
exception PatternMatchingFailure
+(** [special_meta] is the default name of the meta holding the
+ surrounding context in subterm matching *)
val special_meta : metavariable
+(** [bound_ident_map] represents the result of matching binding
+ identifiers of the pattern with the binding identifiers of the term
+ matched *)
type bound_ident_map = (identifier * identifier) list
(** [matches pat c] matches [c] against [pat] and returns the resulting
@@ -31,7 +38,7 @@ val matches : constr_pattern -> constr -> patvar_map
variables or metavariables have the same name, the metavariable,
or else the rightmost bound variable, takes precedence *)
val extended_matches :
- constr_pattern -> constr -> bound_ident_map * patvar_map
+ constr_pattern -> constr -> bound_ident_map * extended_patvar_map
(** [is_matching pat c] just tells if [c] matches against [pat] *)
val is_matching : constr_pattern -> constr -> bool
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 48218f47f2..59f3cde88a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -19,8 +19,10 @@ open Mod_subst
(* Metavariables *)
+type constr_under_binders = identifier list * constr
+
type patvar_map = (patvar * constr) list
-let pr_patvar = pr_id
+type extended_patvar_map = (patvar * constr_under_binders) list
(* Patterns *)
@@ -143,9 +145,9 @@ let pattern_of_constr sigma t =
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)
+ | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
+ | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
+ | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n 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 *)
@@ -153,18 +155,40 @@ let map_pattern_with_binders g f l = function
(* Bound to terms *)
| PFix _ | PCoFix _ as x) -> x
-let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
+let map_pattern f = map_pattern_with_binders (fun _ () -> ()) (fun () -> f) ()
+
+let error_instantiate_pattern id l =
+ let is = if List.length l = 1 then "is" else "are" in
+ errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+ ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
+ ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
-let rec instantiate_pattern lvar = function
- | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x)
+let instantiate_pattern lvar c =
+ let rec aux vars = function
+ | PVar id as x ->
+ (try
+ let ctx,c = List.assoc id lvar in
+ try
+ let inst =
+ List.map (fun id -> mkRel (list_index (Name id) vars)) ctx in
+ let c = substl inst c in
+ snd (pattern_of_constr Evd.empty c)
+ with Not_found (* list_index failed *) ->
+ let vars =
+ list_map_filter (function Name id -> Some id | _ -> None) vars in
+ error_instantiate_pattern id (list_subtract ctx vars)
+ with Not_found (* List.assoc failed *) ->
+ x)
| (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
- | c -> map_pattern (instantiate_pattern lvar) c
+ | 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 succ (liftn_pattern k) n c
+ | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
let lift_pattern k = liftn_pattern k 1
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index d805730e97..3b61c1e437 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -6,6 +6,9 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+(** This module defines the type of pattern used for pattern-matching
+ terms in tatics *)
+
open Pp
open Names
open Sign
@@ -16,12 +19,46 @@ open Nametab
open Rawterm
open Mod_subst
-(** Pattern variables *)
+(** {5 Maps of pattern variables} *)
+
+(** Type [constr_under_binders] is for representing the term resulting
+ of a matching. Matching can return terms defined in a some context
+ of named binders; in the context, variable names are ordered by
+ (<) and referred to by index in the term Thanks to the canonical
+ ordering, a matching problem like
+
+ [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]]
+
+ will be accepted. Thanks to the reference by index, a matching
+ problem like
+
+ [match ... with [(fun x => ?p)] => [forall x => p]]
+
+ will work even if [x] is also the name of an existing goal
+ variable.
+
+ Note: we do not keep types in the signature. Besides simplicity,
+ the main reason is that it would force to close the signature over
+ binders that occur only in the types of effective binders but not
+ in the term itself (e.g. for a term [f x] with [f:A -> True] and
+ [x:A]).
+
+ On the opposite side, by not keeping the types, we loose
+ opportunity to propagate type informations which otherwise would
+ not be inferable, as e.g. when matching [forall x, x = 0] with
+ pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in
+ expression [forall x, h = x] where nothing tells how the type of x
+ could be inferred. We also loose the ability of typing ltac
+ variables before calling the right-hand-side of ltac matching clauses. *)
+
+type constr_under_binders = identifier list * constr
+
+(** Types of substitutions with or w/o bound variables *)
type patvar_map = (patvar * constr) list
-val pr_patvar : patvar -> std_ppcmds
+type extended_patvar_map = (patvar * constr_under_binders) list
-(** Patterns *)
+(** {5 Patterns} *)
type constr_pattern =
| PRef of global_reference
@@ -41,6 +78,8 @@ type constr_pattern =
| PFix of fixpoint
| PCoFix of cofixpoint
+(** {5 Functions on patterns} *)
+
val occur_meta_pattern : constr_pattern -> bool
val subst_pattern : substitution -> constr_pattern -> constr_pattern
@@ -72,6 +111,7 @@ val pattern_of_rawconstr : rawconstr ->
patvar list * constr_pattern
val instantiate_pattern :
- (identifier * constr_pattern Lazy.t) list -> constr_pattern -> constr_pattern
+ (identifier * (identifier list * constr)) list ->
+ constr_pattern -> constr_pattern
val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 71a21f6c88..e63b9a234f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,8 +45,10 @@ open Evarconv
open Pattern
type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * constr_under_binders) list
type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
(************************************************************************)
(* This concerns Cases *)
@@ -131,7 +133,7 @@ sig
*)
val understand_ltac :
- bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+ bool -> evar_map -> env -> ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
(* Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -162,18 +164,15 @@ sig
*)
val pretype :
type_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_judgment
+ ltac_var_map -> rawconstr -> unsafe_judgment
val pretype_type :
val_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_type_judgment
+ ltac_var_map -> rawconstr -> unsafe_type_judgment
val pretype_gen :
bool -> bool -> bool -> evar_map ref -> env ->
- var_map * (identifier * identifier option) list ->
- typing_constraint -> rawconstr -> constr
+ ltac_var_map -> typing_constraint -> rawconstr -> constr
(*i*)
end
@@ -225,7 +224,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
let check_branches_message loc env evdref c (explft,lft) =
for i = 0 to Array.length explft - 1 do
if not (e_cumul env evdref lft.(i) explft.(i)) then
- let sigma = !evdref in
+ let sigma = !evdref in
error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
done
@@ -243,7 +242,14 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| Anonymous -> name'
| _ -> name
- let pretype_id loc env (lvar,unbndltacvars) id =
+ let invert_ltac_bound_name env id0 id =
+ try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+ with Not_found ->
+ errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+ str " depends on pattern variable name " ++ pr_id id ++
+ str " which is not bound in current context.")
+
+ let pretype_id loc env sigma (lvar,unbndltacvars) id =
(* Look for the binder of [id] *)
try
let (n,_,typ) = lookup_rel_id id (rel_context env) in
@@ -251,7 +257,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
with Not_found ->
(* Check if [id] is an ltac variable *)
try
- List.assoc id lvar
+ let (ids,c) = List.assoc id lvar in
+ let subst = List.map (invert_ltac_bound_name env id) ids in
+ let c = substl subst c in
+ { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
with Not_found ->
(* Check if [id] is a section or goal variable *)
try
@@ -295,7 +304,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
| RVar (loc, id) ->
inh_conv_coerce_to_tycon loc env evdref
- (pretype_id loc env lvar id)
+ (pretype_id loc env !evdref lvar id)
tycon
| REvar (loc, evk, instopt) ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 18a6b03a71..00eb613abc 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -6,6 +6,12 @@
* GNU Lesser General Public License Version 2.1
***********************************************************************)
+(** This file implements type inference. It maps [rawconstr]
+ (i.e. untyped terms whose names are located) to [constr]. In
+ particular, it drives complex pattern-matching problems ("match")
+ into elementary ones, insertion of coercions and resolution of
+ implicit arguments. *)
+
open Names
open Sign
open Term
@@ -21,8 +27,10 @@ val search_guard :
type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * unsafe_judgment) list
+type var_map = (identifier * Pattern.constr_under_binders) list
type unbound_ltac_var_map = (identifier * identifier option) list
+type ltac_var_map = var_map * unbound_ltac_var_map
+type rawconstr_ltac_closure = ltac_var_map * rawconstr
module type S =
sig
@@ -56,7 +64,7 @@ sig
*)
val understand_ltac :
- bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
+ bool -> evar_map -> env -> ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
(** Standard call to get a constr from a rawconstr, resolving implicit args *)
@@ -84,18 +92,15 @@ sig
(** Internal of Pretyping... *)
val pretype :
type_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_judgment
+ ltac_var_map -> rawconstr -> unsafe_judgment
val pretype_type :
val_constraint -> env -> evar_map ref ->
- var_map * (identifier * identifier option) list ->
- rawconstr -> unsafe_type_judgment
+ ltac_var_map -> rawconstr -> unsafe_type_judgment
val pretype_gen :
bool -> bool -> bool -> evar_map ref -> env ->
- var_map * (identifier * identifier option) list ->
- typing_constraint -> rawconstr -> constr
+ ltac_var_map -> typing_constraint -> rawconstr -> constr
(**/**)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 03:15:16 +0000