Remove PrintError API and always call to Fatal or Anomaly instead

src/AST/parameterizedtype.go

@@ -131,14 +131,17 @@ func MkParameterizedType(name string, types []TypeApp) ParameterizedType {
 		}
 		if k != len(types) {
 			pMap.lock.Unlock()
-			Glob.PrintInfo("PRMTR_TYPE", fmt.Sprintf("Name of the type: %s, length of the args: %d", name, len(types)))
-			Glob.PrintError("PRMTR_TYPE", "Parameterized type can not be instanciated with this number of arguments.")
+			debug(
+				Lib.MkLazy(func() string {
+					return fmt.Sprintf("Name of the type: %s, length of the args: %d", name, len(types))
+				}))
+			Glob.Fatal("PRMTR_TYPE", "Parameterized type can not be instanciated with this number of arguments.")
 			return ParameterizedType{}
 		}
 		types = nextTypes
 	} else {
 		pMap.lock.Unlock()
-		Glob.PrintError("PRMTR_TYPE", "Parameterized type not found.")
+		Glob.Fatal("PRMTR_TYPE", "Parameterized type not found.")
 		return ParameterizedType{}
 	}
 	pMap.lock.Unlock()

src/AST/term.go

@@ -118,7 +118,7 @@ func TypeAppToTerm(typeApp TypeApp) Term {
 		if nt.IsMeta() {
 			term = typeVarToMeta(nt)
 		} else {
-			Glob.PrintError("TERM", "A TypeVar should be only converted to terms if it has been instantiated.")
+			Glob.Fatal("TERM", "A TypeVar should be only converted to terms if it has been instantiated.")
 			term = nil
 		}
 	case TypeHint:

src/Core/subst_and_form.go

@@ -198,7 +198,7 @@ func MergeSubstAndForm(s1, s2 SubstAndForm) (error, SubstAndForm) {
 	new_subst, _ := Unif.MergeSubstitutions(s1.GetSubst().Copy(), s2.GetSubst().Copy())
 
 	if new_subst.Equals(Unif.Failure()) {
-		Glob.PrintError("MSAF", fmt.Sprintf("Error : MergeSubstitutions returns failure between : %v and %v \n", s1.ToString(), s2.ToString()))
+		Glob.Fatal("MSAF", fmt.Sprintf("Error : MergeSubstitutions returns failure between : %v and %v \n", s1.ToString(), s2.ToString()))
 		return errors.New("Couldn't merge two substitutions"), MakeEmptySubstAndForm()
 	}
 

src/Core/substitutions_search.go

@@ -137,7 +137,7 @@ func RemoveElementWithoutMM(subs Unif.Substitutions, mm Lib.Set[AST.Meta]) Unif.
 	)
 
 	if ms.Equals(Unif.Failure()) {
-		Glob.PrintError("REWM", "MergeSubstitutions returns failure")
+		Glob.Fatal("REWM", "MergeSubstitutions returns failure")
 	}
 
 	return ms

src/Glob/errors.go

@@ -45,11 +45,11 @@ func exitWithError(panicMsg string) {
 
 func Anomaly(label, msg string) {
 	url := "https://github.com/GoelandProver/Goeland/issues"
-	PrintError("Anomaly", fmt.Sprintf("In %s: %s.\nPlease report at %s", label, msg, url))
+	printError("Anomaly", fmt.Sprintf("In %s: %s.\nPlease report at %s", label, msg, url))
 	exitWithError("Anomaly encountered.")
 }
 
 func Fatal(label, msg string) {
-	PrintError(label, msg)
+	printError(label, msg)
 	exitWithError("Fatal error encountered.")
 }

src/Glob/log.go

@@ -169,7 +169,7 @@ func PrintInfo(function, message string) {
 //
 // Use when you want to warn that something is not happening as it should and it is important and must be corrected.
 // The prefix for error messages is '[error]' in red.
-func PrintError(function, message string) {
+func printError(function, message string) {
 	printToLogger(logError, function, message)
 }
 

src/Mods/assisted/assistant.go

@@ -99,7 +99,7 @@ func InitAssisted() {
 	if typed, ok := Search.UsedSearch.(Search.BasicSearchAlgorithm); ok {
 		searchAlgo = typed
 	} else {
-		Glob.PrintError("ASS", "Search algorithm not supported by the Assisted plugin")
+		Glob.Fatal("ASS", "Search algorithm not supported by the Assisted plugin")
 	}
 }
 

src/Mods/dmt/rewrite.go

@@ -89,7 +89,7 @@ func addRewrittenFormulas(rewritten []Core.IntSubstAndForm, unif Unif.MatchingSu
 	useful_subst := Core.RemoveElementWithoutMM(unif.GetSubst(), atomic.GetMetas())
 	meta_search := atomic.GetMetas()
 	if !checkMetaAreFromSearch(meta_search, useful_subst) {
-		Glob.PrintError("DMT", fmt.Sprintf("There is at least one meta in final subst which is not from search : %v - %v - %v", useful_subst.ToString(), atomic.ToString(), unif.GetForm().ToString()))
+		Glob.Fatal("DMT", fmt.Sprintf("There is at least one meta in final subst which is not from search : %v - %v - %v", useful_subst.ToString(), atomic.ToString(), unif.GetForm().ToString()))
 	}
 	filteredUnif := Unif.MakeMatchingSubstitutions(
 		unif.GetForm(),

src/Mods/equality/bse/constraints_type.go

@@ -79,7 +79,7 @@ func (c Constraint) toString() string {
 	case EQ:
 		return c.getTP().GetT1().ToString() + " ≃ " + c.getTP().GetT2().ToString()
 	default:
-		Glob.PrintError("CT", "Constraint type unknown")
+		Glob.Anomaly("CT", "Constraint type unknown")
 		return "Constraint type unknown"
 	}
 }
@@ -114,7 +114,7 @@ func (c *Constraint) checkLPO() (bool, bool) {
 		case EQ:
 			return cs.order == 0, true
 		default:
-			Glob.PrintError("CT", "Constraint type not valid")
+			Glob.Anomaly("CT", "Constraint type not valid")
 			return false, true
 		}
 	}

src/Mods/equality/bse/equality_problem.go

@@ -95,7 +95,7 @@ func (ep EqualityProblem) applySubstitution(s Unif.Substitutions) EqualityProble
 	new_equalities := ep.GetE()
 
 	if !ep.getC().isEmpty() {
-		Glob.PrintError("EQ-AS", fmt.Sprintf("Constraint not null in applySubstitution : %v", ep.getC().toString()))
+		Glob.Fatal("EQ-AS", fmt.Sprintf("Constraint not null in applySubstitution : %v", ep.getC().toString()))
 	}
 
 	for _, subst := range s {

src/Mods/equality/bse/equality_rules_reasoning.go

@@ -191,10 +191,10 @@ func manageEqualityReasoningProblem(ep EqualityProblem, sl []Unif.Substitutions)
 				for _, subst_element := range s_subst {
 					merged_subst, same_key := Unif.MergeSubstitutions(s.Copy(), subst_element.Copy())
 					if same_key {
-						Glob.PrintError("ERPWAS", "Error in EqualityReasoningList : same key appears in merge")
+						Glob.Fatal("ERPWAS", "Error in EqualityReasoningList : same key appears in merge")
 					}
 					if merged_subst.Equals(Unif.Failure()) {
-						Glob.PrintError("ERPWAS", "Error in EqualityReasoningList : merge returns failure")
+						Glob.Fatal("ERPWAS", "Error in EqualityReasoningList : merge returns failure")
 					} else {
 						found = true
 						res_substs = append(res_substs, merged_subst)

src/Mods/equality/bse/equality_types.go

@@ -140,11 +140,11 @@ func retrieveEqualities(dt Unif.DataStructure) Equalities {
 		ms_ordered := orderSubstForRetrieve(ms.GetSubst(), MetaEQ1, MetaEQ2)
 		eq1_term, ok_t1 := ms_ordered.Get(MetaEQ1)
 		if ok_t1 == -1 {
-			Glob.PrintError("RI", "Meta_eq_1 not found in map")
+			Glob.Anomaly("RI", "Meta_eq_1 not found in map")
 		}
 		eq2_term, ok_t2 := ms_ordered.Get(MetaEQ2)
 		if ok_t2 == -1 {
-			Glob.PrintError("RI", "Meta_eq_2 not found in map")
+			Glob.Anomaly("RI", "Meta_eq_2 not found in map")
 		}
 		res = append(res, eqStruct.MakeTermPair(eq1_term, eq2_term))
 	}
@@ -175,11 +175,11 @@ func retrieveInequalities(dt Unif.DataStructure) Inequalities {
 		ms_ordered := orderSubstForRetrieve(ms.GetSubst(), MetaNEQ1, MetaNEQ2)
 		neq1_term, ok_t1 := ms_ordered.Get(MetaNEQ1)
 		if ok_t1 == -1 {
-			Glob.PrintError("RI", "Meta_eq_1 not found in map")
+			Glob.Anomaly("RI", "Meta_eq_1 not found in map")
 		}
 		neq2_term, ok_t2 := ms_ordered.Get(MetaNEQ2)
 		if ok_t2 == -1 {
-			Glob.PrintError("RI", "Meta_eq_1 not found in map")
+			Glob.Anomaly("RI", "Meta_eq_1 not found in map")
 		}
 		res = append(res, eqStruct.MakeTermPair(neq1_term, neq2_term))
 	}
@@ -193,7 +193,7 @@ func orderSubstForRetrieve(s Unif.Substitutions, M1, M2 AST.Meta) Unif.Substitut
 		k, v := subst.Get()
 		if !k.Equals(M1) && !k.Equals(M2) {
 			if !v.IsMeta() {
-				Glob.PrintError("OSFR", "Meta EQ/NEQ not found")
+				Glob.Fatal("OSFR", "Meta EQ/NEQ not found")
 			} else {
 				new_subst.Set(v.ToMeta(), k)
 			}

src/Mods/equality/bse/lpo.go

@@ -88,7 +88,7 @@ func compareLPO(s, t AST.Term) compareStruct {
 			// function & meta : Occurences inside : f(x) < x, f(y) < x
 			return compareMetaFun(t_type, s_type, -1)
 		default:
-			Glob.PrintError("CPR", "Type of t unknown")
+			Glob.Anomaly("CPR", "Type of t unknown")
 		}
 	case AST.Meta:
 		debug(
@@ -108,10 +108,10 @@ func compareLPO(s, t AST.Term) compareStruct {
 			// Meta and meta
 			return compareMetaMeta(s_type, t_type)
 		default:
-			Glob.PrintError("CPR", "Type of t unknown")
+			Glob.Anomaly("CPR", "Type of t unknown")
 		}
 	default:
-		Glob.PrintError("CPR", "Type of s unknown")
+		Glob.Anomaly("CPR", "Type of s unknown")
 	}
 	return makeCompareStruct(0, false, s, t)
 }
@@ -164,7 +164,7 @@ func compareMetaFunInside(m AST.Meta, f AST.Fun, return_code int) (bool, compare
 			res = cs.order
 			is_comparable = cs.is_comparable
 		default:
-			Glob.PrintError("CMFI", "Unexpected return_code in compare")
+			Glob.Anomaly("CMFI", "Unexpected return_code in compare")
 		}
 
 		if is_comparable {
@@ -240,7 +240,7 @@ func caseFEqualsG(s, t AST.Fun) (bool, compareStruct) {
 		Lib.MkLazy(func() string { return "Case F = G" }),
 	)
 	if s.GetArgs().Len() != t.GetArgs().Len() {
-		Glob.PrintError("F=G", fmt.Sprintf("Error : %v and %v don't have the same number of arguments", s.GetID().ToString(), t.GetID().ToString()))
+		Glob.Fatal("F=G", fmt.Sprintf("Error : %v and %v don't have the same number of arguments", s.GetID().ToString(), t.GetID().ToString()))
 		return true, makeCompareStruct(0, false, nil, nil)
 	}
 

src/Mods/gs3/dependency.go

@@ -177,7 +177,7 @@ func getTermAt(form AST.Form, occsArr occurrences) AST.Term {
 		t := getTermAux(form, occ)
 		if term != nil {
 			if !term.Equals(t) {
-				Glob.PrintError("GTA", "The same variable is instanciated as two different terms.")
+				Glob.Anomaly("GTA", "The same variable is instanciated as two different terms.")
 			}
 		} else {
 			term = t

src/Mods/lambdapi/output.go

@@ -75,7 +75,7 @@ var LambdapiOutputProofStruct = &Search.OutputProofStruct{ProofOutput: MakeLambd
 
 func MakeLambdapiOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string {
 	if len(prf) == 0 {
-		Glob.PrintError("LambdaPi", "Nothing to output")
+		Glob.Fatal("LambdaPi", "Nothing to output")
 		return ""
 	}
 

src/Mods/lambdapi/proof.go

@@ -99,7 +99,7 @@ func makeProofStep(proof *gs3.GS3Sequent) string {
 
 	// Weakening rule
 	case gs3.W:
-		Glob.PrintError("LP", "Trying to do a weakening rule but it's not implemented yet")
+		Glob.Fatal("LP", "Trying to do a weakening rule but it's not implemented yet")
 	}
 
 	return "//" + toCorrectString(proof.GetTargetForm()) + "\n" + resultingString

src/Mods/rocq/output.go

@@ -61,7 +61,7 @@ var RocqOutputProofStruct = &Search.OutputProofStruct{ProofOutput: MakeRocqOutpu
 
 func MakeRocqOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string {
 	if len(prf) == 0 {
-		Glob.PrintError("Rocq", "Nothing to output")
+		Glob.Fatal("Rocq", "Nothing to output")
 		return ""
 	}
 

src/Mods/tptp/output.go

@@ -57,7 +57,7 @@ var TptpOutputProofStruct = &Search.OutputProofStruct{ProofOutput: MakeTptpOutpu
 
 func MakeTptpOutput(prf []Search.ProofStruct, meta Lib.List[AST.Meta]) string {
 	if len(prf) == 0 {
-		Glob.PrintError("TPTP", "Nothing to output")
+		Glob.Fatal("TPTP", "Nothing to output")
 		return ""
 	}
 

src/Search/child_management.go

@@ -190,7 +190,7 @@ func (ds *destructiveSearch) passSubstToParent(args wcdArgs, proofChildren [][]P
 		err, merged := Core.MergeSubstAndForm(subst, args.st.GetAppliedSubst())
 
 		if err != nil {
-			Glob.PrintError("WC", "Error when merging the children substitution's with the applied one.")
+			Glob.Fatal("WC", "Error when merging the children substitution's with the applied one.")
 			return err
 		}
 

src/Search/destructive.go

@@ -465,7 +465,7 @@ func (ds *destructiveSearch) waitChildren(args wcdArgs) {
 		}
 
 		if err != nil {
-			Glob.PrintError("WC", "Error when waiting for children. It should be an error when merging substitutions. What to do?")
+			Glob.Fatal("WC", "Error when waiting for children: "+err.Error())
 		}
 	}
 }
@@ -873,7 +873,7 @@ func (ds *destructiveSearch) selectChildren(father Communication, children *[]Co
 						err, new_subst := Core.MergeSubstAndForm(s.Copy(), new_current_subst.Copy())
 
 						if err != nil {
-							Glob.PrintError("SLC", "Error when merging substitutions. What to do?")
+							Glob.Fatal("SLC", "Error when merging substitutions.")
 						}
 
 						new_result_subst = append(new_result_subst, new_subst)
@@ -943,7 +943,7 @@ func (ds *destructiveSearch) manageRewriteRules(fatherId uint64, state State, c
 					return
 				}
 			} else {
-				Glob.PrintError("DMT", err.Error())
+				Glob.Fatal("DMT", err.Error())
 			}
 		}
 	}
@@ -1112,7 +1112,7 @@ func (ds *destructiveSearch) ManageClosureRule(father_id uint64, st *State, c Co
 		for _, subst_for_father := range substs_with_mm {
 			// Check if subst_for_father is failure
 			if subst_for_father.Equals(Unif.Failure()) {
-				Glob.PrintError("MCR", fmt.Sprintf("Error : SubstForFather is failure between : %v and %v \n", subst_for_father.ToString(), st.GetAppliedSubst().ToString()))
+				Glob.Fatal("MCR", fmt.Sprintf("Error : SubstForFather is failure between : %v and %v \n", subst_for_father.ToString(), st.GetAppliedSubst().ToString()))
 			}
 			debug(
 				Lib.MkLazy(func() string { return fmt.Sprintf("Formula = : %v", f.ToString()) }),
@@ -1133,7 +1133,7 @@ func (ds *destructiveSearch) ManageClosureRule(father_id uint64, st *State, c Co
 			err, subst_and_form_for_father := Core.MergeSubstAndForm(subst_and_form_for_father.Copy(), st.GetAppliedSubst())
 
 			if err != nil {
-				Glob.PrintError("MCR", "Contradiction found between applied subst and child subst. What to do?")
+				Glob.Fatal("MCR", "Contradiction found between applied subst and child subst.")
 			} else {
 
 				st.SetSubstsFound(Core.AppendIfNotContainsSubstAndForm(st.GetSubstsFound(), subst_and_form_for_father))

src/Search/incremental/rules.go

@@ -138,11 +138,11 @@ func makeCorrectRule(formula AST.Form, terms Lib.List[AST.Term]) Rule {
 			any.FullString = []string{"GAMMA", "NOT", "EXISTS"}
 			return &GammaNotExists{AnyRule: any}
 		default:
-			Glob.PrintError("RULES", "Could not find the type of the formula")
+			Glob.Anomaly("RULES", "Could not find the type of the formula")
 			return nil
 		}
 	default:
-		Glob.PrintError("RULES", "Could not find the type of the formula")
+		Glob.Anomaly("RULES", "Could not find the type of the formula")
 		return nil
 	}
 }

src/Search/incremental/search.go

@@ -38,11 +38,11 @@ func (is *incrementalSearch) handleSearchResults() bool {
 }
 
 func (is *incrementalSearch) SetApplyRules(func(uint64, Search.State, Search.Communication, Core.FormAndTermsList, int, int, []int)) {
-	Glob.PrintError("NDS", "Incremental search not compatible with the assisted plugin for now.")
+	Glob.Fatal("NDS", "Incremental search not compatible with the assisted plugin for now.")
 }
 
 // ManageClosureRule implements Search.SearchAlgorithm.
 func (is *incrementalSearch) ManageClosureRule(uint64, *Search.State, Search.Communication, []Unif.Substitutions, Core.FormAndTerms, int, int) (bool, []Core.SubstAndForm) {
-	Glob.PrintError("NDS", "Incremental search not compatible with the equality plugin for now.")
+	Glob.Fatal("NDS", "Incremental search not compatible with the equality plugin for now.")
 	return false, []Core.SubstAndForm{}
 }

src/Search/nonDestructiveSearch.go

@@ -50,20 +50,20 @@ type nonDestructiveSearch struct {
 func NewNonDestructiveSearch() BasicSearchAlgorithm {
 	nds := &nonDestructiveSearch{}
 	_ = nds
-	Glob.PrintError("NDS", "Non-destructive search not in working order for now.")
+	Glob.Fatal("NDS", "Non-destructive search not in working order for now.")
 	return nil
 }
 
 func (nds *nonDestructiveSearch) setApplyRules(function func(uint64, State, Communication, Core.FormAndTermsList, int, int, []int)) {
-	Glob.PrintError("NDS", "Non-destructive search not compatible with the assisted plugin for now.")
+	Glob.Fatal("NDS", "Non-destructive search not compatible with the assisted plugin for now.")
 }
 
 func (nds *nonDestructiveSearch) doEndManageBeta(fatherId uint64, state State, c Communication, channels []Communication, currentNodeId int, originalNodeId int, childIds []int, metaToReintroduce []int) {
 	debug(Lib.MkLazy(func() string { return "Die" }))
 }
 
 func (nds *nonDestructiveSearch) manageRewriteRules(fatherId uint64, state State, c Communication, newAtomics Core.FormAndTermsList, currentNodeId int, originalNodeId int, metaToReintroduce []int) {
-	Glob.PrintError("NDS", "Non-destructive search not compatible with the DMT plugin for now.")
+	Glob.Fatal("NDS", "Non-destructive search not compatible with the DMT plugin for now.")
 }
 
 /* Choose substitution - whitout meta in lastAppliedSubst */
@@ -216,14 +216,14 @@ func (nds *nonDestructiveSearch) instantiate(fatherId uint64, state *State, c Co
 		Glob.PrintInfo("PS", "Same key in S2 and S1")
 	}
 	if new_subst.Equals(Unif.Failure()) {
-		Glob.PrintError("PS", "MergeSubstitutions return failure")
+		Glob.Fatal("PS", "MergeSubstitutions return failure")
 	}
 	new_subst, same_key = Unif.MergeSubstitutions(new_subst, s.GetSubst())
 	if same_key {
 		Glob.PrintInfo("PS", "Same key in S2 and S1")
 	}
 	if new_subst.Equals(Unif.Failure()) {
-		Glob.PrintError("PS", "MergeSubstitutions return failure")
+		Glob.Fatal("PS", "MergeSubstitutions return failure")
 	}
 
 	// Then associate with the substitution (if possible)
@@ -260,10 +260,10 @@ func (nds *nonDestructiveSearch) instantiate(fatherId uint64, state *State, c Co
 
 	ms, same_key := Unif.MergeSubstitutions(state.GetAppliedSubst().GetSubst(), new_subst)
 	if same_key {
-		Glob.PrintError("PS", "Same key in S2 and S1")
+		Glob.Fatal("PS", "Same key in S2 and S1")
 	}
 	if ms.Equals(Unif.Failure()) {
-		Glob.PrintError("PS", "MergeSubstitutions return failure")
+		Glob.Fatal("PS", "MergeSubstitutions return failure")
 	}
 	state.SetAppliedSubst(Core.MakeSubstAndForm(ms, s.GetForm()))
 	state.SetLastAppliedSubst(s)

src/Search/rules.go

@@ -497,7 +497,7 @@ func ApplyGammaRules(fnt Core.FormAndTerms, index int, state *State) (Core.FormA
 		setStateRules(state, "GAMMA", "FORALL")
 
 	case AST.AllType:
-		Glob.PrintError("search", "Typed search not handled yet")
+		Glob.PrintInfo("search", "Typed search not handled yet")
 		os.Exit(3)
 	}