From d00902b9f5596d7cda2e45eff3782c64323c8f88 Mon Sep 17 00:00:00 2001 From: Johann Rosain Date: Mon, 23 Mar 2026 18:18:12 +0100 Subject: [PATCH] clean: remove TermForm and unify terms --- src/AST/tptp-native-types.go | 2 - src/AST/ty-syntax.go | 9 +- src/Core/FormListDS.go | 4 + src/Mods/equality/bse/equality_problem.go | 7 +- .../equality/bse/equality_rules_try_apply.go | 4 +- src/Unif/code-trees.go | 89 ++++++----- src/Unif/data_structure.go | 12 ++ src/Unif/machine.go | 4 +- src/Unif/matching.go | 130 +++++++++------ src/Unif/matching_substitutions.go | 65 +++++++- src/Unif/parsing.go | 150 +++++------------- src/Unif/sequence.go | 41 ++++- src/Unif/substitutions_tree.go | 104 ++++++------ 13 files changed, 350 insertions(+), 271 deletions(-) diff --git a/src/AST/tptp-native-types.go b/src/AST/tptp-native-types.go index 320cf3b7..3b4b821d 100644 --- a/src/AST/tptp-native-types.go +++ b/src/AST/tptp-native-types.go @@ -60,8 +60,6 @@ func initTPTPNativeTypes() { tIndividual = MkTyConst("$i") tProp = MkTyConst("$o") - - count_meta = 0 } func TType() Ty { diff --git a/src/AST/ty-syntax.go b/src/AST/ty-syntax.go index 5ea889c8..7f5b28f3 100644 --- a/src/AST/ty-syntax.go +++ b/src/AST/ty-syntax.go @@ -46,7 +46,6 @@ import ( ) var meta_mut sync.Mutex -var count_meta int type TyGenVar interface { isGenVar() @@ -286,6 +285,10 @@ func (p TyPi) VarsLen() int { return p.vars.Len() } +func (p TyPi) Ty() Ty { + return p.ty +} + // Makers func MkTyVar(repr string) Ty { @@ -298,8 +301,8 @@ func MkTyBV(name string, index int) Ty { func MkTyMeta(name string, formula int) Ty { meta_mut.Lock() - meta := TyMeta{name, count_meta, formula} - count_meta += 1 + meta := TyMeta{name, cpt_term, formula} + cpt_term += 1 meta_mut.Unlock() return meta } diff --git a/src/Core/FormListDS.go b/src/Core/FormListDS.go index f9017fa1..1ab41fcd 100644 --- a/src/Core/FormListDS.go +++ b/src/Core/FormListDS.go @@ -90,3 +90,7 @@ func (fl FormListDS) Unify(f AST.Form) (bool, []Unif.MixedSubstitutions) { } return false, []Unif.MixedSubstitutions{} } + +func (fl FormListDS) UnifyTerm(t AST.Term) (bool, []Unif.MixedTermSubstitutions) { + return false, []Unif.MixedTermSubstitutions{} +} diff --git a/src/Mods/equality/bse/equality_problem.go b/src/Mods/equality/bse/equality_problem.go index 803d84e1..7014fe94 100644 --- a/src/Mods/equality/bse/equality_problem.go +++ b/src/Mods/equality/bse/equality_problem.go @@ -136,11 +136,12 @@ func makeEqualityProblem(E Equalities, s AST.Term, t AST.Term, c ConstraintStruc /* Take a list of equalities and build the corresponding code tree */ func makeDataStructFromEqualities(eq Equalities) Unif.DataStructure { - formList := Lib.NewList[AST.Form]() + formList := Lib.NewList[AST.Term]() for _, e := range eq { - formList.Append(Unif.MakerTermForm(e.GetT1()), Unif.MakerTermForm(e.GetT2())) + formList.Append(e.GetT1(), e.GetT2()) } - return Unif.NewNode().MakeDataStruct(Lib.ListCpy(formList), true) + + return Unif.MakeTermUnifProblem(Lib.ListCpy(formList)) } /* Take a list of equalities and build the corresponding assocative map */ diff --git a/src/Mods/equality/bse/equality_rules_try_apply.go b/src/Mods/equality/bse/equality_rules_try_apply.go index cfc5a359..ceba6fa0 100644 --- a/src/Mods/equality/bse/equality_rules_try_apply.go +++ b/src/Mods/equality/bse/equality_rules_try_apply.go @@ -220,7 +220,7 @@ func searchUnifBewteenListAndEq(tl Lib.List[AST.Term], tree Unif.DataStructure) /* Take a (sub)-term t, and retrieve all the term t' unifiable with t */ func checkUnifInTree(t AST.Term, tree Unif.DataStructure) (bool, Lib.List[AST.Term]) { result_list := Lib.NewList[AST.Term]() - res, ms := tree.Unify(Unif.MakerTermForm(t.Copy())) + res, ms := tree.UnifyTerm(t.Copy()) if !res { return false, result_list @@ -232,7 +232,7 @@ func checkUnifInTree(t AST.Term, tree Unif.DataStructure) (bool, Lib.List[AST.Te return fmt.Sprintf("Unif found with: %s", subst.ToString()) }), ) - result_list.Append(subst.GetForm().(Unif.TermForm).GetTerm()) + result_list.Append(subst.Term()) } return result_list.Len() > 0, result_list diff --git a/src/Unif/code-trees.go b/src/Unif/code-trees.go index 6beb3371..3a7e25d1 100644 --- a/src/Unif/code-trees.go +++ b/src/Unif/code-trees.go @@ -58,11 +58,11 @@ func (c CodeBlock) Copy() CodeBlock { type Node struct { value CodeBlock children []*Node - formulas Lib.List[AST.Form] + leafFor Lib.List[Lib.Either[AST.Term, AST.Form]] } func NewNode() *Node { - return &Node{CodeBlock{}, []*Node{}, Lib.NewList[AST.Form]()} + return &Node{CodeBlock{}, []*Node{}, Lib.NewList[Lib.Either[AST.Term, AST.Form]]()} } func (n Node) getValue() CodeBlock { @@ -71,38 +71,48 @@ func (n Node) getValue() CodeBlock { func (n Node) getChildren() []*Node { return CopyNodeList(n.children) } -func (n Node) getFormulas() Lib.List[AST.Form] { - return Lib.ListCpy(n.formulas) -} /* Check if a node is empty */ func (n Node) IsEmpty() bool { return (len(n.value) == 0) } -/* Make data struct */ +func MakeUnifProblem(l Lib.List[AST.Form], is_pos bool) DataStructure { + return NewNode().MakeDataStruct(l, is_pos) +} + +func MakeTermUnifProblem(l Lib.List[AST.Term]) DataStructure { + root := makeNode(nil) + + for _, t := range l.GetSlice() { + root.insert(ParseTerm(transformTerm(t))) + } + + return root +} + func (n Node) MakeDataStruct(fl Lib.List[AST.Form], is_pos bool) DataStructure { return makeCodeTreeFromAtomic(fl, is_pos) } /* Copy a datastruct */ func (n Node) Copy() DataStructure { - return Node{n.getValue(), n.getChildren(), n.getFormulas()} + return Node{n.getValue(), n.getChildren(), n.leafFor.Copy(Lib.EitherCpy[AST.Term, AST.Form])} } /********************/ /* Helper functions */ /********************/ -/* The Node is a leaf when it contains at least one formulae. */ +/* The Node is a leaf whenever one formula or term ends here. */ func (n Node) isLeaf() bool { - return n.getFormulas().Len() > 0 + return n.leafFor.Len() > 0 } -/* Make two code trees (tree_pos and tree_neg) from st.atomic */ func makeCodeTreeFromAtomic(lf Lib.List[AST.Form], is_pos bool) *Node { form := Lib.NewList[AST.Form]() + // fixme: why are we doing this here? for _, f := range lf.GetSlice() { switch nf := f.(type) { case AST.Pred: @@ -116,9 +126,6 @@ func makeCodeTreeFromAtomic(lf Lib.List[AST.Form], is_pos bool) *Node { form.Append(nf.GetForm()) } } - case TermForm: - // EQUALITY - To build a tree of terms - form.Append(nf.Copy()) } } @@ -152,7 +159,7 @@ func makeNode(block CodeBlock) *Node { n := new(Node) n.value = block.Copy() n.children = []*Node{} - n.formulas = Lib.NewList[AST.Form]() + n.leafFor = Lib.NewList[Lib.Either[AST.Term, AST.Form]]() return n } @@ -198,8 +205,17 @@ func (n Node) printAux(tab int) { } if n.isLeaf() { - for _, form := range n.formulas.GetSlice() { - debug(Lib.MkLazy(func() string { return strings.Repeat("\t", tab+1) + form.ToString() })) + for _, tof := range n.leafFor.GetSlice() { + debug( + Lib.MkLazy( + func() string { + return strings.Repeat( + "\t", + tab+1, + ) + tofToString(tof) + }, + ), + ) } } debug(Lib.MkLazy(func() string { return "\n" })) @@ -214,17 +230,17 @@ func (n Node) printAux(tab int) { func (n *Node) insert(sequence Sequence) { if len(n.value) == 0 { n.value = sequence.GetInstructions() - n.formulas = Lib.MkListV(sequence.GetFormula()) + n.leafFor = Lib.MkListV(sequence.GetBase()) } else { - n.followInstructions(sequence.GetInstructions(), sequence.GetFormula()) + n.followInstructions(sequence.GetInstructions(), sequence.GetBase()) } } /* Auxiliary function to follow the sequence of instructions to insert in the Node. */ -func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { +func (n *Node) followInstructions(instructions []Instruction, tof Lib.Either[AST.Term, AST.Form]) { // Initialization of the node we will be working on and of a counter. current := n - oui := 0 + cnt := 0 // For each instruction, there are 2 cases: // * The current instruction is equivalent to the instruction stored in the CodeBlock of the current node at the index of the counter. @@ -234,11 +250,12 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { // If it's equivalent, there are 2 cases: // * It's the end of the sequence & the end of the CodeBlock. In this case, it's a full match, just add the formulae to the leaf. // * It's the end of the CodeBlock, but not of the sequence. In this case, check if the following instruction matches with any child. - if instr.IsEquivalent(current.value[oui]) { - oui += 1 - if i == len(instructions)-1 && oui == len(current.value) && !Lib.ListMem(form, current.formulas) { - current.formulas.Append(form) - } else if i < len(instructions)-1 && oui == len(current.value) { + if instr.IsEquivalent(current.value[cnt]) { + cnt += 1 + if i == len(instructions)-1 && cnt == len(current.value) && + !current.leafFor.Contains(tof, tofCmp) { + current.leafFor.Append(tof) + } else if i < len(instructions)-1 && cnt == len(current.value) { // If the instruction matches, then continue the algorithm with the child as the current node. // If it doesn't, we have a new leaf with the following instructions of the sequence. @@ -246,13 +263,13 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { for _, child := range current.children { if instructions[i+1].IsEquivalent(child.value[0]) { current = child - oui = 0 + cnt = 0 found = true } } if !found { newNode := makeNode(instructions[i+1:]) - newNode.formulas = Lib.MkListV(form) + newNode.leafFor = Lib.MkListV(tof) current.children = append(current.children, newNode) break } @@ -261,15 +278,15 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { // Split the current CodeBlock in 2 parts: // * The first one will contain the remaining instructions of the current CodeBlock, and it will inherit the current's children and formulaes. // * The second one contains the remaining instructions of the sequence plus the formulae. - child1 := makeNode(current.value[oui:]) + child1 := makeNode(current.value[cnt:]) child2 := makeNode(instructions[i:]) - child2.formulas = Lib.MkListV(form) + child2.leafFor = Lib.MkListV(tof) child1.children = current.children - child1.formulas = current.formulas + child1.leafFor = current.leafFor - current.value = current.value[:oui] - current.formulas = Lib.NewList[AST.Form]() + current.value = current.value[:cnt] + current.leafFor = Lib.NewList[Lib.Either[AST.Term, AST.Form]]() current.children = []*Node{child1, child2} break @@ -279,12 +296,12 @@ func (n *Node) followInstructions(instructions []Instruction, form AST.Form) { // It's the end of the sequence, but there are still instructions in the CodeBlock. // In this case, we have to split the CodeBlock in 2 parts. The first one will be a leaf containing the current sequence's formulae. // The second will be the rest of the CodeBlock's instructions, with the current's children and formulaes. - if oui < len(current.value)-1 { - child1 := makeNode(current.value[oui:]) + if cnt < len(current.value)-1 { + child1 := makeNode(current.value[cnt:]) child1.children = current.children - current.value = current.value[:oui] + current.value = current.value[:cnt] current.children = []*Node{child1} - current.formulas = Lib.MkListV(form.Copy()) + current.leafFor = Lib.MkListV(tofCopy(tof)) } } diff --git a/src/Unif/data_structure.go b/src/Unif/data_structure.go index c3d9f2a7..7678be98 100644 --- a/src/Unif/data_structure.go +++ b/src/Unif/data_structure.go @@ -47,6 +47,18 @@ type DataStructure interface { IsEmpty() bool MakeDataStruct(Lib.List[AST.Form], bool) DataStructure InsertFormulaListToDataStructure(Lib.List[AST.Form]) DataStructure + Unify(AST.Form) (bool, []MixedSubstitutions) + UnifyTerm(AST.Term) (bool, []MixedTermSubstitutions) + // FIXME: + // When the unification gets reworked, think a bit more about the exposed interface. + // We want to index on _terms_ while keeping the ability to unify _predicates_. + // (we can easily coerce a predicate to a function) + // We probably want to expose two functions --- one to unify predicates, and the other + // one to unify terms. But maybe we should say that unifying predicates is the "weird" + // case instead of the other way around. + // + // We should also find a more explicit name over `DataStructure`... + Copy() DataStructure } diff --git a/src/Unif/machine.go b/src/Unif/machine.go index 6fa2c0ec..abd835ae 100644 --- a/src/Unif/machine.go +++ b/src/Unif/machine.go @@ -65,7 +65,7 @@ type Machine struct { subst []SubstPair terms Lib.List[AST.Term] meta Substitutions - failure []MatchingSubstitutions + failure []MixMatchSubstitutions topLevelTot int topLevelCount int } @@ -82,7 +82,7 @@ func makeMachine() Machine { subst: []SubstPair{}, terms: Lib.NewList[AST.Term](), meta: Substitutions{}, - failure: []MatchingSubstitutions{}, + failure: []MixMatchSubstitutions{}, topLevelTot: 0, topLevelCount: 0, } diff --git a/src/Unif/matching.go b/src/Unif/matching.go index 2091101a..9ec4a010 100644 --- a/src/Unif/matching.go +++ b/src/Unif/matching.go @@ -56,58 +56,67 @@ func InitDebugger() { /* Helper function to avoid using MakeMachine() outside of this file. */ func (n Node) Unify(formula AST.Form) (bool, []MixedSubstitutions) { machine := makeMachine() - res := machine.unify(n, formula) + var term AST.Term + + if formula_type, is_pred := formula.(AST.Pred); is_pred { + term = transformPred(formula_type) + } else { + Glob.Anomaly("unification", fmt.Sprintf("Expected predicate, got %s", formula.ToString())) + } + + res, matching_substs := machine.unify(n, term) + // As we have transformed type metas to terms, we get everything in a term substitution. // But externally, we want to have a substitution of both (term) metas to terms and (type) metas to types. // We use MixedSubstitution to properly manage things internally. mixed_substs := []MixedSubstitutions{} - for _, subst := range res { + for _, subst := range matching_substs { mixed_substs = append(mixed_substs, subst.toMixed()) } - return !reflect.DeepEqual(machine.failure, res), mixed_substs + + return res, mixed_substs } -/* Tries to find the substitutions needed to unify the formulae with the one described by the sequence of instructions. */ -func (m *Machine) unify(node Node, formula AST.Form) []MatchingSubstitutions { - var result []MatchingSubstitutions - // The formula has to be a predicate. - switch formula_type := formula.(type) { - case AST.Pred: - // Transform the predicate to a function to make the tool work properly - m.terms = Lib.MkListV[AST.Term](AST.MakerFun( - formula_type.GetID(), - Lib.NewList[AST.Ty](), - getFunctionalArguments(formula_type.GetTyArgs(), formula_type.GetArgs()), - )) - result = m.unifyAux(node) - - if !reflect.DeepEqual(m.failure, result) { - filteredResult := []MatchingSubstitutions{} - for _, matchingSubst := range result { - filteredResult = append(filteredResult, - MakeMatchingSubstitutions(matchingSubst.GetForm(), matchingSubst.GetSubst())) - } - result = filteredResult - } - case TermForm: - m.terms = Lib.MkListV(formula_type.GetTerm()) - result = m.unifyAux(node) - default: - result = m.failure +func (n Node) UnifyTerm(t AST.Term) (bool, []MixedTermSubstitutions) { + m := makeMachine() + + res, matching_substs := m.unify( + n, + transformTerm(t), + ) + + mixed_substs := []MixedTermSubstitutions{} + for _, subst := range matching_substs { + mixed_substs = append(mixed_substs, subst.toMixedTerm()) } - return result + return res, mixed_substs +} + +/* Tries to find the substitutions needed to unify the formulae with the one described by the sequence of instructions. */ +func (m *Machine) unify(node Node, t AST.Term) (bool, []MixMatchSubstitutions) { + m.terms = Lib.MkListV(t) + res := m.unifyAux(node) + return !reflect.DeepEqual(m.failure, res), res } /*** Unify aux ***/ -func (m *Machine) unifyAux(node Node) []MatchingSubstitutions { +func (m *Machine) unifyAux(node Node) []MixMatchSubstitutions { for _, instr := range node.value { debug(Lib.MkLazy(func() string { return "------------------------" })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("Instr: %v", instr.ToString()) })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("Meta : %v", m.meta.ToString()) })) - debug(Lib.MkLazy(func() string { return fmt.Sprintf("Subst : %v", SubstPairListToString(m.subst)) })) - debug(Lib.MkLazy(func() string { return fmt.Sprintf("Post : %v", IntPairistToString(m.post)) })) + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("Subst : %v", SubstPairListToString(m.subst)) }, + ), + ) + debug( + Lib.MkLazy( + func() string { return fmt.Sprintf("Post : %v", IntPairistToString(m.post)) }, + ), + ) debug(Lib.MkLazy(func() string { return fmt.Sprintf("IsLocked : %v", m.isLocked()) })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("HasPushed : %v", m.hasPushed) })) debug(Lib.MkLazy(func() string { return fmt.Sprintf("HasPoped : %v", m.hasPoped) })) @@ -131,7 +140,9 @@ func (m *Machine) unifyAux(node Node) []MatchingSubstitutions { Lib.MkLazy(func() string { return fmt.Sprintf("Cursor: %v/%v", m.q, m.terms.Len()) }), ) debug( - Lib.MkLazy(func() string { return fmt.Sprintf("m.terms[cursor] : %v", m.terms.At(m.q).ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("m.terms[cursor] : %v", m.terms.At(m.q).ToString()) }, + ), ) debug( Lib.MkLazy(func() string { @@ -173,26 +184,29 @@ func (m *Machine) unifyAux(node Node) []MatchingSubstitutions { } } - matching := []MatchingSubstitutions{} + matching := []MixMatchSubstitutions{} if node.isLeaf() { - for _, f := range node.formulas.GetSlice() { - if reflect.TypeOf(f) == reflect.TypeOf(AST.Pred{}) || reflect.TypeOf(f) == reflect.TypeOf(TermForm{}) { - // Rebuild final substitution between meta and subst - final_subst := computeSubstitutions(CopySubstPairList(m.subst), m.meta.Copy(), f.Copy()) - if !final_subst.Equals(Failure()) { - matching = append(matching, MakeMatchingSubstitutions(f, final_subst)) - } + for _, f := range node.leafFor.GetSlice() { + // Rebuild final substitution between meta and subst + final_subst := computeSubstitutions( + CopySubstPairList(m.subst), + m.meta.Copy(), + tofMetaList(f), + ) + if !final_subst.Equals(Failure()) { + matching = append(matching, MixMatchSubstitutions{tof: f, subst: final_subst}) } } } + matching = append(matching, m.launchChildrenSearch(node)...) return matching } /* Unify on goroutines - to manage die message */ /* TODO : remove when debug ok */ -func (m *Machine) unifyAuxOnGoroutine(n Node, ch chan []MatchingSubstitutions, father_id uint64) { +func (m *Machine) unifyAuxOnGoroutine(n Node, ch chan []MixMatchSubstitutions, father_id uint64) { debug( Lib.MkLazy(func() string { return fmt.Sprintf("Child of %v, Unify Aux", father_id) }), ) @@ -202,23 +216,37 @@ func (m *Machine) unifyAuxOnGoroutine(n Node, ch chan []MatchingSubstitutions, f } /* Launches each child of the current node in a goroutine. */ -func (m *Machine) launchChildrenSearch(node Node) []MatchingSubstitutions { - channels := []chan []MatchingSubstitutions{} +func (m *Machine) launchChildrenSearch(node Node) []MixMatchSubstitutions { + channels := []chan []MixMatchSubstitutions{} for _, c := range node.children { debug( - Lib.MkLazy(func() string { return fmt.Sprintf("Next symbol = %v", c.getValue()[0].ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("Next symbol = %v", c.getValue()[0].ToString()) }, + ), ) - channels = append(channels, make(chan []MatchingSubstitutions)) + channels = append(channels, make(chan []MixMatchSubstitutions)) } - matching := []MatchingSubstitutions{} + matching := []MixMatchSubstitutions{} for i, n := range node.children { ch := channels[i] st := m.terms.Copy(AST.Term.Copy) ip := CopyIntPairList(m.post) sc := CopySubstPairList(m.subst) - copy := Machine{subst: sc, beginLock: m.beginLock, terms: st, meta: m.meta.Copy(), q: m.q, beginCount: m.beginCount, hasPushed: m.hasPushed, hasPoped: m.hasPoped, post: ip, topLevelTot: m.topLevelTot, topLevelCount: m.topLevelCount} + copy := Machine{ + subst: sc, + beginLock: m.beginLock, + terms: st, + meta: m.meta.Copy(), + q: m.q, + beginCount: m.beginCount, + hasPushed: m.hasPushed, + hasPoped: m.hasPoped, + post: ip, + topLevelTot: m.topLevelTot, + topLevelCount: m.topLevelCount, + } go copy.unifyAuxOnGoroutine(*n, ch, Glob.GetGID()) Glob.IncrGoRoutine(1) @@ -232,7 +260,7 @@ func (m *Machine) launchChildrenSearch(node Node) []MatchingSubstitutions { for cpt_remaining_children > 0 { _, value, _ := reflect.Select(cases) - matching = append(matching, value.Interface().([]MatchingSubstitutions)...) + matching = append(matching, value.Interface().([]MixMatchSubstitutions)...) cpt_remaining_children-- } diff --git a/src/Unif/matching_substitutions.go b/src/Unif/matching_substitutions.go index 7ed91cb5..1cedfd57 100644 --- a/src/Unif/matching_substitutions.go +++ b/src/Unif/matching_substitutions.go @@ -106,11 +106,12 @@ func translateTermRec(term AST.Term) AST.Term { opt_ty := Typing.QueryGlobalEnv(trm.GetName()) switch ty := opt_ty.(type) { case Lib.Some[AST.Ty]: - switch t := ty.Val.(type) { - case AST.TyPi: - for i := 0; i < t.VarsLen(); i++ { - ty_args.Append(AST.TermToTy(trm.GetArgs().At(i))) - } + t := ty.Val + i := 0 + for Glob.Is[AST.TyPi](t) { + ty_args.Append(AST.TermToTy(trm.GetArgs().At(i))) + t = t.(AST.TyPi).Ty() + i += 1 } } args := trm.GetArgs() @@ -268,6 +269,56 @@ func (m MixedSubstitutions) MatchingSubstitutions() MatchingSubstitutions { return MakeMatchingSubstitutions(m.form, m.GetTrmSubsts()) } +type MixMatchSubstitutions struct { + tof Lib.Either[AST.Term, AST.Form] + subst Substitutions +} + +// Pre-requisite: only formulas in the tof +func (s MixMatchSubstitutions) toMatching() MatchingSubstitutions { + switch tof := s.tof.(type) { + case Lib.Left[AST.Term, AST.Form]: + Glob.Anomaly("unification", "expected unification between formulas, got unification between terms") + case Lib.Right[AST.Term, AST.Form]: + return MakeMatchingSubstitutions(tof.Val, s.subst) + } + + Glob.Anomaly("unification", "reached an unreachable case") + return MakeMatchingSubstitutions(AST.MakerTop(), MakeEmptySubstitution()) +} + +func (s MixMatchSubstitutions) toMixed() MixedSubstitutions { + return s.toMatching().toMixed() +} + +type MixedTermSubstitutions struct { + term AST.Term + substs []MixedSubstitution +} + +func (s MixedTermSubstitutions) Term() AST.Term { return s.term } + +func (s MixedTermSubstitutions) ToString() string { + substs_list := Lib.MkListV(s.substs...) + return s.term.ToString() + " {" + Lib.ListToString(substs_list, Lib.WithEmpty("")) + "}" +} + +func (s MixMatchSubstitutions) toMixedTerm() MixedTermSubstitutions { + switch tof := s.tof.(type) { + case Lib.Left[AST.Term, AST.Form]: + substs := []MixedSubstitution{} + for _, subst := range s.subst { + substs = append(substs, translateFromSubst(subst)) + } + return MixedTermSubstitutions{tof.Val, substs} + case Lib.Right[AST.Term, AST.Form]: + Glob.Anomaly("unification", "expected unification between terms, got unification between formulas") + } + + Glob.Anomaly("unification", "reached an unreachable case") + return MixedTermSubstitutions{nil, []MixedSubstitution{}} +} + func translateToSubst(subst MixedSubstitution) Substitution { switch s := subst.s.(type) { case Lib.Left[TySubstitution, Substitution]: @@ -283,7 +334,9 @@ func translateToSubst(subst MixedSubstitution) Substitution { return MakeSubstitution(AST.MakeEmptyMeta(), nil) } -func MergeMixedSubstitutions(substs1, substs2 Lib.List[MixedSubstitution]) (Lib.List[MixedSubstitution], bool) { +func MergeMixedSubstitutions( + substs1, substs2 Lib.List[MixedSubstitution], +) (Lib.List[MixedSubstitution], bool) { translated_substs1 := Lib.ListMap(substs1, translateToSubst).GetSlice() translated_substs2 := Lib.ListMap(substs2, translateToSubst).GetSlice() diff --git a/src/Unif/parsing.go b/src/Unif/parsing.go index c8a80fc6..5e8d080d 100644 --- a/src/Unif/parsing.go +++ b/src/Unif/parsing.go @@ -34,79 +34,30 @@ package Unif import ( "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" "github.com/GoelandProver/Goeland/Lib" ) -type TermForm struct { - index int - t AST.Term +func transformPred(p AST.Pred) AST.Term { + return transformTerm(AST.MakerFun(p.GetID(), p.GetTyArgs(), p.GetArgs())) } -func (t TermForm) ToString() string { return t.ToString() } -func (t TermForm) GetTerm() AST.Term { return t.t.Copy() } -func (t TermForm) Copy() AST.Form { return makeTermForm(t.GetIndex(), t.GetTerm()) } -func (t TermForm) RenameVariables() AST.Form { return t } -func (t TermForm) ReplaceTermByTerm(AST.Term, AST.Term) (AST.Form, bool) { - return t, false -} -func (t TermForm) SubstTy(AST.TyGenVar, AST.Ty) AST.Form { - return t -} -func (t TermForm) GetIndex() int { return t.index } -func (t TermForm) SubstituteVarByMeta(AST.Var, AST.Meta) AST.Form { return t } -func (t TermForm) GetInternalMetas() Lib.List[AST.Meta] { return Lib.NewList[AST.Meta]() } -func (t TermForm) SetInternalMetas(Lib.List[AST.Meta]) AST.Form { return t } -func (t TermForm) GetSubFormulasRecur() Lib.List[AST.Form] { return Lib.NewList[AST.Form]() } -func (t TermForm) GetChildFormulas() Lib.List[AST.Form] { return Lib.NewList[AST.Form]() } - -func (t TermForm) Equals(t2 any) bool { - switch nt := t2.(type) { - case TermForm: - return t.GetTerm().Equals(nt.GetTerm()) - default: - return false - } -} - -func (t TermForm) GetMetas() Lib.Set[AST.Meta] { - switch nt := t.GetTerm().(type) { - case AST.Meta: - return Lib.Singleton(nt) - case AST.Fun: - res := Lib.EmptySet[AST.Meta]() - - for _, m := range nt.GetArgs().GetSlice() { - switch mt := m.(type) { - case AST.Meta: - res = res.Add(mt) - } - } - - return res - default: - return Lib.EmptySet[AST.Meta]() - } -} - -func (t TermForm) GetSubTerms() Lib.List[AST.Term] { - return t.GetTerm().GetSubTerms() -} - -func (t TermForm) ReplaceMetaByTerm(meta AST.Meta, term AST.Term) AST.Form { - return t -} - -func MakerTermForm(t AST.Term) TermForm { - switch trm := t.(type) { +func transformTerm(t AST.Term) AST.Term { + switch term := t.(type) { + case AST.Id, AST.Meta, AST.Var: + return t case AST.Fun: - args := getFunctionalArguments(trm.GetTyArgs(), trm.GetArgs()) - t = AST.MakerFun(trm.GetID(), Lib.NewList[AST.Ty](), args) + args := Lib.ListMap(term.GetTyArgs(), AST.TyToTerm) + args.Append(Lib.ListMap(term.GetArgs(), transformTerm).GetSlice()...) + return AST.MakerFun( + term.GetID(), + Lib.NewList[AST.Ty](), + args, + ) } - return makeTermForm(AST.MakerIndexFormula(), t.Copy()) -} -func makeTermForm(i int, t AST.Term) TermForm { - return TermForm{i, t.Copy()} + Glob.Anomaly("unif parsing", "Unknown term") + return nil } /* Parses a formulae to a sequence of instructions. */ @@ -115,26 +66,17 @@ func ParseFormula(formula AST.Form) Sequence { // The formula has to be a predicate switch formula_type := formula.(type) { case AST.Pred: - instructions := Sequence{formula: formula_type} + instructions := Sequence{base: Lib.MkRight[AST.Term, AST.Form](formula)} - instructions.add(Begin{}) - parsePred(formula_type, &instructions) - instructions.add(End{}) + switch term := transformPred(formula_type).(type) { + case AST.Fun: + instructions.add(Begin{}) + parsePred(formula_type.GetID(), term.GetArgs(), &instructions) + instructions.add(End{}) - return instructions - case TermForm: - instructions := Sequence{formula: formula} - varCount := 0 - postCount := 0 - instructions.add(Begin{}) - parseTerms( - Lib.MkListV(formula_type.GetTerm().Copy()), - &instructions, - Lib.NewList[AST.Meta](), - &varCount, - &postCount, - ) - instructions.add(End{}) + default: + Glob.Anomaly("unification", "error when translating in internal representation") + } return instructions @@ -143,35 +85,15 @@ func ParseFormula(formula AST.Form) Sequence { } } -/* Parses a predicate to machine instructions */ -func getFunctionalArguments(ty_args Lib.List[AST.Ty], trm_args Lib.List[AST.Term]) Lib.List[AST.Term] { - args := Lib.ListMap(ty_args, AST.TyToTerm) - - for _, arg := range trm_args.GetSlice() { - switch term := arg.(type) { - case AST.Meta: - args.Append(arg) - case AST.Fun: - args.Append(AST.MakerFun( - term.GetID(), - Lib.NewList[AST.Ty](), - getFunctionalArguments(term.GetTyArgs(), term.GetArgs()), - )) - } - } - - return args -} - -func parsePred(p AST.Pred, instructions *Sequence) { - instructions.add(makeCheck(p.GetID())) - if !p.GetTyArgs().Empty() || !p.GetArgs().Empty() { +func parsePred(i AST.Id, args Lib.List[AST.Term], instructions *Sequence) { + instructions.add(makeCheck(i)) + if !args.Empty() { instructions.add(Begin{}) instructions.add(Down{}) varCount := 0 postCount := 0 parseTerms( - getFunctionalArguments(p.GetTyArgs(), p.GetArgs()), + args, instructions, Lib.NewList[AST.Meta](), &varCount, @@ -216,7 +138,7 @@ func parseTerms( instructions.add(Right{}) } case AST.Fun: - instructions.add(Begin{}) // TEST 33 + instructions.add(Begin{}) instructions.add(makeCheck(t.GetID())) if downDefined(t.GetArgs()) { @@ -225,18 +147,20 @@ func parseTerms( *postCount++ } instructions.add(Down{}) - subTerms := getFunctionalArguments(t.GetTyArgs(), t.GetArgs()) - subst = parseTerms(subTerms, instructions, subst, varCount, postCount) + if !t.GetTyArgs().Empty() { + Glob.Anomaly("unif parsing", "found type arguments at an unexpected place") + } + subst = parseTerms(t.GetArgs(), instructions, subst, varCount, postCount) if rightDefined(terms, i) { *postCount-- instructions.add(Pop{*postCount}) } instructions.add(makeEnd(t)) } else if rightDefined(terms, i) { - instructions.add(makeEnd(t)) // TEST33 + instructions.add(makeEnd(t)) instructions.add(Right{}) } else { - instructions.add(makeEnd(t)) // TEST33 + instructions.add(makeEnd(t)) } } } @@ -254,6 +178,6 @@ func ParseTerm(term AST.Term) Sequence { &varCount, &postCount, ) - instructions.formula = MakerTermForm(term) + instructions.base = Lib.MkLeft[AST.Term, AST.Form](term) return instructions } diff --git a/src/Unif/sequence.go b/src/Unif/sequence.go index 76a3717a..93ebf324 100644 --- a/src/Unif/sequence.go +++ b/src/Unif/sequence.go @@ -40,13 +40,42 @@ import ( "fmt" "github.com/GoelandProver/Goeland/AST" + "github.com/GoelandProver/Goeland/Glob" + "github.com/GoelandProver/Goeland/Lib" ) /*** Sequence ***/ +func tofToString(tof Lib.Either[AST.Term, AST.Form]) string { + return Lib.EitherToString[AST.Term, AST.Form](tof, "Trm", "Form") +} + +func tofCopy(tof Lib.Either[AST.Term, AST.Form]) Lib.Either[AST.Term, AST.Form] { + return Lib.EitherCpy[AST.Term, AST.Form](tof) +} + +func tofCmp(tof1, tof2 Lib.Either[AST.Term, AST.Form]) bool { + return Lib.EitherEquals[AST.Term, AST.Form](tof1, tof2) +} + +func tofMetaList(tof Lib.Either[AST.Term, AST.Form]) Lib.List[AST.Meta] { + switch tof := tof.(type) { + case Lib.Left[AST.Term, AST.Form]: + return transformTerm(tof.Val).GetMetaList() + case Lib.Right[AST.Term, AST.Form]: + switch f := tof.Val.(type) { + case AST.Pred: + return transformPred(f).GetMetaList() + } + } + + Glob.Anomaly("unification", "Unification has not been launched on terms or on a predicate") + return Lib.NewList[AST.Meta]() +} + type Sequence struct { instructions []Instruction - formula AST.Form + base Lib.Either[AST.Term, AST.Form] } /*** Sequence's methods ***/ @@ -55,22 +84,22 @@ func (s *Sequence) GetInstructions() []Instruction { return CopyInstructionList(s.instructions) } -func (s *Sequence) GetFormula() AST.Form { - return s.formula.Copy() +func (s *Sequence) GetBase() Lib.Either[AST.Term, AST.Form] { + return s.base } func (s *Sequence) add(instr Instruction) { s.instructions = append(s.instructions, instr) } -// ILL TODO: Should not print directly, should return a string that is then printed +// FIXME: Should not print directly, should return a string that is then printed func (s Sequence) Print() { for _, instr := range s.instructions { fmt.Printf("%v", instr) } - fmt.Printf(" - " + s.formula.ToString()) + fmt.Printf(" - " + tofToString(s.base)) } func (s Sequence) Copy() Sequence { - return Sequence{s.GetInstructions(), s.GetFormula()} + return Sequence{s.GetInstructions(), tofCopy(s.base)} } diff --git a/src/Unif/substitutions_tree.go b/src/Unif/substitutions_tree.go index 5a9be9e7..e1d03121 100644 --- a/src/Unif/substitutions_tree.go +++ b/src/Unif/substitutions_tree.go @@ -49,7 +49,11 @@ import ( * MetaToSubs : (meta, term) : meta in formula, term in tree * Merge both of them **/ -func computeSubstitutions(subs []SubstPair, metasToSubs Substitutions, form AST.Form) Substitutions { +func computeSubstitutions( + subs []SubstPair, + metasToSubs Substitutions, + metaList Lib.List[AST.Meta], +) Substitutions { debug( Lib.MkLazy(func() string { return fmt.Sprintf( @@ -57,56 +61,47 @@ func computeSubstitutions(subs []SubstPair, metasToSubs Substitutions, form AST. SubstPairListToString(subs), metasToSubs.ToString()) }), ) - metasFromTreeForm := Lib.NewList[AST.Meta]() treeSubs := Substitutions{} - // Retrieve all the meta of from the tree formula - switch typedForm := form.(type) { - case AST.Pred: - trms := getFunctionalArguments(typedForm.GetTyArgs(), typedForm.GetArgs()) - for _, trm := range trms.GetSlice() { - metasFromTreeForm.Append(trm.GetMetaList().GetSlice()...) - } - case TermForm: - metasFromTreeForm.Append(typedForm.GetTerm().GetMetaList().GetSlice()...) - default: - return Failure() - } - // Transform subst tree into a real substitution for _, value := range subs { - currentMeta := metasFromTreeForm.At(value.GetIndex()) - currentValue := value.GetTerm() - debug( - Lib.MkLazy(func() string { - return fmt.Sprintf( - "Iterate on subst : %v and %v", - currentMeta.ToString(), - currentValue.ToString()) - }), - ) + if value.GetIndex() < metaList.Len() { + currentMeta := metaList.At(value.GetIndex()) + currentValue := value.GetTerm() + debug( + Lib.MkLazy(func() string { + return fmt.Sprintf( + "Iterate on subst : %v and %v", + currentMeta.ToString(), + currentValue.ToString()) + }), + ) - if !currentMeta.Equals(currentValue) { - // Si current_meta a déjà une association dans metas - metaGet, index := metasToSubs.Get(currentMeta) - if HasSubst(metasToSubs, currentMeta) && (index != -1) && !currentValue.Equals(metaGet) { - // On cherche a unifier les deux valeurs - treeSubs.Set(currentMeta, currentValue) - new_unif := AddUnification(currentValue.Copy(), metaGet.Copy(), treeSubs.Copy()) - if new_unif.Equals(Failure()) { - return Failure() - } else { - treeSubs = new_unif - metasToSubs.Remove(index) // Remove from meta + if !currentMeta.Equals(currentValue) { + // Si current_meta a déjà une association dans metas + metaGet, index := metasToSubs.Get(currentMeta) + if HasSubst(metasToSubs, currentMeta) && (index != -1) && + !currentValue.Equals(metaGet) { + // On cherche a unifier les deux valeurs + treeSubs.Set(currentMeta, currentValue) + new_unif := AddUnification(currentValue.Copy(), metaGet.Copy(), treeSubs.Copy()) + if new_unif.Equals(Failure()) { + return Failure() + } else { + treeSubs = new_unif + metasToSubs.Remove(index) // Remove from meta + } + } else { // Ne pas ajouter la susbtitution égalité + treeSubs.Set(currentMeta, currentValue) } - } else { // Ne pas ajouter la susbtitution égalité - treeSubs.Set(currentMeta, currentValue) } } } debug( - Lib.MkLazy(func() string { return fmt.Sprintf("before meta : %v", metasToSubs.ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("before meta : %v", metasToSubs.ToString()) }, + ), ) // Metas_subst eliminate EliminateMeta(&metasToSubs) @@ -114,10 +109,14 @@ func computeSubstitutions(subs []SubstPair, metasToSubs Substitutions, form AST. if metasToSubs.Equals(Failure()) { return Failure() } - debug(Lib.MkLazy(func() string { return fmt.Sprintf("After meta : %v", metasToSubs.ToString()) })) + debug( + Lib.MkLazy(func() string { return fmt.Sprintf("After meta : %v", metasToSubs.ToString()) }), + ) debug( - Lib.MkLazy(func() string { return fmt.Sprintf("before tree_subst : %v", treeSubs.ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("before tree_subst : %v", treeSubs.ToString()) }, + ), ) // Tree subst elminate EliminateMeta(&treeSubs) @@ -126,7 +125,9 @@ func computeSubstitutions(subs []SubstPair, metasToSubs Substitutions, form AST. return Failure() } debug( - Lib.MkLazy(func() string { return fmt.Sprintf("after tree_subst : %v", treeSubs.ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("after tree_subst : %v", treeSubs.ToString()) }, + ), ) // Fusion @@ -152,7 +153,9 @@ func computeSubstitutions(subs []SubstPair, metasToSubs Substitutions, form AST. /* Call addUnification and returns a status - modify m.meta */ func (m *Machine) trySubstituteMeta(i AST.Term, j AST.Term) Status { debug( - Lib.MkLazy(func() string { return fmt.Sprintf("Try substitute : %v and %v", i.ToString(), j.ToString()) }), + Lib.MkLazy( + func() string { return fmt.Sprintf("Try substitute : %v and %v", i.ToString(), j.ToString()) }, + ), ) new_meta := AddUnification(i, j, m.meta.Copy()) if new_meta.Equals(Failure()) { @@ -172,6 +175,9 @@ func AddUnification(term1, term2 AST.Term, subst Substitutions) Substitutions { subst.ToString()) }), ) + term1 = transformTerm(term1) + term2 = transformTerm(term2) + // unify with ct only if the term already has an unification or if there is 2 fun. Just add it and eliminate otherwise. t1v, _ := subst.Get(term1.ToMeta()) t2v, _ := subst.Get(term2.ToMeta()) @@ -213,12 +219,16 @@ func (m *Machine) addUnifications(term1, term2 AST.Term) Status { term2.ToString()) }), ) - meta := tryUnification(term1.Copy(), term2.Copy(), m.meta.Copy()) // Return empty or an array of 1 matching substitution, which is m.meta improved wit (term1, term2) + meta := tryUnification( + term1.Copy(), + term2.Copy(), + m.meta.Copy(), + ) // Return empty or an array of 1 matching substitution, which is m.meta improved wit (term1, term2) if len(meta) == 0 { return Status(ERROR) } else { - m.meta = meta[0].GetSubst() + m.meta = meta[0].subst EliminateMeta(&m.meta) Eliminate(&m.meta) } @@ -227,7 +237,7 @@ func (m *Machine) addUnifications(term1, term2 AST.Term) Status { } /* Tries to unify term1 with term2, depending on the substitutions already found by the parent unification process. */ -func tryUnification(term1, term2 AST.Term, meta Substitutions) []MatchingSubstitutions { +func tryUnification(term1, term2 AST.Term, meta Substitutions) []MixMatchSubstitutions { debug( Lib.MkLazy(func() string { return fmt.Sprintf(