rocq/backend/Extract.v

Extraction of the backend to OCaml, for the driver (extraction/main.ml), which holds each part to the Prolog compiler's output:

the decoder of an asm.pl line term (dline) and the printer of lines (rev_lines_parts), applied to what nanofilasm − terms prints;
the ABI plan of a function (lower_function) and of a module's weak thunks (lower_thunks), each written as its term (plan_term, thunks_term) and compared (term_eqb) with what nanofilabi − terms prints, on the module that command prints first (decode_module, module_symbols).
the code of a function (function_lines) from its plan, of a data object or alias (data_lines, alias_lines), of a weak thunk (thunk_lines) and the end of the file (end_lines), each held line by line to what nanofilemit − terms prints, where it has no todo line (is_todo);
the NFB writer and reader of a module (Nfb.v's encode and decode), held to the words nanofilnfb − terms writes, and enc_module to compare what the reader gives with the module that command prints;
pizlonation (pizlonate_module), on the module term that nanofilpizlonate − terms prints first, compared with the term it prints second;
promotion (promote_module), on the first module term that nanofilpromote − terms prints, compared with the second;
copy propagation (copy_module), on the second module term that command prints, compared with the third;
the standalone compiler (compile, and compile_promoted with promotion, copy propagation and selected branches) on the module read_text reads from IR text, its lines held to what nanofilcompile and nanofilcompile − promoted print.

Integers become zarith's, strings OCaml's and nat OCaml's int, as in the model's extraction. The order of two atoms' names becomes OCaml's comparison of strings, which is by byte; for UTF-8 that is the order of the character codes.

From Stdlib Require Extraction ExtrOcamlBasic ExtrOcamlNativeString ExtrOcamlZBigInt ExtrOcamlNatInt

From Stdlib Require Import ZArith

From Nanofil Require Import Term Maps Transport

From Backend Require Import Text Asm AsmTerm Order Abi PlanTerm Layout Emit EmitData EmitThunk EmitModule Regs Nfb Pizlonate Promote Copy Compile IrText

The hash that picks a name's bucket becomes OCaml's string hash, as in the model's extraction (theories/Extract.v): a lookup compares the names in the bucket, so the hash decides no answer, and the Gallina one took a fifth of the time of SQLite's plans.

50Extract Constant Maps.string_hash =>
  "(fun s h -> Big_int_Z.big_int_of_int
     ((Hashtbl.hash s + 31 * Big_int_Z.int_of_big_int h) land 0xFFFFF))".

54Extract Inlined Constant atom_compare =>
  "(fun a b -> let c = Stdlib.compare (a : string) b in if c < 0 then Lt else if c = 0 then Eq else Gt)".

A nat is OCaml's int, so the conversions between nat and Z are zarith's: the stdlib's count one by one.

59Extract Constant Z.to_nat =>
  "(fun z -> if Big_int_Z.sign_big_int z <= 0 then 0 else Big_int_Z.int_of_big_int z)".

61Extract Constant Z.of_nat => "Big_int_Z.big_int_of_int".

A list's length is OCaml's, which is tail-recursive: the extracted length is not, and NFB's reader takes the length of SQLite's 4.5 million words.

66Extract Inlined Constant length => "List.length".

The IR text reader (IrText.v) takes the file's bytes as lists of characters. A character's code and the character of a code are OCaml's, and a string is filled from its characters, last first, in one pass.

72Extract Constant IrText.code => "Char.code".

73Extract Constant IrText.byte => "Char.chr".

74Extract Constant IrText.string_of_rev =>
  "(fun cs ->
     let n = List.length cs in
     let b = Bytes.create n in
     let rec fill i = function
       | [] -> ()
       | c :: r -> Bytes.unsafe_set b i c; fill (i - 1) r in
     fill (n - 1) cs;
     Bytes.unsafe_to_string b)".

Set Extraction Output Directory extraction

85Extraction "nanofil_backend.ml" dline rev_lines_parts
  decode_module module_symbols lower_function lower_thunks plan_term thunks_term term_eqb
  Nfb.encode Nfb.decode Nfb.decode_input enc_module pizlonate_module promote_module copy_module
  compile compile_promoted compile_allocated read_text
  function_lines data_lines alias_lines thunk_lines end_lines module_pieces module_lines is_todo first_todo.