(**************************************************************)
(* Copyright Dominique Larchey-Wendling * *)
(* *)
(* * Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import List.
Ltac lrev l :=
let rec loop aa ll :=
match ll with
| ?x::?ll => loop (x::aa) ll
| nil => constr:(aa)
end
in match type of l with
| list ?t => loop (@nil t) l
end.
Ltac lflat l :=
let rec loop aa ll :=
match ll with
| ?ss++?rr => let bb := loop aa ss in
let cc := loop bb rr
in constr:(cc)
| ?x::?rr => let bb := loop ((x::nil)::aa) rr
in constr:(bb)
| nil => constr:(aa)
| ?ss => constr:(ss::aa)
end
in match type of l with
| list ?t => let r1 := loop (@nil (list t)) l
in lrev r1
end.
Ltac llin l :=
let rec loop aa ll :=
match ll with
| (?x::nil)::?ll => let bb := loop (x::aa) ll
in constr:(bb)
| ?lx::?ll => let bb := loop (lx++aa) ll
in constr:(bb)
| nil => constr:(aa)
end
in match type of l with
| list (list ?t) =>
match lrev l with
| ?lx::?rr => let bb := loop lx rr
in constr:(bb)
| nil => constr:(@nil t)
end
end.
Ltac lcut x l :=
let rec loop aa x ll :=
match ll with
| x::_ => let bb := lrev aa
in constr:(bb++ll)
| ?lz::?rr => let bb := loop (lz::aa) x rr
in constr:(bb)
end
in match type of l with
| list (list ?t) => loop (@nil (list t)) x l
end.
Ltac lmerge l :=
match l with
| ?aa++?ll => let bb := llin aa in
let cc := llin ll
in constr:(bb++cc)
end.
Ltac focus_lst z r0 :=
let r1 := lflat r0 in
let r2 := lcut z r1 in
let r3 := lmerge r2
in constr:(r3).
Ltac focus_lst_2 z r0 :=
let r1 := focus_lst z r0 in
let r2 := match r1 with
| ?l++?x::?r =>
let r3 := focus_lst z r in
match r3 with
| ?m++?y::?n => constr:((l++x::m)++y::n)
end
end
in constr:(r2).
Ltac focus_lst_3 z r0 :=
let r1 := focus_lst_2 z r0 in
let r2 := match r1 with
| ?l++?x::?r =>
let r3 := focus_lst z r in
match r3 with
| ?m++?y::?n => constr:((l++x::m)++y::n)
end
end
in constr:(r2).
Ltac focus_elt z l := focus_lst (z::nil) l.
Section test.
Variable X : Type.
Variable x y z : list X.
Variable a b c : X.
(*
Goal True.
let rr := lrev (1::2::3::4::nil) in idtac rr.
let rr := lflat ((x++a::nil++nil)++b::z++y++a::nil) in idtac rr.
let rr := llin (x::y::(a::nil)::z::(b::nil)::nil) in idtac rr.
let rr := llin (@nil (list X)) in idtac rr.
let rr := llin (@nil (list X)) in idtac rr.
let rr := lcut z ( (x::y::(a::nil)::y::(b::nil)::z::nil) ) in idtac rr.
let rr := lmerge ( (x::y::(a::nil)::nil)++(y::(b::nil)::z::nil) ) in idtac rr.
let rr := focus_lst_2 (c::nil) ((x++c::nil++nil)++b::z++y++c::nil) in idtac rr.
let rr := focus_lst_2 (c::nil) ((x++c::nil++nil)++b::z++y++c::z++c::x++c::z) in idtac rr.
let rr := focus_lst z ((x++a::nil++nil)++b::z++y++c::nil) in idtac rr.
let rr := focus_elt a (c::(x++a::nil++nil)++b::z++y++c::nil) in idtac rr.
auto.
Qed.
*)
End test.
(* Copyright Dominique Larchey-Wendling * *)
(* *)
(* * Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(**************************************************************)
Require Import List.
Ltac lrev l :=
let rec loop aa ll :=
match ll with
| ?x::?ll => loop (x::aa) ll
| nil => constr:(aa)
end
in match type of l with
| list ?t => loop (@nil t) l
end.
Ltac lflat l :=
let rec loop aa ll :=
match ll with
| ?ss++?rr => let bb := loop aa ss in
let cc := loop bb rr
in constr:(cc)
| ?x::?rr => let bb := loop ((x::nil)::aa) rr
in constr:(bb)
| nil => constr:(aa)
| ?ss => constr:(ss::aa)
end
in match type of l with
| list ?t => let r1 := loop (@nil (list t)) l
in lrev r1
end.
Ltac llin l :=
let rec loop aa ll :=
match ll with
| (?x::nil)::?ll => let bb := loop (x::aa) ll
in constr:(bb)
| ?lx::?ll => let bb := loop (lx++aa) ll
in constr:(bb)
| nil => constr:(aa)
end
in match type of l with
| list (list ?t) =>
match lrev l with
| ?lx::?rr => let bb := loop lx rr
in constr:(bb)
| nil => constr:(@nil t)
end
end.
Ltac lcut x l :=
let rec loop aa x ll :=
match ll with
| x::_ => let bb := lrev aa
in constr:(bb++ll)
| ?lz::?rr => let bb := loop (lz::aa) x rr
in constr:(bb)
end
in match type of l with
| list (list ?t) => loop (@nil (list t)) x l
end.
Ltac lmerge l :=
match l with
| ?aa++?ll => let bb := llin aa in
let cc := llin ll
in constr:(bb++cc)
end.
Ltac focus_lst z r0 :=
let r1 := lflat r0 in
let r2 := lcut z r1 in
let r3 := lmerge r2
in constr:(r3).
Ltac focus_lst_2 z r0 :=
let r1 := focus_lst z r0 in
let r2 := match r1 with
| ?l++?x::?r =>
let r3 := focus_lst z r in
match r3 with
| ?m++?y::?n => constr:((l++x::m)++y::n)
end
end
in constr:(r2).
Ltac focus_lst_3 z r0 :=
let r1 := focus_lst_2 z r0 in
let r2 := match r1 with
| ?l++?x::?r =>
let r3 := focus_lst z r in
match r3 with
| ?m++?y::?n => constr:((l++x::m)++y::n)
end
end
in constr:(r2).
Ltac focus_elt z l := focus_lst (z::nil) l.
Section test.
Variable X : Type.
Variable x y z : list X.
Variable a b c : X.
(*
Goal True.
let rr := lrev (1::2::3::4::nil) in idtac rr.
let rr := lflat ((x++a::nil++nil)++b::z++y++a::nil) in idtac rr.
let rr := llin (x::y::(a::nil)::z::(b::nil)::nil) in idtac rr.
let rr := llin (@nil (list X)) in idtac rr.
let rr := llin (@nil (list X)) in idtac rr.
let rr := lcut z ( (x::y::(a::nil)::y::(b::nil)::z::nil) ) in idtac rr.
let rr := lmerge ( (x::y::(a::nil)::nil)++(y::(b::nil)::z::nil) ) in idtac rr.
let rr := focus_lst_2 (c::nil) ((x++c::nil++nil)++b::z++y++c::nil) in idtac rr.
let rr := focus_lst_2 (c::nil) ((x++c::nil++nil)++b::z++y++c::z++c::x++c::z) in idtac rr.
let rr := focus_lst z ((x++a::nil++nil)++b::z++y++c::nil) in idtac rr.
let rr := focus_elt a (c::(x++a::nil++nil)++b::z++y++c::nil) in idtac rr.
auto.
Qed.
*)
End test.