Compilation of default rules

3 files changed, 54 insertions, 5 deletions

diff --git a/compiler/lean.scm b/compiler/lean.scm
index 18f6833..ad5e234 100644
--- a/compiler/lean.scm
+++ b/compiler/lean.scm
@@ -52,7 +52,10 @@
            #:getter       name)
   (subject #:init-keyword #:subject
            #:getter       subject)
-  ;; rules of inference for the predicate
+  ;; fallback rule, if any
+  (default #:init-keyword #:default
+           #:getter       default)
+  ;; other rules of inference for the predicate
   (facts   #:init-keyword #:facts
            #:getter       facts))
 
@@ -114,6 +117,18 @@
                     (tree-map clauses f scope breadcrumb))))
          (f scope breadcrumb inner)))))
 
+;; Compiled to ∨
+(define-class <lean-disjunction> (<lean-expression>)
+  (clauses #:init-keyword #:clauses
+           #:getter       clauses))
+
+(define-method (tree-map (form <lean-disjunction>) f scope breadcrumb)
+  (match form
+    (($ <lean-disjunction> clauses)
+     (let ((inner (with-modified-slot form 'clauses
+                    (tree-map clauses f scope breadcrumb))))
+         (f scope breadcrumb inner)))))
+
 ;; `Prop'-producing comparison between two Lean values
 (define-class <lean-compare> (<lean-expression>)
   (kind  #:init-keyword #:kind
@@ -185,11 +200,27 @@
       ('field-eqv "_eqv")
       ('set-memq  "_memq")))
   (define inductive-name (string-concatenate `(,(name x) ,suffix)))
+  (define has-default (default x))
+  (define conditional-facts
+    (filter (lambda (fact)
+              (not (equal? fact (default x))))
+            (facts x)))
 
   (with-output-to-string
     (lambda ()
       (format #t "inductive ~a (~a : Rego.Any) : Prop" inductive-name (subject x))
       (newline)
+
+      (when has-default
+        (format #t "| default : ¬ (~a) → (~a = (~a)) → ~a ~a"
+                (compile (make <lean-disjunction>        ; ¬ (~a)
+                           #:clauses (map body conditional-facts)))
+                (subject x)                              ; (~a =( ~a))
+                (compile (conclusion (default x)))
+                inductive-name                           ; → ~a ~a
+                (subject x))
+        (newline))
+
       (for-each
        (lambda (rule i)
          (match (body rule)
@@ -212,8 +243,8 @@
                      (subject x)
                      )))
          (newline))
-       (facts x)
-       (iota (length (facts x)))))))
+       conditional-facts
+       (iota (length conditional-facts))))))
 
 (define-method (compile (x <lean-compare>))
   (define symbol
@@ -270,6 +301,9 @@
 (define-method (compile (x <lean-conjunction>))
   (string-join (map (compose wrap compile) (clauses x)) " ∧ "))
 
+(define-method (compile (x <lean-disjunction>))
+  (string-join (map (compose wrap compile) (clauses x)) " ∨ "))
+
 (define-method (compile (x <lean-tuple>))
   (string-concatenate
    `("("
diff --git a/compiler/passes/emit-specification.scm b/compiler/passes/emit-specification.scm
index 6af8776..37d0aa8 100644
--- a/compiler/passes/emit-specification.scm
+++ b/compiler/passes/emit-specification.scm
@@ -55,6 +55,16 @@
                   (make <lean-conjunction> #:clauses (map compile-expr conjunction))
                   (compile-expr (first conjunction)))))))
 
+(define (find-default rules)
+  (find default-rule? rules))
+
+(define (all-but-default rules)
+  (let ((result (filter (negate default-rule?) rules)))
+    (unless (member (- (length rules) (length result)) '(0 1) )
+      (error "expected at most 1 default rule, found"
+             (- (length rules) (length result))))
+    result))
+
 (define (compile-rule-group group)
   (match group
     ((left rules ...)
@@ -65,7 +75,10 @@
        #:name (reference->string left)
        ;; TODO: Find unique name
        #:subject "v"
-       #:facts (map compile-rule rules)))))
+       #:default (if (find-default rules)
+                     (compile-rule (find-default rules))
+                     #f)
+       #:facts (map compile-rule (all-but-default rules))))))
 
 (define (emit-specification policy)
   "Emit a Lean file specifying the semantics of `policy'."
diff --git a/compiler/types.scm b/compiler/types.scm
index c093981..2e25d78 100644
--- a/compiler/types.scm
+++ b/compiler/types.scm
@@ -43,6 +43,7 @@
             scope-contains?
 
             <rule>
+            default-rule?
             head
             body
             ι-rule-body
@@ -221,7 +222,8 @@ and `identifier' is a <reference>"
 ;; The intensional database of a Rego program is defined by its rules.
 (define-class <rule> ()
   (default #:init-form #f
-           #:init-keyword #:default)
+           #:init-keyword #:default
+           #:accessor     default-rule?)
   (head    #:init-keyword #:head
            #:accessor     head)
   (body    #:init-keyword #:body