repo refactor

.github/workflows/ci.yml

@@ -18,6 +18,8 @@ jobs:
     steps:
       - name: Checkout code
         uses: actions/checkout@v3
+        with:
+          submodules: 'recursive'
 
       - name: Use OCaml ${{ matrix.ocaml-compiler }}
         uses: ocaml/setup-ocaml@v2

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "ext/games"]
+	path = ext/games
+	url = [email protected]:emarzion/games.git

bin/gen/ExtractRomanWheel.v

@@ -10,9 +10,9 @@ Require Import ExtrOCamlInt63.
 Extraction Language OCaml.
 
 Require Import Games.Util.OMap.
-Require Import Games.Bear.Sort.
-Require Import Games.Bear.BearGame.
-Require Import Games.Bear.RomanWheel.
+Require Import TBGen.Bear.Sort.
+Require Import TBGen.Bear.BearGame.
+Require Import TBGen.Bear.RomanWheel.
 Require Import Games.Game.TB.
 
 Extraction "TBGen.ml" RW_TB.

bin/gen/dune

@@ -1,7 +1,7 @@
 (coq.extraction
   (prelude ExtractRomanWheel)
   (extracted_modules TBGen)
-  (theories Games))
+  (theories Games TBGen))
 
 (library
   (name extracted_code)

bin/query/ExtractQuery.v

@@ -13,9 +13,9 @@ Extraction Language OCaml.
 Require Import Games.Util.Show.
 Require Import Games.Util.IntHash.
 Require Import Games.Util.OMap.
-Require Import Games.Bear.Sort.
-Require Import Games.Bear.BearGame.
-Require Import Games.Bear.RomanWheel.
+Require Import TBGen.Bear.Sort.
+Require Import TBGen.Bear.BearGame.
+Require Import TBGen.Bear.RomanWheel.
 Require Import Games.Game.TB.
 Require Import Games.Game.OCamlTB.
 
@@ -164,6 +164,8 @@ Definition rw_tb_strat (pl : Player.Player)
  : Strategy.strategy pl s :=
   tb_strat s pl tb.
 
+Set Warnings "-extraction-default-directory".
+
 Separate Extraction
   make_RW_State
   init_RW_State

bin/query/dune

@@ -24,7 +24,7 @@
     String0
     TB
   )
-  (theories Games))
+  (theories Games TBGen))
 
 (library
   (name query)

configure.sh

@@ -4,6 +4,8 @@
 echo "# !!!" > _CoqProject
 echo "# Generated by configure.sh" >> _CoqProject
 echo "# !!!" >> _CoqProject
-echo "-R _build/default/theory Games" >> _CoqProject
+echo "-R _build/default/theory TBGen" >> _CoqProject
+echo "-R _build/default/ext/games/theory Games" >> _CoqProject 
 echo >> _CoqProject
+find ext/games -name "*.v" |sort >> _CoqProject
 find theory -name "*.v" |sort >> _CoqProject

theory/Bear/BearGame.v

@@ -4,10 +4,11 @@ Require Import String.
 Open Scope string_scope.
 
 Require Coq.Sorting.Sorting.
+Require Import Games.Game.Game.
 
 Require Import Games.Game.Game.
-Require Import Games.Bear.Graph.
-Require Import Games.Bear.Sort.
+Require Import TBGen.Bear.Graph.
+Require Import TBGen.Bear.Sort.
 Require Import Games.Game.TB.
 Require Import Games.Game.Player.
 Require Import Games.Util.IntHash.

theory/Bear/Graph.v

@@ -1,8 +1,7 @@
-
 Require Import Lia.
 Require Import List.
 Import ListNotations.
-Require Import Games.Bear.Sort.
+Require Import TBGen.Bear.Sort.
 
 Require Import Games.Util.Dec.
 

theory/Bear/RomanWheel.v

@@ -7,8 +7,8 @@ Require Import ZArith.
 Require Import Lia.
 
 Require Import Games.Util.IntHash.
-Require Import Games.Bear.Graph.
-Require Import Games.Bear.BearGame.
+Require Import TBGen.Bear.Graph.
+Require Import TBGen.Bear.BearGame.
 Require Import Games.Game.TB.
 
 Inductive Spoke :=