diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 82 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 33 | ||||
| -rw-r--r-- | pretyping/glob_ops.mli | 2 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 8 |
4 files changed, 102 insertions, 23 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 886a982634..daac33f503 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -80,31 +80,70 @@ let add_binders na1 na2 binding_vars (names, terms as subst) = let rec build_lambda vars ctx m = match vars with | [] -> - let len = List.length ctx in - lift (-1 * len) m + if Vars.closed0 m then m else raise PatternMatchingFailure | n :: vars -> (* change [ x1 ... xn y z1 ... zm |- t ] into [ x1 ... xn z1 ... zm |- lam y. t ] *) - let len = List.length ctx in - let init i = - if i < pred n then mkRel (i + 2) - else if Int.equal i (pred n) then mkRel 1 - else mkRel (i + 1) - in - let m = substl (List.init len init) m in let pre, suf = List.chop (pred n) ctx in - match suf with + let (na, t, suf) = match suf with | [] -> assert false - | (_, na, t) :: suf -> - let map i = if i > n then pred i else i in - let vars = List.map map vars in - (** Check that the abstraction is legal *) - let frels = free_rels t in - let brels = List.fold_right Int.Set.add vars Int.Set.empty in - let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in - (** Create the abstraction *) - let m = mkLambda (na, t, m) in - build_lambda vars (pre @ suf) m + | (_, na, t) :: suf -> (na, t, suf) + in + (** Check that the abstraction is legal by generating a transitive closure of + its dependencies. *) + let is_nondep t clear = match clear with + | [] -> true + | _ -> + let rels = free_rels t in + let check i b = b || not (Int.Set.mem i rels) in + List.for_all_i check 1 clear + in + let fold (_, _, t) clear = is_nondep t clear :: clear in + (** Produce a list of booleans: true iff we keep the hypothesis *) + let clear = List.fold_right fold pre [false] in + let clear = List.drop_last clear in + (** If the conclusion depends on a variable we cleared, failure *) + let () = if not (is_nondep m clear) then raise PatternMatchingFailure in + (** Create the abstracted term *) + let fold (k, accu) keep = + if keep then + let k = succ k in + (k, Some k :: accu) + else (k, None :: accu) + in + let keep, shift = List.fold_left fold (0, []) clear in + let shift = List.rev shift in + let map = function + | None -> mkProp (** dummy term *) + | Some i -> mkRel (i + 1) + in + (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *) + let subst = + List.map map shift @ + mkRel 1 :: + List.mapi (fun i _ -> mkRel (i + keep + 2)) suf + in + let map i (id, na, c) = + let i = succ i in + let subst = List.skipn i subst in + let subst = List.map (fun c -> Vars.lift (- i) c) subst in + (id, na, substl subst c) + in + let pre = List.mapi map pre in + let pre = List.filter_with clear pre in + let m = substl subst m in + let map i = + if i > n then i - n + keep + else match List.nth shift (i - 1) with + | None -> + (** We cleared a variable that we wanted to abstract! *) + raise PatternMatchingFailure + | Some k -> k + in + let vars = List.map map vars in + (** Create the abstraction *) + let m = mkLambda (na, Vars.lift keep t, m) in + build_lambda vars (pre @ suf) m let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu @@ -307,6 +346,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when c1 = c2 -> + Array.fold_left2 (sorec ctx env) subst args1 args2 + | _ -> raise PatternMatchingFailure in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818f4..0eda776519 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -559,12 +559,45 @@ let rec cases_pattern_of_glob_constr na = function PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found +open Declarations +open Term +open Context + +(* Keep only patterns which are not bound to a local definitions *) +let drop_local_defs typi args = + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | [], [] -> [] + | Rel.Declaration.LocalDef _ :: decls, pat :: args -> + begin + match pat with + | PatVar (_,Anonymous) -> aux decls args + | _ -> raise Not_found (* The pattern is used, one cannot drop it *) + end + | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) args + +let add_patterns_for_params_remove_local_defs (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + let l = + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in + drop_local_defs typi l in + Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l + (* Turn a closed cases pattern into a glob_constr *) let rec glob_constr_of_closed_cases_pattern_aux = function | PatCstr (loc,cstr,[],Anonymous) -> GRef (loc,ConstructRef cstr,None) | PatCstr (loc,cstr,l,Anonymous) -> let ref = GRef (loc,ConstructRef cstr,None) in + let l = add_patterns_for_params_remove_local_defs cstr l in GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533f..6b8f131f41 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -76,3 +76,5 @@ val map_pattern : (glob_constr -> glob_constr) -> val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr + +val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 2090aad8a0..79e9c727d7 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,7 +160,9 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in @@ -358,9 +360,9 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = + let mkGLambda na c = GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; |