From 4fac133a8f3b529650b2ced56acdd6ba808158d6 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 18:53:38 +0100
Subject: [PATCH 01/11] Removed abstractor.API

---
 abstractor/abstractor.go                      |  32 +----
 abstractor/concretizer.go                     | 129 ------------------
 extractor/extractor.go                        |   2 +-
 extractor/interface.go                        |  50 +++++--
 extractor/test/another_circuit_test.go        |   9 +-
 extractor/test/circuit_with_parameter_test.go |  11 +-
 extractor/test/deletion_mbu_circuit_test.go   |   9 +-
 extractor/test/merkle_recover_test.go         |   9 +-
 extractor/test/my_circuit_test.go             |   7 +-
 extractor/test/slices_optimisation_test.go    |  13 +-
 extractor/test/to_binary_circuit_test.go      |  11 +-
 extractor/test/two_gadgets_test.go            |  11 +-
 12 files changed, 58 insertions(+), 235 deletions(-)
 delete mode 100644 abstractor/concretizer.go

diff --git a/abstractor/abstractor.go b/abstractor/abstractor.go
index 4b8bb85..3da50ba 100644
--- a/abstractor/abstractor.go
+++ b/abstractor/abstractor.go
@@ -7,33 +7,5 @@ type Gadget interface {
 }
 
 type GadgetDefinition interface {
-	DefineGadget(api API) interface{}
-}
-
-type API interface {
-	frontend.API
-	DefineGadget(gadget GadgetDefinition) Gadget
-
-	frontend.API
-	Call(gadget GadgetDefinition) interface{}
-}
-
-type Circuit interface {
-	frontend.Circuit
-	AbsDefine(api API) error
-}
-
-func Concretize(api frontend.API, circuit Circuit) error {
-	return circuit.AbsDefine(&Concretizer{api})
-}
-
-func CallGadget(api frontend.API, circuit GadgetDefinition) interface{} {
-	_, ok := api.(API)
-	if ok {
-		// The consequence of calling CallGadget with abstractor.API is that
-		// the circuit is extracted as a single function instead of
-		// splitting in sub-circuits
-		panic("abstractor.CallGadget can't be called with abstractor.API")
-	}
-	return circuit.DefineGadget(&Concretizer{api})
-}
+	DefineGadget(api frontend.API) interface{}
+}
\ No newline at end of file
diff --git a/abstractor/concretizer.go b/abstractor/concretizer.go
deleted file mode 100644
index bd76575..0000000
--- a/abstractor/concretizer.go
+++ /dev/null
@@ -1,129 +0,0 @@
-package abstractor
-
-import (
-	"github.com/consensys/gnark/backend/hint"
-	"github.com/consensys/gnark/frontend"
-	"math/big"
-)
-
-type ConcreteGadget struct {
-	api API
-}
-
-func (g *ConcreteGadget) Call(gadget GadgetDefinition) interface{} {
-	return gadget.DefineGadget(g.api)
-}
-
-type Concretizer struct {
-	api frontend.API
-}
-
-func (c *Concretizer) Add(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable {
-	return c.api.Add(i1, i2, in...)
-}
-
-func (c *Concretizer) MulAcc(a, b, c_ frontend.Variable) frontend.Variable {
-	return c.api.MulAcc(a, b, c_)
-}
-
-func (c *Concretizer) Neg(i1 frontend.Variable) frontend.Variable {
-	return c.api.Neg(i1)
-}
-
-func (c *Concretizer) Sub(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable {
-	return c.api.Sub(i1, i2, in...)
-}
-
-func (c *Concretizer) Mul(i1, i2 frontend.Variable, in ...frontend.Variable) frontend.Variable {
-	return c.api.Mul(i1, i2, in...)
-}
-
-func (c *Concretizer) DivUnchecked(i1, i2 frontend.Variable) frontend.Variable {
-	return c.api.DivUnchecked(i1, i2)
-}
-
-func (c *Concretizer) Div(i1, i2 frontend.Variable) frontend.Variable {
-	return c.api.Div(i1, i2)
-}
-
-func (c *Concretizer) Inverse(i1 frontend.Variable) frontend.Variable {
-	return c.api.Inverse(i1)
-}
-
-func (c *Concretizer) ToBinary(i1 frontend.Variable, n ...int) []frontend.Variable {
-	return c.api.ToBinary(i1, n...)
-}
-
-func (c *Concretizer) FromBinary(b ...frontend.Variable) frontend.Variable {
-	return c.api.FromBinary(b...)
-}
-
-func (c *Concretizer) Xor(a, b frontend.Variable) frontend.Variable {
-	return c.api.Xor(a, b)
-}
-
-func (c *Concretizer) Or(a, b frontend.Variable) frontend.Variable {
-	return c.api.Or(a, b)
-}
-
-func (c *Concretizer) And(a, b frontend.Variable) frontend.Variable {
-	return c.api.And(a, b)
-}
-
-func (c *Concretizer) Select(b frontend.Variable, i1, i2 frontend.Variable) frontend.Variable {
-	return c.api.Select(b, i1, i2)
-}
-
-func (c *Concretizer) Lookup2(b0, b1 frontend.Variable, i0, i1, i2, i3 frontend.Variable) frontend.Variable {
-	return c.api.Lookup2(b0, b1, i0, i1, i2, i3)
-}
-
-func (c *Concretizer) IsZero(i1 frontend.Variable) frontend.Variable {
-	return c.api.IsZero(i1)
-}
-
-func (c *Concretizer) Cmp(i1, i2 frontend.Variable) frontend.Variable {
-	return c.api.Cmp(i1, i2)
-}
-
-func (c *Concretizer) AssertIsEqual(i1, i2 frontend.Variable) {
-	c.api.AssertIsEqual(i1, i2)
-}
-
-func (c *Concretizer) AssertIsDifferent(i1, i2 frontend.Variable) {
-	c.api.AssertIsDifferent(i1, i2)
-}
-
-func (c *Concretizer) AssertIsBoolean(i1 frontend.Variable) {
-	c.api.AssertIsBoolean(i1)
-}
-
-func (c *Concretizer) AssertIsLessOrEqual(v frontend.Variable, bound frontend.Variable) {
-	c.api.AssertIsLessOrEqual(v, bound)
-}
-
-func (c *Concretizer) Println(a ...frontend.Variable) {
-	c.api.Println(a...)
-}
-
-func (c *Concretizer) Compiler() frontend.Compiler {
-	return c.api.Compiler()
-}
-
-func (c *Concretizer) NewHint(f hint.Function, nbOutputs int, inputs ...frontend.Variable) ([]frontend.Variable, error) {
-	return c.api.NewHint(f, nbOutputs, inputs...)
-}
-
-func (c *Concretizer) ConstantValue(v frontend.Variable) (*big.Int, bool) {
-	return c.api.ConstantValue(v)
-}
-
-func (c *Concretizer) DefineGadget(gadget GadgetDefinition) Gadget {
-	return &ConcreteGadget{c}
-}
-
-func (c *Concretizer) Call(gadget GadgetDefinition) interface{} {
-	return c.DefineGadget(gadget).Call(gadget)
-}
-
-var _ API = &(Concretizer{})
diff --git a/extractor/extractor.go b/extractor/extractor.go
index 638c084..6004ce6 100644
--- a/extractor/extractor.go
+++ b/extractor/extractor.go
@@ -474,4 +474,4 @@ func (ce *CodeExtractor) DefineGadget(gadget abstractor.GadgetDefinition) abstra
 	return &exGadget
 }
 
-var _ abstractor.API = &CodeExtractor{}
+var _ frontend.API = &CodeExtractor{}
diff --git a/extractor/interface.go b/extractor/interface.go
index e483072..a42400f 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -16,37 +16,57 @@ import (
 )
 
 // CallVoid is used to call a Gadget which doesn't return anything
-func CallVoid(api abstractor.API, gadget abstractor.GadgetDefinition) {
-	api.Call(gadget)
+func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
+    if abs, ok := api.(*CodeExtractor); ok {
+        abs.Call(gadget)
+    } else {
+        gadget.DefineGadget(api)
+    }
 }
 
 // Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
-func Call(api abstractor.API, gadget abstractor.GadgetDefinition) frontend.Variable {
-	return api.Call(gadget).(frontend.Variable)
+func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
+    if abs, ok := api.(*CodeExtractor); ok {
+        return abs.Call(gadget).(frontend.Variable)
+    } else {
+        return gadget.DefineGadget(api).(frontend.Variable)
+    }
 }
 
 // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
-func Call1(api abstractor.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
-	return api.Call(gadget).([]frontend.Variable)
+func Call1(api frontend.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
+    if abs, ok := api.(*CodeExtractor); ok {
+        return abs.Call(gadget).([]frontend.Variable)
+    } else {
+        return gadget.DefineGadget(api).([]frontend.Variable)
+    }
 }
 
 // Call2 is used to call a Gadget which returns a [][]frontend.Variable
 // (i.e. `Vector (Vector F a) b` in Lean)
-func Call2(api abstractor.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
-	return api.Call(gadget).([][]frontend.Variable)
+func Call2(api frontend.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
+    if abs, ok := api.(*CodeExtractor); ok {
+        return abs.Call(gadget).([][]frontend.Variable)
+    } else {
+        return gadget.DefineGadget(api).([][]frontend.Variable)
+    }
 }
 
 // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
 // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
-func Call3(api abstractor.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
-	return api.Call(gadget).([][][]frontend.Variable)
+func Call3(api frontend.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
+    if abs, ok := api.(*CodeExtractor); ok {
+        return abs.Call(gadget).([][][]frontend.Variable)
+    } else {
+        return gadget.DefineGadget(api).([][][]frontend.Variable)
+    }
 }
 
 // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`
 // CircuitToLeanWithName and CircuitToLean aren't joined in a single function
 // CircuitToLean(circuit abstractor.Circuit, field ecc.ID, namespace ...string) because the long term view
 // is to add an optional parameter to support custom `set_option` directives in the header.
-func CircuitToLeanWithName(circuit abstractor.Circuit, field ecc.ID, namespace string) (out string, err error) {
+func CircuitToLeanWithName(circuit frontend.Circuit, field ecc.ID, namespace string) (out string, err error) {
 	defer recoverError()
 
 	schema, err := getSchema(circuit)
@@ -62,7 +82,7 @@ func CircuitToLeanWithName(circuit abstractor.Circuit, field ecc.ID, namespace s
 		FieldID: field,
 	}
 
-	err = circuit.AbsDefine(&api)
+	err = circuit.Define(&api)
 	if err != nil {
 		return "", err
 	}
@@ -80,7 +100,7 @@ func CircuitToLeanWithName(circuit abstractor.Circuit, field ecc.ID, namespace s
 // CircuitToLean exports a `circuit` to Lean over a `field` with the namespace being the
 // struct name of `circuit`
 // When the namespace argument is not defined, it uses the name of the struct circuit
-func CircuitToLean(circuit abstractor.Circuit, field ecc.ID) (string, error) {
+func CircuitToLean(circuit frontend.Circuit, field ecc.ID) (string, error) {
 	name := getStructName(circuit)
 	return CircuitToLeanWithName(circuit, field, name)
 }
@@ -110,7 +130,7 @@ func GadgetToLean(gadget abstractor.GadgetDefinition, field ecc.ID) (string, err
 }
 
 // ExtractCircuits is used to export a series of `circuits` to Lean over a `field` under `namespace`.
-func ExtractCircuits(namespace string, field ecc.ID, circuits ...abstractor.Circuit) (out string, err error) {
+func ExtractCircuits(namespace string, field ecc.ID, circuits ...frontend.Circuit) (out string, err error) {
 	defer recoverError()
 
 	api := CodeExtractor{
@@ -142,7 +162,7 @@ func ExtractCircuits(namespace string, field ecc.ID, circuits ...abstractor.Circ
 		past_circuits = append(past_circuits, name)
 
 		circuitInit(circuit, schema)
-		err = circuit.AbsDefine(&api)
+		err = circuit.Define(&api)
 		if err != nil {
 			return "", err
 		}
diff --git a/extractor/test/another_circuit_test.go b/extractor/test/another_circuit_test.go
index e3ce26b..5ed0530 100644
--- a/extractor/test/another_circuit_test.go
+++ b/extractor/test/another_circuit_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -17,7 +16,7 @@ type IntArrayGadget struct {
 	NestedMatrix [2][2]int
 }
 
-func (gadget IntArrayGadget) DefineGadget(api abstractor.API) interface{} {
+func (gadget IntArrayGadget) DefineGadget(api frontend.API) interface{} {
 	r := api.FromBinary(gadget.In...)
 	api.Mul(gadget.Matrix[0], gadget.Matrix[1])
 	return []frontend.Variable{r, r, r}
@@ -28,7 +27,7 @@ type AnotherCircuit struct {
 	Matrix [2][2]int
 }
 
-func (circuit *AnotherCircuit) AbsDefine(api abstractor.API) error {
+func (circuit *AnotherCircuit) Define(api frontend.API) error {
 	r := extractor.Call1(api, IntArrayGadget{
 		circuit.In,
 		circuit.Matrix[0],
@@ -41,10 +40,6 @@ func (circuit *AnotherCircuit) AbsDefine(api abstractor.API) error {
 	return nil
 }
 
-func (circuit AnotherCircuit) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestAnotherCircuit(t *testing.T) {
 	m := [2][2]int{
 		{0, 36},
diff --git a/extractor/test/circuit_with_parameter_test.go b/extractor/test/circuit_with_parameter_test.go
index 22c8cb1..77cc439 100644
--- a/extractor/test/circuit_with_parameter_test.go
+++ b/extractor/test/circuit_with_parameter_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 	"github.com/stretchr/testify/assert"
 )
@@ -17,7 +16,7 @@ type ReturnItself struct {
 	Out  []frontend.Variable
 }
 
-func (gadget ReturnItself) DefineGadget(api abstractor.API) interface{} {
+func (gadget ReturnItself) DefineGadget(api frontend.API) interface{} {
 	for i := 0; i < len(gadget.In_1); i++ {
 		gadget.Out[i] = api.Mul(gadget.In_1[i], gadget.In_1[i])
 	}
@@ -30,7 +29,7 @@ type SliceGadget struct {
 	In_2 []frontend.Variable
 }
 
-func (gadget SliceGadget) DefineGadget(api abstractor.API) interface{} {
+func (gadget SliceGadget) DefineGadget(api frontend.API) interface{} {
 	for i := 0; i < len(gadget.In_1); i++ {
 		api.Mul(gadget.In_1[i], gadget.In_2[i])
 	}
@@ -46,7 +45,7 @@ type CircuitWithParameter struct {
 	Param int
 }
 
-func (circuit *CircuitWithParameter) AbsDefine(api abstractor.API) error {
+func (circuit *CircuitWithParameter) Define(api frontend.API) error {
 	D := make([]frontend.Variable, 3)
 	for i := 0; i < len(circuit.Path); i++ {
 		D = extractor.Call1(api, ReturnItself{
@@ -75,10 +74,6 @@ func (circuit *CircuitWithParameter) AbsDefine(api abstractor.API) error {
 	return nil
 }
 
-func (circuit CircuitWithParameter) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestCircuitWithParameter(t *testing.T) {
 	paramValue := 20
 	assignment := CircuitWithParameter{Path: make([]frontend.Variable, 3), Tree: make([]frontend.Variable, 2)}
diff --git a/extractor/test/deletion_mbu_circuit_test.go b/extractor/test/deletion_mbu_circuit_test.go
index 7ded5c5..7ec28f8 100644
--- a/extractor/test/deletion_mbu_circuit_test.go
+++ b/extractor/test/deletion_mbu_circuit_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -21,7 +20,7 @@ type DeletionProof struct {
 	Depth     int
 }
 
-func (gadget DeletionProof) DefineGadget(api abstractor.API) interface{} {
+func (gadget DeletionProof) DefineGadget(api frontend.API) interface{} {
 	return gadget.PreRoot
 }
 
@@ -42,7 +41,7 @@ type DeletionMbuCircuit struct {
 	Depth     int
 }
 
-func (circuit *DeletionMbuCircuit) AbsDefine(api abstractor.API) error {
+func (circuit *DeletionMbuCircuit) Define(api frontend.API) error {
 	root := extractor.Call(api, DeletionProof{
 		DeletionIndices: circuit.DeletionIndices,
 		PreRoot:         circuit.PreRoot,
@@ -58,10 +57,6 @@ func (circuit *DeletionMbuCircuit) AbsDefine(api abstractor.API) error {
 	return nil
 }
 
-func (circuit DeletionMbuCircuit) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestDeletionMbuCircuit(t *testing.T) {
 	batchSize := 2
 	treeDepth := 3
diff --git a/extractor/test/merkle_recover_test.go b/extractor/test/merkle_recover_test.go
index 44f7ebb..29d625e 100644
--- a/extractor/test/merkle_recover_test.go
+++ b/extractor/test/merkle_recover_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -16,7 +15,7 @@ type DummyHash struct {
 	In_2 frontend.Variable
 }
 
-func (gadget DummyHash) DefineGadget(api abstractor.API) interface{} {
+func (gadget DummyHash) DefineGadget(api frontend.API) interface{} {
 	r := api.Mul(gadget.In_1, gadget.In_2)
 	return r
 }
@@ -28,7 +27,7 @@ type MerkleRecover struct {
 	Proof   [20]frontend.Variable `gnark:",secret"`
 }
 
-func (circuit *MerkleRecover) AbsDefine(api abstractor.API) error {
+func (circuit *MerkleRecover) Define(api frontend.API) error {
 	current := circuit.Element
 	for i := 0; i < len(circuit.Path); i++ {
 		leftHash := extractor.Call(api, DummyHash{current, circuit.Proof[i]})
@@ -40,10 +39,6 @@ func (circuit *MerkleRecover) AbsDefine(api abstractor.API) error {
 	return nil
 }
 
-func (circuit MerkleRecover) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestMerkleRecover(t *testing.T) {
 	assignment := MerkleRecover{}
 	out, err := extractor.CircuitToLean(&assignment, ecc.BN254)
diff --git a/extractor/test/my_circuit_test.go b/extractor/test/my_circuit_test.go
index 5726dc7..577317d 100644
--- a/extractor/test/my_circuit_test.go
+++ b/extractor/test/my_circuit_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -17,16 +16,12 @@ type MyCircuit struct {
 	Out  frontend.Variable
 }
 
-func (circuit *MyCircuit) AbsDefine(api abstractor.API) error {
+func (circuit *MyCircuit) Define(api frontend.API) error {
 	sum := api.Add(circuit.In_1, circuit.In_2)
 	api.AssertIsEqual(sum, circuit.Out)
 	return nil
 }
 
-func (circuit MyCircuit) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestMyCircuit(t *testing.T) {
 	assignment := MyCircuit{}
 	out, err := extractor.CircuitToLean(&assignment, ecc.BN254)
diff --git a/extractor/test/slices_optimisation_test.go b/extractor/test/slices_optimisation_test.go
index 8b5a412..328878f 100644
--- a/extractor/test/slices_optimisation_test.go
+++ b/extractor/test/slices_optimisation_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -15,7 +14,7 @@ type TwoSlices struct {
 	TwoDim [][]frontend.Variable
 }
 
-func (gadget TwoSlices) DefineGadget(api abstractor.API) interface{} {
+func (gadget TwoSlices) DefineGadget(api frontend.API) interface{} {
 	return gadget.TwoDim
 }
 
@@ -23,7 +22,7 @@ type ThreeSlices struct {
 	ThreeDim [][][]frontend.Variable
 }
 
-func (gadget ThreeSlices) DefineGadget(api abstractor.API) interface{} {
+func (gadget ThreeSlices) DefineGadget(api frontend.API) interface{} {
 	return gadget.ThreeDim
 }
 
@@ -32,7 +31,7 @@ type SlicesGadget struct {
 	ThreeDim [][][]frontend.Variable
 }
 
-func (gadget SlicesGadget) DefineGadget(api abstractor.API) interface{} {
+func (gadget SlicesGadget) DefineGadget(api frontend.API) interface{} {
 	return append(gadget.ThreeDim[0][0], gadget.TwoDim[0]...)
 }
 
@@ -43,7 +42,7 @@ type SlicesOptimisation struct {
 	ThreeDim [][][]frontend.Variable
 }
 
-func (circuit *SlicesOptimisation) AbsDefine(api abstractor.API) error {
+func (circuit *SlicesOptimisation) Define(api frontend.API) error {
 	extractor.Call1(api, SlicesGadget{
 		TwoDim:   circuit.TwoDim,
 		ThreeDim: circuit.ThreeDim,
@@ -76,10 +75,6 @@ func (circuit *SlicesOptimisation) AbsDefine(api abstractor.API) error {
 	return nil
 }
 
-func (circuit SlicesOptimisation) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestSlicesOptimisation(t *testing.T) {
 	depthOne := 2
 	depthTwo := 3
diff --git a/extractor/test/to_binary_circuit_test.go b/extractor/test/to_binary_circuit_test.go
index b6575bc..4b9ffca 100644
--- a/extractor/test/to_binary_circuit_test.go
+++ b/extractor/test/to_binary_circuit_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -15,7 +14,7 @@ type OptimisedVectorGadget struct {
 	In frontend.Variable
 }
 
-func (gadget OptimisedVectorGadget) DefineGadget(api abstractor.API) interface{} {
+func (gadget OptimisedVectorGadget) DefineGadget(api frontend.API) interface{} {
 	return api.ToBinary(gadget.In, 3)
 }
 
@@ -26,7 +25,7 @@ type VectorGadget struct {
 	Nested [][]frontend.Variable
 }
 
-func (gadget VectorGadget) DefineGadget(api abstractor.API) interface{} {
+func (gadget VectorGadget) DefineGadget(api frontend.API) interface{} {
 	var sum frontend.Variable
 	for i := 0; i < len(gadget.In_1); i++ {
 		sum = api.Mul(gadget.In_1[i], gadget.In_2[i])
@@ -40,7 +39,7 @@ type ToBinaryCircuit struct {
 	Double [][]frontend.Variable `gnark:",public"`
 }
 
-func (circuit *ToBinaryCircuit) AbsDefine(api abstractor.API) error {
+func (circuit *ToBinaryCircuit) Define(api frontend.API) error {
 	bin := api.ToBinary(circuit.In, 3)
 	bout := api.ToBinary(circuit.Out, 3)
 
@@ -52,10 +51,6 @@ func (circuit *ToBinaryCircuit) AbsDefine(api abstractor.API) error {
 	return nil
 }
 
-func (circuit ToBinaryCircuit) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestGadgetExtraction(t *testing.T) {
 	dim_1 := 3
 	dim_2 := 3
diff --git a/extractor/test/two_gadgets_test.go b/extractor/test/two_gadgets_test.go
index 1451b32..468afa9 100644
--- a/extractor/test/two_gadgets_test.go
+++ b/extractor/test/two_gadgets_test.go
@@ -6,7 +6,6 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -17,7 +16,7 @@ type MyWidget struct {
 	Num    uint32
 }
 
-func (gadget MyWidget) DefineGadget(api abstractor.API) interface{} {
+func (gadget MyWidget) DefineGadget(api frontend.API) interface{} {
 	sum := api.Add(gadget.Test_1, gadget.Test_2)
 	mul := api.Mul(gadget.Test_1, gadget.Test_2)
 	r := api.Div(sum, mul)
@@ -31,7 +30,7 @@ type MySecondWidget struct {
 	Num    int
 }
 
-func (gadget MySecondWidget) DefineGadget(api abstractor.API) interface{} {
+func (gadget MySecondWidget) DefineGadget(api frontend.API) interface{} {
 	mul := api.Mul(gadget.Test_1, gadget.Test_2)
 	snd := extractor.Call(api, MyWidget{gadget.Test_1, gadget.Test_2, uint32(gadget.Num)})
 	api.Mul(mul, snd)
@@ -44,17 +43,13 @@ type TwoGadgets struct {
 	Num  int
 }
 
-func (circuit *TwoGadgets) AbsDefine(api abstractor.API) error {
+func (circuit *TwoGadgets) Define(api frontend.API) error {
 	sum := api.Add(circuit.In_1, circuit.In_2)
 	prod := api.Mul(circuit.In_1, circuit.In_2)
 	extractor.CallVoid(api, MySecondWidget{sum, prod, circuit.Num})
 	return nil
 }
 
-func (circuit TwoGadgets) Define(api frontend.API) error {
-	return abstractor.Concretize(api, &circuit)
-}
-
 func TestTwoGadgets(t *testing.T) {
 	assignment := TwoGadgets{Num: 11}
 	out, err := extractor.CircuitToLean(&assignment, ecc.BN254)

From 858c60d0a1da71b8ce4ac8dedaab23dc990e2bdd Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 18:54:57 +0100
Subject: [PATCH 02/11] Gofmt

---
 abstractor/abstractor.go |  2 +-
 extractor/interface.go   | 50 ++++++++++++++++++++--------------------
 2 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/abstractor/abstractor.go b/abstractor/abstractor.go
index 3da50ba..867f5e6 100644
--- a/abstractor/abstractor.go
+++ b/abstractor/abstractor.go
@@ -8,4 +8,4 @@ type Gadget interface {
 
 type GadgetDefinition interface {
 	DefineGadget(api frontend.API) interface{}
-}
\ No newline at end of file
+}
diff --git a/extractor/interface.go b/extractor/interface.go
index a42400f..7474838 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -17,49 +17,49 @@ import (
 
 // CallVoid is used to call a Gadget which doesn't return anything
 func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
-    if abs, ok := api.(*CodeExtractor); ok {
-        abs.Call(gadget)
-    } else {
-        gadget.DefineGadget(api)
-    }
+	if abs, ok := api.(*CodeExtractor); ok {
+		abs.Call(gadget)
+	} else {
+		gadget.DefineGadget(api)
+	}
 }
 
 // Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
 func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
-    if abs, ok := api.(*CodeExtractor); ok {
-        return abs.Call(gadget).(frontend.Variable)
-    } else {
-        return gadget.DefineGadget(api).(frontend.Variable)
-    }
+	if abs, ok := api.(*CodeExtractor); ok {
+		return abs.Call(gadget).(frontend.Variable)
+	} else {
+		return gadget.DefineGadget(api).(frontend.Variable)
+	}
 }
 
 // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
 func Call1(api frontend.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
-    if abs, ok := api.(*CodeExtractor); ok {
-        return abs.Call(gadget).([]frontend.Variable)
-    } else {
-        return gadget.DefineGadget(api).([]frontend.Variable)
-    }
+	if abs, ok := api.(*CodeExtractor); ok {
+		return abs.Call(gadget).([]frontend.Variable)
+	} else {
+		return gadget.DefineGadget(api).([]frontend.Variable)
+	}
 }
 
 // Call2 is used to call a Gadget which returns a [][]frontend.Variable
 // (i.e. `Vector (Vector F a) b` in Lean)
 func Call2(api frontend.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
-    if abs, ok := api.(*CodeExtractor); ok {
-        return abs.Call(gadget).([][]frontend.Variable)
-    } else {
-        return gadget.DefineGadget(api).([][]frontend.Variable)
-    }
+	if abs, ok := api.(*CodeExtractor); ok {
+		return abs.Call(gadget).([][]frontend.Variable)
+	} else {
+		return gadget.DefineGadget(api).([][]frontend.Variable)
+	}
 }
 
 // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
 // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
 func Call3(api frontend.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
-    if abs, ok := api.(*CodeExtractor); ok {
-        return abs.Call(gadget).([][][]frontend.Variable)
-    } else {
-        return gadget.DefineGadget(api).([][][]frontend.Variable)
-    }
+	if abs, ok := api.(*CodeExtractor); ok {
+		return abs.Call(gadget).([][][]frontend.Variable)
+	} else {
+		return gadget.DefineGadget(api).([][][]frontend.Variable)
+	}
 }
 
 // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`

From c136f07c4af02eaec4688231c8f333024f57eace Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 19:25:27 +0100
Subject: [PATCH 03/11] refactor call

---
 extractor/interface.go | 36 ++++++++++++------------------------
 1 file changed, 12 insertions(+), 24 deletions(-)

diff --git a/extractor/interface.go b/extractor/interface.go
index 7474838..cb5851e 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -15,51 +15,39 @@ import (
 	"golang.org/x/exp/slices"
 )
 
-// CallVoid is used to call a Gadget which doesn't return anything
-func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
+func privateCall(api frontend.API, gadget abstractor.GadgetDefinition) interface{} {
 	if abs, ok := api.(*CodeExtractor); ok {
-		abs.Call(gadget)
+		return abs.Call(gadget).(frontend.Variable)
 	} else {
-		gadget.DefineGadget(api)
+		return gadget.DefineGadget(api).(frontend.Variable)
 	}
 }
 
+// CallVoid is used to call a Gadget which doesn't return anything
+func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
+	privateCall(api, gadget)
+}
+
 // Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
 func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
-	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget).(frontend.Variable)
-	} else {
-		return gadget.DefineGadget(api).(frontend.Variable)
-	}
+	return privateCall(api, gadget).(frontend.Variable)
 }
 
 // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
 func Call1(api frontend.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
-	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget).([]frontend.Variable)
-	} else {
-		return gadget.DefineGadget(api).([]frontend.Variable)
-	}
+	return privateCall(api, gadget).([]frontend.Variable)
 }
 
 // Call2 is used to call a Gadget which returns a [][]frontend.Variable
 // (i.e. `Vector (Vector F a) b` in Lean)
 func Call2(api frontend.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
-	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget).([][]frontend.Variable)
-	} else {
-		return gadget.DefineGadget(api).([][]frontend.Variable)
-	}
+	return privateCall(api, gadget).([][]frontend.Variable)
 }
 
 // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
 // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
 func Call3(api frontend.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
-	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget).([][][]frontend.Variable)
-	} else {
-		return gadget.DefineGadget(api).([][][]frontend.Variable)
-	}
+	return privateCall(api, gadget).([][][]frontend.Variable)
 }
 
 // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`

From 8babf5880fc5afa94dc9504319c125d0584ed4f3 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 19:36:19 +0100
Subject: [PATCH 04/11] Fix rawcall

---
 extractor/interface.go | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/extractor/interface.go b/extractor/interface.go
index cb5851e..d4a33b8 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -15,39 +15,39 @@ import (
 	"golang.org/x/exp/slices"
 )
 
-func privateCall(api frontend.API, gadget abstractor.GadgetDefinition) interface{} {
+func RawCall(api frontend.API, gadget abstractor.GadgetDefinition) interface{} {
 	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget).(frontend.Variable)
+		return abs.Call(gadget)
 	} else {
-		return gadget.DefineGadget(api).(frontend.Variable)
+		return gadget.DefineGadget(api)
 	}
 }
 
 // CallVoid is used to call a Gadget which doesn't return anything
 func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
-	privateCall(api, gadget)
+	RawCall(api, gadget)
 }
 
 // Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
 func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
-	return privateCall(api, gadget).(frontend.Variable)
+	return RawCall(api, gadget).(frontend.Variable)
 }
 
 // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
 func Call1(api frontend.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
-	return privateCall(api, gadget).([]frontend.Variable)
+	return RawCall(api, gadget).([]frontend.Variable)
 }
 
 // Call2 is used to call a Gadget which returns a [][]frontend.Variable
 // (i.e. `Vector (Vector F a) b` in Lean)
 func Call2(api frontend.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
-	return privateCall(api, gadget).([][]frontend.Variable)
+	return RawCall(api, gadget).([][]frontend.Variable)
 }
 
 // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
 // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
 func Call3(api frontend.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
-	return privateCall(api, gadget).([][][]frontend.Variable)
+	return RawCall(api, gadget).([][][]frontend.Variable)
 }
 
 // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`

From 3f161e2d5e2fd0aacbf491ae55d15beaba058016 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 19:38:57 +0100
Subject: [PATCH 05/11] Fix

---
 abstractor/interface.go | 193 ++++++++++++++++++++++++++++++++++++++++
 extractor/interface.go  |  20 ++---
 2 files changed, 201 insertions(+), 12 deletions(-)
 create mode 100644 abstractor/interface.go

diff --git a/abstractor/interface.go b/abstractor/interface.go
new file mode 100644
index 0000000..79854d8
--- /dev/null
+++ b/abstractor/interface.go
@@ -0,0 +1,193 @@
+// This file contains the public API for using the extractor.
+// The Call functions are used to call gadgets and get their returnd object.
+// These methods are prepared for doing automated casting from interface{}.
+// Alternatively it's possible to do manual casting by calling
+// abstractor.API.Call() and casting the result to the needed type.
+package abstractor
+
+// import (
+// 	"fmt"
+// 	"strings"
+
+// 	"github.com/consensys/gnark-crypto/ecc"
+// 	"github.com/consensys/gnark/frontend"
+// 	"golang.org/x/exp/slices"
+// )
+
+// func RawCall(api frontend.API, gadget GadgetDefinition) interface{} {
+// 	if abs, ok := api.(*CodeExtractor); ok {
+// 		return abs.Call(gadget).(frontend.Variable)
+// 	} else {
+// 		return gadget.DefineGadget(api).(frontend.Variable)
+// 	}
+// }
+
+// // CallVoid is used to call a Gadget which doesn't return anything
+// func CallVoid(api frontend.API, gadget GadgetDefinition) {
+// 	RawCall(api, gadget)
+// }
+
+// // Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
+// func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
+// 	return RawCall(api, gadget).(frontend.Variable)
+// }
+
+// // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
+// func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
+// 	return RawCall(api, gadget).([]frontend.Variable)
+// }
+
+// // Call2 is used to call a Gadget which returns a [][]frontend.Variable
+// // (i.e. `Vector (Vector F a) b` in Lean)
+// func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
+// 	return RawCall(api, gadget).([][]frontend.Variable)
+// }
+
+// // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
+// // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
+// func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
+// 	return RawCall(api, gadget).([][][]frontend.Variable)
+// }
+
+// // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`
+// // CircuitToLeanWithName and CircuitToLean aren't joined in a single function
+// // CircuitToLean(circuit abstractor.Circuit, field ecc.ID, namespace ...string) because the long term view
+// // is to add an optional parameter to support custom `set_option` directives in the header.
+// func CircuitToLeanWithName(circuit frontend.Circuit, field ecc.ID, namespace string) (out string, err error) {
+// 	defer recoverError()
+
+// 	schema, err := getSchema(circuit)
+// 	if err != nil {
+// 		return "", err
+// 	}
+
+// 	circuitInit(circuit, schema)
+
+// 	api := CodeExtractor{
+// 		Code:    []App{},
+// 		Gadgets: []ExGadget{},
+// 		FieldID: field,
+// 	}
+
+// 	err = circuit.Define(&api)
+// 	if err != nil {
+// 		return "", err
+// 	}
+
+// 	extractorCircuit := ExCircuit{
+// 		Inputs:  getExArgs(circuit, schema.Fields),
+// 		Gadgets: api.Gadgets,
+// 		Code:    api.Code,
+// 		Field:   api.FieldID,
+// 	}
+// 	out = exportCircuit(extractorCircuit, namespace)
+// 	return out, nil
+// }
+
+// // CircuitToLean exports a `circuit` to Lean over a `field` with the namespace being the
+// // struct name of `circuit`
+// // When the namespace argument is not defined, it uses the name of the struct circuit
+// func CircuitToLean(circuit frontend.Circuit, field ecc.ID) (string, error) {
+// 	name := getStructName(circuit)
+// 	return CircuitToLeanWithName(circuit, field, name)
+// }
+
+// // GadgetToLeanWithName exports a `gadget` to Lean over a `field` with `namespace`
+// // Same notes written for CircuitToLeanWithName apply to GadgetToLeanWithName and GadgetToLean
+// func GadgetToLeanWithName(gadget abstractor.GadgetDefinition, field ecc.ID, namespace string) (out string, err error) {
+// 	defer recoverError()
+
+// 	api := CodeExtractor{
+// 		Code:    []App{},
+// 		Gadgets: []ExGadget{},
+// 		FieldID: field,
+// 	}
+
+// 	api.DefineGadget(gadget)
+// 	gadgets := exportGadgets(api.Gadgets)
+// 	prelude := exportPrelude(namespace, api.FieldID.ScalarField())
+// 	footer := exportFooter(namespace)
+// 	return fmt.Sprintf("%s\n\n%s\n\n%s", prelude, gadgets, footer), nil
+// }
+
+// // GadgetToLean exports a `gadget` to Lean over a `field`
+// func GadgetToLean(gadget abstractor.GadgetDefinition, field ecc.ID) (string, error) {
+// 	name := getStructName(gadget)
+// 	return GadgetToLeanWithName(gadget, field, name)
+// }
+
+// // ExtractCircuits is used to export a series of `circuits` to Lean over a `field` under `namespace`.
+// func ExtractCircuits(namespace string, field ecc.ID, circuits ...frontend.Circuit) (out string, err error) {
+// 	defer recoverError()
+
+// 	api := CodeExtractor{
+// 		Code:    []App{},
+// 		Gadgets: []ExGadget{},
+// 		FieldID: field,
+// 	}
+
+// 	var circuits_extracted []string
+// 	var past_circuits []string
+
+// 	extractorCircuit := ExCircuit{
+// 		Inputs:  []ExArg{},
+// 		Gadgets: []ExGadget{},
+// 		Code:    []App{},
+// 		Field:   api.FieldID,
+// 	}
+
+// 	for _, circuit := range circuits {
+// 		schema, err := getSchema(circuit)
+// 		if err != nil {
+// 			return "", err
+// 		}
+// 		args := getExArgs(circuit, schema.Fields)
+// 		name := generateUniqueName(circuit, args)
+// 		if slices.Contains(past_circuits, name) {
+// 			continue
+// 		}
+// 		past_circuits = append(past_circuits, name)
+
+// 		circuitInit(circuit, schema)
+// 		err = circuit.Define(&api)
+// 		if err != nil {
+// 			return "", err
+// 		}
+
+// 		extractorCircuit.Inputs = args
+// 		extractorCircuit.Code = api.Code
+
+// 		circ := fmt.Sprintf("def %s %s: Prop :=\n%s", name, genArgs(extractorCircuit.Inputs), genCircuitBody(extractorCircuit))
+// 		circuits_extracted = append(circuits_extracted, circ)
+
+// 		// Resetting elements for next circuit
+// 		extractorCircuit.Inputs = []ExArg{}
+// 		extractorCircuit.Code = []App{}
+// 		api.Code = []App{}
+// 	}
+
+// 	prelude := exportPrelude(namespace, extractorCircuit.Field.ScalarField())
+// 	gadgets := exportGadgets(api.Gadgets)
+// 	footer := exportFooter(namespace)
+// 	return fmt.Sprintf("%s\n\n%s\n\n%s\n\n%s", prelude, gadgets, strings.Join(circuits_extracted, "\n\n"), footer), nil
+// }
+
+// // ExtractGadgets is used to export a series of `gadgets` to Lean over a `field` under `namespace`.
+// func ExtractGadgets(namespace string, field ecc.ID, gadgets ...abstractor.GadgetDefinition) (out string, err error) {
+// 	defer recoverError()
+
+// 	api := CodeExtractor{
+// 		Code:    []App{},
+// 		Gadgets: []ExGadget{},
+// 		FieldID: field,
+// 	}
+
+// 	for _, gadget := range gadgets {
+// 		api.DefineGadget(gadget)
+// 	}
+
+// 	gadgets_string := exportGadgets(api.Gadgets)
+// 	prelude := exportPrelude(namespace, api.FieldID.ScalarField())
+// 	footer := exportFooter(namespace)
+// 	return fmt.Sprintf("%s\n\n%s\n\n%s", prelude, gadgets_string, footer), nil
+// }
diff --git a/extractor/interface.go b/extractor/interface.go
index d4a33b8..79baeb6 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -15,39 +15,35 @@ import (
 	"golang.org/x/exp/slices"
 )
 
-func RawCall(api frontend.API, gadget abstractor.GadgetDefinition) interface{} {
+// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
+func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
 	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget)
+		return abs.Call(gadget).(frontend.Variable)
 	} else {
-		return gadget.DefineGadget(api)
+		return gadget.DefineGadget(api).(frontend.Variable)
 	}
 }
 
 // CallVoid is used to call a Gadget which doesn't return anything
 func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
-	RawCall(api, gadget)
-}
-
-// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
-func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
-	return RawCall(api, gadget).(frontend.Variable)
+	Call(api, gadget)
 }
 
 // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
 func Call1(api frontend.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
-	return RawCall(api, gadget).([]frontend.Variable)
+	return Call(api, gadget).([]frontend.Variable)
 }
 
 // Call2 is used to call a Gadget which returns a [][]frontend.Variable
 // (i.e. `Vector (Vector F a) b` in Lean)
 func Call2(api frontend.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
-	return RawCall(api, gadget).([][]frontend.Variable)
+	return Call(api, gadget).([][]frontend.Variable)
 }
 
 // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
 // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
 func Call3(api frontend.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
-	return RawCall(api, gadget).([][][]frontend.Variable)
+	return Call(api, gadget).([][][]frontend.Variable)
 }
 
 // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`

From 7a67112f4b56cd0bc2b94ff984e0585216908413 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 21:54:52 +0100
Subject: [PATCH 06/11] moved interface to abstractor

---
 abstractor/abstractor.go                      |   5 +
 abstractor/interface.go                       | 224 +++---------------
 extractor/extractor.go                        |   5 +-
 extractor/interface.go                        |  31 ---
 extractor/test/another_circuit_test.go        |   3 +-
 extractor/test/circuit_with_parameter_test.go |   7 +-
 extractor/test/deletion_mbu_circuit_test.go   |   3 +-
 extractor/test/merkle_recover_test.go         |   5 +-
 extractor/test/slices_optimisation_test.go    |  17 +-
 extractor/test/to_binary_circuit_test.go      |   3 +-
 extractor/test/two_gadgets_test.go            |   5 +-
 11 files changed, 70 insertions(+), 238 deletions(-)

diff --git a/abstractor/abstractor.go b/abstractor/abstractor.go
index 867f5e6..8fc2439 100644
--- a/abstractor/abstractor.go
+++ b/abstractor/abstractor.go
@@ -9,3 +9,8 @@ type Gadget interface {
 type GadgetDefinition interface {
 	DefineGadget(api frontend.API) interface{}
 }
+
+type API interface {
+	frontend.API
+	Call(gadget GadgetDefinition) interface{}
+}
\ No newline at end of file
diff --git a/abstractor/interface.go b/abstractor/interface.go
index 79854d8..723f1d9 100644
--- a/abstractor/interface.go
+++ b/abstractor/interface.go
@@ -5,189 +5,41 @@
 // abstractor.API.Call() and casting the result to the needed type.
 package abstractor
 
-// import (
-// 	"fmt"
-// 	"strings"
-
-// 	"github.com/consensys/gnark-crypto/ecc"
-// 	"github.com/consensys/gnark/frontend"
-// 	"golang.org/x/exp/slices"
-// )
-
-// func RawCall(api frontend.API, gadget GadgetDefinition) interface{} {
-// 	if abs, ok := api.(*CodeExtractor); ok {
-// 		return abs.Call(gadget).(frontend.Variable)
-// 	} else {
-// 		return gadget.DefineGadget(api).(frontend.Variable)
-// 	}
-// }
-
-// // CallVoid is used to call a Gadget which doesn't return anything
-// func CallVoid(api frontend.API, gadget GadgetDefinition) {
-// 	RawCall(api, gadget)
-// }
-
-// // Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
-// func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
-// 	return RawCall(api, gadget).(frontend.Variable)
-// }
-
-// // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
-// func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
-// 	return RawCall(api, gadget).([]frontend.Variable)
-// }
-
-// // Call2 is used to call a Gadget which returns a [][]frontend.Variable
-// // (i.e. `Vector (Vector F a) b` in Lean)
-// func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
-// 	return RawCall(api, gadget).([][]frontend.Variable)
-// }
-
-// // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
-// // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
-// func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
-// 	return RawCall(api, gadget).([][][]frontend.Variable)
-// }
-
-// // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`
-// // CircuitToLeanWithName and CircuitToLean aren't joined in a single function
-// // CircuitToLean(circuit abstractor.Circuit, field ecc.ID, namespace ...string) because the long term view
-// // is to add an optional parameter to support custom `set_option` directives in the header.
-// func CircuitToLeanWithName(circuit frontend.Circuit, field ecc.ID, namespace string) (out string, err error) {
-// 	defer recoverError()
-
-// 	schema, err := getSchema(circuit)
-// 	if err != nil {
-// 		return "", err
-// 	}
-
-// 	circuitInit(circuit, schema)
-
-// 	api := CodeExtractor{
-// 		Code:    []App{},
-// 		Gadgets: []ExGadget{},
-// 		FieldID: field,
-// 	}
-
-// 	err = circuit.Define(&api)
-// 	if err != nil {
-// 		return "", err
-// 	}
-
-// 	extractorCircuit := ExCircuit{
-// 		Inputs:  getExArgs(circuit, schema.Fields),
-// 		Gadgets: api.Gadgets,
-// 		Code:    api.Code,
-// 		Field:   api.FieldID,
-// 	}
-// 	out = exportCircuit(extractorCircuit, namespace)
-// 	return out, nil
-// }
-
-// // CircuitToLean exports a `circuit` to Lean over a `field` with the namespace being the
-// // struct name of `circuit`
-// // When the namespace argument is not defined, it uses the name of the struct circuit
-// func CircuitToLean(circuit frontend.Circuit, field ecc.ID) (string, error) {
-// 	name := getStructName(circuit)
-// 	return CircuitToLeanWithName(circuit, field, name)
-// }
-
-// // GadgetToLeanWithName exports a `gadget` to Lean over a `field` with `namespace`
-// // Same notes written for CircuitToLeanWithName apply to GadgetToLeanWithName and GadgetToLean
-// func GadgetToLeanWithName(gadget abstractor.GadgetDefinition, field ecc.ID, namespace string) (out string, err error) {
-// 	defer recoverError()
-
-// 	api := CodeExtractor{
-// 		Code:    []App{},
-// 		Gadgets: []ExGadget{},
-// 		FieldID: field,
-// 	}
-
-// 	api.DefineGadget(gadget)
-// 	gadgets := exportGadgets(api.Gadgets)
-// 	prelude := exportPrelude(namespace, api.FieldID.ScalarField())
-// 	footer := exportFooter(namespace)
-// 	return fmt.Sprintf("%s\n\n%s\n\n%s", prelude, gadgets, footer), nil
-// }
-
-// // GadgetToLean exports a `gadget` to Lean over a `field`
-// func GadgetToLean(gadget abstractor.GadgetDefinition, field ecc.ID) (string, error) {
-// 	name := getStructName(gadget)
-// 	return GadgetToLeanWithName(gadget, field, name)
-// }
-
-// // ExtractCircuits is used to export a series of `circuits` to Lean over a `field` under `namespace`.
-// func ExtractCircuits(namespace string, field ecc.ID, circuits ...frontend.Circuit) (out string, err error) {
-// 	defer recoverError()
-
-// 	api := CodeExtractor{
-// 		Code:    []App{},
-// 		Gadgets: []ExGadget{},
-// 		FieldID: field,
-// 	}
-
-// 	var circuits_extracted []string
-// 	var past_circuits []string
-
-// 	extractorCircuit := ExCircuit{
-// 		Inputs:  []ExArg{},
-// 		Gadgets: []ExGadget{},
-// 		Code:    []App{},
-// 		Field:   api.FieldID,
-// 	}
-
-// 	for _, circuit := range circuits {
-// 		schema, err := getSchema(circuit)
-// 		if err != nil {
-// 			return "", err
-// 		}
-// 		args := getExArgs(circuit, schema.Fields)
-// 		name := generateUniqueName(circuit, args)
-// 		if slices.Contains(past_circuits, name) {
-// 			continue
-// 		}
-// 		past_circuits = append(past_circuits, name)
-
-// 		circuitInit(circuit, schema)
-// 		err = circuit.Define(&api)
-// 		if err != nil {
-// 			return "", err
-// 		}
-
-// 		extractorCircuit.Inputs = args
-// 		extractorCircuit.Code = api.Code
-
-// 		circ := fmt.Sprintf("def %s %s: Prop :=\n%s", name, genArgs(extractorCircuit.Inputs), genCircuitBody(extractorCircuit))
-// 		circuits_extracted = append(circuits_extracted, circ)
-
-// 		// Resetting elements for next circuit
-// 		extractorCircuit.Inputs = []ExArg{}
-// 		extractorCircuit.Code = []App{}
-// 		api.Code = []App{}
-// 	}
-
-// 	prelude := exportPrelude(namespace, extractorCircuit.Field.ScalarField())
-// 	gadgets := exportGadgets(api.Gadgets)
-// 	footer := exportFooter(namespace)
-// 	return fmt.Sprintf("%s\n\n%s\n\n%s\n\n%s", prelude, gadgets, strings.Join(circuits_extracted, "\n\n"), footer), nil
-// }
-
-// // ExtractGadgets is used to export a series of `gadgets` to Lean over a `field` under `namespace`.
-// func ExtractGadgets(namespace string, field ecc.ID, gadgets ...abstractor.GadgetDefinition) (out string, err error) {
-// 	defer recoverError()
-
-// 	api := CodeExtractor{
-// 		Code:    []App{},
-// 		Gadgets: []ExGadget{},
-// 		FieldID: field,
-// 	}
-
-// 	for _, gadget := range gadgets {
-// 		api.DefineGadget(gadget)
-// 	}
-
-// 	gadgets_string := exportGadgets(api.Gadgets)
-// 	prelude := exportPrelude(namespace, api.FieldID.ScalarField())
-// 	footer := exportFooter(namespace)
-// 	return fmt.Sprintf("%s\n\n%s\n\n%s", prelude, gadgets_string, footer), nil
-// }
+import (
+	"github.com/consensys/gnark/frontend"
+)
+
+func RawCall(api frontend.API, gadget GadgetDefinition) interface{} {
+	if abs, ok := api.(API); ok {
+		return abs.Call(gadget).(frontend.Variable)
+	} else {
+		return gadget.DefineGadget(api).(frontend.Variable)
+	}
+}
+
+// CallVoid is used to call a Gadget which doesn't return anything
+func CallVoid(api frontend.API, gadget GadgetDefinition) {
+	RawCall(api, gadget)
+}
+
+// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
+func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
+	return RawCall(api, gadget).(frontend.Variable)
+}
+
+// Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
+func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
+	return RawCall(api, gadget).([]frontend.Variable)
+}
+
+// Call2 is used to call a Gadget which returns a [][]frontend.Variable
+// (i.e. `Vector (Vector F a) b` in Lean)
+func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
+	return RawCall(api, gadget).([][]frontend.Variable)
+}
+
+// Call3 is used to call a Gadget which returns a [][][]frontend.Variable
+// (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
+func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
+	return RawCall(api, gadget).([][][]frontend.Variable)
+}
\ No newline at end of file
diff --git a/extractor/extractor.go b/extractor/extractor.go
index 6004ce6..c428219 100644
--- a/extractor/extractor.go
+++ b/extractor/extractor.go
@@ -5,12 +5,11 @@ import (
 	"math/big"
 	"reflect"
 
-	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
-
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/backend/hint"
 	"github.com/consensys/gnark/frontend"
 	"github.com/consensys/gnark/frontend/schema"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 )
 
 type Operand interface {
@@ -474,4 +473,4 @@ func (ce *CodeExtractor) DefineGadget(gadget abstractor.GadgetDefinition) abstra
 	return &exGadget
 }
 
-var _ frontend.API = &CodeExtractor{}
+var _ abstractor.API = &CodeExtractor{}
diff --git a/extractor/interface.go b/extractor/interface.go
index 79baeb6..6836e31 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -15,37 +15,6 @@ import (
 	"golang.org/x/exp/slices"
 )
 
-// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
-func Call(api frontend.API, gadget abstractor.GadgetDefinition) frontend.Variable {
-	if abs, ok := api.(*CodeExtractor); ok {
-		return abs.Call(gadget).(frontend.Variable)
-	} else {
-		return gadget.DefineGadget(api).(frontend.Variable)
-	}
-}
-
-// CallVoid is used to call a Gadget which doesn't return anything
-func CallVoid(api frontend.API, gadget abstractor.GadgetDefinition) {
-	Call(api, gadget)
-}
-
-// Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
-func Call1(api frontend.API, gadget abstractor.GadgetDefinition) []frontend.Variable {
-	return Call(api, gadget).([]frontend.Variable)
-}
-
-// Call2 is used to call a Gadget which returns a [][]frontend.Variable
-// (i.e. `Vector (Vector F a) b` in Lean)
-func Call2(api frontend.API, gadget abstractor.GadgetDefinition) [][]frontend.Variable {
-	return Call(api, gadget).([][]frontend.Variable)
-}
-
-// Call3 is used to call a Gadget which returns a [][][]frontend.Variable
-// (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
-func Call3(api frontend.API, gadget abstractor.GadgetDefinition) [][][]frontend.Variable {
-	return Call(api, gadget).([][][]frontend.Variable)
-}
-
 // CircuitToLeanWithName exports a `circuit` to Lean over a `field` with `namespace`
 // CircuitToLeanWithName and CircuitToLean aren't joined in a single function
 // CircuitToLean(circuit abstractor.Circuit, field ecc.ID, namespace ...string) because the long term view
diff --git a/extractor/test/another_circuit_test.go b/extractor/test/another_circuit_test.go
index 5ed0530..c825af4 100644
--- a/extractor/test/another_circuit_test.go
+++ b/extractor/test/another_circuit_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -28,7 +29,7 @@ type AnotherCircuit struct {
 }
 
 func (circuit *AnotherCircuit) Define(api frontend.API) error {
-	r := extractor.Call1(api, IntArrayGadget{
+	r := abstractor.Call1(api, IntArrayGadget{
 		circuit.In,
 		circuit.Matrix[0],
 		circuit.Matrix,
diff --git a/extractor/test/circuit_with_parameter_test.go b/extractor/test/circuit_with_parameter_test.go
index 77cc439..2c70f8c 100644
--- a/extractor/test/circuit_with_parameter_test.go
+++ b/extractor/test/circuit_with_parameter_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 	"github.com/stretchr/testify/assert"
 )
@@ -48,7 +49,7 @@ type CircuitWithParameter struct {
 func (circuit *CircuitWithParameter) Define(api frontend.API) error {
 	D := make([]frontend.Variable, 3)
 	for i := 0; i < len(circuit.Path); i++ {
-		D = extractor.Call1(api, ReturnItself{
+		D = abstractor.Call1(api, ReturnItself{
 			In_1: circuit.Path,
 			Out:  D,
 		})
@@ -65,10 +66,10 @@ func (circuit *CircuitWithParameter) Define(api frontend.API) error {
 
 	dec := api.FromBinary(bin...)
 	api.AssertIsEqual(circuit.Param, dec)
-	extractor.Call(api, SliceGadget{circuit.Path, circuit.Path})
+	abstractor.Call(api, SliceGadget{circuit.Path, circuit.Path})
 
 	api.Mul(circuit.Path[0], circuit.Path[0])
-	extractor.Call(api, SliceGadget{circuit.Tree, circuit.Tree})
+	abstractor.Call(api, SliceGadget{circuit.Tree, circuit.Tree})
 	api.AssertIsEqual(circuit.Param, circuit.In)
 
 	return nil
diff --git a/extractor/test/deletion_mbu_circuit_test.go b/extractor/test/deletion_mbu_circuit_test.go
index 7ec28f8..8d261cb 100644
--- a/extractor/test/deletion_mbu_circuit_test.go
+++ b/extractor/test/deletion_mbu_circuit_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -42,7 +43,7 @@ type DeletionMbuCircuit struct {
 }
 
 func (circuit *DeletionMbuCircuit) Define(api frontend.API) error {
-	root := extractor.Call(api, DeletionProof{
+	root := abstractor.Call(api, DeletionProof{
 		DeletionIndices: circuit.DeletionIndices,
 		PreRoot:         circuit.PreRoot,
 		IdComms:         circuit.IdComms,
diff --git a/extractor/test/merkle_recover_test.go b/extractor/test/merkle_recover_test.go
index 29d625e..b2850bf 100644
--- a/extractor/test/merkle_recover_test.go
+++ b/extractor/test/merkle_recover_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -30,8 +31,8 @@ type MerkleRecover struct {
 func (circuit *MerkleRecover) Define(api frontend.API) error {
 	current := circuit.Element
 	for i := 0; i < len(circuit.Path); i++ {
-		leftHash := extractor.Call(api, DummyHash{current, circuit.Proof[i]})
-		rightHash := extractor.Call(api, DummyHash{circuit.Proof[i], current})
+		leftHash := abstractor.Call(api, DummyHash{current, circuit.Proof[i]})
+		rightHash := abstractor.Call(api, DummyHash{circuit.Proof[i], current})
 		current = api.Select(circuit.Path[i], rightHash, leftHash)
 	}
 	api.AssertIsEqual(current, circuit.Root)
diff --git a/extractor/test/slices_optimisation_test.go b/extractor/test/slices_optimisation_test.go
index 328878f..d365ffb 100644
--- a/extractor/test/slices_optimisation_test.go
+++ b/extractor/test/slices_optimisation_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -43,32 +44,32 @@ type SlicesOptimisation struct {
 }
 
 func (circuit *SlicesOptimisation) Define(api frontend.API) error {
-	extractor.Call1(api, SlicesGadget{
+	abstractor.Call1(api, SlicesGadget{
 		TwoDim:   circuit.TwoDim,
 		ThreeDim: circuit.ThreeDim,
 	})
-	extractor.Call1(api, SlicesGadget{
+	abstractor.Call1(api, SlicesGadget{
 		TwoDim:   [][]frontend.Variable{circuit.TwoDim[1], circuit.TwoDim[0]},
 		ThreeDim: [][][]frontend.Variable{circuit.ThreeDim[1], circuit.ThreeDim[0]},
 	})
-	extractor.Call1(api, SlicesGadget{
+	abstractor.Call1(api, SlicesGadget{
 		TwoDim:   [][]frontend.Variable{{circuit.TwoDim[1][1]}, {circuit.TwoDim[1][0]}},
 		ThreeDim: [][][]frontend.Variable{circuit.ThreeDim[1], circuit.ThreeDim[0], circuit.ThreeDim[1]},
 	})
-	extractor.Call1(api, SlicesGadget{
+	abstractor.Call1(api, SlicesGadget{
 		TwoDim:   [][]frontend.Variable{circuit.TwoDim[1], {circuit.TwoDim[1][0], circuit.TwoDim[0][0], circuit.TwoDim[1][1]}},
 		ThreeDim: circuit.ThreeDim,
 	})
-	extractor.Call2(api, TwoSlices{
+	abstractor.Call2(api, TwoSlices{
 		TwoDim: circuit.TwoDim,
 	})
-	a := extractor.Call3(api, ThreeSlices{
+	a := abstractor.Call3(api, ThreeSlices{
 		ThreeDim: circuit.ThreeDim,
 	})
-	b := extractor.Call3(api, ThreeSlices{
+	b := abstractor.Call3(api, ThreeSlices{
 		ThreeDim: a,
 	})
-	extractor.Call3(api, ThreeSlices{
+	abstractor.Call3(api, ThreeSlices{
 		ThreeDim: b,
 	})
 
diff --git a/extractor/test/to_binary_circuit_test.go b/extractor/test/to_binary_circuit_test.go
index 4b9ffca..9a34f65 100644
--- a/extractor/test/to_binary_circuit_test.go
+++ b/extractor/test/to_binary_circuit_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -45,7 +46,7 @@ func (circuit *ToBinaryCircuit) Define(api frontend.API) error {
 
 	api.Add(circuit.Double[2][2], circuit.Double[1][1], circuit.Double[0][0])
 	api.Mul(bin[1], bout[1])
-	d := extractor.Call1(api, VectorGadget{circuit.Double[2][:], circuit.Double[0][:], circuit.Double})
+	d := abstractor.Call1(api, VectorGadget{circuit.Double[2][:], circuit.Double[0][:], circuit.Double})
 	api.Mul(d[2], d[1])
 
 	return nil
diff --git a/extractor/test/two_gadgets_test.go b/extractor/test/two_gadgets_test.go
index 468afa9..a996cc8 100644
--- a/extractor/test/two_gadgets_test.go
+++ b/extractor/test/two_gadgets_test.go
@@ -6,6 +6,7 @@ import (
 
 	"github.com/consensys/gnark-crypto/ecc"
 	"github.com/consensys/gnark/frontend"
+	"github.com/reilabs/gnark-lean-extractor/v2/abstractor"
 	"github.com/reilabs/gnark-lean-extractor/v2/extractor"
 )
 
@@ -32,7 +33,7 @@ type MySecondWidget struct {
 
 func (gadget MySecondWidget) DefineGadget(api frontend.API) interface{} {
 	mul := api.Mul(gadget.Test_1, gadget.Test_2)
-	snd := extractor.Call(api, MyWidget{gadget.Test_1, gadget.Test_2, uint32(gadget.Num)})
+	snd := abstractor.Call(api, MyWidget{gadget.Test_1, gadget.Test_2, uint32(gadget.Num)})
 	api.Mul(mul, snd)
 	return nil
 }
@@ -46,7 +47,7 @@ type TwoGadgets struct {
 func (circuit *TwoGadgets) Define(api frontend.API) error {
 	sum := api.Add(circuit.In_1, circuit.In_2)
 	prod := api.Mul(circuit.In_1, circuit.In_2)
-	extractor.CallVoid(api, MySecondWidget{sum, prod, circuit.Num})
+	abstractor.CallVoid(api, MySecondWidget{sum, prod, circuit.Num})
 	return nil
 }
 

From 31dced29a6a0b1bf88b915b46d06b9173facbb59 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 21:56:08 +0100
Subject: [PATCH 07/11] moved interface to abstractor

---
 abstractor/interface.go | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/abstractor/interface.go b/abstractor/interface.go
index 723f1d9..b890555 100644
--- a/abstractor/interface.go
+++ b/abstractor/interface.go
@@ -9,7 +9,8 @@ import (
 	"github.com/consensys/gnark/frontend"
 )
 
-func RawCall(api frontend.API, gadget GadgetDefinition) interface{} {
+// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
+func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
 	if abs, ok := api.(API); ok {
 		return abs.Call(gadget).(frontend.Variable)
 	} else {
@@ -19,27 +20,22 @@ func RawCall(api frontend.API, gadget GadgetDefinition) interface{} {
 
 // CallVoid is used to call a Gadget which doesn't return anything
 func CallVoid(api frontend.API, gadget GadgetDefinition) {
-	RawCall(api, gadget)
-}
-
-// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
-func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
-	return RawCall(api, gadget).(frontend.Variable)
+	Call(api, gadget)
 }
 
 // Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
 func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
-	return RawCall(api, gadget).([]frontend.Variable)
+	return Call(api, gadget).([]frontend.Variable)
 }
 
 // Call2 is used to call a Gadget which returns a [][]frontend.Variable
 // (i.e. `Vector (Vector F a) b` in Lean)
 func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
-	return RawCall(api, gadget).([][]frontend.Variable)
+	return Call(api, gadget).([][]frontend.Variable)
 }
 
 // Call3 is used to call a Gadget which returns a [][][]frontend.Variable
 // (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
 func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
-	return RawCall(api, gadget).([][][]frontend.Variable)
+	return Call(api, gadget).([][][]frontend.Variable)
 }
\ No newline at end of file

From 63e9ffa07c10d8171fbf8672cf56b7dccbc01c5f Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 21:57:06 +0100
Subject: [PATCH 08/11] Gofmt

---
 abstractor/abstractor.go |  2 +-
 abstractor/interface.go  | 82 ++++++++++++++++++++--------------------
 2 files changed, 42 insertions(+), 42 deletions(-)

diff --git a/abstractor/abstractor.go b/abstractor/abstractor.go
index 8fc2439..1bd389d 100644
--- a/abstractor/abstractor.go
+++ b/abstractor/abstractor.go
@@ -13,4 +13,4 @@ type GadgetDefinition interface {
 type API interface {
 	frontend.API
 	Call(gadget GadgetDefinition) interface{}
-}
\ No newline at end of file
+}
diff --git a/abstractor/interface.go b/abstractor/interface.go
index b890555..963ffe3 100644
--- a/abstractor/interface.go
+++ b/abstractor/interface.go
@@ -1,41 +1,41 @@
-// This file contains the public API for using the extractor.
-// The Call functions are used to call gadgets and get their returnd object.
-// These methods are prepared for doing automated casting from interface{}.
-// Alternatively it's possible to do manual casting by calling
-// abstractor.API.Call() and casting the result to the needed type.
-package abstractor
-
-import (
-	"github.com/consensys/gnark/frontend"
-)
-
-// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
-func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
-	if abs, ok := api.(API); ok {
-		return abs.Call(gadget).(frontend.Variable)
-	} else {
-		return gadget.DefineGadget(api).(frontend.Variable)
-	}
-}
-
-// CallVoid is used to call a Gadget which doesn't return anything
-func CallVoid(api frontend.API, gadget GadgetDefinition) {
-	Call(api, gadget)
-}
-
-// Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
-func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
-	return Call(api, gadget).([]frontend.Variable)
-}
-
-// Call2 is used to call a Gadget which returns a [][]frontend.Variable
-// (i.e. `Vector (Vector F a) b` in Lean)
-func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
-	return Call(api, gadget).([][]frontend.Variable)
-}
-
-// Call3 is used to call a Gadget which returns a [][][]frontend.Variable
-// (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
-func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
-	return Call(api, gadget).([][][]frontend.Variable)
-}
\ No newline at end of file
+// This file contains the public API for using the extractor.
+// The Call functions are used to call gadgets and get their returnd object.
+// These methods are prepared for doing automated casting from interface{}.
+// Alternatively it's possible to do manual casting by calling
+// abstractor.API.Call() and casting the result to the needed type.
+package abstractor
+
+import (
+	"github.com/consensys/gnark/frontend"
+)
+
+// Call is used to call a Gadget which returns frontend.Variable (i.e. a single element `F` in Lean)
+func Call(api frontend.API, gadget GadgetDefinition) frontend.Variable {
+	if abs, ok := api.(API); ok {
+		return abs.Call(gadget).(frontend.Variable)
+	} else {
+		return gadget.DefineGadget(api).(frontend.Variable)
+	}
+}
+
+// CallVoid is used to call a Gadget which doesn't return anything
+func CallVoid(api frontend.API, gadget GadgetDefinition) {
+	Call(api, gadget)
+}
+
+// Call1 is used to call a Gadget which returns []frontend.Variable (i.e. `Vector F d` in Lean)
+func Call1(api frontend.API, gadget GadgetDefinition) []frontend.Variable {
+	return Call(api, gadget).([]frontend.Variable)
+}
+
+// Call2 is used to call a Gadget which returns a [][]frontend.Variable
+// (i.e. `Vector (Vector F a) b` in Lean)
+func Call2(api frontend.API, gadget GadgetDefinition) [][]frontend.Variable {
+	return Call(api, gadget).([][]frontend.Variable)
+}
+
+// Call3 is used to call a Gadget which returns a [][][]frontend.Variable
+// (i.e. `Vector (Vector (Vector F a) b) c` in Lean)
+func Call3(api frontend.API, gadget GadgetDefinition) [][][]frontend.Variable {
+	return Call(api, gadget).([][][]frontend.Variable)
+}

From 024517f250ece775b89061bc60778b1a7de2a379 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 21:59:39 +0100
Subject: [PATCH 09/11] Fixed comments

---
 abstractor/interface.go | 2 +-
 extractor/interface.go  | 6 +-----
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/abstractor/interface.go b/abstractor/interface.go
index 963ffe3..7fefa3e 100644
--- a/abstractor/interface.go
+++ b/abstractor/interface.go
@@ -2,7 +2,7 @@
 // The Call functions are used to call gadgets and get their returnd object.
 // These methods are prepared for doing automated casting from interface{}.
 // Alternatively it's possible to do manual casting by calling
-// abstractor.API.Call() and casting the result to the needed type.
+// abstractor.Call() and casting the result to the needed type.
 package abstractor
 
 import (
diff --git a/extractor/interface.go b/extractor/interface.go
index 6836e31..b12333a 100644
--- a/extractor/interface.go
+++ b/extractor/interface.go
@@ -1,8 +1,4 @@
-// This file contains the public API for using the extractor.
-// The Call functions are used to call gadgets and get their returnd object.
-// These methods are prepared for doing automated casting from interface{}.
-// Alternatively it's possible to do manual casting by calling
-// abstractor.API.Call() and casting the result to the needed type.
+// This file contains the public API for running the extractor.
 package extractor
 
 import (

From 2951bb790e98cc849026709f349dc2e5735a2476 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 22:09:25 +0100
Subject: [PATCH 10/11] Removed frontend.API extension to abstractor.API
 interface

---
 abstractor/abstractor.go | 1 -
 1 file changed, 1 deletion(-)

diff --git a/abstractor/abstractor.go b/abstractor/abstractor.go
index 1bd389d..46d7395 100644
--- a/abstractor/abstractor.go
+++ b/abstractor/abstractor.go
@@ -11,6 +11,5 @@ type GadgetDefinition interface {
 }
 
 type API interface {
-	frontend.API
 	Call(gadget GadgetDefinition) interface{}
 }

From de244c93dbf50a19fd919e82b0285994ea2621b3 Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Mon, 25 Sep 2023 22:13:22 +0100
Subject: [PATCH 11/11] Fix readme

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 5dbc80e..84f9ae9 100644
--- a/README.md
+++ b/README.md
@@ -34,7 +34,7 @@ type MyCircuit struct {
     Out  frontend.Variable
 }
 
-func (circuit *MyCircuit) AbsDefine(api abstractor.API) error {
+func (circuit *MyCircuit) Define(api abstractor.API) error {
     sum := api.Add(circuit.In_1, circuit.In_2)
     api.AssertIsEqual(sum, circuit.Out)
     return nil