Library Malfunction.Examples.simple.test_extraction_malfunction

From MetaRocq.Utils Require Import Show.
From MetaRocq.Template Require Import Loader.
From MetaRocq.ErasurePlugin Require Import Loader.
From VerifiedExtraction Require Import Extraction OCamlFFI.
From MetaRocq.Template Require Import All.

From Stdlib Require Import ZArith PrimInt63 Sint63.
Eval compute in PrimInt63.ltb Sint63.min_int Sint63.min_int.

Set Warnings "-primitive-turned-into-axiom".

Definition test := print_int ( Sint63.max_int).
Verified Extraction -fmt -verbose -compile-with-coq -run test "test.mlf".
Verified Extraction -verbose Sint63.min_int.
Verified Extraction -verbose Uint63.max_int.

Definition max_to_Z := print_string (string_of_Z (Uint63.to_Z Uint63.max_int)).
Verified Extraction -verbose -compile-with-coq -run max_to_Z "max_to_Z.mlf".

Definition check_lt := print_string (show (PrimInt63.ltb 1 0)).
Verified Extraction -compile-with-coq -run check_lt "check_lt.mlf".

From Stdlib Require Import PrimFloat.
Definition test_float := print_float (7500.50)%float.
Eval compute in FloatOps.Prim2SF 75000.5%float.
Verified Extraction -fmt -compile-with-coq -run test_float "test_float.mlf".

From Stdlib Require Import PArray.
From Malfunction Require Import utils_array.

Definition val : array nat := PArray.make 3 2.

Definition gettest : nat := PArray.get val 2.
Definition settest : array nat := PArray.set val 2 1.
Definition getsettest : nat := PArray.get settest 2.

Set Warnings "-primitive-turned-into-axiom".

Definition prim_array_get := (print_int (int_of_nat gettest)).
Definition prim_array_get_set := (print_int (int_of_nat getsettest)).

Verified Extraction -fmt -typed -compile-with-coq val "val.mlf".