diff --git a/.gitignore b/.gitignore index eaf0eed..27d61ab 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,4 @@ build/ *.log *.agda *.agdai +*.js diff --git a/aoc2023/Day1.newt b/aoc2023/Day1.newt new file mode 100644 index 0000000..5c6c666 --- /dev/null +++ b/aoc2023/Day1.newt @@ -0,0 +1,94 @@ +module Day1 + +import Lib +ptype Int + +-- TODO fix import of fixity declarations +infixr 4 _::_ +infixl 3 _<_ +infixl 4 _-_ +infixl 4 _+_ +infixl 5 _*_ +infixl 5 _/_ +infixr 0 _$_ +-- Code + + +infixl 7 _._ +_._ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C +(f . g) x = f ( g x) + + +digits1 : List Char -> List Int +digits1 Nil = Nil +digits1 (c :: cs) = let x = ord c in + case x < 58 of + True => case 48 < x of + True => x - 48 :: digits1 cs + False => digits1 cs + False => digits1 cs + +-- This happens with Char and not Nat, but why is Char working at all? +-- I suspect it will fix if PatLit is implemented correctly + +tail : {a : U} -> List a -> List a +tail Nil = Nil +tail (x :: xs) = xs + +-- TODO I used @ patterns in Lean +digits2 : List Char -> List Int +digits2 xs = case xs of + ('o' :: 'n' :: 'e' :: _) => 1 :: digits2 (tail xs) + ('t' :: 'w' :: 'o' :: _) => 2 :: digits2 (tail xs) + ('t' :: 'h' :: 'r' :: 'e' :: 'e' :: _) => 3 :: digits2 (tail xs) + ('f' :: 'o' :: 'u' :: 'r' :: _) => 4 :: digits2 (tail xs) + ('f' :: 'i' :: 'v' :: 'e' :: _) => 5 :: digits2 (tail xs) + ('s' :: 'i' :: 'x' :: _) => 6 :: digits2 (tail xs) + ('s' :: 'e' :: 'v' :: 'e' :: 'n' :: _) => 7 :: digits2 (tail xs) + ('e' :: 'i' :: 'g' :: 'h' :: 't' :: _) => 8 :: digits2 (tail xs) + ('n' :: 'i' :: 'n' :: 'e' :: _) => 9 :: digits2 (tail xs) + (c :: cs) => let x = ord c in + case x < 58 of + True => case 48 < x of + True => x - 48 :: digits2 cs + False => digits2 cs + False => digits2 cs + Nil => Nil + + +combine : List Int -> Int +combine Nil = 0 +combine (x :: Nil) = x * 10 + x +combine (x :: y :: Nil) = x * 10 + y +combine (x :: y :: xs) = combine (x :: xs) + +part1 : String -> (String -> List Int) -> Int +part1 text digits = + let lines = split (trim text) "\n" in + let nums = map combine $ map digits lines in + foldl _+_ 0 nums + +infixl 3 _>>_ + +_>>_ : {A B : U} -> A -> B -> B +a >> b = b + + +runFile : String -> Dummy +runFile fn = + let text = readFile fn in + log fn >> + log "part1" >> + log (part1 text (digits1 . unpack)) >> + log "part2" >> + log (part1 text (digits2 . unpack)) >> + log "" + + +-- Argument is a hack to keep it from running at startup. Need to add IO +main : Int -> Dummy +main _ = + runFile "aoc2023/day1/eg.txt" >> + runFile "aoc2023/day1/eg2.txt" >> + runFile "aoc2023/day1/input.txt" + diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt new file mode 100644 index 0000000..1259e34 --- /dev/null +++ b/aoc2023/Lib.newt @@ -0,0 +1,133 @@ +module Lib + +-- Prelude + +data Bool : U where + True : Bool + False : Bool + +data Nat : U where + Z : Nat + S : Nat -> Nat + +data Maybe : U -> U where + Just : {a : U} -> a -> Maybe a + Nothing : {a : U} -> Maybe a + +data Either : U -> U -> U where + Left : {a b : U} -> a -> Either a b + Right : {a b : U} -> b -> Either a b + + +infixr 4 _::_ +data List : U -> U where + Nil : {a : U} -> List a + _::_ : {a : U} -> a -> List a -> List a + +Cons : {a : U} -> a -> List a -> List a +Cons x xs = x :: xs + +-- TODO where clauses +reverse' : {A : U} -> List A -> List A -> List A +reverse' Nil acc = acc +reverse' (x :: xs) acc = reverse' xs (x :: acc) + +reverse : {A : U} -> List A -> List A +reverse xs = reverse' xs Nil + + +infixr 2 _,_ + +data Pair : U -> U -> U where + _,_ : {a b : U} -> a -> b -> Pair a b + +infixr 0 _$_ + +_$_ : {a b : U} -> (a -> b) -> a -> b +f $ a = f a + +-- JS Bridge + +ptype Dummy + + +ptype World +data IO : U -> U where + MkIO : {a : U} -> (World -> Pair World a) -> IO a + +-- TODO unified Number for now +ptype Int +ptype String + +ptype Char + +ptype Array : U -> U + +pfunc arrayToList : {a : U} -> Array a -> List a := " +(a, arr) => { + let rval = Nil(a) + for (let i = arr.length - 1; i >= 0; i--) { + rval = Cons(a, arr[i], rval) + } + return rval +} +" + +pfunc getArgs : List String := "arrayToList(String, process.argv)" +-- Maybe integrate promises? + + +pfunc ord : Char -> Int := "(c) => c.charCodeAt(0)" + +pfunc _<_ : Int -> Int -> Bool := "(x,y) => (x < y) ? True : False" +pfunc _+_ : Int -> Int -> Int := "(x,y) => x + y" +pfunc _-_ : Int -> Int -> Int := "(x,y) => x - y" +pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y" +pfunc _/_ : Int -> Int -> Int := "(x,y) => x / y" +infixl 3 _<_ +infixl 4 _-_ +infixl 4 _+_ +infixl 5 _*_ +infixl 5 _/_ + + +-- Ideally we'd have newt write the arrows for us to keep things correct +-- We'd still have difficulty with callbacks... +pfunc fs : Dummy := "require('fs')" +pfunc readFile : (fn : String) -> String := "(fn) => fs.readFileSync(fn, 'utf8')" +pfunc log : {a : U} -> a -> Dummy := "(a, obj) => console.log(obj)" + +pfunc p_strHead : (s : String) -> Char := "(s) => s[0]" +pfunc p_strTail : (s : String) -> String := "(s) => s[0]" + +pfunc trim : String -> String := "s => s.trim()" +pfunc split : String -> String -> List String := "(s, by) => { + let parts = s.split(by) + let rval = Nil(String) + parts.reverse() + parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) }) + return rval +}" + +pfunc _++_ : String -> String -> String := "(a,b) => a + b" + + +pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => { + console.log(lab,a) + return a +}" + +pfunc unpack : String -> List Char + := "(s) => { + let acc = Nil(Char) + for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc) + return acc +}" + +foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B +foldl f acc Nil = acc +foldl f acc (x :: xs) = foldl f (f acc x) xs + +map : {A B : U} -> (A -> B) -> List A -> List B +map f Nil = Nil +map f (x :: xs) = f x :: map f xs diff --git a/aoc2023/README.md b/aoc2023/README.md new file mode 100644 index 0000000..c56658b --- /dev/null +++ b/aoc2023/README.md @@ -0,0 +1,2 @@ + +Attempts to port AOC2023 solutions from Lean4 to see how usable newt is. diff --git a/aoc2023/day1/eg.txt b/aoc2023/day1/eg.txt new file mode 100644 index 0000000..4cba7d0 --- /dev/null +++ b/aoc2023/day1/eg.txt @@ -0,0 +1,5 @@ +1abc2 +pqr3stu8vwx +a1b2c3d4e5f +treb7uchet + diff --git a/aoc2023/day1/eg2.txt b/aoc2023/day1/eg2.txt new file mode 100644 index 0000000..41aa89c --- /dev/null +++ b/aoc2023/day1/eg2.txt @@ -0,0 +1,7 @@ +two1nine +eightwothree +abcone2threexyz +xtwone3four +4nineeightseven2 +zoneight234 +7pqrstsixteen diff --git a/aoc2023/day1/input.txt b/aoc2023/day1/input.txt new file mode 100644 index 0000000..495c9b2 --- /dev/null +++ b/aoc2023/day1/input.txt @@ -0,0 +1,1000 @@ +four82nine74 +hlpqrdh3 +eightsevenhrsseven988 +324pzonenine +fglpbone79fourvrgcmgklbmthree +fmbbkvthdcdmcjxzclk42six4 +four22xcqsnvktnpfshtmm +qmfsccxsixfivelnmpjqjcsc1sixpfpmeight +eight1nine5nine9six +s4r91seven +6pspkslrnxpplkhgqlcqfour +sixeightnzrzgjvsrnmtqgx5 +sixtwo1 +h6 +five8pbcsllrbvg787 +dpfhfeight28onefourtwo +vxqbtkxjtwoz3seven +8ksrcjrcmpbq9rtvtvrbgljzqvbnxddnzt +mpftpsgp6fourvdmltwojd9 +2fivetwosix +3qqx2 +jsbdh16snnllpvvgnggfive5nhjpgdzh +4fmgmmbonegtsnqfdqt1pm +2onendvlmcrvzsnpr83nine +8ninelfhkhnqtdfour +8reight +84gnprjhr3eightsixsix +1nc7two +3zcgkgrnd1d4 +nmfqfivervqkxmkdpnine51 +1fdtrptkb3 +nineone7kks +ninelzgncpeight966427 +eightrsniner9 +nine7two4 +253slq +lkhthreetwo982rrc +fivegdsfnfour64sixtqfour +dkfdtgnine9 +1six15ninebgnzhtbmlxpnrqoneightfhp +32fivefivexjvckfourseven5seven +onexxzvptxkn42eightvsdgszdjgp +three6sevennine +mvsrflqjsix22lhd2twodkltkmsk +threetnbfsfxxhseven51cjvmkvzkdhr2 +11twoxjszm93 +trr62fivedvktlheight19 +4hxthreepqptvkkzmfsevenfourxeight +5shqhrjtdgsninepblpjprtqptz +ptwone9kzvjhhfive7qjsblztmfvthreeqrhhmbgjpqrgqhcgzntmvskhh +xltqzgqxbkq7krgnthtqbm3636 +nvvxfxbgldrb2seven7twokxzbfkvptflnhlqjrthreeoneights +7fcvckqszbj +eight1ninethreeninenbmcsqtrl7 +zkqmlqmtszrbvnjnvsevennine9sevenqjrlxqjlql +428 +8seven16nineeight +24bkfzsrxjtbzbknqqxtfftzlnrkeight +two372eightnine +skxf5zpnmzqgvzjv9sixtwo +1fivedsghrseven4 +8hmb75twotwo +2hsnpfourthree3h88cz +6qkqxszvghrdslpckhfivedlx +pnxvtbflleightjpfzlqxhr22ckjrnzhnbvdnj1xnfhmb +cdscn4xksngscvnseven +65oneightpln +ninesix11six41seven5twonesl +f411d +sixonedqppgfdfbthree1sj1sevenqhdjlg +eightsixhzshtg5oneone +tbhdgzphkkvbbclmhgvb3three +dpsxdfmzstpd7rzf3 +kzpctbr3oneninevgcxcvsconeightgk +blmpjv6ltxfqsqfjnjgxtseven82 +99four +onexsxs3sixdnfqlffjnnrfive +4sevenzdjvrqjlx33 +brtbqvzcdtlkn83sevenmmtwo +5bnlmjtmeight +twotwofive2fqbfvqhp65eight +dstwoneninekfourphth4lrfjjrh +mqsndqcxt3 +5mbfxskgnh1twoqbxfbcjkzf +6fourzdcmdl78pvxxjrplmtmvhh +3mzgttvpt8gvzoneseven21 +8253fgfhpmponef8 +nineninelhntskjvd25 +1czbccmrlch27three +one4l5four +sixmcnsxf5two +onethree2five7vzhctscktrcx +14szp5fqtqfzcd +6cgpzjprtsjd8five4vjzfhgkbbf9 +7gt +4lzx +fonexgjsnine8 +1twomvdvdrrneight8fivenine +59eightthreesevenctwon5 +2dxfivenqflqppm3bmtmblbkltwomc +36mplfgblgff6 +threeseven8gf9sevennine85 +hfssbghbnonesvdm7onekssjbthxjjvnqmcgmrcx +eightfrbrstlh8 +eight34sevendlhvhszcnvdlvctkdzsgq +seven2eightmtsmflrx2three44rsk +fg6 +mbf44 +5926386nine +48vqvcffsq2eight7zktszfour +djstrfnqsixone8oneightc +5seventwoqtr3eight5 +dttwo88three +8rdxmnrtmt +r2tzcbr867onetwo +2v489four2 +vsmfszr5 +84nxrm48 +5cp4five51three +four3six3 +4zglqmdngeight1sqb +3twosrlvbzfh6nkrhmnjqeightseven +eightgjhs276five +j15one683 +hnnonefvhnxggtwoz2five +threeseven2fourkltqmthree +bmksn4 +11ntrt +5tctbxqjcngdhffqqrjfive +vcstnf1 +98tgzlvtwobjpxj6 +one6j5hqgbvhtmsjkbt7mglhvjjxmtwo +1sixq +three8lbqdd38ljfourtwoccntjgnmv +two5msdsntdrjl4six15tdpnknrxnine +sevenzkbfmqxb2sixsevenbvnbxtxvfournine +1nzdfninednkhghlscsc +onefive3gvjsqqgx7seventhree +8dglgts4slg5sixninevzsj +dxdmkshgssevenfour967ninetwo +4ninevrhsbqnjtwo +358fiveseven +two8sixzt2 +93ninefztjqrhdlxxsjnnflczbsjqpkrmsixtngxqk +ltpnkxtwoeightcfpjhthree5brzhffour +four3five6q645qxn +fourjxqghk6 +8dznl428nine +1djftqndtmkcbptxs22 +27one +543 +qgtbvgnl4tzfgch7zqtmpsix +fourxfgqcsgxbg741922nine +two4sixmkvkftwo5one +lrlnnbdzr82g58fkgvfninezmqv +2xbkhjbrlztnphmcsfcln +2xlxksqkb +rcnzsrtfive9scnnvqx6kmkvgmxlpqtkmbjtvsfmvseven +6oneninekfpnbngn2 +2nnxlthmxqc9eighttcznxdchdthree +dznqtbkgtwo5zpthvsnone +7nxjjzhfhpshccknpbpttrjhqkxmmssvtlxtmbxlhvtjczone5twonecf +96eight +7qvckkdtvzjd +14nine1two +eight87one8ncdzkptqrgtfclsevenc +8fourfive +jjqbpmp42589stwosix +vtrbqpv9sevenone1qlvmzkthnnsevenseven +pxnxptttxh6fourmbpcldrlfnjtcxtwoonefour +8njghfrsix82 +gvns197fsgtwo +9sljnsix8 +rnine7ninethreenjxnrqgzbxbtvrltbss +4stzbqg44f +3ninesevennvvdmgkxzmttcxfbsvjrg +eightsix3twofmnvs +one2fmzxnhhrnvlttxnhbrjsgjsqkvfn5 +qz9ptnxfngfrh65bvvbhtsrsntczgj +qfvqfpb2txnxxd2fiventvznljcqj +fiveqvmzqlgzdbvqzjbllzeight5bgt +qggflvv753clcqqjqmngdm6onefour +3fourfiveeightbbgcgtwo857 +one5nineeightg44 +6zmqxcl16twofivedjxhzmhffive +jnnsixsixtwo2bgsnbrzlnlltb +six63oneightgdg +pftmhdnqdgfive1three42four +8hkcjlskh82 +84 +1ninefour9sxmppxjqqxpn +ndrgrhsp1gxcrfgxctv +fiverzmcmbqd78gqm +fiveeight4 +vxktmrcdlsfiveoneftvqnnvjfour8sixlmldnrceight +hpfprllctdjtwo9ksszn8eightcfdbzz +nine5fourfbgf8one7t +8sqxm5 +6fxcxhn +2prktdcvnine1 +2vqrlpffvjlfourktdhxxgvonedvnsvlld +qk7294fl +sevenfivesevensevensn4 +rnpqmrgczhllzszvkfzmcljzpthree8 +fdcqknlctq74 +1xnvpvfgsbslkkktxxhn +one5eight3zrldkdj +nlvgbz71fourk33 +sixfourfour6three2three +7lszpqqq795nzdfxbzsqlsix +one8nkqdtctsjj +7xfphzjzndr1 +keightwo25hmqthbeight +2sixdm +l4eight1fourfour +2ldzseven3eightmdmsgkrrfivetwobbzz +mtwoneonezdfour22two6 +7fnjbjqdxvkntlfkhkvnzt +dhqsqnslccxgdd63x +nine6fourthree +7qzbrpplm9 +pqbdbxxxggn9fivebfttnine +58h152eightjmjqlzjjp +8vjrtblqzsx +7sevenonesevenhqkvxxsvrsix +four6hcxdtwozjnpsdtpzxxninevzvsxffxpctcjbtmlm +3xznljnjz4ms3seven +8892 +3jrzlmpnxhfivefivetwoseven7 +onethreetjpmpvpr6threethreeone +one5thcfourndbphpxszjmt7eightwof +r5s +fmjzjqlnhxqhvbdvdfbdnb4 +nine9mrqdgnkc +nm5jxpjgsm31stkvxjseven5 +hplgpfrtlb8dgsbbljfdgknfvqbonexbcddflz +4bmfrjvj81vvnztchfrjfive +xvvb2nfqxdmpzjvrbmvvtmc16 +txrfivecjq6hlgjbvzp3threefourone +sixlthreeeightn9hqmxhxfjrb15 +six6eightone3 +9six7 +nineoneseven2eightbr5nine +sixqqdsdmtkgkfq9 +3fivefiveffive +8eightfive2six +7rnlhrhlfive +kvkrxgkk6one2ninermqtpbbnmpdpjxc +nhltwonesix3five3two45sixk +eightsmjnzfzjk8 +sixhxsprkfour5b9 +vkvhvhrvbnvz7rg944 +ccvzjppvjtthreetwoqdc4eight +threefive9qlg3hkhvrbdxzdthree11 +onesevenczvffoureight28 +three39jddkzzjninetwo5 +63nine3sixlqnbtrq7jctmgdmk +zxsqngxxfd9rvjjt14978five +9983eight +sevenddfpzjp3skz +bzdpg73eight71ppzkeight3 +onevphctjs4 +twofive2jxsthree8sixqeightwozrv +6klpdhhsdng +thxtwonefive57rpseven2 +qtcdgdfj77sixrhtczdcbp3 +seventhree47 +threekjqqht883 +two3jfgsdnqbxcbzjtteight +5zcpgcgsixdskfszmmq9hxtknineqmhg8 +snjs1lxkpbk5 +seventwo7bknk9 +rstbvlzlk1tpqjsjmhgdcvpfdqzl2bcbtn +3eight4six2 +twonine8xkqp3eightgheightxplcqbvppj +ninevkrvzvseven6eightcmmvgzb +77n7fourthreecrcq +xlvszfhhffhmvxfour8skpvl +9nine3kfhgngkd1 +sevenfivesxdxhtkmeight4 +28four92 +mjzm465qffive9 +dqlghfxbkfourfivegfkmgmdgzxtm1 +six13lrc +8qbvnhbplbl6 +13lmgbfsgnxone1 +ttdznnjsgjtwo5 +eightfourtwotwoltjxfourone3 +8threethreeeighthbbxfbmpj611 +ninekpjcrvlqbmsixseven5four +8jmgspsevenfour7 +6nineone5hthbrbsjrhbnn2 +ninezzdlfiveseven4 +fhrxvsevenlvnztq4one +cvmlmzz8njtfztfzfoneonejbckeight6 +ninexdgtgjjnrb1hrhjvchm +63gqjvjtmzgkpbfthreesix +fkstfchxcbrkfivemzhfdhsffd4mnbbmgprxcgmsl +87rslqkvbzncfxddt +7fiveeightxqjhdkbbgdjksn +four375 +sixftdrnbzq84688three +eightseven8kqdcbgtmvlsvxx24fqrfp +four7vprrmq91 +six85ndzvnplxhkmrjftsixeight +5twofourzfdxbffive +4jbvmpnqcpbdfrkzone9ndcxtgsfive +nine3jzpsrhb +nine6cpqsfour +78kzczxbcthreesixxtdkflhzfour5 +14sixsevennzgfnmppnmcddd9six +fourncvgmhfl2fivefnlndmj +rzgqvdgksz6six +23seven2rhlv5 +9xlnnvnvccj +3fivethreembplpfdjnineseven2 +jk1 +3threevgklhnnnccrmone2 +threefourfive4 +qtpbdrsix67threekslkmqt +five3ghvqnrhtbqnvtmdlnine +84lvnfx9nine +nine7onethree46 +vtshvtcch5kxkzgkfourrtmbq +5czsbzl3threeeighttwo +38nine +twovcxn9sixklflgptlkt +fcjpjrxdleight87 +cfn6 +sixfourtpzpnsvghlqp3ssptlls +trsjxmzvhxgvtzrhxqbb66nfp1knf +twosevenmdmmcjjgxj96qxrqqteight +sfcpfs9dpkvxrmjfiveseven +6dblskzfsrpcnszqtwo9rgrdkjshb5three +5fourfsblzr3onesix +gcxsc9 +txjtwone12 +twovpgthxxrpsevenqxpmlbrr3three5 +csqkgmzl93xrxjs64gptsix +33qjjzgjtrsflgpr6 +twoeightseven6zdtdltvzsxvlgsevensixpmxlfrb +gjnvdxbveightone8two +24vjdfhninezfvlgrdvsh8 +ninehn1685nineone +twoonegsix4threeninezrsnvrltqlms +5cdfdldjxddrjhncxtsndl8 +1mqg3nspfxnkfoursix9nine +1tfcrfpqmk1stfrrnrz +721dgsmsixjtxcxmj4jhkdsfj +9plbxnrnlgsvtshfgzbkfive5qfbzgrxzk +fourgjdt2 +ninethreeqqxrjjgskm1fourseven6 +rbrr1 +threekrslrrqngjtwo6 +llkbxgqp2cmnmgdfgrcshlmseightgjzs +66sixeightthree +64vdnrrqfxonespgfhzdcdrbrqone +threervnhkgdg7oneeight +nkbrvsvlzkonermsvxh65dlvxbxvlnq8 +twozbkclqppd9txxzbvfppz3 +two9nine +7vnlqfgxlmninek2two +qjzggvqj1ninefourrc2szbmczr +seven6kfkkm7 +nqlgfzmdfsevenshvcnxdjvxveightfour9 +seventdrqkrxkeight75qjfbb44 +four3cxhlvthree3tcvrzk +six5seven2 +3ninehcsjfstwo5xsgmkz6 +3fourlnthree1fourseven +lsxzsskbsqmeightcrddxvxk93fivevfshztv +nxqxrsevenl3eight +239fourjcrffkeightfivezmfsvqvpz2 +hprcp6 +rklbzvhll4nstdjb7fourthreeonefour +9jlnthv +65six4dvtftwo +nine5five3kqvrs183 +sixrgtckzc7nmczdx8three2 +4six61pzjhnhpbnmsq +1fivembsixsevenddmrlkfour1 +qhgxrbnfc8one2vxc +rdsttzt1sixonefive +lsdoneight5pmlztbkvzffourfour7 +7g3 +3sevenlnjfvms9two +dclkonefour5 +tskeightwo9one25ddmdmkqrpffoureight2 +rmkqgbh1slrtshgkgbdsftvbgm4 +qkhxmpfzf51 +648 +three4gfnxzrs2 +hmcskdltfourllp7sixfiveszgnfbpjt +hf27ninep1fqdbglxngkf7 +seven6bfhtdztzvqhqnj2xfxchxpfc9 +8vfksvbfive9lxjhcfive +626txvseventwo +1bgzkmzx1 +nineeightlzv2l +8ninetwo68twohhntdvjpzfone +jsjfive535fdfnj3 +fnzrsevenhcgzccslt92twonine71 +4twothreemx +6vbtgjssfoneqpsrdfrbcgmrfckfourpzdlb +91svfsxrseight +nzmnpbdqjdh2four +blqjhjxplrxsevenonefive13 +fivef11gtdpgbdrxnbtrfqxfb7r +l5fivethreenine +oneffcdpqmvpcdcn6six944 +4mmfjltf7 +29threenine26 +8zrthtv56 +c21hxksz +nqcbjkb7 +fourxtkrn7bvpbqtcg78 +qjvmvzbkxlseven756 +6g31dk1mnsgxhbdvndjgvsjr +73eight +61jlzgrrpkvgdpjzbbqkxp +3368nineeightwodzl +9tlqcrxsix7 +cmrrnf8five1 +4three72 +hhcghmtvznine6nineseventwo +22tvjnfvzshdtpxzxrnzvtwo +8threeqlkxrkfsevenfivegxmbhqg +5mzzsldbk7ninefourjfjv +rloneightcjhxsstwotwombktzlkdxtwo8 +three92nine1sixeightwof +drxgb14twoone +7one7seven258nineoneighthkd +4four4sixninem +fivejkjpdbfpsttjnpkv4one8phckjllc +5bmeighteightgkjfkjthree +98lkzpdnvs7chnmkxzql +twosix2two15xzkpmctwo +951 +four481six +3tdvlonefiveone +88fourgktxksmhninecfpljsix +cphlzlx45fourxjphtthree +6eight4gfjjdvslqv1six1kxlmn2eightwof +5vxrzxgdpg7vrsrxrrhncfour +5threethreemrzfbjq +ninecsg9lseven828bjttzx +5kqnine +fivetdhxq39 +rcvlsix6pqzsggz59 +47fnrs +724onesixtwo +tdbb7 +sevenseven4 +two7mlzgdqthree +2gxzbnlrglnvmqmzbznfngxfeightnrcrqsjnftfourone +fivetwovsbvrfour2ndmltmprsqkbbztwo +j3twoc6mmzt +six47nine6tkpjleightwopzf +sevenmshrczkdqfiverkmhlqjzqqhgppbsm58 +pkbgvlvzckvone26rfqbmtwo6 +sr9qsxjnine9zbc6three +eight4qxlmtwo27threesix6 +fourone417oneone +6fpvfbrrtwoeight +79rj4eight88 +6vhfivevrj +7tmqhchfive6jxgmqcfmq59eight +threeone3xqcrjzszhseven2csbflgnds +1qsxxxmsknhseven3nine +fivemqxjlggcnsngflb5qtshllseven1onefive +7476qfcmqqbfhvrvksfztskmzgvjjsrsc +twosxlbrgdtptwo16 +kffmtjnjjk2fourtgv6rvsrzcvdrklplndseven +eightzhrfgpjfqgccn2khrfdzfour28 +ninetwoxvnhfdjsxslone4four +92nine48b +ptwonefourclthree56 +hshqjfknineeightlkdxvxcsljfptlbb6kt +fxjbr1four +nine36gqbt6 +nsbcvzninebvlpvlx1three +1ltlxzlmzxhjlfvtnrrpdk +3jpqgspseven5qm +553npbeightxf +fourbspjfbxk4 +238 +xjrsdsvgncxddpmj3tlqone89 +68bkvsslntwo +dxcmpjfprnthree98sbh +reightwoeightseven76xqfhvbkfouronegkrfvdzzdx +9lfpjff +gcvs5 +hnctpgpxdlvklfsdfour2hnvtklhgqxhjpzknine +ceightwoninefivetwo9plndfive4 +pjnzdrhtddjgllbf9f25eightb +fpsdpfl8cnhkjtzhfbhdftkvm +3cqqkflmjmpfmkk79lvkjljd71 +bfpfmkjpnkgspsz7nine +threethreetmpntmpg3lfzzsrzr36plfvxv +nvssix83 +dznrcvvgb8 +csrffxrtvmpfgbkcmmdlzxneightzvfgxdpljpcnrcn5 +9sixtxxthree +seveneight2kpzpvvtzq8 +jbmmeighttwo12seven96bcvcs +b68pvjcsnine8 +4vphtk7 +mxmjvnbqseven2 +3two2foureightxvvtxpcdmsdzvkg2mthmx +cxslpdtnnx5five65 +97mp3qbkxmhl5dkphzgmpg5 +7f11sixcnrqone +8fxjdjxc6drjxnhptdeightseven1six +sixffvgcsfourhmnrf8 +qtpjrmlgnlkbbbr7sjcpm91five3 +5pqv69one +eightnine8 +1three8 +39cspknxbsjhtfourpcbqsvlgz +5nine15 +zgjgjfcdphnqqv4eightsixsevenkv +6ggfxblx47nine2onenine +1twoone2xfxfcr5 +sjvpxd7ncpclnc57one1 +4sixdgone +89ptctqvnpg +threefour1four4 +8seven5pfeightfive8hclpxjgftc3 +mznfsbmdtltwoqlf9 +425 +n51891 +one5l +8ninefive2jhhbnjsvdqtlmsjgshvlvlh +58ggdlkpcmkgeight2vcprcttwo +twoseven3eightfivesevend +krrzfivexrmvdtbr1zvqpmthreeonenqnmx +2sixhjpxptnthreezkfsix +jchkkkgrdmkvdgksevensevenfour8five6 +1tzbzthree +xkone7zvgtv5qvln +6fivetwohjblzsixnine +onelpgkpggl9nsdxtgh4tgjfgpcsn3 +bjdxc7krrt16xbgvl +sevenrpftshchmkkflxseven4eightsix +groneightfftfvk6 +hrcshqtxpqgxeightsix1xxxrczpcr +foureightthree9sdffivebdtrng +ninefourthree9eighttwonine7xjrsm +fivefour64 +51onefivetkcdbbslzmeighttwo8 +4rssgjpzgnczqtdrfivesix7bjxslhzthreefive +5kgkv7ninethree +84ninepsbvzkgrvqpzmtqgmcxpvgfbffns +fourrvdzsntddfoursevenqq54lgdrtdcq +4nineeightfdh +9twoonefour2kmnb9 +qcvmnq13tsptksgmqj8 +113twonine4zjsbtjkpbdsix +sevencvnineq6jvnshmg +pjhmbnjqflvp452sevenfive69 +2three1sixninekmfcsbsevenfive3oneightg +six3six62onevrhtsskzrhtthree +5bxcmdnrf1szdgfournine +fourxdxmk6 +3lsnfgffnlrqboneeight +9sfsv4gqhpbqg86 +two17567fournqkmh +7threesevenzgxvkhf +vlmz7sevenfourfour8bqzdrdktklfivefq +xxsvcqqeight6flrffzxpfourkzfstj9 +fourlzpdxg3knxgl +msb246fourlc1crhlbjgdgr6 +1q1cmrmqponeightd +twoeightncz513 +nine1nine +8sixonesixnine +193sixthree2rgthk +tvhqp44hmjhzvmhgrbprgttgrt +52bdszlvsvgzonefiveeight +sdxnpkllmnninethree5jxsgkdbmknfrfvthree2 +six23hdzmppf67threeseven +eight5nine76vbggdlp +4onevrxnnbszk +9ninezhdsfbfive12 +sixnine5xqmkmthz +fiveskklnrr13sevenfour3nqs1 +sixqcxqnjxxzqmdlqtwo83 +8eight7 +9psvqdzpchr +492jseven1 +xrccslcthreetsnfoursixsixsix1 +gskqmvnclfgxbtcq9hsix +5two4twofive +sqqhrvtszzjs1vfskhsdsvvhlskn +nineseveneightcjcgnb9three3xfkst8 +ktwone4one73 +five6xncdddspkcbgklzlzn687 +xgnlvnskgklcpdqvks2 +zscmhb7mrrshccm +five8hplscnineeight +2hrgc86dsgjbvsrv9 +8lncmqrxcnm9ctpxjxlz8 +jdqt39336 +1gntnqbstzrnine5cqlrrtfllb13kfleight +3jscjlvvkd89 +5nineseven66nine6twoonetwonek +sevenxrqj4bfivesix1 +8msix8 +six6ninesevenfourbttvtt66 +4cmvvdfdgqphjzleight +55mltlnxc4dmcrhjsjc8seven +26197jtlvpsixcmzkslvzh +rjzn2 +krlvgxone54hdddkspmfkpnzcbtbz +four2two2 +one5vjjs3one6six +6cmt88three +reightwo7lrjqxbmgjj3seven2 +ntrkndgqzpfkjrone9 +5dvktjpseightxxmbtrm +four6seven9936six7 +fourhqstnjbbdscjngp5fpxmg +77five +qrzg9five1qqcsonekgvckmmpfx6mpxd +qzjqstcll7donekkpmkgpdthkjclrpth +14seven +bpbfnnq4rpppcjfeightsfcsqzg +2one7eighttwo2vhzhjpgg9xhsdvlgxf +eightonepn38ztcqzbthjz8 +lnsix7eightskqhrbx +sixvnpkpsdzsbjgjkbxreight8five4 +vfrvkmnvnhk5one +eight9nine7 +oneone5 +7584zprfmjtwo1 +4szpqtwoflcr9bhtthreeeight5 +385 +ninekdqknptxhsevenmrmjzqjvnppsrgbkv9jeight7 +5fs1sixeightthree +sevenxkvxzqhckfourninetwo3eight +9eightgfjvv +xh8 +brbs3fiverzrtwo4jtdsvrljxone +qcvfnlvfivetwofourgsdlcmkb5 +klnsqmblkffsq4threetwo6 +nine4eightx8eightwohrk +c1 +sevennine55eightttlbshbfive3 +6ssmtjnxsixthreengrlndcb3 +vgpq8sixsix +96xhrnine9 +grpsjz1zqzthreeone2four +r6twosevenrdmczdz +jdjz4ninefour +one88 +ninerzdfc8rxnfbpndznctqd4tlb +cshoneightnbdfmpdh2fnvjtxtshseven +gtpljthree1six +63eightfournncq +twoonegsdpfkfqdf7 +xccnnscfivexbqmxfouroneeightgvndxgnine3 +mktvsff76bfqkq9fivetwo8lv +3four5 +qhdgmcninethreevssbxqbsd35 +one6mprksdcz6hpxhrdznfpkmp +six55ninernnmmlgmblttbgph8pqrjtjhtdj +jnpbmnbqonemjcsgbg1 +9eightfourmkknzgmqh7two +7five9 +2eight44skdlfbhfsshpvhgfseven +2cqrzrhbfn +three8419two7 +rvpblkzgkmxkghsbfn3one +nine58 +74spkcfzsdmkf2six1 +2threeseven +sf84qnthree5bmxnrmqff3seven +oneonecxxv96 +gpdbgxgjqzdzlxgqphdr63twofourkspvxmvrfx +fivesflg9fivesixonexfb1 +8pc56fourqpqmfour2eight +3qvgqqldcr8 +tssixfourlbqstcmj1 +pf2sixpzxcpmxtp7twoseven +5429 +drtlhzlqltwosevenfivetwo29 +eightlqtfronebqhdh1nineonembxnbpgg +vlvnzcpbpqeightjspbbqqeight6 +sixkkmgcnhdfldplzk3five +93ninekcmgjm8ckqjdz +3dmskrqjd9 +five5threefivesix +lgvbpdnp8oneeight7eight +seven37 +2onesixtgbqbnn9eight +5ndhfjrvt5fivetrhzsmqtwo +bdcrhzdr33ninefive9 +cgsdzcninetwofive6one +fiveljbtcqcqdglvjnd8onefour +two2b5lzbjsqx7 +three593sevenfivetwovptpnmxffrkbsp +sixonesixthree8btmzlnkvxt +2jf59 +eightfivethreenine57qpdkcfr +eightsix31threeeight512 +fourseven2twoninenineeightone +pqtnqdtsix1 +3zpnvhlsjcmcdvzzlqp5 +sixvnmhckrzxfmjglc964nine +mftxdnhdzmfnrgvvz59nlhhvr7spjrh +eightls148mmvsjjldzlmvxjd +3five5mlfhszsevensixthree +4zpllkssevenfourtgbhdkltwoc +ffourhnjhmtxxfjg511 +63jddsfqsmjdmgxnthree3four +eight3onetwotwo7 +fmfour9tvfourfourtwonef +qseven91two2fgnzcjnm +rpzmsseven1jcxvxgnvthreeeight +onefourrflrntpkskseven1kthreetwo +5lpmhn1six +ttvdgvf67btpqbslt +3twovkbrhqsmv2lzggdlbfvgonenine +rstknqvqtwo55sixjpzmgjsm +nkgfnrxzj7jszsixfiveeightsixfourflqlzmhl +sevenbbbmdgbv9oneightqg +mzmksix42oneonexxmndklncn3bqj +3xxcsfonefour +1threeeightnine46zzscxblntplpd +6four77sneight +pcjxrxtwoseven71threethree +5spmqztljvbtthreefivenineonesl +6zlkxrbhlgf6 +228 +2seventhreesixfoursrhxxrcd +vhkkr33 +twokzcchqdmpf3 +qrz9 +8lfkxtknx +76n +dpxthreeqgtjsqs33pzjxgrmtck +1xhhdhqv6sixlcgfour +four9chmvmrqmfq +one5cvxtvjc96three3 +one6eight +sevenxdncpgzqqv6five9 +fnlrctrph4mpdninetwo4threedm +one3nine5two +8prrdscmtgfivecsnxjrpssix56 +foursclkcvrkvkhrbnnchlsbllfive6djnprhmkxfnine +five2twojknineddzszxsgxxgzfour +9532chktx5 +two47 +42sscxflsevenjssjmzn3xgzpvfsneight +7fltzgtkmqkgjj +1one5six +6gstggspddlninezrzcl5eightqdvjlgz +eight2stxftmtsbn +vqpqvbjvgklxrtvnkgsvlljgxlpxthkeight8fp +sixpjhzscgthree8eight +vgxfxhssbsixfivehxllx9 +nrszzljfrthree8 +dvthfklrvtworxtvhljnsqnbcnpj5eight53 +76threeqclnine +eightvdc7one2four +46five1threeeight3six +five52k557sixxctdrb +hk2twoggmfchleightxnshxrcvncbxvrzhone7 +21rpnnttwo4fivefivedvtpfmnbmg +onetkgkv14sixdjfznpdrvl +onezctthreemfnqcczxpffz2six5 +kzeightwovrtjp94vhn9mjlrxqm9xdzbvgqfqt +34one17hl +9332r +zeightwottpsrgnljcmnglbfsxdkgffrlgm6jnzvkxn9 +pmzdljpgsix7 +zmhxkpskqzgrkptwofour4 +pkoneightsix7 +9695tfivexmspcgz +ninerrlfckbs7vcmbhkninelbhfclninesevenbppk +78k2qhvkzgkgkskhfiveone8 +ndxnqczhlkdvd97threeseven +jmmdfvftbeightone8eight1twosevenseven +five9six98grthvvqdjbrkxn1 +4qxvqfrkgnfcxkkdm1mnczs +n3b +three9bzfour57 +8threexkglxf2 +onedxfivedxvgxjmzkone3kbmplxbkdnpknjzrbmt +nine3two9fivefrmjgxkrtrmzh +tlgpkzfdlnine9fivezdl +9fourtsnhlf5ljxrhflckjrrzfjbndhlcbv +3tthree6zqrhbpqczsixrgvlcpm5 +twosixnzqtvhhnm8 +five6one6 +4fournine946nine7 +one8rzlnlcvdseven4seven +tnmkgnbrzg5nmlqsevenone7oneeight +eight985sjrfjdhtkrbd +4threexlm6twoone5mthree +four8fiveghddxqlp +1kjtrpktpkq +2grqpqfsclsgdzmkglxbzxcshrs811one +9seven94ffkfdmvxr +8tvnnbpj7bjmvlnnj +sixthreeflggjxmlk54 +6five6ninecjdmkggsixnine +sfjlhbbx6onexxjsix4z +9bbnhtpgbntzlxct85 +2bltznvqgs8sixsix +nms7vst8 +eight9vnrqbv +two663 +1h6prckcqdqn +2ninesevensixtwogkvtjrp6rbgc +sbsncmpsixhfvttwo27fsb +fourtwoshvjffjdeight83knlxbdjphsn +bkbhjcgkjbcgjsix1 +cfkpjctlnztlsgjonehrmvtl7vksr +8eightphhd +6eighttwosix5one +8dtnqgtrddjfqmlrptphfxkcgoneeight7 +32eightjfgtqjllmxtf6s +twovqnctjcvsdfjbhtnzccd2gshchnhrpx +twovqqpbrf9 +four4onelkjf15psdspgvvdfcvmnkhmfive +xdpg4ninetsbrmpqfive +fiveonefive19 +46qtppz +twoseveneighteight72 +fivefourthreesevenbxtpqctslbkeight2qmvgth +355ncxjffxt +eight4zslht5six +sdnsrghmbxxjhjqd1njqjcghsspmggzd2 +vcthxnqqkvqsjrkxrs71onetwo +fivexcjvm9 +3kddthreehfhjmq9ninesix6 +rclqzddvxtm2nineninethreefour +vlfgxbkdgnxrsprd386onethreetwo +5sixjscbvzkxtl5fourone +317dnqnqntwo65jnthjbxnfive +mxtwonethreetwo2ninefour35lnhczqfpt4 +nlctnjrr9twopthreefmxgjeightwofqh +nz8threefourbhcjvssgcnine +sevensixzspvzjseven9 +six6onetwocnvmjfour4eightone +7xfd5qlmtzhhgr +8twonesch +nineqvlsrfpdn2 +ptrfgdnine7gpxsix +pfx4sixfoursix4fivesix +68lqzp +nine53jmtsxjptgmzpfoureight31 +two1msjf8 +gpgrpptthreetwomfrmkszrv8 +3five4 +threelqgs2kjvlsbmjkf +4fourzgqkfhqhvhpgfkt +jnlbcbgrp7 +onecdcmbrqxxlpbd1rthree +99mbfdcgbhv +nine6cvmfourfivesixhcsqfpxkdk +eighthjbqsbz6ndpkdlnpmpxqvpmsrbvksnnleightnzxmjg +gvvpnfzbb7zxfschnrteight6two5tnp +sixrctqxdpkxpfdkglvthreenine47rzs +jtwonefour8rkmtclhlf97fqpjmggtztwo +slmfjkfgbjt6 +8lbh +eightnqtfvvm2 +vseven31 +one54qrnzfrbdqfive +8twokfivel9 +vfcsqvxkdxfiveqdvgqdmstn5 +5l63 +two8fourzskrqbcszfzbchlh9ldcp6 +hqhszsgmqzlksq5 +sb6fivefourpmtptjtkzhbxjjnqsixkt9 +twohrktppz5sevenhppmnjzlrkdqddsgs +two37ninefive +fourllczb9 +sixfourone83two +ktgpc7 +fjsnkdj6sixsixtworlhgnbqlbm +51zscxpk6onesevenjxxzcp6hqrtjmhqpk +dmxfcfmfsbfpjfive4 +one47 +9jdlkcpzsevengfddvzxdnfkxf8 +fourdxnine3four39 +nine1one7fjcjjckngthreec +5dlqjlbpt +twooneeight9gf6zvtsqvrlnf +three3six7 +3jnhfivethree +1pzdqvjftwofive348 +four7kcrqkf9 +9cxglsdg +twobgmghbrqdngthreervxjbmp7xvrskhfcf +cpvhhkgmftttdtwoqfncthree1tzlbqcr5 +kmxqkfmlgtmztzpr74ninebqgcjkksljrphc +mrsmtdhpsixslxg9five7 +53two +xpfzv3 +twosdjhone551twozgqc4 +89fourfournfhc +five7chqddxtwo1tjmlhqsix +dkrnxgh5xqzcnjzrhg +lcvfqpglmntwo1sixthreevdndckjgpkzpsp +foursixnineseven1llbdvckff +6four15fivettfivefive +684cfnqfxkxgeightnfgqqmthreelbfxxdsmn +fourdcxxseven28hxqqfhxtd +1threegjffmjrfxppnsqthree +3khnfmcmtj33 +9ninejvdl88 +3four9seven8fourmpjpkn7 +tmfourkc1sixfournglfl +24xgscdtfxhttglvhczrstpfcjvnine2fiveone +psqoneight4twojxkcvgdteight1rhcgmkmmjbbnzdhqj +sfrgqk1two +fiverzjbzssone4nineninefive +twonineonergqsg2eight7eightwolf +rztthree6sixsixxsxtvjthree +78fourcvthree +17hjphkdthree +tdprffbgqseven7 +58eightbchzffmkhh8twofivethree +zpbfstbb71hgldfkrvfourthreeonesixfour +fiveseven1eightnine +four8nine4vxpfpgxtlfhcrndscfgn4seven +pgtznpnqvm1one1dfsix16 +ddffoureightpmqkznnseven75two +6lklqx1sevenzhfdb1 +mq113scstpnnveightfive3nine +threetwox79 +284mrsixthreefour +1seven7zk4lldz2 +271nine2fourfive9 +fourthree37xxkvlgsixzpkblnine +xbbnj2eight33 +seven5sevenonekzpnhzx +247xgmlnntrcsixbstnine +3ninezxtbqbfgtdjpgmjv +tvxkssrfthree3 +fourfoureight12 +onefdszsvrzt2fdeightzkbmz +cqrqkfgb3sevenqtqntxxhqlvrcthreefour +2one5ptslgxsp4six4two6 +rskmbsfglone913vlmqtmpvfsevenp +7c +nkzrdb66crhk +onevdttzljsmzvvhlf1tzqsqnnchdxbmngtlzzjdszvlvfzhx +eightbtstrjzmfmzvcgsbgfxfour4one1 +pttthttfftkp41 +two9rlqrxvsevenfive +v2four4 +two2one +rdvhthhzrmeight5jtgf +flshgbbtztkjfive8 +7sfc181fivefive +fivenine1bfnchprbsix +six2zpqshtndsgsevenone3one4 +fq8 +seven4eightvzfq7kthqh +4vxtllmlnine8gsqkngfdzeight +vhfzmbgseven5 +skqfzlconefivertzchfkvthreeeightfive22 +72oneeightone +7ccs8vjx7vvszsn +xrtmgqk95five849 +threebqeight8hg +drdhjjtdrdxonenineninefourfkzrrggvz97 +8xxldtmdctllqssgdqp83 +dfqrjzv9rqbtn6 +3ninenhgqkglfvjbmgcdrsbhfournine +five821 +54foursix7pv2qsix +7197threescjkqhpqvzgjthpmcgtzrcd +ltpzstwo78fivefourstwox +mcqcmxxzcmpzrz4ntgnsgqbqjmkzpqvxtvsixrzzr3seven +foursixfourzrnxsixgpx7eight +41448sevenhxjpbvhvlmqrpjsvhblts +1geightgtxlzdmpprjvg856five +2tgrll648four +3pkcd6eight948 +94sfznqjqlkvfjgczm +twockgseven4seven6bp +sixsix6eightsixeight +nine3threenpsmshnchm +threemqfptponesevendbjs17 +2ninehnsnnvj21fkeightwodmz +jcptspngbc38nvtnrmvqtwo1 +6qsmcvfoursmlsevensix4lkpxxcnk +xmtjrsrkjd5 +7psvffqn4 +3sh +jdklghtbz1eightrhvfmnlknlghg77 +62tbtjfkltkdrxsxhhxpvbfvpnrpflh +fpctmmvvnbftv2 +nkxmdshm5twoseven672 +88788jnscmpqr66sxcjx diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 4fd45c2..5c81289 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -48,8 +48,16 @@ Cont e = JSExp -> JSStmt e ||| JSEnv contains `Var` for binders or `Dot` for destructured data. It ||| used to translate binders -JSEnv : Type -JSEnv = List JSExp +record JSEnv where + constructor MkEnv + env : List JSExp + depth : Nat + +push : JSEnv -> JSExp -> JSEnv +push env exp = { env $= (exp ::) } env + +empty : JSEnv +empty = MkEnv [] Z litToJS : Literal -> JSExp litToJS (LString str) = LitString str @@ -57,23 +65,24 @@ litToJS (LChar c) = LitString $ cast c litToJS (LInt i) = LitInt i -- Stuff nm.h1, nm.h2, ... into environment -mkEnv : String -> Nat -> List JSExp -> List String -> List JSExp +-- TODO consider JSExp instead of nm, so we can have $foo.h1 instead of assigning a sc. +mkEnv : String -> Nat -> JSEnv -> List String -> JSEnv mkEnv nm k env [] = env -mkEnv nm k env (x :: xs) = mkEnv nm (S k) (Dot (Var nm) "h\{show k}" :: env) xs +mkEnv nm k env (x :: xs) = mkEnv nm (S k) (push env (Dot (Var nm) "h\{show k}")) xs envNames : Env -> List String ||| given a name, find a similar one that doesn't shadow in Env fresh : String -> JSEnv -> String -fresh nm env = if free env nm then nm else go nm 1 +fresh nm env = if free env.env nm then nm else go nm 1 where - free : JSEnv -> String -> Bool + free : List JSExp -> String -> Bool free [] nm = True free (Var n :: xs) nm = if n == nm then False else free xs nm free (_ :: xs) nm = free xs nm go : String -> Nat -> String - go nm k = let nm' = "\{nm}\{show k}" in if free env nm' then nm' else go nm (S k) + go nm k = let nm' = "\{nm}\{show k}" in if free env.env nm' then nm' else go nm (S k) -- This is inspired by A-normalization, look into the continuation monad -- There is an index on JSStmt, adopted from Stefan Hoeck's code. @@ -81,30 +90,28 @@ fresh nm env = if free env nm then nm else go nm 1 -- Here we turn a Term into a statement (which may be a sequence of statements), there -- is a continuation, which turns the final JSExpr into a JSStmt, and the function returns -- a JSStmt, wrapping recursive calls in JSnoc if necessary. -termToJS : List JSExp -> CExp -> Cont e -> JSStmt e -termToJS env (CBnd k) f = case getAt k env of +termToJS : JSEnv -> CExp -> Cont e -> JSStmt e +termToJS env (CBnd k) f = case getAt k env.env of (Just e) => f e Nothing => ?bad_bounds termToJS env (CLam nm t) f = let nm' = fresh nm env -- "\{nm}$\{show $ length env}" - env' = (Var nm' :: env) + env' = push env (Var nm') in f $ JLam [nm'] (termToJS env' t JReturn) termToJS env (CFun nms t) f = let nms' = map (\nm => fresh nm env) nms - env' = foldl (\ e, nm => Var nm :: e) env nms' + env' = foldl (\ e, nm => push e (Var nm)) env nms' in f $ JLam nms' (termToJS env' t JReturn) termToJS env (CRef nm) f = f $ Var nm termToJS env (CMeta k) f = f $ LitString "META \{show k}" -termToJS env (CLit (LString str)) f = f (LitString str) -termToJS env (CLit (LChar c)) f = f (LitString $ cast c) -termToJS env (CLit (LInt i)) f = f (LitInt i) +termToJS env (CLit lit) f = f (litToJS lit) -- if it's a var, just use the original -termToJS env (CLet nm (CBnd k) u) f = case getAt k env of - Just e => termToJS (e :: env) u f +termToJS env (CLet nm (CBnd k) u) f = case getAt k env.env of + Just e => termToJS (push env e) u f Nothing => ?bad_bounds2 termToJS env (CLet nm t u) f = let nm' = fresh nm env - env' = (Var nm' :: env) + env' = push env (Var nm') -- If it's a simple term, use const in case termToJS env t (JAssign nm') of (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) @@ -124,20 +131,24 @@ termToJS env (CCase t alts) f = termToJS env t $ \case (Var nm) => maybeCaseStmt env nm alts - t' => - let nm = fresh "sc" env in - JSnoc (JConst nm t') (maybeCaseStmt (Var nm :: env) nm alts) + t' => do + -- TODO refactor nm to be a JSExp with Var{} or Dot{} + let nm = "sc$\{show env.depth}" + let env' = { depth $= S } env + JSnoc (JConst nm t') (maybeCaseStmt env' nm alts) where - termToJSAlt : List JSExp -> String -> CAlt -> JAlt + termToJSAlt : JSEnv -> String -> CAlt -> JAlt termToJSAlt env nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f) -- intentionally reusing scrutinee name here - termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (Var nm :: env) u f) - termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS (Var nm :: env) u f) + termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (env) u f) + termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f) - maybeCaseStmt : List JSExp -> String -> List CAlt -> JSStmt e + maybeCaseStmt : JSEnv -> String -> List CAlt -> JSStmt e -- If there is a single alt, assume it matched maybeCaseStmt env nm [(CConAlt _ args u)] = (termToJS (mkEnv nm 0 env args) u f) + maybeCaseStmt env nm alts@(CLitAlt _ _ :: _) = + (JCase (Var nm) (map (termToJSAlt env nm) alts)) maybeCaseStmt env nm alts = (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts)) @@ -233,7 +244,7 @@ entryToDoc (MkEntry name ty (Fn tm)) = do debug "compileFun \{pprint [] tm}" ct <- compileFun tm -- If ct has zero arity and is a compount expression, this fails.. - let body@(JPlain {}) = termToJS [] ct JPlain + let body@(JPlain {}) = termToJS empty ct JPlain | js => error (getFC tm) "Not a plain expression: \{render 80 $ stmtToDoc js}" pure (text "const" <+> jsIdent name <+> text "=" <+/> stmtToDoc body) entryToDoc (MkEntry name type Axiom) = pure "" @@ -243,7 +254,7 @@ entryToDoc (MkEntry name type PrimTCon) = pure $ dcon name (piArity type) entryToDoc (MkEntry name _ (PrimFn src)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src export -compile : M Doc +compile : M (List Doc) compile = do top <- get - pure $ stack $ !(traverse entryToDoc top.defs) + traverse entryToDoc top.defs diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index c035734..2379e87 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -680,7 +680,7 @@ buildLitCase ctx prob fc scnm scty lit = do buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt) buildLitCases ctx prob fc scnm scty = do - let lits = getLits scnm prob.clauses + let lits = nub $ getLits scnm prob.clauses alts <- traverse (buildLitCase ctx prob fc scnm scty) lits -- TODO build default case -- run getLits diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index 5cfb744..af299f6 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -44,6 +44,7 @@ unquote str = case unpack str of go : List Char -> List Char go [] = [] go ['"'] = [] + go ('\\' :: ('n' :: xs)) = '\n' :: go xs go ('\\' :: (x :: xs)) = x :: go xs go (x :: xs) = x :: go xs @@ -55,7 +56,7 @@ rawTokens <|> match (is '#' <+> many alpha) (Tok Pragma) <|> match charLit (Tok Character) <|> match (exact "_" <+> (some opChar <|> exact ",") <+> exact "_") (Tok MixFix) - <|> match (quo <+> manyUntil quo ((esc any <+> any) <|> any) <+> opt quo) (Tok StringKind . unquote) + <|> match (quo <+> manyUntil quo (esc any <|> any) <+> quo) (Tok StringKind . unquote) <|> match (lineComment (exact "--")) (Tok Space) <|> match (blockComment (exact "/-") (exact "-/")) (Tok Space) <|> match (exact ",") (Tok Oper) diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index bb95290..b35ec86 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -73,7 +73,6 @@ Show Literal where public export data CaseAlt : Type where CaseDefault : Tm -> CaseAlt - -- I've also seen a list of stuff that gets replaced CaseCons : (name : String) -> (args : List String) -> Tm -> CaseAlt CaseLit : Literal -> Tm -> CaseAlt @@ -98,7 +97,6 @@ data Tm : Type where App : FC -> Tm -> Tm -> Tm U : FC -> Tm Pi : FC -> Name -> Icit -> Tm -> Tm -> Tm - -- REVIEW - do we want to just push it up like idris? Case : FC -> Tm -> List CaseAlt -> Tm -- need type? Let : FC -> Name -> Tm -> Tm -> Tm @@ -173,7 +171,7 @@ pprint names tm = render 80 $ go names tm goAlt : List String -> CaseAlt -> Doc goAlt names (CaseDefault t) = "_" <+> "=>" <+> go ("_" :: names) t - goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go (args ++ names) t + goAlt names (CaseCons name args t) = text name <+> spread (map text args) <+> "=>" <+/> go (reverse args ++ names) t goAlt names (CaseLit lit t) = text (show lit) <+> "=>" <+/> go names t go names (Bnd _ k) = case getAt k names of diff --git a/src/Main.idr b/src/Main.idr index c64c8ef..3707912 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -38,15 +38,13 @@ dumpContext top = do go [] = pure () go (x :: xs) = putStrLn " \{show x}" >> go xs -dumpSource : M () -dumpSource = do - doc <- compile - putStrLn $ render 90 doc writeSource : String -> M () writeSource fn = do - doc <- compile - let src = "#!/usr/bin/env node\n" ++ render 90 doc ++ "\nmain();" + docs <- compile + let src = unlines $ ["#!/usr/bin/env node"] + ++ map (render 90) docs + ++ [ "main();" ] Right _ <- writeFile fn src | Left err => fail (show err) Right _ <- chmodRaw fn 493 | Left err => fail (show err) diff --git a/tests/black/Prelude.newt b/tests/black/Prelude.newt index ba6b0e0..070e670 100644 --- a/tests/black/Prelude.newt +++ b/tests/black/Prelude.newt @@ -12,3 +12,13 @@ data Either : U -> U -> U where Left : {a b : U} -> a -> Either a b Right : {a b : U} -> b -> Either a b +data List : U -> U where + Nil : {a : U} -> List a + Cons : {a : U} -> a -> List a -> List a + +-- Currently if I say _::_ = Cons, it gets curried + +infixr 4 _::_ +_::_ : {a : U} -> a -> List a -> List a +_::_ x xs = Cons x xs +