Library CFML.Stdlib.Array_ml
Set Implicit Arguments.
Require Coq.ZArith.BinInt TLC.LibLogic TLC.LibRelation TLC.LibInt TLC.LibListZ CFML.Shared CFML.CFHeaps CFML.CFApp CFML.CFPrint CFML.CFBuiltin.
Require Import Coq.ZArith.BinIntDef CFML.CFHeader.
Delimit Scope Z_scope with Z.
Local Open Scope cfheader_scope.
Require Pervasives_ml.
Parameter of_list : CFML.CFApp.func.
Parameter length : CFML.CFApp.func.
Parameter get : CFML.CFApp.func.
Parameter set : CFML.CFApp.func.
Parameter make : CFML.CFApp.func.
Parameter init : CFML.CFApp.func.
Parameter init__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat init) (
forall A_ : Type,
forall n : Coq.ZArith.BinInt.Z,
forall f : CFML.CFApp.func,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__)) (
0
)%Z n
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array A_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array A_)
)
) (
fun res : CFML.CFBuiltin.array A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (1)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
) A_
)
) (
fun x2__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) res
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x2__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q res
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def init (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF init) => CFHeader_Provide init__cf.
Parameter copy : CFML.CFApp.func.
Parameter copy__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat copy) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array A_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
)
) (
fun x2__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x1__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x1__
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x2__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array A_)
)
) (
fun r : CFML.CFBuiltin.array A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q r
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def copy (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF copy) => CFHeader_Provide copy__cf.
Parameter append : CFML.CFApp.func.
Parameter append__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat append) (
forall A_ : Type,
forall a1 : CFML.CFBuiltin.array A_,
forall a2 : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n1 : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n2 : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n1 (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n2 (
0
)%Z
)
)
)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool
)
)
)
) H Q
)
)
)
) (
fun x2__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x2__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Coq.Init.Datatypes.list A_
) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array A_)
) H Q
) (
Coq.Init.Logic.eq x2__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.not (Coq.Init.Logic.eq x__ y__))) n1 (
0
)%Z
)
)
)
)
) (
fun x3__ :
Coq.Init.Datatypes.bool
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x3__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
) H Q
) (
Coq.Init.Logic.eq x3__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
) H Q
)
)
)
) (
fun d : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add n1 n2
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ d
) Coq.Lists.List.nil
)
) (
CFML.CFBuiltin.array A_
)
)
) (
fun a :
CFML.CFBuiltin.array A_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (
0
)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n1
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x4__ :
A_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x4__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (
0
)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n2
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x5__ :
A_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add n1 i
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x5__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q a
)
)
) (
Q' Coq.Init.Datatypes.tt
) Q
)
)
)
) (
Q' Coq.Init.Datatypes.tt
) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def append (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF append) => CFHeader_Provide append__cf.
Parameter sub : CFML.CFApp.func.
Parameter sub__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat sub) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall ofs : Coq.ZArith.BinInt.Z,
forall len : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) ofs (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) ofs (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) len (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) len (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x4__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) ofs (
Coq.ZArith.BinInt.Z.sub x4__ len
)
)
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
) (
fun x5__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (TLC.LibBool.neg x5__)
)
)
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_fun (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
forall f0__ : CFML.CFApp.func,
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat f0__) (
forall i : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add ofs i
)
) Coq.Lists.List.nil
)
) A_
) H Q ->
CFML.CFApp.app_def f0__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
) H Q
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def init (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z len
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn CFML.CFApp.func f0__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array A_)
) H Q
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def sub (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z ofs) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z len) Coq.Lists.List.nil
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF sub) => CFHeader_Provide sub__cf.
Parameter fill : CFML.CFApp.func.
Parameter fill__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (4)%nat fill) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall start : Coq.ZArith.BinInt.Z,
forall nb : Coq.ZArith.BinInt.Z,
forall v : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x4__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start (
Coq.ZArith.BinInt.Z.sub x4__ nb
)
)
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
) (
fun x5__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (TLC.LibBool.neg x5__)
)
)
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for start (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) (
Coq.ZArith.BinInt.Z.add start nb
)
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ v) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def fill (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z start) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z nb) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ v) Coq.Lists.List.nil
)
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF fill) => CFHeader_Provide fill__cf.
Parameter blit : CFML.CFApp.func.
Parameter blit__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (5)%nat blit) (
forall A_ : Type,
forall a1 : CFML.CFBuiltin.array A_,
forall start1 : Coq.ZArith.BinInt.Z,
forall a2 : CFML.CFBuiltin.array A_,
forall start2 : Coq.ZArith.BinInt.Z,
forall nb : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start1 (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start1 (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a1
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x21__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start1 (
Coq.ZArith.BinInt.Z.sub x21__ nb
)
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start1 (
Coq.ZArith.BinInt.Z.sub x21__ nb
)
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start2 (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start2 (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a2
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x26__ :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start2 (
Coq.ZArith.BinInt.Z.sub x26__ nb
)
)
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
) (
fun x27__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (TLC.LibBool.neg x27__)
)
)
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) nb
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add start1 i
)
) Coq.Lists.List.nil
)
) A_
)
) (
fun x28__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add start2 i
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x28__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def blit (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z start1) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z start2
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z nb) Coq.Lists.List.nil
)
)
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF blit) => CFHeader_Provide blit__cf.
Parameter iter : CFML.CFApp.func.
Parameter iter__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat iter) (
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x1__) Coq.Lists.List.nil
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def iter (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF iter) => CFHeader_Provide iter__cf.
Parameter map : CFML.CFApp.func.
Parameter map__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat map) (
forall B_ : Type,
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array B_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) Coq.Lists.List.nil
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array B_)
)
) (
fun r : CFML.CFBuiltin.array B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (1)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
) B_
)
) (
fun x4__ :
B_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array B_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x4__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q r
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def map (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF map) => CFHeader_Provide map__cf.
Parameter iteri : CFML.CFApp.func.
Parameter iteri__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat iteri) (
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x1__) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def iteri (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF iteri) => CFHeader_Provide iteri__cf.
Parameter mapi : CFML.CFApp.func.
Parameter mapi__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat mapi) (
forall B_ : Type,
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array B_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) Coq.Lists.List.nil
)
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array B_)
)
) (
fun r : CFML.CFBuiltin.array B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (1)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
)
) B_
)
) (
fun x4__ :
B_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array B_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x4__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q r
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def mapi (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF mapi) => CFHeader_Provide mapi__cf.
Parameter to_list : CFML.CFApp.func.
Parameter to_list__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat to_list) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_fun (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
forall tolist : CFML.CFApp.func,
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat tolist) (
forall i : Coq.ZArith.BinInt.Z,
forall res : Coq.Init.Datatypes.list A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) i (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q res)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) i (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x0__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def tolist (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.sub i (1)%Z
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Coq.Init.Datatypes.list A_
) (
Coq.Lists.List.cons x0__ res : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
)
) (Coq.Init.Datatypes.list A_)
)
)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def tolist (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) res
) Coq.Lists.List.nil
)
) H Q
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x1__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def tolist (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.sub x1__ (1)%Z
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
)
) (Coq.Init.Datatypes.list A_)
)
)
)
) H Q
)
) H Q ->
CFML.CFApp.app_def to_list (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF to_list) => CFHeader_Provide to_list__cf.
Parameter fold_left : CFML.CFApp.func.
Parameter fold_left__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat fold_left) (
forall A_ : Type,
forall B_ : Type,
forall f : CFML.CFApp.func,
forall x : A_,
forall a : CFML.CFBuiltin.array B_,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.ref (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
) (Pervasives_ml.ref_ A_)
)
) (
fun r : Pervasives_ml.ref_ A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array B_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array B_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ A_
) r
) Coq.Lists.List.nil
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ A_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Pervasives_ml.ref_ A_) r
) Coq.Lists.List.nil
) A_
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def fold_left (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array B_) a
) Coq.Lists.List.nil
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF fold_left) => CFHeader_Provide fold_left__cf.
Parameter fold_right : CFML.CFApp.func.
Parameter fold_right__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat fold_right) (
forall B_ : Type,
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall x : B_,
forall H : CFML.CFHeaps.hprop,
forall Q : B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.ref (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn B_ x) Coq.Lists.List.nil
) (Pervasives_ml.ref_ B_)
)
) (
fun r : Pervasives_ml.ref_ B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for_down (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for_down (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (0)%Z (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ B_
) r
) Coq.Lists.List.nil
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) B_
)
) (
fun x3__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ B_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x3__
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Pervasives_ml.ref_ B_) r
) Coq.Lists.List.nil
) B_
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def fold_right (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn B_ x) Coq.Lists.List.nil
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF fold_right) => CFHeader_Provide fold_right__cf.
Require Coq.ZArith.BinInt TLC.LibLogic TLC.LibRelation TLC.LibInt TLC.LibListZ CFML.Shared CFML.CFHeaps CFML.CFApp CFML.CFPrint CFML.CFBuiltin.
Require Import Coq.ZArith.BinIntDef CFML.CFHeader.
Delimit Scope Z_scope with Z.
Local Open Scope cfheader_scope.
Require Pervasives_ml.
Parameter of_list : CFML.CFApp.func.
Parameter length : CFML.CFApp.func.
Parameter get : CFML.CFApp.func.
Parameter set : CFML.CFApp.func.
Parameter make : CFML.CFApp.func.
Parameter init : CFML.CFApp.func.
Parameter init__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat init) (
forall A_ : Type,
forall n : Coq.ZArith.BinInt.Z,
forall f : CFML.CFApp.func,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.le _ TLC.LibInt.le_int_inst x__ y__)) (
0
)%Z n
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array A_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array A_)
)
) (
fun res : CFML.CFBuiltin.array A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (1)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
) A_
)
) (
fun x2__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) res
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x2__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q res
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def init (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF init) => CFHeader_Provide init__cf.
Parameter copy : CFML.CFApp.func.
Parameter copy__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat copy) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array A_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
)
) (
fun x2__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x1__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z x1__
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x2__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array A_)
)
) (
fun r : CFML.CFBuiltin.array A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q r
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def copy (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF copy) => CFHeader_Provide copy__cf.
Parameter append : CFML.CFApp.func.
Parameter append__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat append) (
forall A_ : Type,
forall a1 : CFML.CFBuiltin.array A_,
forall a2 : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n1 : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n2 : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n1 (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n2 (
0
)%Z
)
)
)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool
)
)
)
) H Q
)
)
)
) (
fun x2__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x2__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Coq.Init.Datatypes.list A_
) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array A_)
) H Q
) (
Coq.Init.Logic.eq x2__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.not (Coq.Init.Logic.eq x__ y__))) n1 (
0
)%Z
)
)
)
)
) (
fun x3__ :
Coq.Init.Datatypes.bool
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x3__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
) H Q
) (
Coq.Init.Logic.eq x3__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
) H Q
)
)
)
) (
fun d : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add n1 n2
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ d
) Coq.Lists.List.nil
)
) (
CFML.CFBuiltin.array A_
)
)
) (
fun a :
CFML.CFBuiltin.array A_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (
0
)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n1
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x4__ :
A_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x4__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (
0
)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n2
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x5__ :
A_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add n1 i
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x5__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q a
)
)
) (
Q' Coq.Init.Datatypes.tt
) Q
)
)
)
) (
Q' Coq.Init.Datatypes.tt
) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def append (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF append) => CFHeader_Provide append__cf.
Parameter sub : CFML.CFApp.func.
Parameter sub__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat sub) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall ofs : Coq.ZArith.BinInt.Z,
forall len : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) ofs (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) ofs (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) len (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) len (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x4__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) ofs (
Coq.ZArith.BinInt.Z.sub x4__ len
)
)
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
) (
fun x5__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (TLC.LibBool.neg x5__)
)
)
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_fun (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
forall f0__ : CFML.CFApp.func,
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat f0__) (
forall i : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add ofs i
)
) Coq.Lists.List.nil
)
) A_
) H Q ->
CFML.CFApp.app_def f0__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
) H Q
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def init (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z len
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn CFML.CFApp.func f0__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array A_)
) H Q
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def sub (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z ofs) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z len) Coq.Lists.List.nil
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF sub) => CFHeader_Provide sub__cf.
Parameter fill : CFML.CFApp.func.
Parameter fill__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (4)%nat fill) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall start : Coq.ZArith.BinInt.Z,
forall nb : Coq.ZArith.BinInt.Z,
forall v : A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x4__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start (
Coq.ZArith.BinInt.Z.sub x4__ nb
)
)
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
) (
fun x5__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (TLC.LibBool.neg x5__)
)
)
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for start (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) (
Coq.ZArith.BinInt.Z.add start nb
)
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ v) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def fill (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z start) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z nb) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ v) Coq.Lists.List.nil
)
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF fill) => CFHeader_Provide fill__cf.
Parameter blit : CFML.CFApp.func.
Parameter blit__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (5)%nat blit) (
forall A_ : Type,
forall a1 : CFML.CFBuiltin.array A_,
forall start1 : Coq.ZArith.BinInt.Z,
forall a2 : CFML.CFBuiltin.array A_,
forall start2 : Coq.ZArith.BinInt.Z,
forall nb : Coq.ZArith.BinInt.Z,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_assert (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) nb (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start1 (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start1 (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a1
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x21__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start1 (
Coq.ZArith.BinInt.Z.sub x21__ nb
)
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start1 (
Coq.ZArith.BinInt.Z.sub x21__ nb
)
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start2 (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
)
)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) start2 (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a2
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x26__ :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.gt _ (@TLC.LibOrder.gt_of_le _ TLC.LibInt.le_int_inst) x__ y__)) start2 (
Coq.ZArith.BinInt.Z.sub x26__ nb
)
)
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
)
)
) H Q
)
)
) H Q
)
)
)
) (
fun x27__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (TLC.LibBool.neg x27__)
)
)
)
)
)
) H (
fun _b : Coq.Init.Datatypes.bool =>
CFML.CFHeaps.heap_is_star (
CFML.CFHeaps.heap_is_empty_st (
Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
)
) H
)
) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) nb
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add start1 i
)
) Coq.Lists.List.nil
)
) A_
)
) (
fun x28__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.add start2 i
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x28__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
) H Q ->
CFML.CFApp.app_def blit (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a1) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z start1) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a2
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z start2
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z nb) Coq.Lists.List.nil
)
)
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF blit) => CFHeader_Provide blit__cf.
Parameter iter : CFML.CFApp.func.
Parameter iter__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat iter) (
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x1__) Coq.Lists.List.nil
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def iter (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF iter) => CFHeader_Provide iter__cf.
Parameter map : CFML.CFApp.func.
Parameter map__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat map) (
forall B_ : Type,
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array B_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) Coq.Lists.List.nil
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array B_)
)
) (
fun r : CFML.CFBuiltin.array B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (1)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
) B_
)
) (
fun x4__ :
B_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array B_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x4__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q r
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def map (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF map) => CFHeader_Provide map__cf.
Parameter iteri : CFML.CFApp.func.
Parameter iteri__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat iteri) (
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x1__) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def iteri (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF iteri) => CFHeader_Provide iteri__cf.
Parameter mapi : CFML.CFApp.func.
Parameter mapi__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat mapi) (
forall B_ : Type,
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : CFML.CFBuiltin.array B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun n : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (
Q (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
0
)%Z
)
)
)
)
) (
fun x0__ : Coq.Init.Datatypes.bool =>
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def of_list (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
)
) Coq.Lists.List.nil
) (CFML.CFBuiltin.array B_)
) H Q
) (
Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
0
)%Z
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) Coq.Lists.List.nil
)
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def make (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) (CFML.CFBuiltin.array B_)
)
) (
fun r : CFML.CFBuiltin.array B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.ex (
fun Q' :
_ -> CFML.CFHeaps.hprop
=>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (1)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) n
) (
fun i :
Coq.ZArith.BinInt.Z
=>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
)
) B_
)
) (
fun x4__ :
B_
=>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def set (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array B_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x4__
) Coq.Lists.List.nil
)
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H :
CFML.CFHeaps.hprop
=>
fun Q :
_ ->
CFML.CFHeaps.hprop
=>
TLC.LibLogic.pred_incl H (
Q r
)
)
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
)
)
)
) H Q
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def mapi (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF mapi) => CFHeader_Provide mapi__cf.
Parameter to_list : CFML.CFApp.func.
Parameter to_list__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat to_list) (
forall A_ : Type,
forall a : CFML.CFBuiltin.array A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_fun (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
forall tolist : CFML.CFApp.func,
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat tolist) (
forall i : Coq.ZArith.BinInt.Z,
forall res : Coq.Init.Datatypes.list A_,
forall H : CFML.CFHeaps.hprop,
forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_if (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) i (
0
)%Z
) Coq.Init.Datatypes.true ->
CFML.CFPrint.tag CFML.CFPrint.tag_ret (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
TLC.LibLogic.pred_incl H (Q res)
)
) H Q
) (
Coq.Init.Logic.eq (
(fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.lt _ (@TLC.LibOrder.lt_of_le Coq.ZArith.BinInt.Z TLC.LibInt.le_int_inst) x__ y__)) i (
0
)%Z
) Coq.Init.Datatypes.false ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x0__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def tolist (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.sub i (1)%Z
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Coq.Init.Datatypes.list A_
) (
Coq.Lists.List.cons x0__ res : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
)
) (Coq.Init.Datatypes.list A_)
)
)
)
) H Q
)
)
) H Q ->
CFML.CFApp.app_def tolist (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) res
) Coq.Lists.List.nil
)
) H Q
)
) ->
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x1__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def tolist (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
Coq.ZArith.BinInt.Z.sub x1__ (1)%Z
)
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
)
) Coq.Lists.List.nil
)
) (Coq.Init.Datatypes.list A_)
)
)
)
) H Q
)
) H Q ->
CFML.CFApp.app_def to_list (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) Coq.Lists.List.nil
) H Q
)
)
).
Hint Extern 1 (RegisterCF to_list) => CFHeader_Provide to_list__cf.
Parameter fold_left : CFML.CFApp.func.
Parameter fold_left__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat fold_left) (
forall A_ : Type,
forall B_ : Type,
forall f : CFML.CFApp.func,
forall x : A_,
forall a : CFML.CFBuiltin.array B_,
forall H : CFML.CFHeaps.hprop,
forall Q : A_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.ref (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) Coq.Lists.List.nil
) (Pervasives_ml.ref_ A_)
)
) (
fun r : Pervasives_ml.ref_ A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array B_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for (0)%Z (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array B_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ A_
) r
) Coq.Lists.List.nil
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) A_
)
) (
fun x3__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ A_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x3__
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Pervasives_ml.ref_ A_) r
) Coq.Lists.List.nil
) A_
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def fold_left (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ x) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array B_) a
) Coq.Lists.List.nil
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF fold_left) => CFHeader_Provide fold_left__cf.
Parameter fold_right : CFML.CFApp.func.
Parameter fold_right__cf :
CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat fold_right) (
forall B_ : Type,
forall A_ : Type,
forall f : CFML.CFApp.func,
forall a : CFML.CFBuiltin.array A_,
forall x : B_,
forall H : CFML.CFHeaps.hprop,
forall Q : B_ -> CFML.CFHeaps.hprop,
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.ref (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn B_ x) Coq.Lists.List.nil
) (Pervasives_ml.ref_ B_)
)
) (
fun r : Pervasives_ml.ref_ B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def length (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a
) Coq.Lists.List.nil
) Coq.ZArith.BinInt.Z
)
) (
fun x0__ : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_seq (
CFML.CFHeaps.local (
fun H : CFML.CFHeaps.hprop =>
fun Q : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.ex (
fun Q' : _ -> CFML.CFHeaps.hprop =>
Coq.Init.Logic.and (
CFML.CFPrint.tag CFML.CFPrint.tag_for_down (
CFML.CFHeaps.local (
CFML.CFPrint.cf_for_down (
(fun x__ => Coq.ZArith.BinInt.Zminus x__ (1)%Z) x0__
) (0)%Z (
fun i : Coq.ZArith.BinInt.Z =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ B_
) r
) Coq.Lists.List.nil
) B_
)
) (
fun x2__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def get (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
CFML.CFBuiltin.array A_
) a
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
) Coq.Lists.List.nil
)
) A_
)
) (
fun x1__ : A_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_let (
CFML.CFHeaps.local (
CFML.CFPrint.cf_let (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def f (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn A_ x1__
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x2__
) Coq.Lists.List.nil
)
) B_
)
) (
fun x3__ : B_ =>
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_colon_eq__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (
Pervasives_ml.ref_ B_
) r
) (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn B_ x3__
) Coq.Lists.List.nil
)
) Coq.Init.Datatypes.unit
)
)
)
)
)
)
)
)
)
)
)
)
) H Q'
) (
CFML.CFPrint.tag CFML.CFPrint.tag_apply (
@CFML.CFApp.app_def Pervasives_ml.infix_emark__ (
Coq.Lists.List.cons (
@CFML.CFHeaps.dyn (Pervasives_ml.ref_ B_) r
) Coq.Lists.List.nil
) B_
) (Q' Coq.Init.Datatypes.tt) Q
)
)
)
)
)
)
)
)
)
) H Q ->
CFML.CFApp.app_def fold_right (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn (CFML.CFBuiltin.array A_) a) (
Coq.Lists.List.cons (@CFML.CFHeaps.dyn B_ x) Coq.Lists.List.nil
)
)
) H Q
)
)
).
Hint Extern 1 (RegisterCF fold_right) => CFHeader_Provide fold_right__cf.