Skip to content

Commit

Permalink
tests/baseline_compat/hyperon-mettalog_sanity/time_synthesize.metta
Browse files Browse the repository at this point in the history
  • Loading branch information
@TeamSPoon
TeamSPoon committed Aug 30, 2024
1 parent 8949194 commit ec6f6c1
Showing 1 changed file with 156 additions and 0 deletions.
156 changes: 156 additions & 0 deletions tests/baseline_compat/hyperon-mettalog_sanity/time_synthesize.metta
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,156 @@
;; Import modules

;; Define Nat
(: Nat Type)
(: Z Nat)
(: S (-> Nat Nat))

;; Enumerate all programs up to a given depth that are consistent with
;; the query
;; using the given axiom non-deterministic functions and rules.
;;
;; The arguments are:
;;
;; $query: an Atom under the form (: TERM TYPE). The atom may contain
;; free variables within TERM and TYPE to form various sort of
;; queries
;; such as:
;; 1. Backward chaining: (: $term (Inheritance $x Mammal))
;; 2. Forward chaining: (: ($rule $premise AXIOM) $type)
;; 3. Mixed chaining: (: ($rule $premise AXIOM) (Inheritance $x Mammal))
;; 4. Type checking: (: TERM TYPE)
;; 5. Type inference: (: TERM $type)
;;
;; $kb: a nullary function to axiom
;; to non-deterministically pick up
;; an axiom. An axiom is an Atom of the form (: TERM TYPE).
;;
;; $rb: a nullary function to rule
;; to non-deterministically pick up a
;; rule. A rule is a function mapping premises to conclusion
;;
;; where premises and conclusion have the form (: TERM TYPE).
;;
;; $depth: a Nat representing the maximum depth of the generated
;; programs.
;;
;; TODO: recurse over curried rules instead of duplicating code over
;; tuples.
(: synthesize (-> $a (-> $kt) (-> $rt) Nat $a))
;; Nullary rule (axiom)
(= (synthesize $query $kb $rb $depth)
(let $query ($kb) $query))
;; Unary rule
(= (synthesize $query $kb $rb (S $k))
(let* (((: $ructor (-> $premise $conclusion)) ($rb))
((: ($ructor $proof) $conclusion) $query)
((: $proof $premise) (synthesize (: $proof $premise) $kb $rb $k)))
$query))
;; Binary rule
(= (synthesize $query $kb $rb (S $k))
(let* (((: $ructor (-> $premise1 $premise2 $conclusion)) ($rb))
((: ($ructor $proof1 $proof2) $conclusion) $query)
((: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
((: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k)))
$query))
;; Trinary rule
(= (synthesize $query $kb $rb (S $k))
(let* (((: $ructor (-> $premise1 $premise2 $premise3 $conclusion)) ($rb))
((: ($ructor $proof1 $proof2 $proof3) $conclusion) $query)
((: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
((: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))
((: $proof3 $premise3) (synthesize (: $proof3 $premise3) $kb $rb $k)))
$query))
;; Quaternary rule
(= (synthesize $query $kb $rb (S $k))
(let* (((: $ructor (-> $premise1 $premise2 $premise3 $premise4 $conclusion)) ($rb))
((: ($ructor $proof1 $proof2 $proof3 $proof4) $conclusion) $query)
((: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
((: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))
((: $proof3 $premise3) (synthesize (: $proof3 $premise3) $kb $rb $k))
((: $proof4 $premise4) (synthesize (: $proof4 $premise4) $kb $rb $k)))
$query))
;; Quintenary rule
(= (synthesize $query $kb $rb (S $k))
(let* (((: $ructor (-> $premise1 $premise2 $premise3 $premise4 $premise5 $conclusion)) ($rb))
((: ($ructor $proof1 $proof2 $proof3 $proof4 $proof5) $conclusion) $query)
((: $proof1 $premise1) (synthesize (: $proof1 $premise1) $kb $rb $k))
((: $proof2 $premise2) (synthesize (: $proof2 $premise2) $kb $rb $k))
((: $proof3 $premise3) (synthesize (: $proof3 $premise3) $kb $rb $k))
((: $proof4 $premise4) (synthesize (: $proof4 $premise4) $kb $rb $k))
((: $proof5 $premise5) (synthesize (: $proof5 $premise5) $kb $rb $k)))
$query))

(: kb (-> Atom))
(= (kb) (: a A))
(= (kb) (: a B))
(= (kb) (: abc (Implication (AndLink A B) C)))
(= (kb) (: cde (Implication (OrLink C D) E)))

!(assertEqualToResult
(kb)
( (: abc (Implication (AndLink A B) C))
(: a A)
(: a B)
(: cde (Implication (OrLink C D) E))))


(: rb (-> Atom))
(= (rb) (: ModusPonens (-> (ImplicationLink $p $q) $p $q)))
(= (rb) (: Deduction (-> (ImplicationLink $p $q) (ImplicationLink $q $r) (ImplicationLink $p $r))))
(= (rb) (: DisjunctiveSyllogism (-> (OrLink $p $q) (NotLink $p) $q)))
(= (rb) (: DisjunctiveSyllogism (-> (OrLink $p $q) (NotLink $q) $p)))
(= (rb) (: ConjunctionIntroduction (-> $p $q (AndLink $p $q))))
(= (rb) (: ConjunctionEliminationLeft (-> (AndLink $p $q) $p)))
(= (rb) (: ConjunctionEliminationRight (-> (AndLink $p $q) $q)))
(= (rb) (: DisjunctionIntroduction (-> $p $q (OrLink $p $q))))


!(assertEqualToResult
(rb)
( (: ModusPonens (-> (ImplicationLink $p_191 $q_192) $p_191 $q_192))
(: Deduction (-> (ImplicationLink $p_193 $q_194) (ImplicationLink $q_194 $r_195) (ImplicationLink $p_193 $r_195)))
(: ConjunctionIntroduction (-> $p_196 $q_197 (AndLink $p_196 $q_197)))
(: DisjunctiveSyllogism (-> (OrLink $p_198 $q_199) (NotLink $q_199) $p_198))
(: DisjunctiveSyllogism (-> (OrLink $p_200 $q_201) (NotLink $p_200) $q_201))
(: ConjunctionEliminationLeft (-> (AndLink $p_202 $q_203) $p_202))
(: DisjunctionIntroduction (-> $p_204 $q_205 (OrLink $p_204 $q_205)))
(: ConjunctionEliminationRight (-> (AndLink $p_206 $q_207) $q_207))))


!(assertEqualToResult
(synthesize (: $term $type) kb rb (S Z))
((: abc (Implication (AndLink A B) C))
(: cde (Implication (OrLink C D) E)) (: a A) (: a B)
(: (ConjunctionIntroduction abc abc) (AndLink (Implication (AndLink A B) C) (Implication (AndLink A B) C)))
(: (ConjunctionIntroduction abc cde) (AndLink (Implication (AndLink A B) C) (Implication (OrLink C D) E)))
(: (ConjunctionIntroduction abc a) (AndLink (Implication (AndLink A B) C) A))
(: (ConjunctionIntroduction abc a) (AndLink (Implication (AndLink A B) C) B))
(: (ConjunctionIntroduction cde abc) (AndLink (Implication (OrLink C D) E) (Implication (AndLink A B) C)))
(: (ConjunctionIntroduction cde cde) (AndLink (Implication (OrLink C D) E) (Implication (OrLink C D) E)))
(: (ConjunctionIntroduction cde a) (AndLink (Implication (OrLink C D) E) A))
(: (ConjunctionIntroduction cde a) (AndLink (Implication (OrLink C D) E) B))
(: (ConjunctionIntroduction a abc) (AndLink A (Implication (AndLink A B) C)))
(: (ConjunctionIntroduction a cde) (AndLink A (Implication (OrLink C D) E)))
(: (ConjunctionIntroduction a a) (AndLink A A))
(: (ConjunctionIntroduction a a) (AndLink A B))
(: (ConjunctionIntroduction a abc) (AndLink B (Implication (AndLink A B) C)))
(: (ConjunctionIntroduction a cde) (AndLink B (Implication (OrLink C D) E)))
(: (ConjunctionIntroduction a a) (AndLink B A))
(: (ConjunctionIntroduction a a) (AndLink B B))
(: (DisjunctionIntroduction abc abc) (OrLink (Implication (AndLink A B) C) (Implication (AndLink A B) C)))
(: (DisjunctionIntroduction abc cde) (OrLink (Implication (AndLink A B) C) (Implication (OrLink C D) E)))
(: (DisjunctionIntroduction abc a) (OrLink (Implication (AndLink A B) C) A))
(: (DisjunctionIntroduction abc a) (OrLink (Implication (AndLink A B) C) B))
(: (DisjunctionIntroduction cde abc) (OrLink (Implication (OrLink C D) E) (Implication (AndLink A B) C)))
(: (DisjunctionIntroduction cde cde) (OrLink (Implication (OrLink C D) E) (Implication (OrLink C D) E)))
(: (DisjunctionIntroduction cde a) (OrLink (Implication (OrLink C D) E) A))
(: (DisjunctionIntroduction cde a) (OrLink (Implication (OrLink C D) E) B))
(: (DisjunctionIntroduction a abc) (OrLink A (Implication (AndLink A B) C)))
(: (DisjunctionIntroduction a cde) (OrLink A (Implication (OrLink C D) E)))
(: (DisjunctionIntroduction a a) (OrLink A A))
(: (DisjunctionIntroduction a a) (OrLink A B))
(: (DisjunctionIntroduction a abc) (OrLink B (Implication (AndLink A B) C)))
(: (DisjunctionIntroduction a cde) (OrLink B (Implication (OrLink C D) E)))
(: (DisjunctionIntroduction a a) (OrLink B A))
(: (DisjunctionIntroduction a a) (OrLink B B))))

0 comments on commit ec6f6c1

Please sign in to comment.