-
Notifications
You must be signed in to change notification settings - Fork 0
/
program-fact.rkt
86 lines (77 loc) · 4.04 KB
/
program-fact.rkt
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
#lang racket
(require (only-in plai define-type test print-only-errors))
(require "definitions.rkt")
(require "chspans.rkt")
(require "complex-pred-to-facts.rkt")
(define (program-to-structure program scope [outer-let-chs #f])
(define (get-proper-range original-chs)
(if outer-let-chs
outer-let-chs
original-chs))
(match program
[(ifB tst thn els chs)
(define tst-result (complex-pred-to-facts tst scope))
(if tst-result
(let ([thn-result (program-to-structure thn scope)]
[els-result (program-to-structure els scope)])
(ifP tst-result thn-result els-result (get-proper-range chs)))
(program-to-structure tst scope))]
[(errorB chs)
(errorP (get-proper-range chs))]
[(letB bindings body chs)
(if (charset-empty? chs)
(program-to-structure body (put-bindings-to-scope bindings scope))
(program-to-structure body (put-bindings-to-scope bindings scope) (get-proper-range chs)))]
[_ (codeP (get-proper-range (BasicExpand-cs program)))]))
(define (structure-to-fact structure)
(define (structure-to-fact-inner structure)
(match structure
[(codeP cs) (nonef)]
[(errorP cs) (anyf)]
[(ifP tst thn els cs) (iff
tst
(structure-to-fact-inner thn)
(structure-to-fact-inner els))]))
(notf (structure-to-fact-inner structure)))
(provide
structure-to-fact
program-to-structure)
(module+ test
(print-only-errors)
(test (program-to-structure (ifB (appB (idB `pred1 (empty-charset)) (list (idB `arg0 (empty-charset))) (empty-charset))
(appB (idB `void (empty-charset)) (list ) (empty-charset))
(letB (list )
(errorB (empty-charset))
(empty-charset))
(empty-charset))
(hash `arg0 (func-arg)))
(ifP (predf 'pred1 'arg0 (hash 'arg0 (func-arg))) (codeP (empty-charset)) (errorP (empty-charset)) (empty-charset)))
(test (program-to-structure (ifB
(ifB
(appB (idB 'positive? (empty-charset)) (list (idB 'arg0 (empty-charset))) (empty-charset))
(appB (idB 'exact-integer? (empty-charset)) (list (idB 'arg0 (empty-charset))) (empty-charset))
(bool #f (empty-charset))
(empty-charset))
(appB (idB 'void (empty-charset)) '() (empty-charset))
(letB '() (errorB (empty-charset)) (empty-charset))
(empty-charset))
(hash 'arg0 (func-arg)))
(ifP
(iff (predf 'positive? 'arg0 (hash 'arg0 (func-arg))) (predf 'exact-integer? 'arg0 (hash 'arg0 (func-arg))) (nonef))
(codeP (empty-charset))
(errorP (empty-charset))
(empty-charset)))
(test (program-to-structure (ifB
(ifB (appB (idB 'exact? (empty-charset)) (list (idB 'arg0 (empty-charset))) (empty-charset))
(letB '() (errorB (empty-charset)) (empty-charset))
(appB (idB 'void (empty-charset)) '() (empty-charset))
(empty-charset))
(letB '() (errorB (empty-charset)) (empty-charset))
(appB (idB 'void (empty-charset)) '() (empty-charset))
(empty-charset) )
(hash 'arg0 (func-arg)))
(ifP (predf 'exact? 'arg0 (hash 'arg0 (func-arg))) (errorP (empty-charset)) (codeP (empty-charset)) (empty-charset)))
(test (structure-to-fact
(ifP (predf 'exact? 'arg0 '#hash()) (errorP (empty-charset)) (codeP (empty-charset)) (empty-charset)))
(notf (iff (predf 'exact? 'arg0 '#hash()) (anyf) (nonef))))
)