path: root/rego-proofs/compiler/types.scm

;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org>
;;;
;;; This program is free software; you can redistribute it and/or
;;; modify it under the terms of the GNU General Public License as
;;; published by the Free Software Foundation; either version 3 of the
;;; License, or (at your option) any later version.
;;;
;;; This program is distributed in the hope that it will be useful,
;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
;;; General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with this program. If not, see
;;; <http://www.gnu.org/licenses/>.

(define-module (compiler types)
  #:use-module ((rnrs base) #:select (assert))
  #:use-module (compiler utilities)
  #:use-module (ice-9 match)
  #:use-module (lens)
  #:use-module (oop goops)
  #:use-module (srfi srfi-1)
  #:use-module (srfi srfi-26)
  #:use-module (srfi srfi-69)
  #:export (policy-map
            tree-map

            <policy>
            scope
            rules
            ι-policy-scope
            ι-policy-rules

            <scope>
            identifiers
            with-anonymous-identifiers
            add-to-scope
            originating-breadcrumb
            canonicalize
            collapse-constraints
            all-valid-identifiers
            scope-contains?
            find-local

            <local>
            inner
            constraints
            lean-name
            resolved?
            variable-ref->local

            <definition>

            <rule>
            default-rule?
            head
            body
            ι-rule-body
            inductive-name

            <head>
            name
            kind
            left
            right

            <body>
            ι-body-conjunction

            <funcall>
            args

            <for-all>

            <exists-some>

            <constant>
            scheme-value->type

            <set-literal>

            <object-literal>

            <comprehension>

            <variable-ref>

            <reference>))

(define (policy-map policy f)
  "Return POLICY where F has been applied to every form in the rules"
  (over (ι-policy-rules)
        (lambda (rule-groups)
          (map (match-lambda
                 ;; ((group-head rules ...)
                 ;;  `(,group-head
                 ;;    ,@(map (lambda (rule i)
                 ;;             (let ((breadcrumb `(,(name (head rule)) ,i)))
                 ;;               (tree-map rule f (scope policy) breadcrumb)))
                 ;;           rules
                 ;;           (iota (length rules)))))
                 (($ <definition> kind left right default rules)
                  (let ((collective-rules `(,default ,@rules)))
                    (make <definition>
                      #:kind    kind
                      #:left    left
                      #:right   right
                      #:default (tree-map default f (scope policy) `(,left default))
                      #:rules   (map (lambda (rule i)
                                       (let ((breadcrumb `(,left ,i)))
                                         (tree-map rule f (scope policy) breadcrumb)))
                                     rules
                                     (iota (length rules)))))))
               rule-groups))
        policy))

;; `f' is called with `scope' and `breadcrumb' as auxiliary arguments.
;;
;; `scope' is a `<scope>', which gives opaque access to the variables that have
;; been defined in the policy, and any constraints we've mined thus far in the
;; compilation process. (In general, it's devoid of helpful information until
;; the `extract-identifiers' pass runs.)
;;
;; `breadcrumb' is a marker that specifies where the `form' argument exists in
;; the policy. Rego is lexically scoped, so this information is important for
;; determining which identifiers are in-scope for a particular place in the
;; program. The breadcrumb is always a list that begins with (1.) the name of
;; the current rule group and (2.) the index of the head being observed.
;; Following that is a sequence of list indices corresponding to this particular
;; path in the tree. For example:
;;
;; ("q" 0 0)
;;
;; Corresponds to the first clause in the conjunction of the first rule that
;; defines `q'.

(define-method (tree-map form f scope breadcrumb)
  form)

(define-method (tree-map (form <list>) f scope breadcrumb)
  (f scope breadcrumb
     (map (lambda (x i)
            (let ((breadcrumb (add-to-end breadcrumb i)))
              (f scope breadcrumb (tree-map x f scope breadcrumb))))
          form
          (iota (length form)))))



;; Type representing an individual `.rego' file
(define-class <policy> ()
  (package  #:init-value #f
            #:init-keyword #:package)
  (imports  #:init-value #f
            #:init-keyword #:imports)
  (scope    #:init-value #f
            #:init-keyword #:scope
            #:accessor scope)
  (rules    #:init-value #f
            #:init-keyword #:rules
            #:accessor rules)
  (comments #:init-value #f
            #:init-keyword #:comments))

;; Lens for focusing the rules of a <policy>
(define-slot-lens ι-policy-rules 'rules)

;; Lens for focusing the global of a <policy>
(define-slot-lens ι-policy-scope 'scope)



(define-class <scope> ()
  (identifiers #:init-keyword #:identifiers
               #:accessor     inner))

(define-class <local> ()
  (resolved    #:init-form #f
               #:init-keyword #:resolved
               #:accessor     resolved?)
  (identifier  #:init-keyword #:identifier
               #:accessor     inner)
  (constraints #:init-form    '()
               #:init-keyword #:constraints
               #:accessor     constraints)
  ;; Name of the object as it will appear in the emitted Lean code.
  (lean-name   #:init-keyword #:lean-name
               #:accessor     lean-name))

(define (variable-ref->local ref)
  ;; TODO: Document me!
  ;;
  ;; This produces a dumb "it's just a name, haha" local with no constraints
  ;; attached.
  (make <local> #:identifier ref #:lean-name ref #:resolved #t))

(define-syntax with-anonymous-identifiers
  (lambda (stx)
    (syntax-case stx ()
      ((_ (new-identifiers ids ...) body ...)
       (let ((let-clauses
              (flat-map (lambda (id)
                          #`((#,(datum->syntax stx id) (fresh-identifier new-identifiers))
                             (new-identifiers (cons #,(datum->syntax stx id) new-identifiers))
                             (#,(datum->syntax stx id) (make <variable-ref>
                                                         #:name #,(datum->syntax stx id)))))
                        (syntax->datum #'(ids ...)))))
         #`(let* (#,@let-clauses)
             body ...))))))

(define (add-to-scope scope breadcrumb local)
  "Add a new LOCAL to BREADCRUMB in SCOPE"
  (define looking-at (hash-table-ref/default (inner scope) breadcrumb '()))
  (assert (is-a? scope <scope>))
  (assert (is-a? local <local>))
  (assert (list? breadcrumb))
  (hash-table-append-item! (inner scope) breadcrumb local))

(define (originating-breadcrumb scope breadcrumb identifier)
  "Return the part of the program in which IDENTIFIER was defined

This is for the variable that `identifier' names in `breadcrumb' /only/. In
practice, `identifier' can refer to many distinct variables depending, on the
context, hence the restriction.

Returns `#f' if `identifier' is not valid in `breadcrumb.'"
  (define (recur breadcrumb)
    (define looking-at (hash-table-ref/default (inner scope) breadcrumb '()))
    (cond ((null? breadcrumb) #f)
          ((assoc identifier looking-at) breadcrumb)
          (else (recur (drop-right breadcrumb 1)))))
  (assert (is-a? scope <scope>))
  (assert (is-a? identifier <variable-ref>))
  (assert (list? breadcrumb))
  (recur breadcrumb))

(define (canonicalize identifier breadcrumb)
  "Return a unique symbol for IDENTIFIER

Uniqueness is determined by the scope in which an identifier is /introduced/, so
`breadcrumb' is expected to be the region of the program where `identifier' was
defined. If this needs to be determined (i.e., for uses of identifiers aside
from definitions), `originating-breadcrumb' can determine the provenance of an
identifier."
  (string->symbol
   (format #f "~a.~a"
           identifier
           (hash (with-output-to-string
                   (lambda () (write `(,@breadcrumb ,identifier))))
                 (* 1024 1024)))))

(define any-type '(null bool number string array object))

(define (collapse-constraints scope)
  "Return all constraints in SCOPE

This is independent of context, which is okay, because the identifiers in the
resulting list of constraints are canonicalized such that they are unique and
can be associated with identifiers as they appear in the AST programmatically."
  (flat-map (lambda (grouping)
              (let ((breadcrumb (first grouping))
                    (identifiers (drop grouping 1)))
                (flat-map (lambda (local)
                            `((membero ,(canonicalize (inner local) breadcrumb) ,any-type)
                              ,@(constraints local)))
                          identifiers)))
            (hash-table->alist (inner scope))))

(define (all-valid-identifiers scope breadcrumb)
  "Return all identifiers that can be referenced in the scope specified by BREADCRUMB"
  (define (recur breadcrumb)
    (define looking-at (hash-table-ref/default (inner scope) breadcrumb '()))
    (if (null? breadcrumb)
        looking-at
        `(,@looking-at ,@(recur (drop-right breadcrumb 1)))))
  (assert (is-a? scope <scope>))
  (assert (list? breadcrumb))
  (recur breadcrumb))

(define (scope-contains? scope breadcrumb identifier)
  "Whether SCOPE contains IDENTIFIER at the point indicated by BREADCRUMB

`scope' is a <scope>, `breadcrumb' is a list given to the `f' of `mutate-tree',
and `identifier' is a <reference>"
  (match identifier
    ;; FIXME: It isn't clear to me that this is correct. There might be other
    ;; variables within `parts' that also need to be validated. But, then,
    ;; what's the point in using this function?
    (($ <reference> parts) (cut scope-contains? scope breadcrumb (first parts)))
    (($ <variable-ref> _)  (member identifier (map inner (all-valid-identifiers scope breadcrumb))))
    (_ (error "type unsupp"))))

(define (find-local scope breadcrumb name)
  ;; TODO: Document me!
  (find (lambda (identifier)
          (equal? name (inner identifier)))
        (all-valid-identifiers scope breadcrumb)))



(define-class <definition> ()
  ;; the sort object in question encoded by this predicate
  (kind     #:init-keyword #:kind
            #:getter       kind) ; memq '(plain value-eqv field-eqv set-memq array-memq)
  (left     #:init-keyword #:left
            #:accessor     left)
  (right    #:init-form    #f
            #:init-keyword #:right
            #:accessor     right)
  (default  #:init-keyword #:default
            #:accessor     default)
  (rules    #:init-keyword #:rules
            #:accessor     rules))

;; The intensional database of a Rego program is defined by its rules.
(define-class <rule> ()
  (default  #:init-form #f
            #:init-keyword #:default
            #:accessor     default-rule?)
  (head     #:init-keyword #:head
            #:accessor     head)
  (body     #:init-keyword #:body
            #:accessor     body)
  (else-arm #:init-form #f
            #:init-keyword #:else-arm
            #:accessor     else-arm))

;; Lens for focusing the body of a <rule>
(define-slot-lens ι-rule-body 'body)

(define-method (tree-map (form <rule>) f scope breadcrumb)
  (match form
    (($ <rule> default head body)
     ;; A rule body introduces a new scope.
     (let* ((inner (with-modified-slot form 'head
                     (tree-map head f scope breadcrumb)))
            (inner (with-modified-slot inner 'body
                     (tree-map body f scope breadcrumb))))
       (f scope breadcrumb inner)))))

(define (inductive-name x)
  (define suffix
    (match (kind x)
      ('value-eqv "_eqv")
      ('field-eqv "_eqv")
      ('set-memq  "_memq")))
  (match (left x)
    (($ <reference> (($ <variable-ref> name) _maybe-more ...))
     (string-concatenate `(,name ,suffix)))))



;; A (named) relation (equality or inclusion) that holds if the body of the rule is true.
(define-class <head> ()
  (name #:init-keyword #:name
        #:accessor     name)
  (kind #:init-keyword #:kind ; memq '(value-eqv field-eqv set-memq array-memq)
        #:accessor     kind)
  (lhs  #:init-keyword #:lhs
        #:accessor     left)
  (rhs  #:init-keyword #:rhs
        #:accessor     right))

(define-method (tree-map (form <head>) f scope breadcrumb)
  (match form
    (($ <head> name kind lhs rhs)
     ;; A rule body introduces a new scope.
     (let* ((inner (with-modified-slot form 'kind
                     (tree-map kind f scope breadcrumb)))
            ;; (inner (with-modified-slot inner 'lhs
            ;;          (tree-map lhs f scope breadcrumb)))
            (inner (with-modified-slot inner 'rhs
                     (tree-map rhs f scope breadcrumb))))
       (f scope breadcrumb inner)))))



;; A conjunction that defines whether a rule should apply.
(define-class <body> ()
  (conjunction #:init-keyword #:conjunction
               #:accessor     inner))

(define-method (tree-map (form <body>) f scope breadcrumb)
  (match form
    (($ <body> conjunction)
     (let ((inner (with-modified-slot form 'conjunction
                    (tree-map conjunction f scope breadcrumb))))
         (f scope breadcrumb inner)))))

;; Lens for focusing the contents of a <body>
(define-slot-lens ι-body-conjunction 'conjunction)



;; Call to a Rego function
(define-class <funcall> ()
  (ref  #:init-keyword #:name  ; <reference> (to the function being called)
        #:accessor name)
  (args #:init-keyword #:args  ; list of <term>
        #:accessor args))

;; Universal quantification over some domain of Rego values
(define-class <for-all> ()
  (domain #:init-keyword #:domain)
  (key    #:init-keyword #:key)
  (value  #:init-keyword #:value)
  (body   #:init-keyword #:body))

(define-method (tree-map (form <for-all>) f scope breadcrumb)
  (match form
    (($ <for-all> domain key value body)
     (let ((inner (with-modified-slot form 'body
                    (tree-map body f scope breadcrumb))))
       (f scope breadcrumb inner)))))

;; Existential quantification over some domain of Rego values
(define-class <exists-some> ()
  (identifiers #:init-keyword #:identifiers
               #:accessor     identifiers))

(define-method (tree-map (form <exists-some>) f scope breadcrumb)
  (match form
    (($ <exists-some> identifiers)
     (let ((inner (with-modified-slot form 'identifiers
                    (map (cut tree-map <> f scope breadcrumb)
                         identifiers))))
       (f scope breadcrumb inner)))))



;; Any literal that evaluates to itself, inclusive of comprehensions.
(define-class <constant> ()
  (value #:init-keyword #:value)) ; scheme value

(define-method (tree-map (form <constant>) f scope breadcrumb)
  (f scope breadcrumb form))

(define-class <set-literal> ()
  (elems #:init-keyword #:elems)) ; list of [scheme value | <set-literal> | <object-literal>]

(define-class <object-literal> ()
  (pairs #:init-keyword #:pairs)) ; list of [(string, scheme value | <set-literal> | <object-literal>)]

(define-class <comprehension> ()
  (kind  #:init-keyword #:kind)  ; one of '(array set object)
  (key   #:init-keyword #:key)
  (value #:init-keyword #:value)
  (body  #:init-keyword #:body))

(define (scheme-value->type x)
  (cond ((boolean? x) 'bool)
        ((number? x) 'number)
        (else 'any)))



;; A place within a (possibly nested) data structure.
;;
;; As described in the documentation for `<variable-ref>', this is our semantic
;; encoding for variable dereferencing. Referring to a variable in scope would
;; be encoded as a `<reference>' containing a single `<variable-ref>'.
(define-class <reference> ()
  (parts #:init-keyword #:parts
         #:accessor inner))

(define-method (equal? (x <reference>) (y <reference>))
  (equal? (inner x) (inner y)))

(define-method (tree-map (form <reference>) f scope breadcrumb)
  (match form
    (($ <reference> parts)
     (let ((inner (with-modified-slot form 'parts
                    (tree-map parts f scope breadcrumb))))
       (f scope breadcrumb inner)))))

;; A name within a lexical environment.
;;
;; Semantically, we don't treat a bare `<variable-ref>' as evaluating to the
;; value it refers to. For such an operation, we wrap the `<variable-ref>' in a
;; `<reference>'.
(define-class <variable-ref> ()
  (name #:init-keyword #:name ; <string>
        #:accessor     inner))

(define-method (equal? (x <variable-ref>) (y <variable-ref>))
  (equal? (inner x) (inner y)))