Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

rackety

  • Loading branch information...
commit 444f4ff7e3e5a412605948f7985321afb0748f08 1 parent 041477b
Jay McCarthy jeapostrophe authored

Showing 2 changed files with 278 additions and 0 deletions. Show diff stats Hide diff stats

  1. +274 0 basic.rkt
  2. +4 0 basic.v
274 basic.rkt
... ... @@ -0,0 +1,274 @@
  1 +#lang racket/base
  2 +(require racket/match
  3 + racket/list)
  4 +
  5 +(struct A_Linear (f) #:transparent)
  6 +(struct A_Intuit (f) #:transparent)
  7 +
  8 +(struct F_Atom (a) #:transparent)
  9 +(struct F_Impl (f g) #:transparent)
  10 +(struct F_Both (f g) #:transparent)
  11 +(struct F_Choo (f g) #:transparent)
  12 +(struct F_Eith (f g) #:transparent)
  13 +(struct F_OfCo (f) #:transparent)
  14 +
  15 +(define all_P_L_Id
  16 + (lambda (a)
  17 + (match a
  18 + ((list) (list))
  19 + ((cons a0 l)
  20 + (match l
  21 + ((list)
  22 + (match a0
  23 + ((A_Linear f) (cons f (list)))
  24 + ((A_Intuit f) (list))))
  25 + ((cons y l0) (list)))))))
  26 +
  27 +(define all_splits
  28 + (lambda (a) (cons (cons (list) a)
  29 + (match a
  30 + ((list) (list))
  31 + ((cons f t)
  32 + (map (lambda (p)
  33 + (match p
  34 + ((cons x y) (cons (cons f x) y)))) (all_splits t)))))))
  35 +
  36 +(define all_P_OfCoEl
  37 + (lambda (a)
  38 + (append-map (lambda (gamma_delta)
  39 + (match gamma_delta
  40 + ((cons gamma delta)
  41 + (let ((gamma_proves (all gamma)))
  42 + (append-map (lambda (f)
  43 + (match f
  44 + ((F_Atom a0) (list))
  45 + ((F_Impl f0 f1) (list))
  46 + ((F_Both f0 f1) (list))
  47 + ((F_Choo f0 f1) (list))
  48 + ((F_Eith f0 f1) (list))
  49 + ((F_OfCo f_a)
  50 + (all (append delta (cons (A_Intuit f_a) (list)))))))
  51 + gamma_proves))))) (all_splits a))))
  52 +
  53 +(define all_P_I_Id
  54 + (lambda (a)
  55 + (match a
  56 + ((list) (list))
  57 + ((cons a0 l)
  58 + (match l
  59 + ((list)
  60 + (match a0
  61 + ((A_Linear f) (list))
  62 + ((A_Intuit f) (cons f (list)))))
  63 + ((cons y l0) (list)))))))
  64 +
  65 +(define all_P_Exc
  66 + (lambda (a)
  67 + (append-map (lambda (gamma_delta)
  68 + (match gamma_delta
  69 + ((cons gamma delta) (all (append delta gamma))))) (all_splits a))))
  70 +
  71 +(define all_P_Contract
  72 + (lambda (a)
  73 + (match a
  74 + ((list) (list))
  75 + ((cons a0 t)
  76 + (match a0
  77 + ((A_Linear f) (list))
  78 + ((A_Intuit f_a)
  79 + (all (cons (A_Intuit f_a) (cons (A_Intuit f_a) t)))))))))
  80 +
  81 +(define all_P_Weaken
  82 + (lambda (a)
  83 + (match a
  84 + ((list) (list))
  85 + ((cons a0 t)
  86 + (match a0
  87 + ((A_Linear f) (list))
  88 + ((A_Intuit f_a) (all t)))))))
  89 +
  90 +(define (all_intuit l)
  91 + (andmap (lambda (a)
  92 + (match a
  93 + ((A_Linear f) #f)
  94 + ((A_Intuit f) #t)))
  95 + l))
  96 +
  97 +(define all_P_OfCoId
  98 + (lambda (a)
  99 + (let ((gamma_proves
  100 + (match (all_intuit a)
  101 + (#t (all a))
  102 + (#f (list)))))
  103 + (append-map (lambda (f) (cons (F_OfCo f) (list))) gamma_proves))))
  104 +
  105 +(define all_P_ImplEl
  106 + (lambda (a)
  107 + (append-map (lambda (gamma_delta)
  108 + (match gamma_delta
  109 + ((cons gamma delta)
  110 + (let ((gamma_proves (all gamma)))
  111 + (let ((delta_proves (all delta)))
  112 + (append-map (lambda (fd)
  113 + (append-map (lambda (fg)
  114 + (match fg
  115 + ((F_Atom a0) (list))
  116 + ((F_Impl f_a f_b)
  117 + (match (equal? fd f_a)
  118 + (#t (cons f_b (list)))
  119 + (#f (list))))
  120 + ((F_Both f f0) (list))
  121 + ((F_Choo f f0) (list))
  122 + ((F_Eith f f0) (list))
  123 + ((F_OfCo f) (list)))) gamma_proves)) delta_proves))))))
  124 + (all_splits a))))
  125 +
  126 +(define all_P_BothId
  127 + (lambda (a)
  128 + (append-map (lambda (gamma_delta)
  129 + (match gamma_delta
  130 + ((cons gamma delta)
  131 + (let ((gamma_proves (all gamma)))
  132 + (let ((delta_proves (all delta)))
  133 + (append-map (lambda (fd)
  134 + (append-map (lambda (fg) (cons (F_Both fg fd) (list)))
  135 + gamma_proves)) delta_proves)))))) (all_splits a))))
  136 +
  137 +(define all_P_BothEl
  138 + (lambda (a)
  139 + (append-map (lambda (gamma_delta)
  140 + (match gamma_delta
  141 + ((cons gamma delta)
  142 + (let ((gamma_proves (all gamma)))
  143 + (append-map (lambda (f)
  144 + (match f
  145 + ((F_Atom a0) (list))
  146 + ((F_Impl f0 f1) (list))
  147 + ((F_Both f_a f_b)
  148 + (all
  149 + (append delta (cons (A_Linear f_a) (cons (A_Linear
  150 + f_b) (list))))))
  151 + ((F_Choo f0 f1) (list))
  152 + ((F_Eith f0 f1) (list))
  153 + ((F_OfCo f0) (list)))) gamma_proves))))) (all_splits a))))
  154 +
  155 +(define all_P_ChooId
  156 + (lambda (a)
  157 + (let ((gamma_proves (all a)))
  158 + (append-map (lambda (f_a)
  159 + (append-map (lambda (f_b) (cons (F_Choo f_a f_b) (list)))
  160 + gamma_proves)) gamma_proves))))
  161 +
  162 +(define all_P_ChooEl1
  163 + (lambda (a)
  164 + (let ((gamma_proves (all a)))
  165 + (append-map (lambda (fChoo)
  166 + (match fChoo
  167 + ((F_Atom a0) (list))
  168 + ((F_Impl f f0) (list))
  169 + ((F_Both f f0) (list))
  170 + ((F_Choo f_a f_b) (cons f_a (list)))
  171 + ((F_Eith f f0) (list))
  172 + ((F_OfCo f) (list)))) gamma_proves))))
  173 +
  174 +(define all_P_ChooEl2
  175 + (lambda (a)
  176 + (let ((gamma_proves (all a)))
  177 + (append-map (lambda (fChoo)
  178 + (match fChoo
  179 + ((F_Atom a0) (list))
  180 + ((F_Impl f f0) (list))
  181 + ((F_Both f f0) (list))
  182 + ((F_Choo f_a f_b) (cons f_b (list)))
  183 + ((F_Eith f f0) (list))
  184 + ((F_OfCo f) (list)))) gamma_proves))))
  185 +
  186 +(define all_P_EithEl
  187 + (lambda (a)
  188 + (append-map (lambda (gamma_delta)
  189 + (match gamma_delta
  190 + ((cons gamma delta)
  191 + (let ((gamma_proves (all gamma)))
  192 + (append-map (lambda (f)
  193 + (match f
  194 + ((F_Atom a0) (list))
  195 + ((F_Impl f0 f1) (list))
  196 + ((F_Both f0 f1) (list))
  197 + ((F_Choo f0 f1) (list))
  198 + ((F_Eith f_a f_b)
  199 + (let ((delta_a_proves
  200 + (all (append delta (cons (A_Linear f_a) (list))))))
  201 + (let ((delta_b_proves
  202 + (all (append delta (cons (A_Linear f_b) (list))))))
  203 + (append-map (lambda (f_c1)
  204 + (append-map (lambda (f_c2)
  205 + (match (equal? f_c1 f_c2)
  206 + (#t (cons f_c1 (list)))
  207 + (#f (list)))) delta_b_proves))
  208 + delta_a_proves))))
  209 + ((F_OfCo f0) (list)))) gamma_proves))))) (all_splits a))))
  210 +
  211 +(define all-core
  212 + (lambda (a)
  213 + (append (all_P_L_Id a)
  214 + (append (all_P_I_Id a)
  215 + (append (all_P_Exc a)
  216 + (append (all_P_Contract a)
  217 + (append (all_P_Weaken a)
  218 + (append (all_P_OfCoId a)
  219 + (append (all_P_OfCoEl a)
  220 + (append (all_P_ImplEl a)
  221 + (append (all_P_BothId a)
  222 + (append (all_P_BothEl a)
  223 + (append (all_P_ChooId a)
  224 + (append (all_P_ChooEl1 a)
  225 + (append (all_P_ChooEl2 a)
  226 + (all_P_EithEl a))))))))))))))))
  227 +
  228 +;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  229 +
  230 +(define CACHE
  231 + (make-hash))
  232 +(define (all a)
  233 + (define how-deep
  234 + (length
  235 + (continuation-mark-set->list
  236 + (current-continuation-marks)
  237 + 'all)))
  238 + (cond
  239 + [(how-deep . > . LIMIT)
  240 + empty]
  241 + [(hash-has-key? CACHE a)
  242 + (or (hash-ref CACHE a)
  243 + empty)]
  244 + [else
  245 + (with-continuation-mark
  246 + 'all #t
  247 + (let ()
  248 + (hash-set! CACHE a #f)
  249 + (define r (all-core a))
  250 + (hash-set! CACHE a r)
  251 + r))]))
  252 +
  253 +(define LIMIT 5)
  254 +
  255 +(require racket/pretty
  256 + racket/file)
  257 +
  258 +(define convert
  259 + (match-lambda
  260 + [(list 'and f g)
  261 + (F_Impl
  262 + (convert f)
  263 + (convert g))]
  264 + [(list 'implies f g)
  265 + (F_Choo
  266 + (convert f)
  267 + (convert g))]
  268 + [(? string? s)
  269 + (F_Atom s)]))
  270 +
  271 +(all
  272 + (map A_Linear
  273 + (map convert
  274 + (file->list "rooms.rktd"))))
4 basic.v
@@ -934,6 +934,10 @@ Admitted.
934 934
935 935 Check theorem_prover. *)
936 936
  937 +Extraction Language Scheme.
  938 +
  939 +Extraction "basic" all_theorems.
  940 +
937 941 Extraction Language Ocaml.
938 942
939 943 Extract Constant Atom => "string".

0 comments on commit 444f4ff

Please sign in to comment.
Something went wrong with that request. Please try again.