-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
5 changed files
with
934 additions
and
0 deletions.
There are no files selected for viewing
69 changes: 69 additions & 0 deletions
69
tests/baseline_compat/hyperon-mettalog_sanity/unify_true_false.metta
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,69 @@ | ||
|
||
(= (same $X $X) True) | ||
(= (eq $X $Y) | ||
(let $C (same $X $Y) (if (== $C True) True False))) | ||
|
||
(= (unif $X $Y) | ||
(unify $X $Y True False)) | ||
|
||
|
||
|
||
|
||
!(assertEqualToResult (unif (+ 1 1) ($_1 $_2 $_)) (False)) ;; eager eval? | ||
!(assertEqualToResult (unif (+ 1 1) 2) (True)) ;; eager eval on plus? | ||
!(assertEqualToResult (unif (+ 1 1) (+ 1 1)) (True)) | ||
!(assertEqualToResult (unif (+ 1 1) (+ 0 2)) (True)) ;; eager eval? | ||
!(assertEqualToResult (unif (+ 1 1) (+ $a $b)) (False)) ;; eager eval? | ||
!(assertEqualToResult (unif $x $x) (True)) | ||
!(assertEqualToResult (unif $x $y) (True)) ;; identity? | ||
!(assertEqualToResult (unif (+ 1 1) $x) (True)) ;; eager eval? | ||
!(assertEqualToResult (unif (+ 1 2 3) (+ 1 2 3)) (True)) ;; Arity error? | ||
!(assertEqualToResult (unif (+ 1 2 3) (+ 1 $two 3)) (True)) | ||
!(assertEqualToResult (unif (+ 1 2) (+ 1 $two)) (False)) ;; overly eager eval? | ||
|
||
!(assertEqualToResult (same (+ 1 1) ($_1 $_2 $_)) ((same 2 ($_1 $_2 $_)))) | ||
!(assertEqualToResult (same (+ 1 1) 2) (True)) | ||
!(assertEqualToResult (same (+ 1 1) (+ 1 1)) (True)) | ||
!(assertEqualToResult (same (+ 1 1) (+ 0 2)) (True)) | ||
!(assertEqualToResult (same (+ 1 2 3) (+ 1 2 3)) (True)) | ||
!(assertEqualToResult (same (+ 1 1) (+ $a $b)) ((same 2 (+ $a $b)))) | ||
!(assertEqualToResult (same $x $y) (True)) | ||
!(assertEqualToResult (same $x $x) (True)) | ||
!(assertEqualToResult (same (+ 1 1) $x) (True)) | ||
!(assertEqualToResult (same (+ 1 2 3) (+ 1 2 3)) (True)) | ||
!(assertEqualToResult (same (+ 1 2 3) (+ 1 $two 3)) (True)) | ||
!(assertEqualToResult (same (+ 1 2) (+ 1 $two)) ((same 3 (+ 1 $two)))) | ||
|
||
!(assertEqualToResult (eq (+ 1 1) ($_1 $_2 $_)) (False)) | ||
!(assertEqualToResult (eq (+ 1 1) 2) (True)) | ||
!(assertEqualToResult (eq (+ 1 1) (+ 1 1)) (True)) | ||
!(assertEqualToResult (eq (+ 1 1) (+ 0 2)) (True)) | ||
!(assertEqualToResult (eq (+ 1 2 3) (+ 1 2 3)) (True)) | ||
!(assertEqualToResult (eq (+ 1 1) (+ $a $b)) (False)) | ||
!(assertEqualToResult (eq $x $y) (True)) | ||
!(assertEqualToResult (eq $x $x) (True)) | ||
!(assertEqualToResult (eq (+ 1 1) $x) (True)) | ||
!(assertEqualToResult (eq (+ 1 2 3) (+ 1 2 3)) (True)) | ||
!(assertEqualToResult (eq (+ 1 2 3) (+ 1 $two 3)) (True)) | ||
!(assertEqualToResult (eq (+ 1 2) (+ 1 $two)) (False)) | ||
|
||
|
||
|
||
|
||
|
||
(unify-atom (-> Atom Atom)) | ||
(= (unify-atom $X $Y) | ||
(unify $X $Y (quote (u $X $Y)) False)) | ||
|
||
!(assertEqualToResult (unify-atom (+ 1 1) ($_1 $_2 $_)) (False)) ;; eager eval? | ||
!(assertEqualToResult (unify-atom (+ 1 1) 2) ((quote (u 2 2)))) ;; eager eval? | ||
!(assertEqualToResult (unify-atom (+ 1 1) (+ 1 1)) ((quote (u 2 2)))) | ||
!(assertEqualToResult (unify-atom (+ 1 1) (+ 0 2)) ((quote (u 2 2)))) ;; eager eval? | ||
!(assertEqualToResult (unify-atom (+ 1 1) (+ $a $b)) (False)) ;; eager eval? | ||
!(assertEqualToResult (unify-atom $x $x) ((quote (u $x $x)))) | ||
!(assertEqualToResult (unify-atom $x $y) ((quote (u $y $y)))) ;; identity? | ||
!(assertEqualToResult (unify-atom (+ 1 1) $x) ((quote (u 2 2)))) ;; eager eval? | ||
!(assertEqualToResult (unify-atom (+ 1 2 3) (+ 1 2 3)) ((quote (u (Error (+ 1 2 3) IncorrectNumberOfArguments) (Error (+ 1 2 3) IncorrectNumberOfArguments))))) ;; Arity error? | ||
!(assertEqualToResult (unify-atom (+ 1 2 3) (+ 1 $two 3)) ((quote (u (Error (+ 1 2 3) IncorrectNumberOfArguments) (Error (+ 1 2 3) IncorrectNumberOfArguments))))) | ||
!(assertEqualToResult (unify-atom (+ 1 2) (+ 1 $two)) (False)) ;; overly eager eval? | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,81 @@ | ||
;!(pragma! compile full) | ||
|
||
(: is-variable (-> Atom Bool)) | ||
(= (is-variable $x) (== (get-metatype $x) Variable)) | ||
|
||
(: lazy-or (-> Bool Atom Bool)) | ||
(= (lazy-or False $x) $x) | ||
(= (lazy-or True $x) True) | ||
|
||
(: is-expression (-> Atom Bool)) | ||
(= (is-expression $x) (== (get-metatype $x) Expression)) | ||
|
||
(: is-ground (-> Atom Bool)) | ||
(= (is-ground $x) (if (is-variable $x) | ||
False | ||
(if (== () $x) True | ||
(if (is-expression $x) | ||
(and (let $head (car-atom $x) (is-ground $head)) | ||
(let $tail (cdr-atom $x) (is-ground $tail))) | ||
True)))) | ||
|
||
|
||
;; KB | ||
!(bind! &kb (new-space)) | ||
|
||
!(add-atom &kb (: axiom (nums 2 3))) | ||
|
||
!(add-atom &kb (: rule1 | ||
(-> (nums $x $y) | ||
(rule1output $x $y)))) | ||
|
||
!(add-atom &kb | ||
(: rule | ||
(-> (rule1output $x $y) | ||
(-> (lt $x $y) | ||
(less $x $y))))) | ||
|
||
; !(add-atom &kb | ||
; (: rule | ||
; (-> (lt $x $y) | ||
; (-> (rule1output $x $y) | ||
; (less $x $y))))) | ||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
;; DTL Backward chaining Curried ;; | ||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
|
||
|
||
(: bc (-> $a hyperon::space::DynSpace Nat $a)) | ||
;; Base case | ||
(= (bc (: $prf $ccln) $space $_1) (match $space (: $prf $ccln) (: $prf $ccln))) | ||
;; if conclusion equals (lt $X $Y), then return (: CPU (lt $X $Y)) | ||
;; if $x and $Y are fully grounded and (< $X $Y) | ||
(= (bc (: CPU (lt $X $Y)) $space $_2) | ||
(if (and (and (is-ground $X) (is-ground $Y)) (< $X $Y)) | ||
(: CPU (lt $X $Y)) | ||
(empty))) | ||
|
||
;; Recursive step | ||
(= (bc (: ($prfabs $prfarg) $ccln) $space (S $k)) | ||
(let* (((: $prfabs (-> $prms $ccln)) | ||
(bc (: $prfabs (-> $prms $ccln)) $space $k)) | ||
((: $prfarg $prms) | ||
(bc (: $prfarg $prms) $space $k))) | ||
|
||
(: ($prfabs $prfarg) $ccln))) | ||
|
||
;!(pragma! e trace) | ||
;!(pragma! e-args debug) | ||
|
||
; Test | ||
!(bc (: CPU (lt 2 3)) &kb Z) | ||
!(bc (: CPU (lt 4 3)) &kb Z) | ||
|
||
;!(pragma! eval debug) | ||
|
||
;! ( rtrace! (bc (: $prf (less $x $y)) (S (S (S Z))))) | ||
|
||
!(bc (: $prf (less $x $y)) &kb (S (S (S Z)))) | ||
|
||
|
140 changes: 140 additions & 0 deletions
140
tests/direct_comp/important/fish_riddle_1_no_states.metta
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,140 @@ | ||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
;; Backward chaining logic | ||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
|
||
;; Interface for backward chaining (quotes the arguement) | ||
(: backward-chain (-> Atom Atom Atom Atom Atom)) | ||
(= (backward-chain $info $goal $kb $rb) | ||
(backward-chain-q $info (quote $goal) $kb $rb)) | ||
|
||
;; Handle specific cases during backward chaining | ||
(: backward-chain-q (-> Atom Atom Atom Atom Atom)) | ||
(= (backward-chain-q $info (quote $goal) $kb $rb) | ||
(case (quote $goal) ( | ||
((quote (is $a $b)) (let $a $b (quote $goal))) ; Assignment | ||
((quote (bool $expr)) (if $expr (quote $goal) (empty))) ; Boolean evaluation | ||
((quote (eval= $a $expr)) (let $a $expr (quote $goal))) ; Expression evaluation | ||
((quote (nonvar $var)) (if (== Variable (get-metatype $var)) (empty) (quote $goal))) ; Non-variable check | ||
((quote (var $var)) (if (== Variable (get-metatype $var)) (quote $goal) (empty))) ; Variable check | ||
((quote (true)) (quote $goal)) ; Always succeeds | ||
((quote (fail)) (empty)) ; Always fails | ||
((quote (cut $signal)) (if (equalz $info $signal) (quote $goal) (quote $goal))) ; Cut operator for pruning | ||
((quote (naf $expr)) (if (has-match $kb $expr) (empty) (quote $goal))) ; Negation as failure | ||
((quote (qnaf $expr)) (let (Failed $_1) (backward-chain $info2 $expr $kb $rb) (quote $goal))) ; Negation as failure at query level | ||
($_2 (backward-chain-q2 $info (quote $goal) $kb $rb)) ; Match against knowledge base | ||
))) | ||
|
||
(= (backward-chain-q2 $info (quote $goal) $kb $rb) | ||
(match $kb $goal (quote $goal))) | ||
;; Recursive case for backward chaining | ||
(= (backward-chain-q2 $old_info (quote $goal) $kb $rb) | ||
(function | ||
(return ;; if $info is bound that means a clause has called a cut (thus we return empty) | ||
(if (== Variable (get-metatype $old_info)) | ||
(let $r (match $rb ($goal :- $body) | ||
(match-body $info $body $kb $rb $goal)) | ||
(if (== Variable (get-metatype $info)) ;; if not cut | ||
$r ;; then return normal | ||
(return $r))) ;; else return early | ||
(empty))))) | ||
|
||
|
||
;; Match predicate: checks if a goal has at least one match in a space | ||
;; This is less efficient, as it processes the entire space to find matches | ||
(: has-match (-> Atom Atom Bool)) | ||
(= (has-match $space $g) | ||
(let $m (collapse (match $space $g True)) ; Attempt to match $g in $space | ||
(if (== $m ()) ; If no match is found | ||
False ; Return False | ||
True ; Otherwise, return True | ||
) | ||
) | ||
) | ||
|
||
;; Predicate to check if a function definition exists in a given space | ||
(= (has-fundef $space $g) | ||
(let $m (collapse (match $space (= $g $_1) True)) ; Match $g as a function in $space | ||
(if (== $m ()) ; If no match is found | ||
False ; Return False | ||
True ; Otherwise, return True | ||
) | ||
) | ||
) | ||
|
||
;; Chain through each element in the body and return the goal | ||
(: match-body (-> Atom Atom Atom Atom Atom Atom)) | ||
(= (match-body $info $body $kb $rb $goal) | ||
(if (== $body ()) | ||
(quote $goal) ; Base case: no more elements to match | ||
(let* ( | ||
(($cur $rest) (decons-atom $body)) ; Deconstruct body | ||
($debugging False) ;; Print debug or not | ||
($bugcheck False) ;; Catch a bug where we dont return the quoted goals | ||
(() (if $debugging (println! (quote (IN (cur= $cur) (goal= $goal)))) ())) ; Debugging: log input | ||
($_12 (if $bugcheck | ||
(let* (($retVal (backward-chain $info $cur $kb $rb)) ; Recursive chaining | ||
($m (collapse (equalz (quote $cur) $retVal))) ; Check match | ||
(() (if (== $m ()) (println! (quote (BAD!!!!!!!! (cur= $cur) (retVal= $retVal))) ()))) | ||
) ()) ())) | ||
((quote $cur) (backward-chain $info $cur $kb $rb)) ; Recursive chaining | ||
(() (if $debugging (println! (quote (OUT (cur= $cur) (goal= $goal)))) ())) ; Debugging: log output | ||
) | ||
(match-body $info $rest $kb $rb $goal) ; Continue matching | ||
) | ||
) | ||
) | ||
|
||
|
||
;; Predicate for general atom equality | ||
(: equalz (-> Atom Atom Bool)) ; Compares two atoms | ||
(= (equalz $A $A) True) ; Atoms are equal if they are identical | ||
|
||
;!(equalz $a (+ 1 1)) | ||
|
||
;; Query execution logic | ||
(: query (-> Atom Atom Atom)) | ||
(= (query $kb $goal) | ||
(let $m (collapse (backward-chain $info $goal $kb $kb)) | ||
(if (== $m ()) (Failed (quote $goal)) (Succeed $m))) | ||
) | ||
|
||
|
||
;; Predicate: Check if an element is a member of a list | ||
(member $Elem ($Cons $Elem $_1)) ; Base case: element found | ||
((member $Elem ($Cons $_1 $Tail)) :- | ||
((member $Elem $Tail))) ; Recursive case: continue checking | ||
|
||
;; Predicate to check equality of two values | ||
(same $x $x) | ||
|
||
((because $color house keeps $other the $nationality is the $type owner) :- | ||
((same $Houses | ||
(Cons ( 1 $_1 $_2 $_3 $_4 $_5) ; First house | ||
(Cons ( 2 $_6 $_7 $_8 $_9 $_10) ; Second house | ||
$Open))) | ||
|
||
(same $Open Nil) | ||
|
||
; Clue 1: The Norwegian lives in the first house | ||
(member ( 1 norwegian $_11 $_12 $_13 $_14) $Houses) | ||
; Clue 2: The Brit lives in the red house | ||
(member ( $_15 brit red $_16 $_17 $_18) $Houses) | ||
; Clue 3: The owner of the blue house drinks tea | ||
(member ( $_19 $_20 blue tea $_21 $_22) $Houses) | ||
; Clue 4: The owner of the red house keeps $other | ||
(member ( $_23 $_24 $color $_25 $other $_26) $Houses) | ||
; Clue 5: The owner of the tea-drinking house smokes Prince | ||
(member ( $_27 $_28 $_29 tea $_30 prince) $Houses) | ||
; Determine the $nationality of owns the $type | ||
(member ( $_31 $nationality $_32 $_33 $type $_34) $Houses))) | ||
|
||
;;;;;;;;;;;;;;;;;; | ||
;; TEST Queries ;; | ||
;;;;;;;;;;;;;;;;;; | ||
|
||
!(query &self (because red house keeps dogs the $norwegian is the fish owner)) | ||
|
||
!(query &self (because blue house keeps dogs the $brit is the fish owner)) | ||
|
||
!(query &self (because red house keeps cats the $norwegian is the fish owner)) | ||
|
Oops, something went wrong.