Commit Graph

  • e20170a8bb auto fix files - sonnet ghc_compiled_only Victor Taelin 2024-07-05 13:00:18 -0300
  • d409b9d5b7 U60 to U48, use let to make match expr, WIPs Victor Taelin 2024-07-05 10:06:49 -0300
  • 24510cedbe WIP Victor Taelin 2024-07-05 02:03:05 -0300
  • 89c6a0d155 initial syntax guide Victor Taelin 2024-07-05 01:09:41 -0300
  • 1142db1144 Update ADT param syntax; update many things (WIP) Victor Taelin 2024-07-05 00:47:13 -0300
  • c44314af75 main.rs compilation errors enricozb/remove-auto-format Enrico Zandomeni Borba 2024-07-04 11:13:19 +0200
  • 98022098f2 Display for Book Enrico Zandomeni Borba 2024-07-04 11:13:06 +0200
  • 9473678ebd fix term/show.rs warning Enrico Zandomeni Borba 2024-07-04 11:13:00 +0200
  • 424201c33f sugar/mod.rs: Display Enrico Zandomeni Borba 2024-07-04 11:03:13 +0200
  • 469bb29ccb term/show.rs: rearrange Enrico Zandomeni Borba 2024-07-04 11:03:05 +0200
  • 560cf18dab sugar: rm whitespace Enrico Zandomeni Borba 2024-07-04 10:20:19 +0200
  • 8541573426 Display for Term and Oper Enrico Zandomeni Borba 2024-07-04 10:19:22 +0200
  • 667b9cedb8 rm show/mod.rs Enrico Zandomeni Borba 2024-07-04 10:19:16 +0200
  • 70a7ceafc5 some trailing whitespace Enrico Zandomeni Borba 2024-07-03 14:46:05 +0200
  • c6779b7581 parse _ in name, fix hole parser Victor Taelin 2024-06-22 23:37:35 -0300
  • 314aaeee1c use compiled GHC checker only Victor Taelin 2024-06-22 23:00:56 -0300
  • d5438cd7df
    Merge 1988935b87 into 2434f5f901 Luna 2024-06-12 21:59:57 +0200
  • 2bdca98f75
    Merge c8fd3d4614 into 2434f5f901 Eduardo Sandalo Porto 2024-06-10 08:13:39 -0400
  • e10d3e42fe
    Merge 67abc5cdf8 into 2434f5f901 Eduardo Sandalo Porto 2024-06-09 01:22:14 +0300
  • 2434f5f901
    Merge pull request #14 from NoamDev/ascii-alternatives master Victor Taelin 2024-06-08 12:27:06 -0300
  • 906bc6474b fix ascii syntax for lambda and forall previously, it collided with names starting with lambda/forall. NoamDev 2024-05-26 18:59:59 +0300
  • 80e3ff76c2
    Merge pull request #13 from NoamDev/ascii-alternatives Victor Taelin 2024-05-25 15:07:50 -0300
  • b516d3b7ea Ascii alternatives to forall and lambda NoamDev 2024-05-25 20:51:12 +0300
  • 058633c6c9 desugar match with implicit args Victor Taelin 2024-05-24 23:40:13 -0300
  • ecc1455231 Merge branch 'master' of github.com:HigherOrderCO/kind2 Victor Taelin 2024-05-19 18:10:38 -0300
  • 12fc18c697 fix match motive on proofs WIP Victor Taelin 2024-05-19 18:10:31 -0300
  • 1988935b87 Remove some functions from kind2.hs prelude, update kind2.hvm2 LunaAmora 2024-03-21 12:27:15 -0300
  • 8f498bf1b9 Apply style polishments from hs to kind2.hvm2 LunaAmora 2024-03-20 15:46:07 -0300
  • 28e8fda2ca
    Merge pull request #11 from Eduardogbg/patch-1 Yan Mendes 2024-05-16 14:07:53 -0300
  • 5e13be733c
    WIP update Yan Mendes 2024-05-15 16:57:01 -0300
  • d84640201d
    fix typo in equality docs Eduardo Gomes 2024-04-18 11:21:37 -0300
  • 67abc5cdf8 Refactor code generation to use Show Eduardo Sandalo Porto 2024-04-11 20:18:54 -0300
  • af819567fd Add specific Kind2 tests for constructor generation Eduardo Sandalo Porto 2024-04-11 17:52:12 -0300
  • 63f0dc3466 Test nested module Eduardo Sandalo Porto 2024-04-11 16:10:49 -0300
  • 258104ad48 (Mostly) fully test constructor generation Eduardo Sandalo Porto 2024-04-10 21:43:22 -0300
  • 67ea1e648c Add test for constructor generation Eduardo Sandalo Porto 2024-04-10 13:11:30 -0300
  • 735628816f Start testing constructor generation Eduardo Sandalo Porto 2024-04-09 22:23:32 -0300
  • c11e0819cb Solve one of the TODO questions Eduardo Sandalo Porto 2024-04-09 12:41:44 -0300
  • b8a382c586 Improve description of the constructor generation result Eduardo Sandalo Porto 2024-04-09 11:50:05 -0300
  • ac6438b563 Create folder structure for the constructor if it does not exist Eduardo Sandalo Porto 2024-04-09 11:12:44 -0300
  • c428ebc967 Format type indices into construtors, finishing constructor generation Eduardo Sandalo Porto 2024-04-09 10:26:00 -0300
  • cbad45f15b Make constructor generation code prettier Eduardo Sandalo Porto 2024-04-08 21:04:44 -0300
  • 1f25fb8a09 Save and load generated constructor Eduardo Sandalo Porto 2024-04-08 11:58:54 -0300
  • f60bea55f7 Generate full constructor code Eduardo Sandalo Porto 2024-04-07 22:10:09 -0300
  • 3320fafe97 Correctly resugar ADT for constructor generation Eduardo Sandalo Porto 2024-04-06 11:45:30 -0300
  • c4552a079a Start implementing automatic constructor generation Eduardo Sandalo Porto 2024-04-05 19:58:06 -0300
  • c8fd3d4614 Resolve linearity suggestions Eduardo Sandalo Porto 2024-04-04 13:47:43 -0300
  • cb33a5b3e1 Implement and slightly change BMap (bitmap) data type Eduardo Sandalo Porto 2024-04-01 17:59:50 -0300
  • 9e8daa7630 Add Bits data type and functions Eduardo Sandalo Porto 2024-04-01 17:59:13 -0300
  • 2764c4c17d
    Merge pull request #8 from imaqtkatt/refactor-book Victor Taelin 2024-03-22 15:38:06 -0300
  • 4b4b398139 Refactor String/Map functions imaqtkatt 2024-03-22 13:23:43 -0300
  • 78fc259958 some fixes and add BMap data structure imaqtkatt 2024-03-20 15:33:17 -0300
  • ae64132af2 Merge branch 'master' of github.com:HigherOrderCO/kind2 Victor Taelin 2024-03-20 13:43:07 -0300
  • db5856b1ef style polishments Victor Taelin 2024-03-20 13:38:13 -0300
  • 9f53ef7c5e
    Merge pull request #7 from LunaAmora/kind2-hvm2 Victor Taelin 2024-03-20 12:48:14 -0300
  • 56ec0f7951 add more List and Nat functions imaqtkatt 2024-03-20 12:47:25 -0300
  • 22c3cf42ff refactor IO and HVM imaqtkatt 2024-03-20 10:01:34 -0300
  • af0ed6bb8d refactor BBT to new syntax imaqtkatt 2024-03-20 09:28:46 -0300
  • 5008491fe9 Add unification polishments to kind2.hvm2 LunaAmora 2024-03-18 17:20:39 -0300
  • 3c89c73d2f Remove commented fn LunaAmora 2024-03-18 16:59:44 -0300
  • c2200dd30a Fix generated name on generate_check_hvm2 LunaAmora 2024-03-18 16:54:01 -0300
  • bf65d89f09 Update kind2 file and compilation LunaAmora 2024-03-18 11:10:40 -0300
  • de14d56d3d Merge branch 'master' of github.com:HigherOrderCO/kind2 Victor Taelin 2024-03-18 17:02:39 -0300
  • 29d8338f4a unification fine polishments - see notes Victor Taelin 2024-03-18 16:59:21 -0300
  • 8c8c68cce9 fix repeated meta uids across refs Victor Taelin 2024-03-18 14:53:47 -0300
  • 5571be7715
    Update README.md Victor Taelin 2024-03-15 23:38:31 -0300
  • c7c4a0345a
    Update README.md Victor Taelin 2024-03-15 23:38:02 -0300
  • 9201bebc01 first kind2-hvm2 program run! sum-tree via fold Victor Taelin 2024-03-15 23:06:44 -0300
  • 70288ef011 diff savida Victor Taelin 2024-03-15 22:07:01 -0300
  • 0647ea9bc7 implicits args and stuff Victor Taelin 2024-03-15 18:51:25 -0300
  • dd6706a7d5 refactored CLI - by Claude3 Victor Taelin 2024-03-14 19:33:21 -0300
  • 6726b552b3 Merge branch 'LunaAmora-kind2-hvm2' Victor Taelin 2024-03-14 18:32:10 -0300
  • d98da0863e Merge branch 'kind2-hvm2' of https://github.com/LunaAmora/kind2 into LunaAmora-kind2-hvm2 Victor Taelin 2024-03-14 18:32:03 -0300
  • f8ab510b1e Merge branch 'master' of github.com:HigherOrderCO/kind2 Victor Taelin 2024-03-14 18:27:06 -0300
  • b061e8f3a3 HVM2 compiler WIP Victor Taelin 2024-03-14 18:26:59 -0300
  • f96624ddcb rename to_hs to to_hs_checker, to differentiate between compiling to hoas checker file, and the compiler to actually run Victor Taelin 2024-03-14 17:34:38 -0300
  • c918ee680e
    Merge pull request #6 from Derenash/master Victor Taelin 2024-03-14 17:14:47 -0300
  • 867602746d
    Merge branch 'HigherOrderCO:master' into master Derenash 2024-03-14 17:11:00 -0300
  • 74ee9a3c97 fix Vector.concat using switch instead of match Derenash 2024-03-14 17:08:08 -0300
  • 144c3210df Fix some syntaxes uses of switch +: to _: Derenash 2024-03-14 17:07:40 -0300
  • 4d421106bd update the README Victor Taelin 2024-03-14 16:46:00 -0300
  • 3ce20b7003 Merge branch 'master' of https://github.com/Derenash/kind2.0 Derenash 2024-03-14 16:34:44 -0300
  • f4be6b5e45 Merge branch 'master' of https://github.com/Derenash/kind2.0 Derenash 2024-03-14 16:31:59 -0300
  • 357cc111a6 Fix typing in BBT.has.linear.kind2 Derenash 2024-03-14 16:31:30 -0300
  • 65d9b7c6c4 fix long-switch Victor Taelin 2024-03-14 16:28:32 -0300
  • 4639202430 long-switch notation, remove unused files Victor Taelin 2024-03-14 16:19:00 -0300
  • 2666e5de0e U60 syntax without hashtag; numeric match now called switch Victor Taelin 2024-03-14 13:35:03 -0300
  • 9cbaf6c4d5 prevent recursive holes (check condition 3) Victor Taelin 2024-03-14 12:10:05 -0300
  • 057c8d51de fix equalSimilar not following described algo Victor Taelin 2024-03-14 10:31:04 -0300
  • 69bbdfc382 Update kind2.hvm2 to the latest changes LunaAmora 2024-03-14 09:05:21 -0300
  • f1615e4a6b Add Kind2.hvm2 and cli for choosing the runtime LunaAmora 2024-03-14 08:01:40 -0300
  • 981b8afe90 fix unchecked let Victor Taelin 2024-03-14 00:21:21 -0300
  • b489c148bf equal / refl syntax and stuff Victor Taelin 2024-03-13 22:32:30 -0300
  • 3f1cdd2996 cleanup ai interactions Victor Taelin 2024-03-13 16:20:44 -0300
  • d059c82c1f ADTs & match - complete Victor Taelin 2024-03-13 15:05:52 -0300
  • 0c34404c0b use-declarations with shadowing Victor Taelin 2024-03-12 18:01:12 -0300
  • dc993b5de0 pattern-match syntax Victor Taelin 2024-03-12 13:44:49 -0300
  • 24b83350c6 ADT syntax continuation Victor Taelin 2024-03-12 11:55:09 -0300
  • 29de8994d2 progress on ADT parsing Victor Taelin 2024-03-11 22:45:46 -0300
  • 76320ddb7f initial ADT formatter Victor Taelin 2024-03-09 19:16:24 -0300