start simple inference dataset

Makefile

@@ -53,3 +53,9 @@ typetopology:
 		-o$(TYPETOP)/json/ -i $(TYPETOP)/source/ $(TYPETOP)/source/index.lagda
 	zip -j data/typetopology.zip $(TYPETOP)/*.json
 
+	  # +RTS -H3G -M3G -RTS \
+   # --no-privates \
+
+testInfer:
+	cabal run agda2train -- -r -v agda2train:10 \
+	  -oinfer-test/json/ -i infer-test/ infer-test/All.agda

infer-test/All.agda

@@ -0,0 +1,3 @@
+module All where
+import Simple
+import SimpleEnum

infer-test/Simple.agda

@@ -0,0 +1,23 @@
+module Simple where
+
+open import SimpleLib
+
+Theorem1 : Set
+Theorem1 = A -> B
+
+theorem : Theorem1
+theorem = lemma1
+
+theorem1 :  A -> B
+theorem1 = lemma1
+
+Theorem2 : Set
+Theorem2 = B -> A
+
+theorem2 :  B -> C
+theorem2 = lemma2
+
+theorem3 : A -> C
+theorem3 x = lemma2 (lemma1 x)
+
+

infer-test/SimpleEnum.agda

@@ -0,0 +1,14 @@
+module SimpleEnum where
+
+open import SimpleEnumLib
+
+theorem : A -> B
+theorem = lemma1
+
+theorem2 :  B -> C
+theorem2 = lemma2
+
+theorem3 : A -> C
+theorem3 x = lemma2 (lemma1 x)
+
+

infer-test/SimpleEnumLib.agda

@@ -0,0 +1,19 @@
+module SimpleEnumLib where
+
+data A : Set where
+  aa : A
+
+data B : Set where
+  bb bb1 : B
+
+data C : Set where
+  cc cc2 cc3 : C
+
+lemma1 : A -> B
+lemma1 aa = bb
+
+lemma2 : B -> C
+lemma2 bb = cc
+lemma2 bb1 = cc2
+
+

infer-test/SimpleLib.agda

@@ -0,0 +1,25 @@
+module SimpleLib where
+
+data A : Set where
+  aa : A
+-- in the nominal approach (which is true to Agda), it is as if we had:
+
+-- A : Set
+-- A = <name "A">
+
+-- aa : A
+-- aa = <name "aa">
+
+data B : Set where
+  bb : B
+
+data C : Set where
+  cc  : C
+
+lemma1 : A -> B
+lemma1 aa = bb
+
+lemma2 : B -> C
+lemma2 bb = cc
+
+