Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API by jrosain · Pull Request #53 · GoelandProver/Goeland

jrosain · 2025-07-27T10:01:09Z

Bug fix

Closes: #38

Description

I've totally removed the old typing system and reworked it in something new:

There is no more layering of types in the internal representation, we trust the elaboration between parsing terms and internal terms to handle this stuff. This is less confusing when working with types in the internal syntax.
Types are not embedded into terms / formulas anymore: only metavariables get their type. This makes the API of terms/formulas more easily maintainable as we don't need to worry about types.
The typing system itself has been simplified to make it more maintainable: we don't check well-formedness of contexts anymore as it's useless.
Moreover, there's only one global environment. This makes it easy to interpret a type statement: simply add the pair (name, type) to the global env using the only exposed function that does that.
The global environment can be queried with type instantiations, and lets the user do the error management in these types using option types.
Overall, the typing system yields better errors and has a way better debug environment using a high-level and a low-level debugger.
Added MixedSubstitution, which stores both term and type substitutions. Adapted the destructive proof search to make use of it. DMT is not fully supported yet, but I think the update is straightforward. Non-destructive search does not support mixed substitutions (as an aside, maybe we should cleanup the non destructive version, it doesn't work anyway so we could simply return errors saying this isn't implemented yet or simply remove the option to do non-destructive search).
Cleaned-up some old functions out of the proof search.
Disabled context printing of typed problems in Rocq/LambdaPi output as they were mostly useless anyway. I'm planning to fix it when taking care of Syntax error in Rocq output due to illegal character in skolem symbols / types #52

PR dependencies

Test-suite update

added basic TFF1 file to check that type metas are properly substituted in proofs test-suite/proofs/tf1_basic_thm.p
added basic TFF1 file to check that skolemized type variables are properly instantiated in proofs test-suite/proofs/tf1_basic_thm-2.p
added TFF1 file that should fail at typechecking that allowed me to find a bug in the generic parallel library and the function calls test-suite/bugs/bug_53-1.p
added elaboration tests test-suite/basic/test-typing-elab-n.p to check the ad-hoc polymorphism of defined arithmetic functions and the edge case of quotients

jcailler · 2026-03-20T07:49:57Z

 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 a.quantifier.Equals(typed.quantifier)


We don't have to check the variable list anymore?

It is checked but inside the quantifier interface instead.

jcailler · 2026-03-20T09:57:03Z

+		if !replaced {
+			newBv := MkTyBV(newVar.name, newVar.index)
+			f = f.SubstTy(v.ToTyBoundVar(), newBv)
+			newTyBv.Append(Lib.MkPair(v.ToTyBoundVar(), newBv))
+		}


It wasn't there before, why do we need that now?

This is because previously quantifiers over terms and types were heterogeneous: there was an All formula and an AllType formula. Now we have unified these two to simplify the interface and so we have to substitute either in the term or in the type. If we cannot substitute in the term, then the variable either does not appear in the formula or it appears in the types, so we try to substitute it inside the type.

Anyway the function renaming bound variables is bound to disappear (no pun intended) once bound variables are transformed into de bruijn indices.

jcailler · 2026-03-20T14:08:15Z

+	// context := AST.GetGlobalContext()
+	// for k, v := range context {
+	// 	if k != "=" && k[0] != '$' {
+	// 		switch typed := v[0].App.(type) {
+	// 		case AST.TypeArrow:
+	// 			primitives := typed.GetPrimitives()
+	// 			typesStr := ""
+
+	// 			for i, prim := range primitives {
+	// 				if i != len(primitives)-1 {
+	// 					typesStr += "τ (" + prim.ToString() + ") → "
+	// 				} else {
+	// 					typesStr += prim.ToString()
+	// 				}
+	// 			}
+	// 			arrows = append(arrows, Glob.MakePair(k, typesStr))
+	// 		case AST.QuantifiedType:
+	// 			primitives := typed.GetPrimitives()
+	// 			typesStr := ""
+	// 			contextualized := []string{}
+
+	// 			for i, prim := range primitives {
+	// 				if i != len(primitives)-1 {
+	// 					switch typedPrim := prim.(type) {
+	// 					case AST.TypeVar:
+	// 						str := AST.SimpleStringMappable(typedPrim.ToString())
+	// 						symbol := addToContext(&str)
+	// 						typesStr += "τ (" + symbol + ") → "
+	// 						contextualized = append(contextualized, symbol)
+	// 					case AST.TypeHint:
+	// 						typesStr += "τ (" + prim.ToString() + ") → "
+	// 					}
+	// 				} else {
+	// 					typesStr += prim.ToString()
+	// 				}
+	// 			}
+	// 			arrows = append(arrows, Glob.MakePair(k, fmt.Sprintf("Π (%s : Type), %s", strings.Join(contextualized, " : Type), ("), typesStr)))
+	// 		case AST.TypeHint:
+	// 			if k == typed.ToString() {
+	// 				types = append(types, Glob.MakePair(k, "Type"))
+	// 			} else {
+	// 				others = append(others, Glob.MakePair(k, fmt.Sprintf("τ (%s)", typed.ToString())))
+	// 			}
+	// 		}
+	// 	}
+	// }
+
+	// return types, arrows, others


Do we want to keep this?

Yes we actually want to do something alike when fixing the LP output (#67)

jcailler · 2026-03-20T14:10:10Z

+	// } else {
+	// 	context := AST.GetGlobalContext()
+	// 	for k, v := range context {
+	// 		if typed, ok := v[0].App.(AST.TypeHint); ok {
+	// 			if k[0] != '$' && k == typed.ToString() {
+	// 				resultingString += "Parameter " + k + ": Type.\n"
+
+	// 			}
+	// 		}
+	// 	}
+
+	// 	resultingString += strings.Join(getContextFromFormula(root), "\n") + "\n"
+
+	// 	if metaList.Len() > 0 {
+	// 		resultingString += contextualizeMetas(metaList)
+	// 	}
+	// }


Do we want to keep this?

Yes we actually want to keep it to do the same thing when fixing the rocq output (#59)

* non destructive search **does not** manage typed search, only destructive search does * dmt might be incompatible with typed search

jrosain requested a review from jcailler July 27, 2025 10:01

github-actions bot added the needs:ci Needs a CI run before merging label Jul 27, 2025

jrosain added this to the 1.2 milestone Jul 27, 2025

github-actions bot removed the request:ci Requests a CI run from the workflow label Jul 27, 2025

jrosain force-pushed the update-type-system branch from 2780a16 to cc89202 Compare July 27, 2025 10:14

jrosain added the request:ci Requests a CI run from the workflow label Jul 27, 2025

github-actions bot removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Jul 27, 2025

jrosain force-pushed the update-type-system branch from cc89202 to f0c5429 Compare July 27, 2025 15:50

github-actions bot added the needs:ci Needs a CI run before merging label Jul 27, 2025

jrosain added the request:ci Requests a CI run from the workflow label Jul 27, 2025

github-actions bot removed the request:ci Requests a CI run from the workflow label Jul 27, 2025

jrosain force-pushed the update-type-system branch from f0c5429 to c064455 Compare July 27, 2025 16:45

jrosain added the request:ci Requests a CI run from the workflow label Jul 27, 2025

github-actions bot added needs:ci Needs a CI run before merging and removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Jul 27, 2025

jrosain force-pushed the update-type-system branch from ab5b778 to 917dfa1 Compare July 28, 2025 07:33

jrosain added the request:ci Requests a CI run from the workflow label Jul 28, 2025

github-actions bot removed request:ci Requests a CI run from the workflow needs:ci Needs a CI run before merging labels Jul 28, 2025

jrosain mentioned this pull request Jul 29, 2025

Fix syntax error on Rocq output by using a better printing system #59

Merged

github-actions bot removed the needs:ci Needs a CI run before merging label Mar 19, 2026

jrosain removed has:other-pr-dependency This PR cannot be merged before another PR (the maintainer should specify the dependency(ies)) needs:rebase When the PR needs to get rebased in order to get merged labels Mar 19, 2026

jrosain added 4 commits March 20, 2026 11:22

Removal of invasive type system

b25f85e

Updated syntax of types and reintroduced them in the internals

e21b017

Implementation of the new typing system

28770d4

Updated gamma and delta rules to deal with type variables

e4263d0

jrosain force-pushed the update-type-system branch from 6524fb1 to ab51ebc Compare March 20, 2026 10:26

github-actions bot added the needs:ci Needs a CI run before merging label Mar 20, 2026

jrosain added the request:ci Requests a CI run from the workflow label Mar 20, 2026

github-actions bot removed needs:ci Needs a CI run before merging request:ci Requests a CI run from the workflow labels Mar 20, 2026

jcailler requested changes Mar 20, 2026

View reviewed changes

jrosain force-pushed the update-type-system branch from ab51ebc to 54a1cd4 Compare March 20, 2026 15:20

github-actions bot added the needs:ci Needs a CI run before merging label Mar 20, 2026

jrosain added the request:ci Requests a CI run from the workflow label Mar 20, 2026

github-actions bot removed needs:ci Needs a CI run before merging request:ci Requests a CI run from the workflow labels Mar 20, 2026

jrosain added 4 commits March 20, 2026 17:10

Manage typed proof search and add related tests

7e47707

* non destructive search **does not** manage typed search, only destructive search does * dmt might be incompatible with typed search

Fix equality of quantified formulas (forall, exists)

c4b4e6f

Add proper debugging facilities in typing rules

8d519f9

Add some basic tests on the elaboration

7695826

jrosain force-pushed the update-type-system branch from 54a1cd4 to 7695826 Compare March 20, 2026 16:10

github-actions bot added the needs:ci Needs a CI run before merging label Mar 20, 2026

jrosain added the request:ci Requests a CI run from the workflow label Mar 20, 2026

github-actions bot removed needs:ci Needs a CI run before merging request:ci Requests a CI run from the workflow labels Mar 20, 2026

jcailler approved these changes Mar 25, 2026

View reviewed changes

jcailler merged commit b7cb6f8 into GoelandProver:master Mar 25, 2026
9 checks passed

jrosain deleted the update-type-system branch March 25, 2026 12:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API#53

Major overhaul of the type system to manage typed proof search with an easier-to-maintain and less invasive API#53
jcailler merged 8 commits intoGoelandProver:masterfrom
jrosain:update-type-system

jrosain commented Jul 27, 2025 •

edited

Loading

Uh oh!

jcailler Mar 20, 2026

Uh oh!

jrosain Mar 20, 2026 •

edited

Loading

Uh oh!

jcailler Mar 20, 2026

Uh oh!

jrosain Mar 20, 2026

Uh oh!

Uh oh!

jcailler Mar 20, 2026

Uh oh!

jrosain Mar 20, 2026

Uh oh!

jcailler Mar 20, 2026

Uh oh!

jrosain Mar 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

jrosain commented Jul 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Bug fix

Description

PR dependencies

Test-suite update

Uh oh!

jcailler Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

jrosain Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcailler Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

jrosain Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jcailler Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

jrosain Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

jcailler Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

jrosain Mar 20, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

jrosain commented Jul 27, 2025 •

edited

Loading

jrosain Mar 20, 2026 •

edited

Loading