Library Malfunction.Examples.simple.test_extract

From Equations Require Import Equations.
From Malfunction Require Import FFI.
From VerifiedExtraction Require Import Extraction OCamlFFI.
From MetaRocq.Template Require Import All.
From Stdlib Require ZArith Streams.StreamMemo.

From Stdlib Require Import String.
From Stdlib Require Vector.


From Stdlib Require Import .
Definition test_primint :=
  let _ := print_int Sint63.min_int in
  let _ := print_newline tt in
  let _ := print_int Sint63.max_int in tt.
Eval compute in test_primint.

Verified Extraction (plus, mult).

Verified Extraction -fmt -compile-with-coq -run test_primint "test_primint.mlf".

From Stdlib Require Import PrimFloat.
Definition test_floats := print_float (100.5)%float.
Eval compute in test_floats.
Verified Extraction -fmt -compile-with-coq -run test_floats "test_floats.mlf".


Module NegativeCoind.
Set Primitive Projections.
CoInductive stream := Cons
  { head : ; tail : stream }.

Fixpoint take (n : ) (s : stream) : list :=
  match n with
  | 0 ⇒ []
  | S ns.(head) :: take n s.(tail)
  end.

CoFixpoint ones : stream := {| head := 1; tail := ones |}.

Definition test_ones := print_string (show (take 10 ones)).

Verified Extraction -fmt -unsafe -compile-with-coq -run test_ones "ones.mlf".

CoFixpoint naturals (n : ) : stream :=
  {| head := n; tail := naturals (S n) |}.

Verified Extraction -fmt -unsafe naturals.

Definition test_take := print_string (show (take 10 (naturals 0))).

Verified Extraction -fmt -unsafe -compile-with-coq -run test_take "naturals.mlf".

Import ZArith Streams.StreamMemo.
Local Open Scope Z_scope.
Fixpoint tfact (n: ) :=
  match n with
   | O ⇒ 1
   | S Z.of_nat n × tfact
  end.

Definition lfact_list :=
  dimemo_list _ tfact ( n z ⇒ (Z.of_nat (S n) × z)).

Definition lfact n := dmemo_get _ tfact n lfact_list.

Theorem lfact_correct n: lfact n = tfact n.
Proof.
unfold lfact, lfact_list.
rewrite dimemo_get_correct; auto.
Qed.


Fixpoint nop p :=
  match p with
   | xH ⇒ 0
   | xI nop
   | xO nop
  end.

Definition test z :=
  match z with
   | ⇒ 0
   | Zpos nop
   | Zneg nop
  end.

Arguments print_string s%bs.
Definition arg := 1000%.
Definition test_lfact := test (lfact arg).
Definition show_lfact := print_string ("test_lfact: " ++ show (lfact arg)).

Verified Extraction -time -fmt -typed -unsafe -compile-with-coq -run test_lfact "test_lfact_typed.mlf". Verified Extraction -time -fmt -unsafe -compile-with-coq -run test_lfact "test_lfact.mlf". Verified Extraction -optimize -time -fmt -typed -unsafe -compile-with-coq -run
  test_lfact "test_lfact_typed_opt.mlf".
Verified Extraction -time -fmt -typed -unsafe -compile-with-coq -run
  show_lfact "show_lfact_typed.mlf". Verified Extraction -time -fmt -unsafe -compile-with-coq -run
  show_lfact "show_lfact.mlf".
End NegativeCoind.

Module Unboxed.

  Definition t := { x : | x < 3 }.
  Program Definition ex : t := 1.
  Program Definition test_ex := coq_msg_info (string_of_nat ex).

  Verified Extraction -typed -unsafe -fmt -compile-plugin -run test_ex "test_ex.mlf".
End Unboxed.

Typed extraction

Definition sub : { x : | x = 0 } := @exist _ _ 0 eq_refl.
Verified Extraction sub.
Verified Extraction -typed sub.

Equations idnat (n : ) : by wf n lt :=
 | 0 ⇒ 0
 | S nS (idnat n).

Extraction idnat.

Verified Extract Inline [ Equations.Prop.Subterm.FixWf, Corelib.Init.Wf.Fix, Corelib.Init.Wf.Fix_F, idnat_functional ].

Verified Extraction -fmt -unsafe -typed idnat "idnat.mlf".

Inductive three := ZERO | ONE | TWO | THREE.

Definition two := TWO.

From MetaRocq.Utils Require Import bytestring.

Definition test_bytestring (u : unit) := bytestring.String.compare "" "bug".

Verified Extraction -compile-with-coq test_bytestring "test_bytestring.mlf".

Verified Extraction two "two.mlf".

Axiom axiom : .

Verified Extraction axiom "axiom.mlf".

From Malfunction Require Import Compile Pipeline.

From Stdlib Require Import List.
Import ListNotations.

Polymorphic Record myprod@{i j} (A : Type@{i}) (B : Type@{j}) := mypair { fst : A; snd : B }.

Notation "( x , y , .. , z )" := (mypair _ _ .. (mypair _ _ x y) .. z) : core_scope.
Definition many_list_functions : myprod _ _ := (@List.firstn , @List.filter , @List.skipn ).

Verified Extraction -fmt -typed many_list_functions "list.mlf".

Definition prf := match conj I I with conj x y ⇒ (x,0) end.

Verified Extraction prf "proof.mlf".

Verified Extraction blocks_until "mcase.mlf".

Definition test_add := plus 2 5.

Verified Extraction test_add "add.mlf".

Verified Extraction (match cons THREE nil with cons x _x | _ONE end).
Verified Extraction -help.

Fixpoint ack (n m:) {struct n} : :=
  match n with
    | 0 ⇒ S m
    | S plet fix ackn (m:) {struct m} :=
                 match m with
                   | 0 ⇒ ack p 1
                   | S qack p (ackn q)
                 end
             in ackn m
  end.

Verified Extraction (ack 3 5).

Verified Extraction (@exist ( xx = 0) 0 (@eq_refl _ 0)).

Definition vplus {n:} :
  Vector.t nVector.t nVector.t n := (Vector.map2 plus).
Definition : Vector.t 2 :=
  (Vector.cons 0 1 (Vector.cons 1 0 (Vector.nil ))).
Definition : Vector.t 2 :=
  (Vector.cons 2 1 (Vector.cons 3 0 (Vector.nil ))).
Definition := Vector.hd (vplus ).

Verified Extraction .

Inductive tree (A:Set) : Set :=
  node : Aforest Atree A
with forest (A:Set) : Set :=
     | leaf : Aforest A
     | fcons : tree Aforest Aforest A.
Arguments leaf {A}.
Arguments fcons {A}.
Arguments node {A}.

Fixpoint tree_size (t:tree bool) : :=
  match t with
    | node a fS (forest_size f)
  end
with forest_size (f:forest bool) : :=
       match f with
         | leaf b ⇒ 1
         | fcons t ⇒ (tree_size t + forest_size )
       end.

Definition arden: forest bool :=
  fcons (node true (fcons (node true (leaf false)) (leaf true)))
        (fcons (node true (fcons (node true (leaf false)) (leaf true)))
               (leaf false)).

Verified Extraction (forest_size arden).