Skip to content

Commit

Permalink
CallsVSpace=True
Browse files Browse the repository at this point in the history
  • Loading branch information
@TeamSPoon
TeamSPoon committed Nov 19, 2023
1 parent 41da1bc commit 130152e
Show file tree
Hide file tree
Showing 17 changed files with 524 additions and 368 deletions.
2 changes: 1 addition & 1 deletion 2-VSpaceTest.metta
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
!(extend-py! metta_learner)
!(extend-py! metta_vspace/metta_learner)

;! metta_vspace ; hyperon.runner.MeTTa object (`metta_vspace` is registered 'manually' now)
;! metta_learner ; just a symbol, because `metta_learner` extension doesn''t 'register itself', but it could be possible to automate this
Expand Down
5 changes: 5 additions & 0 deletions 7-FlybaseResults.metta
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@



!(extend-py! metta_vspace/metta_learner)

2 changes: 2 additions & 0 deletions 8-FlybaseQuestions.metta
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

!(extend-py! metta_vspace.metta_learner)
24 changes: 17 additions & 7 deletions examples/compat/dependent-types/DeductionDTLTest.metta
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,22 @@
;; ;; TODO: fix the following
;; !(assertEqual (record synthesize ((: $proof (≞ (→ P R) (STV $s $c))) kb rb (S Z))) (: (Deduction Pm Qm Rm PQm QRm) (≞ (→ P R) (STV 0.8 0.1))))

!(assertEqualToResult (record synthesize ((: $proof (≞ (→ P R) (STV $s $c))) kb rb (S Z)))
((⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P P) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P P) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ P R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ P R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm Pm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.5) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.5 $QRs_C35_2959))) (- 1 0.5)))) (if (< 0.1 (if (< 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z))
(: (Deduction Pm Qm Rm PQm QRm) (≞ (→ P R) (STV 0.8 0.1))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P R) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P R) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ R R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ R R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm Rm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.7) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.7 $QRs_C35_2959))) (- 1 0.7)))) (if (< 0.1 (if (< 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P (→ P Q)) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P (→ P Q)) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ (→ P Q) R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ (→ P Q) R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm PQm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.8) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.8 $QRs_C35_2959))) (- 1 0.8)))) (if (< 0.1 (if (< 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P (→ Q R)) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P (→ Q R)) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ (→ Q R) R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ (→ Q R) R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm QRm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.9) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.9 $QRs_C35_2959))) (- 1 0.9)))) (if (< 0.1 (if (< 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))))
!(assertEqualToResult
(record synthesize
((: $proof
(≞ (→ P R) (STV $s $c)))
kb rb (S Z)))
((⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z))

(let* (((: $proof4_C35_2952 (≞ (→ P P)
(STV $PQs_C35_2958 $PQc_C35_2963)))
(synthesize (: $proof4_C35_2952 (≞ (→ P P) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z))
((: $proof5_C35_2953 (≞ (→ P R) (STV $QRs_C35_2959 $QRc_C35_2964)))
(synthesize (: $proof5_C35_2953 (≞ (→ P R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm Pm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.5) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.5 $QRs_C35_2959))) (- 1 0.5)))) (if (< 0.1 (if (< 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.1 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z))
(: (Deduction Pm Qm Rm PQm QRm) (≞ (→ P R) (STV 0.8 0.1))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P R) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P R) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ R R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ R R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm Rm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.7) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.7 $QRs_C35_2959))) (- 1 0.7)))) (if (< 0.1 (if (< 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.3 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P (→ P Q)) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P (→ P Q)) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ (→ P Q) R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ (→ P Q) R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm PQm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.8) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.8 $QRs_C35_2959))) (- 1 0.8)))) (if (< 0.1 (if (< 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.4 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))
(⊷ synthesize ((: $proof (≞ (→ P R) $tv)) kb rb (S Z)) (let* (((: $proof4_C35_2952 (≞ (→ P (→ Q R)) (STV $PQs_C35_2958 $PQc_C35_2963))) (synthesize (: $proof4_C35_2952 (≞ (→ P (→ Q R)) (STV $PQs_C35_2958 $PQc_C35_2963))) kb rb Z)) ((: $proof5_C35_2953 (≞ (→ (→ Q R) R) (STV $QRs_C35_2959 $QRc_C35_2964))) (synthesize (: $proof5_C35_2953 (≞ (→ (→ Q R) R) (STV $QRs_C35_2959 $QRc_C35_2964))) kb rb Z))) (: (Deduction Pm QRm Rm $proof4_C35_2952 $proof5_C35_2953) (≞ (→ P R) (STV (if (< 0.9999 0.9) 0.7 (+ (* $PQs_C35_2958 $QRs_C35_2959) (/ (* (- 1 $PQs_C35_2958) (- 0.7 (* 0.9 $QRs_C35_2959))) (- 1 0.9)))) (if (< 0.1 (if (< 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))) 0.1 (if (< 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964))) 0.5 (if (< 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)) 0.3 (if (< $PQc_C35_2963 $QRc_C35_2964) $PQc_C35_2963 $QRc_C35_2964)))))))))))


Loading

0 comments on commit 130152e

Please sign in to comment.