rocq/backend/crane/CraneSelfTest.v
From Crane Require Extraction
From BackendCrane Require Import CraneMap
From Stdlib Require Import OrderedType OrderedTypeEx String ZArith NArith PArith List Ascii Bool
From Nanofil Require Import Term Maps
From Backend Require Import Text Order IrText
Import ListNotations
Open Scope string_scope
Open Scope Z_scope
0; 1; −1; 2; −2; 3; 7; −7; 8; 10; 63; 64; 255; 256; −256; 1000; 4095; 65535; 65536; 2147483647; 2147483648; −2147483648; 4294967295; 4294967296; 9223372036854775807; 9223372036854775808; −9223372036854775808; −9223372036854775809; 18446744073709551615; 18446744073709551616; 123456789012345678901234567890
0; 1; −1; 2; 3; −3; 7; 64; −64; 100; 4294967296; −9223372036854775808
0; 1; −1; 2; 3; −3; 7; 64; −64; 100; 1000; 5000
0; 1; 2; 3; 9; 10; 64; 255; 1000%nat
""; "a"; "b"; "ab"; "abc"; "abd"; "ret"; "rets"; "phi"; "Z"; "~"; "a b"
"000"; "001"; "009"; "010"; " "; "0"; "9"; "A"; "a"; "z"; "~"; "127"; "128"; "200"; "255"%char
"decimal", und; "add", binλx y ⇒ dx + y; "sub", binλx y ⇒ dx − y; "mul", binλx y ⇒ dx × y; "div", binλx y ⇒ dx / y; "mod", binλx y ⇒ dx mod y; "quot", binλx y ⇒ dZ.quotx y; "rem", binλx y ⇒ dZ.remx y; "opp", unλx ⇒ d−x; "abs", unλx ⇒ dZ.absx; "succ", unλx ⇒ dZ.succx; "pred", unλx ⇒ dZ.predx; "eqb", binλx y ⇒ bx =? y; "ltb", binλx y ⇒ bx <? y; "leb", binλx y ⇒ bx ≤? y; "gtb", binλx y ⇒ bx >? y; "geb", binλx y ⇒ bx ≥? y; "compare", binλx y ⇒ cZ.comparex y; "eq_dec", binλx y ⇒ bif Z.eq_decx y then true else false; "min", binλx y ⇒ dZ.minx y; "max", binλx y ⇒ dZ.maxx y; "land", binλx y ⇒ dZ.landx y; "lor", binλx y ⇒ dZ.lorx y; "lxor", binλx y ⇒ dZ.lxorx y; "ldiff", binλx y ⇒ dZ.ldiffx y; "shiftl", binλx y ⇒ if −70 <? y && y <? 70 then dZ.shiftlx y else ""; "shiftr", binλx y ⇒ if −70 <? y && y <? 70 then dZ.shiftrx y else ""; "pow", binλx y ⇒ if y <? 70 then dx ^ y else ""; "log2", unλx ⇒ dZ.log2x; "div2", unλx ⇒ dZ.div2x; "even", unλx ⇒ bZ.evenx; "odd", unλx ⇒ bZ.oddx; "sgn", unλx ⇒ dZ.sgnx; "testbit", binλx y ⇒ bZ.testbitx y; "to_N", unλx ⇒ dZ.of_NZ.to_Nx; "N.land", binλx y ⇒ dZ.of_NN.landZ.to_Nx Z.to_Ny; "N.lor", binλx y ⇒ dZ.of_NN.lorZ.to_Nx Z.to_Ny; "N.sub", binλx y ⇒ dZ.of_NN.subZ.to_Nx Z.to_Ny; "N.add", binλx y ⇒ dZ.of_NN.addZ.to_Nx Z.to_Ny; "N.mul", binλx y ⇒ dZ.of_NN.mulZ.to_Nx Z.to_Ny; "N.div", binλx y ⇒ dZ.of_NN.divZ.to_Nx Z.to_Ny; "N.mod", binλx y ⇒ dZ.of_NN.moduloZ.to_Nx Z.to_Ny; "N.compare", binλx y ⇒ cN.compareZ.to_Nx Z.to_Ny; "N.eqb", binλx y ⇒ bN.eqbZ.to_Nx Z.to_Ny; "N.leb", binλx y ⇒ bN.lebZ.to_Nx Z.to_Ny; "N.ltb", binλx y ⇒ bN.ltbZ.to_Nx Z.to_Ny; "Pos.add", binλx y ⇒ dZposPos.addZ.to_posx Z.to_posy; "Pos.mul", binλx y ⇒ dZposPos.mulZ.to_posx Z.to_posy; "Pos.sub", binλx y ⇒ dZposPos.subZ.to_posx Z.to_posy; "Pos.compare", binλx y ⇒ cPos.compareZ.to_posx Z.to_posy; "Pos.eqb", binλx y ⇒ bPos.eqbZ.to_posx Z.to_posy; "Pos.succ", unλx ⇒ dZposPos.succZ.to_posx; "Pos.pred", unλx ⇒ dZposPos.predZ.to_posx; "Pos.size_nat", unλx ⇒ nat_sPos.size_natZ.to_posx; "Pos.to_nat", sepmapλx ⇒ nat_sPos.to_natZ.to_posx tiny; "to_nat", sepmapλx ⇒ nat_sZ.to_natx tiny; "of_nat", sepmapnat_s ns; "N.to_nat", sepmapλx ⇒ nat_sN.to_natZ.to_Nx tiny; "N.of_nat", sepmapλx ⇒ dZ.of_NN.of_natx ns; "Pos.of_nat", sepmapλx ⇒ dZposPos.of_natx ns; "Pos.of_succ_nat", sepmapλx ⇒ dZposPos.of_succ_natx ns; "Z.abs_nat", sepmapλx ⇒ nat_sZ.abs_natx tiny; "nat.add", nbinλx y ⇒ nat_sx + y; "nat.sub", nbinλx y ⇒ nat_sx − y; "nat.mul", nbinλx y ⇒ nat_sx × y; "nat.div", nbinλx y ⇒ nat_sx / y; "nat.mod", nbinλx y ⇒ nat_sx mod y; "nat.eqb", nbinλx y ⇒ bNat.eqbx y; "nat.leb", nbinλx y ⇒ bNat.lebx y; "nat.ltb", nbinλx y ⇒ bNat.ltbx y; "nat.compare", nbinλx y ⇒ cNat.comparex y; "nat.min", nbinλx y ⇒ nat_sNat.minx y; "nat.max", nbinλx y ⇒ nat_sNat.maxx y; "nat.pred", sepmapλx ⇒ nat_sNat.predx ns; "nat.match", sepmapλx ⇒ match x with O ⇒ "O" Sy ⇒ nat_sy end ns; "nat.eq_dec", nbinλx y ⇒ bif Nat.eq_decx y then true else false; "str.eqb", sbinλx y ⇒ bString.eqbx y; "str.compare", sbinλx y ⇒ cString.comparex y; "str.append", sbinλx y ⇒ x ++ y; "str.prefix", sbinλx y ⇒ bString.prefixx y; "str.length", sepmapλx ⇒ nat_sString.lengthx strs; "str.dec", sbinλx y ⇒ bif string_decx y then true else false; "str.substring", sepmapλx ⇒ substring1 2 x strs; "str.get", sepmapλx ⇒ match get1 x with Somea ⇒ Stringa "" None ⇒ "-" end strs; "str.index", sbinλx y ⇒ match index0 x y with Somen ⇒ nat_sn None ⇒ "-" end; "str.list", sepmapλx ⇒ string_of_list_asciirevlist_ascii_of_stringx strs; "str.match", sepmapλx ⇒ match x with "" ⇒ "e" Stringa r ⇒ Stringa "" ++ "|" ++ r end strs; "asc.nat", sepmapλa ⇒ nat_snat_of_asciia chars; "asc.N", sepmapλa ⇒ dZ.of_NN_of_asciia chars; "asc.of_nat", sepmapλn ⇒ nat_snat_of_asciiascii_of_natn 0; 1; 65; 127; 128; 255; 256; 300%nat; "asc.of_N", sepmapλn ⇒ nat_snat_of_asciiascii_of_NZ.to_Nn 0; 1; 65; 127; 128; 255; 256; 300; "asc.eqb", sepflat_mapλx ⇒ mapλy ⇒ bAscii.eqbx y chars chars; "asc.compare", sepflat_mapλx ⇒ mapλy ⇒ cAscii.comparex y chars chars; "asc.ltb", sepflat_mapλx ⇒ mapλy ⇒ bAscii.ltbx y chars chars; "asc.leb", sepflat_mapλx ⇒ mapλy ⇒ bAscii.lebx y chars chars; "asc.dec", sepflat_mapλx ⇒ mapλy ⇒ bif ascii_decx y then true else false chars chars; "asc.match", sepmapλa ⇒ match a with Asciib0 b1 b2 b3 b4 b5 b6 b7 ⇒ bb0 ++ bb1 ++ bb2 ++ bb3 ++ bb4 ++ bb5 ++ bb6 ++ bb7 end chars; "hash", sepmapλx ⇒ dstring_hashx 2 strs; "hash.big", sepmapλx ⇒ dstring_hashx 123456789012345678901234567890 strs; "hash.neg", sepmapλx ⇒ dstring_hashx −5 strs; "name_eqb", sbinλx y ⇒ bname_eqbTAtomx TAtomy; "string_of_rev", sepmapλx ⇒ string_of_revlist_ascii_of_stringx strs; "code", sepmapλa ⇒ nat_scodea chars; "byte", sepmapλn ⇒ nat_scodebyten 0; 1; 65; 127; 128; 255; 256; 300%nat; "length", sepmapλx ⇒ nat_sList.lengthlist_ascii_of_stringx strs; "Pos.eq_dec", binλx y ⇒ bif Pos.eq_decZ.to_posx Z.to_posy then true else false; "atom_compare", sbinλx y ⇒ catom_comparex y; "term_eqb", sbinλx y ⇒ bterm_eqbTAppx TAtomy; TInt3 TAppy TAtomx; TInt3; "zmap", let m ≔ fold_leftλm x ⇒ ZMap.addx dx m small ZMap.empty_ in sepmapλx ⇒ match ZMap.findx m with Somey ⇒ y None ⇒ "-" end 55 :: small; "zmap1", let m ≔ ZMap.add5 "five" ZMap.empty_ in match ZMap.find5 m with Somey ⇒ y None ⇒ "-" end; "zcard", let m ≔ fold_leftλm x ⇒ ZMap.addx dx m small ZMap.empty_ in nat_sZMap.cardinalm; "zelems", let m ≔ fold_leftλm x ⇒ ZMap.addx dx m small ZMap.empty_ in sepmapsnd ZMap.elementsm; "zcmp", binλx y ⇒ match Z_as_OT.comparex y with OrderedType.LT_ ⇒ "<" OrderedType.EQ_ ⇒ "=" OrderedType.GT_ ⇒ ">" end; "lookup", let l ≔ fold_leftλl x ⇒ putTAtomx x l strs [ ] in sepmapλx ⇒ match lookupTAtomx l with Somey ⇒ y None ⇒ "-" end "zz" :: strs; "key", sepmapλx ⇒ dname_keyTAtomx strs; "key2", sepmapλx ⇒ dname_keyTAppx TAtomx; TInt5; TListTInt1; TAtom"q" strs; "nm1", match nm_findTAtom"a" nm_addTAtom"a" "va" nm_empty with Somey ⇒ y None ⇒ "-" end; "nm2", let m ≔ nm_addTAtom"a" "va" nm_empty in nat_sZMap.cardinalm; "nm3", let m ≔ nm_addTAtom"a" "va" nm_empty in match ZMap.findname_keyTAtom"a" m with Somel ⇒ nat_sList.lengthl None ⇒ "-" end; "nm4", let m ≔ nm_of_listTAtom"a", "va" in nat_sZMap.cardinalm; "nm5", let m ≔ fold_leftλm p ⇒ nm_addfstp sndp m TAtom"a", "va" nm_empty in nat_sZMap.cardinalm; "nm6", let m ≔ nm_of_listTAtom"a", "va" in match nm_findTAtom"a" m with Somey ⇒ y None ⇒ "-" end; "nmap", let m ≔ nm_of_listmapλx ⇒ TAtomx, x strs in sepmapλx ⇒ match nm_findTAtomx m with Somey ⇒ y None ⇒ "-" end "zz" :: strs
Set Crane Format Style None
Set Crane Extraction Output Directory .
175Crane Extraction "st" tests expected.