synthesis/util.rkt at master · Quetzal-RDF/synthesis · 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
#lang rosette

(define/match (ite? e)
    [((expression op child ...)) (or (string=? "ite" (~v op)) (string=? "ite*" (~v op)))]
    [(_) #f])

(define/match (expression? e)
    [((expression op child ...)) #t]
    [(_) #f])

(define-syntax for/all/*
  (syntax-rules ()
    ((_ ([val expr]) body ...)
     (letrec ((push
               (lambda (val)
                 (if (or (union? val) (ite? val))
                     (for/all ([e val])
                       (push e))
                     (begin
                       body
                       ...)))))
       (push expr)))))

(define/match (ite-cases e)
    [((expression op child ...))
     (if (or (string=? "ite" (~v op)) (string=? "ite*" (~v op)))
         (cdr child)
         '())]
    [(_) '()])

(define/match (ite-pred e)
    [((expression op child ...))
     (if (string=? "⊢" (~v op))
         (car child)
         '())]
    [(_) '()])

(define/match (ite-case e)
    [((expression op child ...))
     (if (string=? "⊢" (~v op))
         (cadr child)
         '())]
    [(_) '()])

(define/match (ite-preds e)
    [((expression op child ...))
     (cond ((string=? "ite" (~v op))
            (let ((p (first child)))
              (append
               (let ((l (ite-preds (second child))))
                 (if (null? l) (list p) (map (lambda (lp) (and p lp)) l)))
               (let ((r (ite-preds (third child))))
                 (if (null? r) (list (not p)) (map (lambda (rp) (and (not p) rp)) r))))))
           ((string=? "ite*" (~v op))
            (apply append
                   (map (lambda (c)
                          (let ((ps (ite-preds (second child))))
                            (if (null? ps)
                                (list (ite-pred c))
                                (map (lambda (p) (and (ite-pred c) p))
                                     (ite-preds (ite-case c))))))
                        child)))
           (#t (apply append (map ite-preds child))))]
    [(_) '()])

(define (get-cases x)
  (ite-preds (for/all ([z x #:exhaustive]) z)))

(define (constraints vars e)
  (remove '()
    (match e
      [(expression op child ...)
       (let ((my-vars (set-intersect child vars)))
         (if (and (= (length child) 2) (= (length (set-intersect child vars)) 1))
             (list (cons op child))
             (apply append (map (lambda (c) (constraints vars c)) child))))]
      [_ (list)])))

(provide ite? for/all/* get-cases ite-preds)