Library ASCommon.CExtraction

From Stdlib Require Import ZArith.
#[warnings="-deprecated-library-file-since-8.20"]
From Stdlib Require Import Zeuclid.
From Stdlib Require Import Extraction.

Require Import Options.
Require Import Common Effects HVec Exec.

Base defaults

From Stdlib Require Import ExtrOcamlBasic.

Extraction Inline fmap.
Extraction Inline mbind.
Extraction Inline mcall.
Extraction Inline mchoose.
Extraction Inline lookup_total.
Extraction Inline mchoosel.
Extraction Inline mret.

By default the parameters of eff_ret are extracted as 'eff and 'effect, but effect is a keyword since OCaml 5.3

Extract Constant eff_ret "'eff" "'ret" ⇒ "'ret".

Bools

Extract Inlined Constant Decision ⇒ "bool".
Extract Inlined Constant Bool.eqb ⇒ "(=)".
Extraction Inline decide.
Extraction Inline decide_rel.

Integers

All integers types go to Zarith

Extract Inductive positive ⇒ "ZO.t"
  ["(fun x -> ZO.((x lsl 1) lor one))"
   "(fun x -> ZO.(x lsl 1))"
   "ZO.one"]
  "ZO.(fun f2p1 f2p f1 p -> if p == one then f1 () else if is_odd p then f2p1 (p asr 1) else f2p (p asr 1))".

Extract Inductive Z ⇒ "ZO.t" ["ZO.zero" "" "ZO.neg"]
  "ZO.(fun f0 fp fn z -> match sign z with 0 -> f0 () | 1 -> fp z | _ -> fn (neg z))".

Extract Inductive N ⇒ "ZO.t" ["ZO.zero" ""]
  "ZO.(fun f0 fp n -> match sign n with 0 -> f0 () | _ -> fp n)".

Extract Inductive nat ⇒ "ZO.t" ["ZO.zero" "ZO.succ"]
  "ZO.(fun f0 fS n -> match sign n with 0 -> f0 () | _ -> fS (pred n))".

Extract Inlined Constant BinPos.Pos.succ ⇒ "ZO.succ".
Extract Inlined Constant PosDef.Pos.succ ⇒ "ZO.succ".
Extract Inlined Constant N.succ ⇒ "ZO.succ".
Extract Inlined Constant Z.succ ⇒ "ZO.succ".

Extract Inlined Constant Pos.pred ⇒ "ZO.pred_pos".
Extract Inlined Constant Pos.pred_N ⇒ "ZO.pred_nat".
Extract Inlined Constant N.pred ⇒ "ZO.pred_nat".
Extract Inlined Constant Z.pred ⇒ "ZO.pred".
Extract Inlined Constant Init.Nat.pred ⇒ "ZO.pred_nat".
Extract Inlined Constant PeanoNat.Nat.pred ⇒ "ZO.pred_nat".

Basic arithmetic

Extract Inlined Constant BinPos.Pos.add ⇒ "ZO.add".
Extract Inlined Constant PosDef.Pos.add ⇒ "ZO.add".
Extract Inlined Constant BinNat.N.add ⇒ "ZO.add".
Extract Inlined Constant BinNatDef.N.add ⇒ "ZO.add".
Extract Inlined Constant Z.add ⇒ "ZO.add".
Extract Inlined Constant Init.Nat.add ⇒ "ZO.add".
Extract Inlined Constant PeanoNat.Nat.add ⇒ "ZO.add".

Extract Inlined Constant Z.opp ⇒ "ZO.neg".

Extract Inlined Constant BinPos.Pos.sub ⇒ "ZO.sub_pos".
Extract Inlined Constant PosDef.Pos.sub ⇒ "ZO.sub_pos".
Extract Inlined Constant BinNat.N.sub ⇒ "ZO.sub_nat".
Extract Inlined Constant NatDef.N.sub ⇒ "ZO.sub_nat".
Extract Inlined Constant Z.sub ⇒ "ZO.sub".
Extract Inlined Constant Z.pos_sub ⇒ "ZO.sub".
Extract Inlined Constant Init.Nat.sub ⇒ "ZO.sub_nat".
Extract Inlined Constant PeanoNat.Nat.sub ⇒ "ZO.sub_nat".

Extract Inlined Constant BinPos.Pos.mul ⇒ "ZO.mul".
Extract Inlined Constant PosDef.Pos.mul ⇒ "ZO.mul".
Extract Inlined Constant BinNat.N.mul ⇒ "ZO.mul".
Extract Inlined Constant BinNatDef.N.mul ⇒ "ZO.mul".
Extract Inlined Constant Z.mul ⇒ "ZO.mul".
Extract Inlined Constant Init.Nat.mul ⇒ "ZO.mul".
Extract Inlined Constant PeanoNat.Nat.mul ⇒ "ZO.mul".

Extract Inlined Constant PeanoNat.Nat.pow ⇒ "ZO.powZ".
Extract Inlined Constant Z.pow_pos ⇒ "ZO.powZ".
Extract Inlined Constant Z.pow ⇒ "ZO.powZ".

Comparisons

Extract Inlined Constant BinPos.Pos.min ⇒ "ZO.min".
Extract Inlined Constant BinNat.N.min ⇒ "ZO.min".
Extract Inlined Constant BinNatDef.N.min ⇒ "ZO.min".
Extract Inlined Constant Z.min ⇒ "ZO.min".
Extract Inlined Constant Init.Nat.min ⇒ "ZO.min".
Extract Inlined Constant PeanoNat.Nat.min ⇒ "ZO.min".

Extract Inlined Constant BinPos.Pos.max ⇒ "ZO.max".
Extract Inlined Constant BinNat.N.max ⇒ "ZO.max".
Extract Inlined Constant BinNatDef.N.max ⇒ "ZO.max".
Extract Inlined Constant Z.max ⇒ "ZO.max".
Extract Inlined Constant Init.Nat.max ⇒ "ZO.max".
Extract Inlined Constant PeanoNat.Nat.max ⇒ "ZO.max".

Extract Inlined Constant BinPos.Pos.compare ⇒ "ZO.compare_rocq".
Extract Inlined Constant PosDef.Pos.compare ⇒ "ZO.compare_rocq".
Extract Inlined Constant BinPos.Pos.compare_cont ⇒ "ZO.compare_rocq".
Extract Inlined Constant PosDef.Pos.compare_cont ⇒ "ZO.compare_rocq".
Extract Inlined Constant BinNat.N.compare ⇒ "ZO.compare_rocq".
Extract Inlined Constant NatDef.N.compare ⇒ "ZO.compare_rocq".
Extract Inlined Constant Z.compare ⇒ "ZO.compare_rocq".
Extract Inlined Constant PeanoNat.Nat.compare ⇒ "ZO.compare_rocq".
Extract Inlined Constant Init.Nat.compare ⇒ "ZO.compare_rocq".

Extract Inlined Constant Pos.eqb ⇒ "ZO.equal".
Extract Inlined Constant PosDef.Pos.eqb ⇒ "ZO.equal".
Extract Inlined Constant BinPos.Pos.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant Pos.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant N.eqb ⇒ "ZO.equal".
Extract Inlined Constant N.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant BinNat.N.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant Z.eqb ⇒ "ZO.equal".
Extract Inlined Constant Z.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant BinInt.Z.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant PeanoNat.Nat.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant numbers.Nat.eq_dec ⇒ "ZO.equal".
Extract Inlined Constant PeanoNat.Nat.eqb ⇒ "ZO.equal".
Extract Inlined Constant Init.Nat.eqb ⇒ "ZO.equal".
Extract Inlined Constant EqNat.eq_nat_decide ⇒ "ZO.equal".

Extract Inlined Constant PeanoNat.Nat.leb ⇒ "ZO.leq".
Extract Inlined Constant Init.Nat.leb ⇒ "ZO.leq".
Extract Inlined Constant PeanoNat.Nat.ltb ⇒ "ZO.lt".
Extract Inlined Constant Init.Nat.ltb ⇒ "ZO.lt".
Extract Inlined Constant Z.leb ⇒ "ZO.leq".
Extract Inlined Constant Z.ltb ⇒ "ZO.lt".
Extract Inlined Constant Z.geb ⇒ "ZO.geq".
Extract Inlined Constant Z.gtb ⇒ "ZO.gt".
Extract Inlined Constant Z.le_dec ⇒ "ZO.leq".
Extract Inlined Constant Z.lt_dec ⇒ "ZO.lt".
Extract Inlined Constant N.leb ⇒ "ZO.leq".
Extract Inlined Constant N.ltb ⇒ "ZO.lt".
Extract Inlined Constant N.le_dec ⇒ "ZO.leq".
Extract Inlined Constant N.lt_dec ⇒ "ZO.lt".
Extract Inlined Constant numbers.Nat.le_dec ⇒ "ZO.leq".
Extract Inlined Constant numbers.Nat.lt_dec ⇒ "ZO.lt".
Extract Inlined Constant CArith.le_dec ⇒ "ZO.leq".
Extract Inlined Constant CArith.lt_dec ⇒ "ZO.lt".

Conversions

Extract Inlined Constant N.of_nat ⇒ "Fun.id".
Extract Inlined Constant N.to_nat ⇒ "Fun.id".

Extract Inlined Constant Z.of_N ⇒ "Fun.id".
Extract Inlined Constant Z.of_nat ⇒ "Fun.id".
Extract Inlined Constant Z.to_N ⇒ "ZO.to_nat".
Extract Inlined Constant Z.to_nat ⇒ "ZO.to_nat".
Extract Inlined Constant Z.to_pos ⇒ "ZO.to_pos".

Extract Inlined Constant Z.abs ⇒ "ZO.abs".
Extract Inlined Constant Z.abs_nat ⇒ "ZO.abs".
Extract Inlined Constant Z.abs_N ⇒ "ZO.abs".
Extract Inlined Constant Z.sgn ⇒ "ZO.signZ".

Divisions

Extract Inlined Constant N.div ⇒ "ZO.divZ".
Extract Inlined Constant N.modulo ⇒ "ZO.remZ".
Extract Inlined Constant N.div_eucl ⇒ "ZO.div_remZ".

Z.div and Z.modulo are the floor division which gives a modulo of the sign of the divisor

Extract Inlined Constant Z.div ⇒ "ZO.fdivZ".
Extract Inlined Constant Z.modulo ⇒ "ZO.fmodZ".
Extract Inlined Constant Z.div_eucl ⇒ "ZO.fdiv_modZ".

Quot and rem round the quotient toward 0

Extract Inlined Constant Z.quot ⇒ "ZO.divZ".
Extract Inlined Constant Z.rem ⇒ "ZO.remZ".
Extract Inlined Constant Z.quotrem ⇒ "ZO.div_remZ".

Zeuclid implement the euclidian division that makes the modulo always non-negative

Extract Inlined Constant Zeuclid.ZEuclid.div ⇒ "ZO.edivZ".
Extract Inlined Constant Zeuclid.ZEuclid.modulo ⇒ "ZO.emodZ".

Shifts

Extract Inlined Constant N.shiftl ⇒ "ZO.shiftl".
Extract Inlined Constant Z.shiftl ⇒ "ZO.shiftl".
Extract Inlined Constant N.shiftr ⇒ "ZO.shiftr".
Extract Inlined Constant Z.shiftr ⇒ "ZO.shiftr".

Extract Inlined Constant Nat.double ⇒ "ZO.double".
Extract Inlined Constant N.double ⇒ "ZO.double".
Extract Inlined Constant NatDef.N.double ⇒ "ZO.double".
Extract Inlined Constant Z.double ⇒ "ZO.double".

Extract Inlined Constant PeanoNat.Nat.div2 ⇒ "ZO.div2".
Extract Inlined Constant Init.Nat.div2 ⇒ "ZO.div2".
Extract Inlined Constant Z.div2 ⇒ "ZO.div2".
Extract Inlined Constant N.div2 ⇒ "ZO.div2".
Extract Inlined Constant Pos.div2 ⇒ "ZO.div2_pos".

Bitwise operators

Extract Inlined Constant PosDef.Pos.lor ⇒ "ZO.logor".
Extract Inlined Constant Pos.lor ⇒ "ZO.logor".
Extract Inlined Constant Nat.lor ⇒ "ZO.logor".
Extract Inlined Constant N.lor ⇒ "ZO.logor".
Extract Inlined Constant NatDef.N.lor ⇒ "ZO.logor".
Extract Inlined Constant Z.lor ⇒ "ZO.logor".

Extract Inlined Constant PosDef.Pos.land ⇒ "ZO.logand".
Extract Inlined Constant Pos.land ⇒ "ZO.logand".
Extract Inlined Constant Nat.land ⇒ "ZO.logand".
Extract Inlined Constant N.land ⇒ "ZO.logand".
Extract Inlined Constant NatDef.N.land ⇒ "ZO.logand".
Extract Inlined Constant Z.land ⇒ "ZO.logand".

Extract Inlined Constant PosDef.Pos.lxor ⇒ "ZO.logxor".
Extract Inlined Constant Pos.lxor ⇒ "ZO.logxor".
Extract Inlined Constant Nat.lxor ⇒ "ZO.logxor".
Extract Inlined Constant N.lxor ⇒ "ZO.logxor".
Extract Inlined Constant NatDef.N.lxor ⇒ "ZO.logxor".
Extract Inlined Constant Z.lxor ⇒ "ZO.logxor".

Extract Inlined Constant Z.lnot ⇒ "ZO.lognot".

Extract Inlined Constant Z.odd ⇒ "ZO.is_odd".
Extract Inlined Constant N.odd ⇒ "ZO.is_odd".
Extract Inlined Constant Nat.odd ⇒ "ZO.is_odd".
Extract Inlined Constant Z.even ⇒ "ZO.is_even".
Extract Inlined Constant N.even ⇒ "ZO.is_even".
Extract Inlined Constant Nat.even ⇒ "ZO.is_even".

Extract Inlined Constant Pos.testbit ⇒ "ZO.testbitZ".
Extract Inlined Constant Nat.testbit ⇒ "ZO.testbitZ".
Extract Inlined Constant N.testbit ⇒ "ZO.testbitZ".
Extract Inlined Constant Z.testbit ⇒ "ZO.testbitZ".

Bit twiddling

Extract Inlined Constant Pos.reverse ⇒ "Pos_reverse.pos_reverse".

Extraction Implicit prod_countable [EqDecision0 EqDecision1].
Extract Constant prod_countable ⇒ "fun h h0 -> { encode = (fun xy -> Bit_interleaving.encode (h.encode (fst xy)) (h0.encode (snd xy))); decode = (fun c -> let (p, q) = Bit_interleaving.decode c in if p == ZO.zero || q == ZO.zero then None else Stdlib.Option.bind (h.decode p) (fun np -> Stdlib.Option.bind (h0.decode q) (fun nq -> Some (np, nq)))) }".

Bitvector

Extract Inlined Constant bv_modulus ⇒ "Support.bv_modulus".
Extract Inlined Constant bv_half_modulus ⇒ "Support.bv_half_modulus".
Extract Inlined Constant bv_wrap ⇒ "Support.bv_wrap".
Extract Inlined Constant bv_swrap ⇒ "Support.bv_swrap".
Extraction Implicit bv_extract [n].
Extract Inlined Constant bv_extract ⇒ "Support.bv_extract".

Extraction Inline Z_to_bv.
Extraction Implicit bv_eq_dec [n].
Extraction Inline bv_eq_dec.
Extraction Implicit bv_0 [n].
Extraction Inline bv_0.
Extraction Implicit bv_inhabited [n].
Extraction Inline bv_inhabited.

Extraction Implicit bv_concat [n1].

Extraction Implicit bv_zero_extend [n].
Extraction Inline bv_zero_extend.
Extraction Implicit bv_or [n].
Extraction Inline bv_or.
Extraction Implicit bv_and [n].
Extraction Inline bv_and.
Extraction Implicit bv_xor [n].
Extraction Inline bv_xor.
Extraction Implicit bv_shiftr [n].
Extraction Inline bv_shiftr.

Strings

From Stdlib Require Import ExtrOcamlNativeString.
Extraction Blacklist String.

From Stdlib Require BinaryString.

Extract Inlined Constant BinaryString.Raw.to_N ⇒ "Support.bin_str_to_N".
Extract Inlined Constant HexString.Raw.to_N ⇒ "Support.hex_str_to_N".
Extract Inlined Constant HexString.of_Z ⇒ "Support.hex_str_of_Z".

Lists

Extract Inlined Constant map ⇒ "Support.list_map".
Extract Inlined Constant list_fmap ⇒ "Support.list_map".
Extract Inlined Constant length ⇒ "Support.lengthZ".

Extraction Blacklist List.

Finite numbers

Extract Inductive fin ⇒ "ZO.t"
[ "ZO.zero" "ZO.succ" ]
"Support.fin_case".

Extraction Implicit Fin.F1 [n].
Extraction Implicit Fin.FS [n].

Extraction Implicit fin_dec [n].
Extract Constant fin_dec ⇒ "ZO.equal".

Extraction Implicit fin_to_nat [n].
Extract Inlined Constant fin_to_nat ⇒ "Fun.id".

Extract Inlined Constant fin0_magic ⇒ "Support.fin0_magic".

Vector

Extracted as lists for now

Extract Inductive vec ⇒ list [ "[]" "( :: )" ].
Extraction Implicit vnil [A].
Extraction Implicit vcons [A n].
Extraction Implicit vmap [A B n].
Extract Inlined Constant vmap ⇒ "Support.list_map".
Extract Inlined Constant list_to_vec ⇒ "(fun x -> x)".

Extraction Implicit Vector.last [A n].
Extract Inlined Constant Vector.last ⇒ "Support.list_last".
Extraction Implicit Vector.append [A n p].
Extract Inlined Constant Vector.append ⇒ "List.append".

Extraction Implicit vector_lookup_total [A m].
Extract Inlined Constant vector_lookup_total ⇒ "Support.list_get".

Extraction Implicit vinsert [A n].
Extract Inlined Constant vinsert ⇒ "Support.list_set".

Extraction Implicit vec_to_list [A n].
Extract Inlined Constant vec_to_list ⇒ "(fun x -> x)".

Extraction Implicit cprodn [A n].
Extraction Implicit vmapM [A B n].
Extraction Implicit vimapM [A B n].

Extraction Implicit vec_dec [A n].
Extract Inlined Constant vec_dec ⇒ "List.equal".

Extract Inlined Constant vec_eqdep_dec ⇒ "Support.vec_eqdep_dec".

HVec

Extraction Implicit hget [n].
Extraction Implicit hset [n].

Result

Extract Inductive result ⇒ "Support.cresult" [ "Ok" "Error"].

CTrans

Extract transport to identity function

Extract Inlined Constant ctrans ⇒ "(fun x -> x)".
Extraction Implicit ctrans [CTrans x y].