diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-15 22:51:20 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-20 15:39:53 +0200 |
commit | 1fb4d1ef961f056e3575c5e034cace85f2340509 (patch) | |
tree | 1ee7b34b2f30d9076c304476b532a1c4ac86060a /pretyping/constr_matching.ml | |
parent | 59b0041147a9d2dddc1fe14f624a2cf5695f2ea2 (diff) |
Fix bug #5377: @? patterns broken.
Diffstat (limited to 'pretyping/constr_matching.ml')
-rw-r--r-- | pretyping/constr_matching.ml | 78 |
1 files changed, 59 insertions, 19 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 886a98263..3c47cfdc4 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -80,31 +80,71 @@ 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 |