Improve formatting by using golines

.github/workflows/linter.yml

@@ -0,0 +1,36 @@
+name: Lint
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - master
+
+jobs:
+  Linting:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: cachix/install-nix-action@v31
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+      - uses: actions/setup-go@v3
+        with:
+          go-version: '>=1.22.0'
+      - run: go install golang.org/x/tools/cmd/goyacc@latest
+      - run: cd src && make
+      - uses: rrbutani/use-nix-shell-action@v1
+        with:
+          file: shell.nix
+          script: |
+            failure=0
+            for f in `find . -type f -name "src/*.go"`; do
+              if [[ ! -z `cmp $f <(golines -m 100 $f)` ]]; then
+                echo "$f is not properly formatted."
+                failure=1
+              fi
+            done
+
+            exit $failure

CONTRIBUTING.md

@@ -26,6 +26,29 @@ master*.
 If you are solving a bug referenced in the issue tracker, do not forget to link
 it in the PR.
 
+### Code formatting
+
+We expect the code to be formatted using the `golines` tool, with the linebreak configured
+at *100* characters. `golines` is furnished in the Nix environment, but can otherwise be
+installed by following the instructions of the [official
+repository](https://github.com/golangci/golines). You can enable `golines` to run on save
+in your IDE.
+
+#### Formatting on save in `emacs`
+
+```elisp
+(use-package go-mode
+  :init
+  (defun my/go-format ()
+    (interactive)
+	(when (eq major-mode 'go-mode)
+	  (shell-command
+	   (format "golines -m 100 -w %s" buffer-file-name))))
+
+  :hook ((after-save-hook . my/go-format)))
+```
+Moreover, if you don't have the `auto-revert-mode` enabled globally, you should probably hook it to `go-mode`.
+
 ### Error management
 
 When you add code or fix old code, try to find the possible error cases where an

shell.nix

@@ -5,6 +5,7 @@ pkgs.mkShell {
     go
     gopls
     gotools
+    golines
     python314
     rocq-core
     ocamlPackages.lambdapi

src/AST/formsDef.go

@@ -101,7 +101,8 @@ func MakerAll(vars []Var, forms Form) All {
 
 func (a All) Equals(other any) bool {
 	if typed, ok := other.(All); ok {
-		return AreEqualsVarList(a.GetVarList(), typed.GetVarList()) && a.GetForm().Equals(typed.GetForm())
+		return AreEqualsVarList(a.GetVarList(), typed.GetVarList()) &&
+			a.GetForm().Equals(typed.GetForm())
 	}
 
 	return false
@@ -157,7 +158,8 @@ func MakerEx(vars []Var, forms Form) Ex {
 
 func (e Ex) Equals(other any) bool {
 	if typed, ok := other.(Ex); ok {
-		return AreEqualsVarList(e.GetVarList(), typed.GetVarList()) && e.GetForm().Equals(typed.GetForm())
+		return AreEqualsVarList(e.GetVarList(), typed.GetVarList()) &&
+			e.GetForm().Equals(typed.GetForm())
 	}
 
 	return false
@@ -239,18 +241,31 @@ func (a AllType) GetType() TypeScheme   { return DefaultPropType(0) }
 /* Form interface */
 
 func (a AllType) ToMappedString(mapping MapString, displayTypes bool) string {
-	return mapping[QuantVarOpen] + Glob.ListToString(a.GetVarList(), ", ", "") + " : " + mapping[TypeVarType] + mapping[QuantVarClose] + mapping[QuantVarSep] + " (" + a.GetForm().ToString() + ")"
+	return mapping[QuantVarOpen] + Glob.ListToString(
+		a.GetVarList(),
+		", ",
+		"",
+	) + " : " + mapping[TypeVarType] + mapping[QuantVarClose] + mapping[QuantVarSep] + " (" + a.GetForm().
+		ToString() +
+		")"
 }
 
 func (a AllType) ToString() string {
 	return a.MappedString.ToString()
 }
 
 func (a AllType) ToMappedStringSurround(mapping MapString, displayTypes bool) string {
-	return "(" + mapping[AllTypeQuant] + " " + mapping[QuantVarOpen] + Glob.ListToString(a.GetVarList(), ", ", "") + " : " + mapping[TypeVarType] + mapping[QuantVarClose] + mapping[QuantVarSep] + " (%s))"
+	return "(" + mapping[AllTypeQuant] + " " + mapping[QuantVarOpen] + Glob.ListToString(
+		a.GetVarList(),
+		", ",
+		"",
+	) + " : " + mapping[TypeVarType] + mapping[QuantVarClose] + mapping[QuantVarSep] + " (%s))"
 }
 
-func (a AllType) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (a AllType) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return "", ""
 }
 
@@ -406,7 +421,10 @@ func (o Or) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return "(%s)"
 }
 
-func (o Or) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (o Or) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return " " + mapping[OrConn] + " ", ""
 }
 
@@ -474,8 +492,13 @@ func MakeAndSimpleBinary(i int, forms *FormList, metas Lib.Set[Meta]) And {
 	default:
 		return MakeAndSimple(
 			i,
-			NewFormList([]Form{forms.Get(0), MakerAnd(NewFormList(forms.GetElements(1, forms.Len())...), true)}...),
-			metas)
+			NewFormList(
+				[]Form{
+					forms.Get(0),
+					MakerAnd(NewFormList(forms.GetElements(1, forms.Len())...), true),
+				}...),
+			metas,
+		)
 	}
 }
 
@@ -549,7 +572,10 @@ func (a And) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return "(%s)"
 }
 
-func (a And) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (a And) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return " " + mapping[AndConn] + " ", ""
 }
 
@@ -626,7 +652,10 @@ func (e Equ) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return "(%s)"
 }
 
-func (e Equ) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (e Equ) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return " " + mapping[EquConn] + " ", ""
 }
 
@@ -671,7 +700,11 @@ func (e Equ) Equals(f any) bool {
 }
 
 func (e Equ) ReplaceTypeByMeta(varList []TypeVar, index int) Form {
-	return MakeEqu(e.GetIndex(), e.GetF1().ReplaceTypeByMeta(varList, index), e.GetF2().ReplaceTypeByMeta(varList, index))
+	return MakeEqu(
+		e.GetIndex(),
+		e.GetF1().ReplaceTypeByMeta(varList, index),
+		e.GetF2().ReplaceTypeByMeta(varList, index),
+	)
 }
 
 func (e Equ) ReplaceTermByTerm(old Term, new Term) (Form, bool) {
@@ -711,7 +744,11 @@ func (e Equ) GetChildFormulas() *FormList {
 }
 
 func (e Equ) ReplaceMetaByTerm(meta Meta, term Term) Form {
-	return MakeEqu(e.GetIndex(), e.f1.ReplaceMetaByTerm(meta, term), e.f2.ReplaceMetaByTerm(meta, term))
+	return MakeEqu(
+		e.GetIndex(),
+		e.f1.ReplaceMetaByTerm(meta, term),
+		e.f2.ReplaceMetaByTerm(meta, term),
+	)
 }
 
 // -----------------------------------------------------------------------------
@@ -749,7 +786,10 @@ func (i Imp) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return "(%s)"
 }
 
-func (i Imp) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (i Imp) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return " " + mapping[ImpConn] + " ", ""
 }
 
@@ -796,7 +836,11 @@ func (i Imp) Equals(other any) bool {
 }
 
 func (i Imp) ReplaceTypeByMeta(varList []TypeVar, index int) Form {
-	return MakeImp(i.GetIndex(), i.GetF1().ReplaceTypeByMeta(varList, index), i.GetF2().ReplaceTypeByMeta(varList, index))
+	return MakeImp(
+		i.GetIndex(),
+		i.GetF1().ReplaceTypeByMeta(varList, index),
+		i.GetF2().ReplaceTypeByMeta(varList, index),
+	)
 }
 
 func (i Imp) ReplaceTermByTerm(old Term, new Term) (Form, bool) {
@@ -837,7 +881,11 @@ func (i Imp) GetChildFormulas() *FormList {
 }
 
 func (i Imp) ReplaceMetaByTerm(meta Meta, term Term) Form {
-	return MakeImp(i.GetIndex(), i.f1.ReplaceMetaByTerm(meta, term), i.f2.ReplaceMetaByTerm(meta, term))
+	return MakeImp(
+		i.GetIndex(),
+		i.f1.ReplaceMetaByTerm(meta, term),
+		i.f2.ReplaceMetaByTerm(meta, term),
+	)
 }
 
 // -----------------------------------------------------------------------------
@@ -915,7 +963,10 @@ func (n Not) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return mapping[NotConn] + "(%s)"
 }
 
-func (n Not) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (n Not) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return "", ""
 }
 
@@ -1093,10 +1144,18 @@ func (p Pred) ToMappedStringSurround(mapping MapString, displayTypes bool) strin
 		return "(" + strings.Join(args, " "+mapping[PredTypeVarSep]+" ") + ")"
 	}
 
-	return p.GetID().ToMappedString(mapping, displayTypes) + "(" + strings.Join(args, " "+mapping[PredTypeVarSep]+" ") + ")"
+	return p.GetID().
+		ToMappedString(mapping, displayTypes) +
+		"(" + strings.Join(
+		args,
+		" "+mapping[PredTypeVarSep]+" ",
+	) + ")"
 }
 
-func (p Pred) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (p Pred) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	if p.GetID().GetName() == "=" {
 		return " = ", mapping[PredEmpty]
 	}
@@ -1274,7 +1333,10 @@ func (t Top) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return "%s"
 }
 
-func (t Top) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (t Top) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return "", mapping[TopType]
 }
 
@@ -1318,7 +1380,10 @@ func (b Bot) ToMappedStringSurround(mapping MapString, displayTypes bool) string
 	return "%s"
 }
 
-func (b Bot) ToMappedStringChild(mapping MapString, displayTypes bool) (separator, emptyValue string) {
+func (b Bot) ToMappedStringChild(
+	mapping MapString,
+	displayTypes bool,
+) (separator, emptyValue string) {
 	return "", mapping[BotType]
 }
 

src/AST/maker.go

@@ -157,7 +157,13 @@ func MakerMeta(s string, formula int, t ...TypeApp) Meta {
 
 /* Const maker (given a id, create a fun without args) */
 func MakerConst(id Id, t ...TypeApp) Fun {
-	return MakeFun(id, Lib.NewList[Term](), []TypeApp{}, getType(t).(TypeScheme), Lib.EmptySet[Meta]())
+	return MakeFun(
+		id,
+		Lib.NewList[Term](),
+		[]TypeApp{},
+		getType(t).(TypeScheme),
+		Lib.EmptySet[Meta](),
+	)
 }
 
 /* Fun maker, with given id and args */

src/AST/manage_apps_types.go

@@ -83,13 +83,19 @@ func SaveTypeScheme(name string, in TypeApp, out TypeApp) error {
 		if tScheme.Equals(tArrow) {
 			return nil
 		}
-		return fmt.Errorf("trying to save a known type scheme with different return types for the function %s", name)
+		return fmt.Errorf(
+			"trying to save a known type scheme with different return types for the function %s",
+			name,
+		)
 	}
 
 	// It's not in the map, it should be added
 	typeSchemesMap.lock.Lock()
 	if found {
-		typeSchemesMap.tsMap[name] = append(typeSchemesMap.tsMap[name], App{in: in, out: out, App: tArrow})
+		typeSchemesMap.tsMap[name] = append(
+			typeSchemesMap.tsMap[name],
+			App{in: in, out: out, App: tArrow},
+		)
 	} else {
 		typeSchemesMap.tsMap[name] = []App{{in: in, out: out, App: tArrow}}
 	}
@@ -102,7 +108,10 @@ func SavePolymorphScheme(name string, scheme TypeScheme) error {
 	tScheme, found := getPolymorphSchemeFromArgs(name, scheme)
 	if tScheme != nil {
 		if !GetOutType(tScheme).Equals(GetOutType(scheme)) {
-			return fmt.Errorf("trying to save a known type scheme with different return types for the function %s", name)
+			return fmt.Errorf(
+				"trying to save a known type scheme with different return types for the function %s",
+				name,
+			)
 		}
 		return nil
 	}
@@ -126,7 +135,10 @@ func SaveConstant(name string, out TypeApp) error {
 	if arr, found := typeSchemesMap.tsMap[name]; found {
 		var err error
 		if !arr[0].out.Equals(out) {
-			err = fmt.Errorf("trying to save a known type scheme with different return types for the function %s", name)
+			err = fmt.Errorf(
+				"trying to save a known type scheme with different return types for the function %s",
+				name,
+			)
 		}
 		typeSchemesMap.lock.Unlock()
 		return err
@@ -190,7 +202,8 @@ func GetPolymorphicType(name string, lenVars, lenTerms int) TypeScheme {
 	typeSchemesMap.lock.Lock()
 	if arr, found := typeSchemesMap.tsMap[name]; found {
 		for _, fun := range arr {
-			if fun.App.Size()-1 == lenTerms && (Glob.Is[QuantifiedType](fun.App) && len(fun.App.(QuantifiedType).vars) == lenVars) {
+			if fun.App.Size()-1 == lenTerms &&
+				(Glob.Is[QuantifiedType](fun.App) && len(fun.App.(QuantifiedType).vars) == lenVars) {
 				typeSchemesMap.lock.Unlock()
 				return fun.App
 			}