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

devtools/test-suite/basic/test-typing-elab-1.p

@@ -0,0 +1,7 @@
+% should fail because $lesseq is a defined function for $int, $rat and $real but is not polymorphic
+% for any type
+% exit: 1
+
+tff(ty_type, type, ty : $tType).
+
+tff(conj, conjecture, ! [A : ty] : $lesseq(A, A)).

devtools/test-suite/basic/test-typing-elab-2.p

@@ -0,0 +1,7 @@
+% should fail because $quotient is a defined function for $int, $rat and $real but is not polymorphic
+% for any type
+% exit: 1
+
+tff(ty_type, type, ty : $tType).
+
+tff(conj, conjecture, ! [A : ty] : $lesseq($quotient(A, A), 1)).

devtools/test-suite/basic/test-typing-elab-3.p

@@ -0,0 +1,4 @@
+% quotient is defined specifically for integers
+% result: NOT VALID
+
+tff(conj, conjecture, $lesseq($quotient(2, 2), 1)).

devtools/test-suite/basic/tf1_syntax_chk.p

@@ -1,5 +1,5 @@
-% TODO: args -one_step and result NOT_VALID once typing is working again (this is satisfiable)
-% exit: 3
+% args: -one_step
+% result: NOT VALID
 
 tff(beverage_type,type,
     beverage: $tType ).

devtools/test-suite/basic/tfa_syntax_chk.p

@@ -1,5 +1,5 @@
 % As arithmetic is not handled by Goeland, we simply check that parsing is OK
-% args: -ari -one_step -l 1
+% args: -one_step -l 1
 % result: NOT VALID
 
 tff(p_int_type,type,

devtools/test-suite/bugs/bug_53-1.p

@@ -0,0 +1,33 @@
+% args: -one_step
+% exit: 1
+
+tff(list_type,type,
+	list: $tType > $tType ).
+
+tff(maybe_type,type,
+	maybe: $tType > $tType ).
+
+%----Polymorphic symbols
+tff(nil_type,type,
+	nil:
+	  !>[A: $tType] : list(A) ).
+
+tff(cons_type,type,
+	cons:
+	  !>[A: $tType] : ( ( A * list(A) ) > list(A) ) ).
+
+tff(none_type,type,
+	none:
+	  !>[A: $tType] : maybe(A) ).
+
+tff(some_type,type,
+	some:
+	  !>[A: $tType] : ( A > maybe(A) ) ).
+
+tff(head_type,type,
+	head:
+	  !>[A: $tType] : ( list(A) > maybe(A) ) ).
+
+%----This cannot be well typed, the last cons is not well formed
+tff(solve_this,conjecture,
+	  head($int,cons($int,1,cons($int,2,cons($int,3)))) = some($int,1) ).

devtools/test-suite/proofs/tf1_basic_thm-2.out

@@ -0,0 +1,28 @@
+[0] ALPHA_AND : ((! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))) & (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))) & ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23))))))
+	-> [1] (! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;)))), (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17)))), ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23)))))
+
+[1] DELTA_NOT_FORALL : ~((! [A21 X23 Y25 Z27]: ((maybe(A21) ; head(A21;cons(A21;X23, cons(A21;Y25, cons(A21;Z27, nil(A21;))))) = some(A21;X23)))))
+	-> [2] ~((! [X23 Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;X23)))))
+
+[2] DELTA_NOT_FORALL : ~((! [X23 Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;X23)))))
+	-> [3] ~((! [Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))
+
+[3] DELTA_NOT_FORALL : ~((! [Y25 Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))
+	-> [4] ~((! [Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))
+
+[4] DELTA_NOT_FORALL : ~((! [Z27]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))))
+	-> [5] ~((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23)))
+
+[5] GAMMA_FORALL : (! [A13]: ((maybe(A13) ; head(A13;nil(A13;)) = none(A13;))))
+	-> [6] (maybe(A13_1) ; head(A13_1;nil(A13_1;)) = none(A13_1;))
+
+[6] GAMMA_FORALL : (! [A15 X17 XS19]: ((maybe(A15) ; head(A15;cons(A15;X17, XS19)) = some(A15;X17))))
+	-> [7] (! [X17 XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X17, XS19)) = some(skoTy;X17))))
+
+[7] GAMMA_FORALL : (! [X17 XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;X17, XS19)) = some(skoTy;X17))))
+	-> [8] (! [XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, XS19)) = some(skoTy;skolem@X23))))
+
+[8] GAMMA_FORALL : (! [XS19]: ((maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, XS19)) = some(skoTy;skolem@X23))))
+	-> [9] (maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))
+
+[9] CLOSURE : (maybe(skoTy) ; head(skoTy;cons(skoTy;skolem@X23, cons(skoTy;skolem@Y25, cons(skoTy;skolem@Z27, nil(skoTy;))))) = some(skoTy;skolem@X23))

devtools/test-suite/proofs/tf1_basic_thm-2.p

@@ -0,0 +1,40 @@
+% args: -proof -no_id
+% result: VALID
+
+tff(list_type,type,
+	list: $tType > $tType ).
+
+tff(maybe_type,type,
+	maybe: $tType > $tType ).
+
+%----Polymorphic symbols
+tff(nil_type,type,
+	nil:
+	  !>[A: $tType] : list(A) ).
+
+tff(cons_type,type,
+	cons:
+	  !>[A: $tType] : ( ( A * list(A) ) > list(A) ) ).
+
+tff(none_type,type,
+	none:
+	  !>[A: $tType] : maybe(A) ).
+
+tff(some_type,type,
+	some:
+	  !>[A: $tType] : ( A > maybe(A) ) ).
+
+tff(head_type,type,
+	head:
+	  !>[A: $tType] : ( list(A) > maybe(A) ) ).
+
+%----Use of polymorphic symbols
+tff(head_nil,axiom,
+	! [A: $tType] : ( head(A,nil(A)) = none(A) )).
+
+tff(head_cons,axiom,
+	! [A: $tType,X : A,XS : list(A)] : ( head(A,cons(A,X,XS)) = some(A,X) ) ).
+
+%----With integers
+tff(solve_this,conjecture,
+	! [A: $tType,X : A,Y : A,Z : A] : ( head(A,cons(A,X,cons(A,Y,cons(A,Z,nil(A))))) = some(A,X) ) ).

devtools/test-suite/proofs/tf1_basic_thm.out

@@ -0,0 +1,16 @@
+[0] ALPHA_AND : ((! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))) & (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))) & ~((maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))))
+	-> [1] (! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;)))), (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18)))), ~((maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1)))
+
+[1] GAMMA_FORALL : (! [A14]: ((maybe(A14) ; head(A14;nil(A14;)) = none(A14;))))
+	-> [2] (maybe(A14_1) ; head(A14_1;nil(A14_1;)) = none(A14_1;))
+
+[2] GAMMA_FORALL : (! [A16 X18 XS20]: ((maybe(A16) ; head(A16;cons(A16;X18, XS20)) = some(A16;X18))))
+	-> [3] (! [X18 XS20]: ((maybe($int) ; head($int;cons($int;X18, XS20)) = some($int;X18))))
+
+[3] GAMMA_FORALL : (! [X18 XS20]: ((maybe($int) ; head($int;cons($int;X18, XS20)) = some($int;X18))))
+	-> [4] (! [XS20]: ((maybe($int) ; head($int;cons($int;1, XS20)) = some($int;1))))
+
+[4] GAMMA_FORALL : (! [XS20]: ((maybe($int) ; head($int;cons($int;1, XS20)) = some($int;1))))
+	-> [5] (maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))
+
+[5] CLOSURE : (maybe($int) ; head($int;cons($int;1, cons($int;2, cons($int;3, nil($int;))))) = some($int;1))

devtools/test-suite/proofs/tf1_basic_thm.p

@@ -0,0 +1,40 @@
+% args: -proof -no_id
+% result: VALID
+
+tff(list_type,type,
+	list: $tType > $tType ).
+
+tff(maybe_type,type,
+	maybe: $tType > $tType ).
+
+%----Polymorphic symbols
+tff(nil_type,type,
+	nil:
+	  !>[A: $tType] : list(A) ).
+
+tff(cons_type,type,
+	cons:
+	  !>[A: $tType] : ( ( A * list(A) ) > list(A) ) ).
+
+tff(none_type,type,
+	none:
+	  !>[A: $tType] : maybe(A) ).
+
+tff(some_type,type,
+	some:
+	  !>[A: $tType] : ( A > maybe(A) ) ).
+
+tff(head_type,type,
+	head:
+	  !>[A: $tType] : ( list(A) > maybe(A) ) ).
+
+%----Use of polymorphic symbols
+tff(head_nil,axiom,
+	! [A: $tType] : ( head(A,nil(A)) = none(A) )).
+
+tff(head_cons,axiom,
+	! [A: $tType,X : A,XS : list(A)] : ( head(A,cons(A,X,XS)) = some(A,X) ) ).
+
+%----With integers
+tff(solve_this,conjecture,
+	  head($int,cons($int,1,cons($int,2,cons($int,3,nil($int))))) = some($int,1) ).

src/Typing/wf_rules.go → src/AST/form-list.go

@@ -30,38 +30,43 @@
 * knowledge of the CeCILL license and that you accept its terms.
 **/
 
-package Typing
-
 /**
- * This file defines the WF rules.
- **/
+* This file contains utility functions for list of formulas
+**/
 
-/* WF1 rule first empties the variables, and then the types. */
-func applyWF2(state Sequent, root *ProofTree, fatherChan chan Reconstruct) Reconstruct {
-	root.appliedRule = "WF_2"
+package AST
 
-	// Try to empty vars first
-	if len(state.localContext.vars) > 0 {
-		// Launch child on the type of the first var
-		var_, newLocalContext := state.localContext.popVar()
-		child := []Sequent{
-			{
-				localContext:  newLocalContext,
-				globalContext: state.globalContext,
-				consequence:   Consequence{a: var_.GetTypeApp()},
-			},
-		}
-		return launchChildren(child, root, fatherChan)
+import (
+	"github.com/GoelandProver/Goeland/Lib"
+)
+
+// ex-name: ReplaceMetaByTerm
+func LsSubstByTerm(formulas Lib.List[Form], meta Meta, term Term) Lib.List[Form] {
+	for i, f := range formulas.GetSlice() {
+		formulas.Upd(i, f.ReplaceMetaByTerm(meta, term))
 	}
+	return formulas
+}
 
-	// Then, if vars is not empty, empty the types
-	_, newLocalContext := state.localContext.popTypeVar()
-	child := []Sequent{
-		{
-			localContext:  newLocalContext,
-			globalContext: state.globalContext,
-			consequence:   Consequence{a: metaType},
-		},
+// ex-name: ToMappableStringSlice
+func LsToMappableStringSlice(formulas Lib.List[Form]) []MappableString {
+	forms := []MappableString{}
+	for _, form := range formulas.GetSlice() {
+		forms = append(forms, form.(MappableString))
 	}
-	return launchChildren(child, root, fatherChan)
+	return forms
+}
+
+func LsFlatten(formulas Lib.List[Form]) Lib.List[Form] {
+	result := Lib.NewList[Form]()
+
+	for _, form := range formulas.GetSlice() {
+		if typed, ok := form.(And); ok {
+			result.Append(LsFlatten(typed.GetChildFormulas()).GetSlice()...)
+		} else {
+			result.Append(form)
+		}
+	}
+
+	return result
 }