staged-miniKanren/tests/infer.rkt at main · namin/staged-miniKanren · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
#lang racket/base

(require racket/pretty
         "../main.rkt"
         "../test-check.rkt")

(defrel/staged/fallback (!- exp env t)
  (conde
    [(fresh (env-t)
       (symbolo exp)
       (later (== t env-t))
       (lookupo exp env env-t))]
    [(fresh (x e t-x t-e)
       (== `(lambda (,x) ,e) exp)
       (symbolo x)
       (not-in-envo 'lambda env)
       (later (== `(-> ,t-x ,t-e) t))
       (!- e `((,x . ,t-x) . ,env) t-e))]
    [(fresh (rator rand t-x)
       (== `(,rator ,rand) exp)
       (!- rator env `(-> ,t-x ,t))
       (!- rand env t-x))]))

(defrel/staged/fallback (lookupo x env t)
  (fresh (rest y v)
    (== `((,y . ,v) . ,rest) env)
    (conde
      ((== y x) (== v t))
      ((=/= y x) (lookupo x rest t)))))

(defrel/staged/fallback (not-in-envo x env)
  (conde
    ((== '() env))
    ((fresh (y v rest)
       (== `((,y . ,v) . ,rest) env)
       (=/= y x)
       (not-in-envo x rest)))))

(test
  (run 1 (t) (staged (!- '(lambda (x) (lambda (f) (f x))) '() t)))
  '((-> _.0 (-> (-> _.0 _.1) _.1))))

(test
  (run 3 (e t) (staged (!- `(lambda (x) (lambda (f) (f ,e))) '() t)))
  '((x (-> _.0 (-> (-> _.0 _.1) _.1)))
    (((lambda (_.0) _.0) (-> _.1 (-> (-> (-> _.2 _.2) _.3) _.3))) $$ (sym _.0))
    (((lambda (_.0) x) (-> _.1 (-> (-> (-> _.2 _.1) _.3) _.3)))
     $$
     (=/= ((_.0 x)))
     (sym _.0))))

(test
  (run 1 (t) (staged (!- '(lambda (x) (x x)) '() t)))
  '())

(pretty-print
 (generated-code))

(test
 (run 1 (t)
   (staged (!- '((app f) x)
               '((app . (-> (-> a b) (-> a b)))
                 (f . (-> a b))
                 (x . a))
               t)))
 '(b))

(test
  (run 3 (e t)
    (fresh (ef ex)
      (== e `((app ,ef) ,ex))
      (staged (!- e
                  '((app . (-> (-> a b) (-> a b)))
                    (f . (-> a b))
                    (x . a))
                  t))))
  '((((app f) x) b)
    (((app (app f)) x) b)
    ((((app f) ((lambda (_.0) _.0) x)) b) $$ (sym _.0))))

(pretty-print
 (generated-code))

(test
  (run 3 (e t)
    (fresh (ef)
      (== e `((app (app ,ef)) x))
      (staged (!- e
                  '((app . (-> (-> a b) (-> a b)))
                    (f . (-> a b))
                    (x . a))
                  t))))
  '((((app (app f)) x) b)
    (((app (app (app f))) x) b)
    ((((app (app (lambda (_.0) (f _.0)))) x) b) $$ (=/= ((_.0 f))) (sym _.0))))

(pretty-print
 (generated-code))

(test
  (run 3 (e t)
    (fresh (ea ef ex)
      (== e `((,ea (,ea ,ef)) ,ex))
      (staged (!- e
                  '((app . (-> (-> a b) (-> a b)))
                    (f . (-> a b))
                    (x . a))
                  t))))
  '((((app (app f)) x) b)
    ((((app (app f)) ((lambda (_.0) _.0) x)) b) $$ (sym _.0))
    ((((app (app f)) ((lambda (_.0) x) app)) b) $$ (=/= ((_.0 x))) (sym _.0))))

(pretty-print
 (generated-code))