Refactor directory names

Signed-off-by: zeramorphic <[email protected]>

ConNF.lean

@@ -8,25 +8,13 @@ import ConNF.Basic.Set
 import ConNF.Basic.Transfer
 import ConNF.Basic.WellOrder
 import ConNF.Construction.Code
-import ConNF.Construction.ConstructHypothesis
-import ConNF.Construction.ConstructMotive
-import ConNF.Construction.Externalise
-import ConNF.Construction.Hailperin
-import ConNF.Construction.InductionStatement
 import ConNF.Construction.NewModelData
-import ConNF.Construction.RaiseStrong
-import ConNF.Construction.Result
-import ConNF.Construction.RunInduction
-import ConNF.Construction.TTT
 import ConNF.Counting.BaseCoding
 import ConNF.Counting.BaseCounting
 import ConNF.Counting.CodingFunction
 import ConNF.Counting.Conclusions
 import ConNF.Counting.CountSupportOrbit
 import ConNF.Counting.Recode
-import ConNF.Counting.SMulSpec
-import ConNF.Counting.Spec
-import ConNF.Counting.SpecSame
 import ConNF.Counting.Strong
 import ConNF.Counting.Twist
 import ConNF.FOA.BaseAction
@@ -38,6 +26,15 @@ import ConNF.FOA.StrAction
 import ConNF.FOA.StrActionFOA
 import ConNF.FOA.StrApprox
 import ConNF.FOA.StrApproxFOA
+import ConNF.Model.ConstructHypothesis
+import ConNF.Model.ConstructMotive
+import ConNF.Model.Externalise
+import ConNF.Model.Hailperin
+import ConNF.Model.InductionStatement
+import ConNF.Model.RaiseStrong
+import ConNF.Model.Result
+import ConNF.Model.RunInduction
+import ConNF.Model.TTT
 import ConNF.Setup.Atom
 import ConNF.Setup.BasePerm
 import ConNF.Setup.BasePositions
@@ -59,3 +56,6 @@ import ConNF.Setup.StrSet
 import ConNF.Setup.Support
 import ConNF.Setup.Tree
 import ConNF.Setup.TypeIndex
+import ConNF.Strong.SMulSpec
+import ConNF.Strong.Spec
+import ConNF.Strong.SpecSame

ConNF/Counting/BaseCoding.lean

@@ -1,4 +1,4 @@
-import ConNF.Counting.SpecSame
+import ConNF.Strong.SpecSame
 
 /-!
 # Coding the base type

ConNF/Counting/CountSupportOrbit.lean

@@ -1,5 +1,5 @@
-import ConNF.Counting.SMulSpec
-import ConNF.Counting.SpecSame
+import ConNF.Strong.SMulSpec
+import ConNF.Strong.SpecSame
 
 /-!
 # Counting support orbits

ConNF/Construction/ConstructHypothesis.lean → ConNF/Model/ConstructHypothesis.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.ConstructMotive
+import ConNF.Model.ConstructMotive
 
 /-!
 # New file

ConNF/Construction/ConstructMotive.lean → ConNF/Model/ConstructMotive.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.InductionStatement
+import ConNF.Model.InductionStatement
 import ConNF.Construction.NewModelData
 import ConNF.Counting.Conclusions
 

ConNF/Construction/Externalise.lean → ConNF/Model/Externalise.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.RunInduction
+import ConNF.Model.RunInduction
 
 /-!
 # Externalisation

ConNF/Construction/Hailperin.lean → ConNF/Model/Hailperin.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.TTT
+import ConNF.Model.TTT
 
 /-!
 # New file

ConNF/Construction/RaiseStrong.lean → ConNF/Model/RaiseStrong.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.Externalise
+import ConNF.Model.Externalise
 
 /-!
 # New file

ConNF/Construction/Result.lean → ConNF/Model/Result.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.Hailperin
+import ConNF.Model.Hailperin
 
 /-!
 # New file

ConNF/Construction/RunInduction.lean → ConNF/Model/RunInduction.lean

@@ -1,5 +1,5 @@
 import ConNF.Basic.InductiveConstruction
-import ConNF.Construction.ConstructHypothesis
+import ConNF.Model.ConstructHypothesis
 
 /-!
 # New file

ConNF/Construction/TTT.lean → ConNF/Model/TTT.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.RaiseStrong
+import ConNF.Model.RaiseStrong
 
 /-!
 # New file

ConNF/Counting/SMulSpec.lean → ConNF/Strong/SMulSpec.lean

@@ -1,4 +1,4 @@
-import ConNF.Counting.Spec
+import ConNF.Strong.Spec
 
 /-!
 # Action on specifications

ConNF/Counting/SpecSame.lean → ConNF/Strong/SpecSame.lean

@@ -1,6 +1,6 @@
 import ConNF.FOA.StrActionFOA
 import ConNF.Counting.Strong
-import ConNF.Counting.Spec
+import ConNF.Strong.Spec
 
 /-!
 # Supports with the same specification

DependencyGraph.lean

@@ -43,7 +43,7 @@ elab "#deptree " : command => do
   for (gp, _) in groups imports do
     h.write ("subgraph cluster_" ++ nameCode gp ++ " {\n").toUTF8
     for (k, v) in imports do
-      if (`ConNF).isPrefixOf k && group k = gp then do
+      if (`ConNF).isPrefixOf k && k != `ConNF && group k = gp then do
         printDeps₁ k v (fun s => h.write s.toUTF8)
     h.write ("label = \"" ++ gp.toString ++ "\";\n").toUTF8
     h.write ("margin = 32;\n").toUTF8
@@ -52,7 +52,7 @@ elab "#deptree " : command => do
     h.write ("color = cyan4;\n").toUTF8
     h.write "}\n".toUTF8
   for (k, v) in imports do
-    if (`ConNF).isPrefixOf k then do
+    if (`ConNF).isPrefixOf k && k != `ConNF then do
       printDeps₂ k v (fun s => h.write s.toUTF8)
   h.write "}\n".toUTF8
 
@@ -77,10 +77,10 @@ def allFiles (env : Environment) : List Name :=
     (toString · < toString ·)
 
 def allDecls (env : Environment) : Elab.Command.CommandElabM NameSet :=
-  (fun l => RBTree.ofList (l.map (fun a => a.toList)).join) <$>
+  (fun l => RBTree.ofList (l.map (fun a => a.toList)).flatten) <$>
     (mapM allDeclsIn (allFiles env))
 
-/-- `#index` computes an index of the declations in the project and saves it to `index.csv`. -/
+/-- `#index` computes an index of the declarations in the project and saves it to `index.csv`. -/
 elab "#index " : command => do
   let env ← getEnv
   let allDecls ← allDecls env