From 30c890ed93f17f0cf8c294eb4c1a72f472dbcc94 Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Sun, 27 Jul 2025 19:11:11 +0200 Subject: [PATCH] Removed PrintError API and replaced its calls with Fatal or Anomaly --- src/AST/parameterizedtype.go | 9 ++++++--- src/AST/term.go | 2 +- src/Core/subst_and_form.go | 2 +- src/Core/substitutions_search.go | 2 +- src/Glob/errors.go | 4 ++-- src/Glob/log.go | 2 +- src/Mods/assisted/assistant.go | 2 +- src/Mods/dmt/rewrite.go | 2 +- src/Mods/equality/bse/constraints_type.go | 4 ++-- src/Mods/equality/bse/equality_problem.go | 2 +- src/Mods/equality/bse/equality_rules_reasoning.go | 4 ++-- src/Mods/equality/bse/equality_types.go | 10 +++++----- src/Mods/equality/bse/lpo.go | 10 +++++----- src/Mods/gs3/dependency.go | 2 +- src/Mods/lambdapi/output.go | 2 +- src/Mods/lambdapi/proof.go | 2 +- src/Mods/rocq/output.go | 2 +- src/Mods/tptp/output.go | 2 +- src/Search/child_management.go | 2 +- src/Search/destructive.go | 10 +++++----- src/Search/incremental/rules.go | 4 ++-- src/Search/incremental/search.go | 4 ++-- src/Search/nonDestructiveSearch.go | 14 +++++++------- src/Search/rules.go | 2 +- src/main.go | 2 +- 25 files changed, 53 insertions(+), 50 deletions(-) diff --git a/src/AST/parameterizedtype.go b/src/AST/parameterizedtype.go index 5b2d4a42..c905c1a1 100644 --- a/src/AST/parameterizedtype.go +++ b/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() diff --git a/src/AST/term.go b/src/AST/term.go index 4ebc116a..87d0a729 100644 --- a/src/AST/term.go +++ b/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: diff --git a/src/Core/subst_and_form.go b/src/Core/subst_and_form.go index 92629c59..3c44fa22 100644 --- a/src/Core/subst_and_form.go +++ b/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() } diff --git a/src/Core/substitutions_search.go b/src/Core/substitutions_search.go index 51403ed8..6177239c 100644 --- a/src/Core/substitutions_search.go +++ b/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 diff --git a/src/Glob/errors.go b/src/Glob/errors.go index 2bcc8623..9151383b 100644 --- a/src/Glob/errors.go +++ b/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.") } diff --git a/src/Glob/log.go b/src/Glob/log.go index 91543837..af7d9bcc 100644 --- a/src/Glob/log.go +++ b/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) } diff --git a/src/Mods/assisted/assistant.go b/src/Mods/assisted/assistant.go index 1064567e..46cc47cc 100644 --- a/src/Mods/assisted/assistant.go +++ b/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") } } diff --git a/src/Mods/dmt/rewrite.go b/src/Mods/dmt/rewrite.go index 2fdbbac6..b04c4495 100644 --- a/src/Mods/dmt/rewrite.go +++ b/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(), diff --git a/src/Mods/equality/bse/constraints_type.go b/src/Mods/equality/bse/constraints_type.go index f63692bc..453456f7 100644 --- a/src/Mods/equality/bse/constraints_type.go +++ b/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 } } diff --git a/src/Mods/equality/bse/equality_problem.go b/src/Mods/equality/bse/equality_problem.go index b2e4ad91..dc3156c1 100644 --- a/src/Mods/equality/bse/equality_problem.go +++ b/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 { diff --git a/src/Mods/equality/bse/equality_rules_reasoning.go b/src/Mods/equality/bse/equality_rules_reasoning.go index 1346031d..48383c3f 100644 --- a/src/Mods/equality/bse/equality_rules_reasoning.go +++ b/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) diff --git a/src/Mods/equality/bse/equality_types.go b/src/Mods/equality/bse/equality_types.go index ac16dd5c..9a2147ee 100644 --- a/src/Mods/equality/bse/equality_types.go +++ b/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) } diff --git a/src/Mods/equality/bse/lpo.go b/src/Mods/equality/bse/lpo.go index 314c5916..864119fc 100644 --- a/src/Mods/equality/bse/lpo.go +++ b/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) } diff --git a/src/Mods/gs3/dependency.go b/src/Mods/gs3/dependency.go index 7823a9ec..0251237e 100644 --- a/src/Mods/gs3/dependency.go +++ b/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 diff --git a/src/Mods/lambdapi/output.go b/src/Mods/lambdapi/output.go index cd5de4d0..0e171326 100644 --- a/src/Mods/lambdapi/output.go +++ b/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 "" } diff --git a/src/Mods/lambdapi/proof.go b/src/Mods/lambdapi/proof.go index 852a7697..ca03e41e 100644 --- a/src/Mods/lambdapi/proof.go +++ b/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 diff --git a/src/Mods/rocq/output.go b/src/Mods/rocq/output.go index 1efaaff6..fec5e8ef 100644 --- a/src/Mods/rocq/output.go +++ b/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 "" } diff --git a/src/Mods/tptp/output.go b/src/Mods/tptp/output.go index ee48f084..66e4fa65 100644 --- a/src/Mods/tptp/output.go +++ b/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 "" } diff --git a/src/Search/child_management.go b/src/Search/child_management.go index a02c580c..6c1121c2 100644 --- a/src/Search/child_management.go +++ b/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 } diff --git a/src/Search/destructive.go b/src/Search/destructive.go index ba555609..b13a291d 100644 --- a/src/Search/destructive.go +++ b/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)) diff --git a/src/Search/incremental/rules.go b/src/Search/incremental/rules.go index 4fffd124..52336789 100644 --- a/src/Search/incremental/rules.go +++ b/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 } } diff --git a/src/Search/incremental/search.go b/src/Search/incremental/search.go index a052eec6..9f37b97c 100644 --- a/src/Search/incremental/search.go +++ b/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{} } diff --git a/src/Search/nonDestructiveSearch.go b/src/Search/nonDestructiveSearch.go index 46c70f2b..2b5db864 100644 --- a/src/Search/nonDestructiveSearch.go +++ b/src/Search/nonDestructiveSearch.go @@ -50,12 +50,12 @@ 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) { @@ -63,7 +63,7 @@ func (nds *nonDestructiveSearch) doEndManageBeta(fatherId uint64, state State, c } 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) diff --git a/src/Search/rules.go b/src/Search/rules.go index a2f653dc..3f6e3723 100644 --- a/src/Search/rules.go +++ b/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) } diff --git a/src/main.go b/src/main.go index 07107474..c6bbe285 100644 --- a/src/main.go +++ b/src/main.go @@ -219,7 +219,7 @@ func StatementListToFormula(statements []Core.Statement, old_bound int, problemD debug(Lib.MkLazy(func() string { return fmt.Sprintf("File to parse : %s\n", realname) })) if err != nil { - Glob.PrintError(main_label, err.Error()) + Glob.Fatal(main_label, err.Error()) return nil, -1, false }