big wip

emarzion · Oct 13, 2024 · 6d35d20 · 6d35d20
1 parent 6aeaa7a
commit 6d35d20
Show file tree

Hide file tree

Showing 11 changed files with 978 additions and 125 deletions.
diff --git a/bin/gen/ExtractRomanWheel.v b/bin/gen/ExtractRomanWheel.v
@@ -13,6 +13,7 @@ Require Import TBGen.Util.OMap.
 Require Import TBGen.Bear.Sort.
 Require Import TBGen.Bear.BearGame.
 Require Import TBGen.Bear.RomanWheel.
+Require Import TBGen.Bear.RomanWheelSym.
 Require Import TBGen.TB.TB.
 
 Set Warnings "-extraction-default-directory".

diff --git a/bin/gen/dune b/bin/gen/dune
@@ -29,4 +29,4 @@
 (rule
   (targets tb_w.json tb_b.json)
   (deps gen_file.exe)
-  (action (run ./gen_file.exe)))
+  (action (run time ./gen_file.exe)))
diff --git a/bin/query/ExtractQuery.v b/bin/query/ExtractQuery.v
@@ -17,8 +17,9 @@ Require Import TBGen.Bear.Sort.
 Require Import TBGen.Bear.BearGame.
 Require Import TBGen.Bear.RomanWheelExtras.
 Require Import TBGen.Bear.RomanWheel.
-Require Import TBGen.TB.TB.
-Require Import TBGen.TB.OCamlTB.
+Require Import TBGen.Bear.RomanWheelSym.
+Require Import TBGen.SymTB.TB.
+Require Import TBGen.SymTB.OCamlTB.
 
 Definition make_BG_State {G} (pl : Player.Player)
   (b h1 h2 h3 : Graph.Vert G) : option (BG_State G).

diff --git a/bin/query/dune b/bin/query/dune
@@ -3,20 +3,25 @@
   (extracted_modules
     Ascii
     BearGame
+    Bisim
     Compare_dec
     Datatypes
     Dec
     ExtractQuery
     Game
     Graph
+    GroupAction
     IntHash
     IntMap
     List0
+    Nat
     OCamlTB
     OMap
+    PeanoNat
     Player
     PrimInt63
     RomanWheel
+    RomanWheelSym
     Show
     Sort
     Specif
@@ -36,20 +41,25 @@
     ;; Extracted code
     Ascii
     BearGame
+    Bisim
     Compare_dec
     Datatypes
     Dec
     ExtractQuery
     Game
     Graph
+    GroupAction
     IntHash
     IntMap
     List0
+    Nat
     OCamlTB
     OMap
+    PeanoNat
     Player
     PrimInt63
     RomanWheel
+    RomanWheelSym
     Show
     Sort
     Specif