ssaavedra/.gitignore

## .gitignore
*~
*.swp
*.fasl
*.FASL
*.lisp-temp


## README.md

      
    Raw
  

              README.md
            
          
    CLIR Executable Rewriter

This compiles CAVI-ART project's CLIR to an executable program.
Requirements

Needs a Common Lisp compiler with ASDF System Definition support.
Tested with SBCL.
How to use

$ cd path/to/here
$ sbcl --load init.lisp
> (load "your-file.clir")
> (|package-name|::my-function) ;; Just call the function you want to execute in its package


## builtins.lisp
(cl:in-package :cl-user)
(load (merge-pathnames (directory-namestring *load-pathname*) "core.lisp"))
(defpackage :ir.builtins
  (:use :ir.core :common-lisp)
  (:shadow + - * / < <= > >= 1+ 1-)
  (:export + - * / < <= > >= 1+ 1-)

  (:shadowing-import-from :common-lisp :let :let* :case :load)

  ;; Export generalized boolean constants
  (:export :t :nil)

  ;; Export our minimal core-lisp for execution
  (:export :format)

  ;; Export types
  (:export :fixnum :number :real :float)

  ;; Export simulated heap and array
  (:export :assertion :defun-with-assertion)
  (:export :heap :heap-p :loc :new-heap :sel-heap :mod-heap :newptr-in-heap)
  (:export :sel-array :mod-array :sel-array-heap
	   :mod-array-heap :len-array-heap))
(in-package :ir.builtins)

(eval-when (:compile-toplevel :load-toplevel :execute)
  (declaim (optimize safety)))

;; PARAMETERS
(defparameter *assertions-executable-p* nil
  "This parameter influences whether assertions are to be executable or not.")

;; Redeclare some CL builtins so that they operate only on fixnums
;; Do not pollute the package with define-op definitions.
(macrolet ((define-op (opname)
	     `(defun ,opname (&rest vals)
		(declare (optimize speed (safety 0)))
		(the fixnum (apply (function ,(find-symbol (symbol-name opname) "COMMON-LISP")) vals))))

	   (boolean-op (opname)
	     (let ((result (gensym)))
	       `(defun ,opname (&rest vals)
		  (declare (optimize speed (safety 0)))
		  (let ((,result (apply (function ,(find-symbol (symbol-name opname) "COMMON-LISP")) vals)))
		    (if ,result
			'true
			'false)))))

	   (define-op1 (opname)
	     `(defun ,opname (val)
		(declare (type fixnum val)
			 (optimize speed (safety 0)))
		(the fixnum (funcall (function ,(find-symbol (symbol-name opname) "COMMON-LISP")) val)))))
  (define-op +)
  (define-op -)
  (define-op *)
  (define-op /)
  (boolean-op <)
  (boolean-op <=)
  (boolean-op >)
  (boolean-op >=)
  (define-op1 1+)
  (define-op1 1-))


;;
;; Now the assertion basics get here


(defun assert-get (type form)
  (assoc type form))

(defun assert-precd (form) (assert-get 'precd form))
(defun assert-postcd (form) (assert-get 'postcd form))

(eval-when (:compile-toplevel :execute :load-toplevel)
  ;; We need these accessible on compiling so that
  ;; `defun-with-assertion' can be computed in compile-time
  (defun get-decls (body)
    "Gets the `declare'-d and docstring forms (if there are any) of a
defun-ish body"
    (let ((form (car body)))
      (if (or (and (listp form)
		   (eq (car form)
		       'declare))
	      (stringp form))
	  (cons form (get-decls (cdr body)))
	  nil)))

  (defun remove-decls (body)
    "Returns the `declare'-stripped forms of a `defun'-ish body so
that only executable things get there."
    (let ((form (car body)))
      (if (or (and (listp form)
		   (eq (car form)
		       'declare))
	      (stringp form))
	  (remove-decls (cdr body))
	  body))))

(defun assert-as-code (assertion &key fname)
  "TODO: Make it work. Now it is just returning t and printing that it should be checked"
  `(prog1 t (format t "[At ~a] Should now be checking ~a~%" ',fname ',assertion)))


(defmacro defun-with-assertion (name args assertion-form &body full-body)
  "This macro is like a defun but it also introduces assertions as
declarations in the function metadata as well as allows executing the
assertions, provided a working implementation of `assert-as-code' for
assertion formulae and a non-nil `*assertions-executable-p*' parameter
value."
  (let ((body (remove-decls full-body))
	(decls (get-decls full-body)))
    (flet ((structured-body-with-postconditions-maybe (body &key postcd)
	     (if (and *assertions-executable-p*
		      postcd)
		 (let ((first-forms (butlast body))
		       (last-form (last body)))
		   (list first-forms
			 `(assert ,(assert-as-code postcd))
			 last-form))
		 body)
	     ))
      `(defun ,name ,args
	 (declare (assertion ,@assertion-form))
	 ,@decls
	 ,@(when (and *assertions-executable-p*
		      (assert-precd assertion-form))
		 `((assert ,(assert-as-code (assert-precd assertion-form)))))

	 ,@(structured-body-with-postconditions-maybe body :postcd (assert-postcd assertion-form))))))


;; Define the builtin functions

(defun heap-p (h)
  "Test whether a given parameter is a heap"
  (assoc :is-heap h))

(deftype heap () '(and list
		   (satisfies heap-p)))

;; For the while the information attached to loc is not really useful,
;; but we should eventually annotate a loc with its associated heap
;; and type check the value at the end.
(deftype loc (a) 'symbol)

(defun get-heap (H L)
  (declare (type heap H)
	   (type (loc (array fixnum)) L))
  "Dereferences a pointer from a heap"
  (cdr (assoc L H)))

(defun mod-heap (H L V)
  (declare (type heap H)
	   (type (loc (array fixnum)) L)
	   (type cons V))
  "Modifies a heap `H' so that the position pointed by `L' should
point to `V' in the resulting heap. TODO: should not be fixed to fixnum"
  (cons (cons L V) (remove L H :key #'car)))

(defun newptr-in-heap (H V)
  (declare (type heap H)
	   (type cons V))
  "Creates a new pointer in the heap and returns `values' for both the
newly allocated loc and the modified heap with such a pointer pointing
to value `V'"
  (let ((p (gensym)))
    (values (the (loc (array fixnum)) p)
	    (the heap (cons (cons p V) H)))))

(defmacro with-pointer-in-heap (H H2 V &body body)
  (assert (and (typep H2 'atom)
	       (typep V  'atom)))
  `(multiple-value-bind (,V ,H2) (newptr-in-heap ,H nil)
     ,@body))

(defun new-heap ()
  "Creates an empty heap"
  '((:is-heap . t)))

(defun sel-array (E I)
  (declare (type cons E)
	   (type fixnum I))
  "Returns a value by index in a modelled array"
  (the fixnum (cdr (assoc I E))))

(defun mod-array (E I V)
  "Modifies an array `E' so that position `I' now points to `V'"
  (the cons (cons (cons I V) (remove I E :key #'car))))

(defun sel-array-heap (H V I)
  "Convenience method for selecting an array without dereferencing the
pointer to the heap before."
  (sel-array (get-heap H V) I))

(defun mod-array-heap (H L I V)
  "Convenience method for modifying an array without dereferencing the
pointer to the heap before."
  (the heap (mod-heap H L (mod-array (get-heap H L) I V))))

(defun len-array-heap (H V)
  "Convenience method for getting the length of an array without
dereferencing the pointer to the heap before."
  (the fixnum (length (the list (get-heap H V)))))

;; END OF BUILTIN DECLS


;; Local Variables:
;; mode: common-lisp
;; coding: utf-8
;; End:

## cl-reexport.lisp
#|
  This file is a part of cl-reexport project.
  Taken from: https://github.com/takagi/cl-reexport/blob/master/src/cl-reexport.lisp
  Copyright (c) 2014 Masayuki Takagi (kamonama@gmail.com)
|#

(in-package :cl-user)
(defpackage cl-reexport
  (:use :cl)
  (:export :reexport-from))
(in-package :cl-reexport)


;;;
;;; Helpers
;;;

(defun external-symbols (package)
  (let (ret)
    (do-external-symbols (var package ret)
      (push var ret))))

(defun exclude-symbols (exclude symbols)
  (flet ((aux (symbol)
           (member symbol exclude :key #'symbol-name
                                  :test #'string=)))
    (remove-if #'aux symbols)))

(defun include-symbols (include symbols)
  (flet ((aux (symbol)
           (member symbol include :key #'symbol-name
                                  :test #'string=)))
    (if include
        (remove-if-not #'aux symbols)
        symbols)))


;;;
;;; Syntax:
;;;
;;;   REEXPORT-FROM package-from &key include exclude
;;;
;;; Arguments and values:
;;;
;;;   package-from --- a package designator from which symbols are reexported
;;;

(defun reexport-from (package-from &key include exclude)
  (unless (not (and include exclude))
    (error "INCLUDE option and EXCLUDE option are exclusive."))
  (let ((symbols (include-symbols include
                   (exclude-symbols exclude
                     (external-symbols package-from)))))
    (import symbols)
    (export symbols)))

## clir.asd
(defsystem "clir"
  :description "Common Lisp-like Intermediate Representation for CAVI-ART"
  :version "0.0.1"
  :author "Santiago Saavedra <s.saavedra@fdi.ucm.es>"
  :licence "GPL3"
  :components ((:file "cl-reexport")
	       (:file "core")
	       (:file "builtins" :depends-on ("core"))
	       (:file "rt" :depends-on ("cl-reexport" "core" "builtins"))
	       ))

## core.lisp
(cl:in-package :cl-user)

(defpackage :ir.rt
  (:documentation "Runtime package. Defines no symbols a priori."))

(defpackage :ir.core.impl
  (:use :cl)
  (:export :assertion :get-package-symbol :assertion-decl-to-code :signature-to-typedecl
	   :lambda-list-type-decls :maybe-macroexpand))

(defpackage :ir.core
  (:use :ir.core.impl)
  (:import-from :cl :nil :t)
  (:import-from :cl &allow-other-keys &body &key &rest)
  (:import-from :cl :let*)
  (:import-from :cl :declare :optimize :speed :debug :safety)
  (:import-from :cl :require :the :type)
  (:import-from :cl :defmacro :let* :cons :car :cdr :length :if :eq "=" :symbolp :first :and :or :nconc :append :consp )
  (:import-from :cl :list :funcall)

  (:export :list)
  (:export :int)
  (:export :bool :true :false)
  (:export :load :assertion :declare :the :type :optimize :speed :debug :safety)
  (:export :*assume-verified* :*verify-only*)
  (:export :define :lettype :letvar :letconst :let :let* :letfun :case "@"))

(in-package :ir.core.impl)
;;;; Package ir.core.impl follows.

;; Declare that "assertion" is a valid "declare" form.
(eval-when (:compile-toplevel :load-toplevel :execute)
  (declaim (declaration assertion)))

(defparameter *auto-macroexpand* t)

(defun get-package-symbol (input-package-symbol)
  (return-from get-package-symbol input-package-symbol)
  (flet ((get-package-name (input-package-symbol)
	   (symbol-name input-package-symbol)))
    (intern (get-package-name input-package-symbol) "IR.RT")))

(defun assertion-decl-to-code (body-forms)
  (if (assoc 'declare body-forms)
      (let ((declarations (cdr (assoc 'declare body-forms))))
	(declare (cl:ignore declarations))
	body-forms
	)
      body-forms))

(defun maybe-macroexpand (forms)
  (if *auto-macroexpand*
      (mapcar #'macroexpand-1 forms)
      forms))

(cl:defun lambda-list-type-decls (typed-lambda-list)
  (cl:mapcar
   (cl:lambda (e)
     (list 'type (cadr e) (car e)))
   typed-lambda-list))

;;;; Package ir.core must define vars before overriding package in cl-user.
(in-package :ir.core)

(cl:deftype int () `(cl:integer ,cl:most-negative-fixnum ,cl:most-positive-fixnum))
(cl:deftype bool () '(cl:member true false))

(cl:defparameter *assume-verified* nil)
(cl:defparameter *verify-only* nil)

;; Override CL-USER environment to define package (CLIR entry point)
(cl:in-package :cl-user)

(defmacro verification-unit (package-id &key sources uses documentation verify-only assume-verified)
  (declare (ignorable sources))
  (let ((pkg (ir.core.impl:get-package-symbol package-id)))
      `(progn (when (find-package ,pkg)
		(unuse-package ,@uses ,pkg)
		(delete-package ,pkg))
	      (defpackage ,pkg
		 (:use ,@uses)
		 (:documentation ,documentation))
	    (in-package ,pkg)
	    (mapcar (lambda (f) (push f ir.core:*assume-verified*)) ,assume-verified)
	    (mapcar (lambda (f) (push f ir.core:*verify-only*)) ,verify-only))))

;;;; Rest of ir.core follows.
(cl:in-package :ir.core)

(cl:defmacro lettype (type-symbol param-list type-boolean-expresssion optional-data)
  (declare (cl:ignore optional-data))
  "Defines a type globally in the environment."
  `(cl:deftype ,type-symbol ,param-list ,type-boolean-expresssion)
  ;; TODO: Use `optional-data'
  )


(cl:defmacro define (function-name typed-lambda-list &body full-body)
  "Defines an exportable function in the verification unit. The
function may be mutually recursive with other DEFINE-d functions."
  (cl:let ((body
	       (assertion-decl-to-code full-body)))
    `(cl:defun ,function-name ,(cl:mapcar #'cl:car typed-lambda-list)
       (declare ,@(lambda-list-type-decls typed-lambda-list))
       ,@ (maybe-macroexpand body))))


(cl:defmacro letfun (function-decls &body body)
  "Defines a lexically bound set of possibly mutually-recursive
functions."
  (cl:assert (= 1 (length body)))
  `(cl:labels
       ,(cl:mapcar (cl:lambda (f)
		     (cons (car f) (cons (cl:mapcar #'car (cl:cadr f)) (maybe-macroexpand (cl:cddr f))))) function-decls)
     ,@(maybe-macroexpand body)))

(cl:defmacro let (typed-var-list val &body body)
  "Lexically binds a var, syntax is: (let var val body-form). It can
destructure tuples as (let (a b) (list a b) a)"
  (cl:assert (= 1 (length body)))
  (cl:if (= 1 (length typed-var-list))
	 `(let ,(car typed-var-list) ,val ,@(maybe-macroexpand body))
	 (cl:if (and (= 2 (length typed-var-list))
		     (symbolp (first typed-var-list)))

		(cl:destructuring-bind
		      (var-name var-type) typed-var-list
		  `(cl:let ((,var-name ,val))
		       (declare (type ,var-type ,var-name))
		     ,@ (maybe-macroexpand body)))

		;; TODO Correctly treat constructor application
		(cl:labels
		    ((strip-var-types (typed-var-list)
		       "Strips variable types from a let-pattern (more
or less, a simple destructuring lambda list)"
		       (cl:if (consp (car typed-var-list))
			      (cons (strip-var-types (car typed-var-list))
				    (strip-var-types (cdr typed-var-list)))
			      (car typed-var-list)))
		     (get-type-for-decl (typed-var-list)
		       (cl:reduce #'get-type-for-decl-acc typed-var-list))

		     (get-type-for-decl-acc (typed-var-list acc)
		       (cl:if (consp (car typed-var-list))
			      (nconc (get-type-for-decl typed-var-list) acc)
			      (cons 'type typed-var-list))))
		  `(cl:destructuring-bind ,(strip-var-types typed-var-list) ,val
		     (declare ,@(get-type-for-decl typed-var-list))
		     ,@ (maybe-macroexpand body))))))

(cl:defmacro case (condition &body cases)
  "Defines a case conditional."
  ;; TODO The cases may be destructuring
  `(cl:case
       ,condition
     ,@ (cl:mapcar
	 (cl:lambda (c)
	   (cl:destructuring-bind
		 (pattern form) c
	     (list pattern (car (maybe-macroexpand (list form)))))) cases)))

(cl:defmacro @ (fname &rest args)
    "Substitutes the @ function application form for the appropriate
executable funcall."
    (if (eq fname :external)
	`(funcall #'call-external ,@args)
	`(funcall #',fname ,@args)))


## init.lisp
(cl:in-package :cl-user)
(require "asdf")
(push (directory-namestring *load-pathname*) asdf:*central-registry*)

(cl:in-package :asdf-user)
(oos 'load-op 'clir)


## inssort.clir
;; These instructions makes the code available at any time. They can
;; be removed, but then a Common-Lisp runtime will not know how to
;; parse the file.
(cl:eval-when (:compile-toplevel :load-toplevel :execute)
  (load "init.lisp"))
;; End of bogus instruction

(package :inssort
	 :uses (:ir)
	 :documentation "This is the implementation of a verified insertion sort in CLIR")


;; Test function (outside core for the moment)
(define create-list-and-heap ()
  (let l '((0 . 1)
	   (1 . 2)
	   (2 . 234)
	   (3 . 23)
	   (4 . 56)
	   (5 . 41))
       (cl:multiple-value-bind (v h) (newptr-in-heap (new-heap) l)
	 (inssort v h))))


(define f1 (V H)
  (declare (type heap H)
	   (type (loc (array int)) V))
  (let I (the int 0)
    (f2 V I H)))

(define f2 (V I H)
  (declare
   (assertion
    (precd (:forall ((E (array fixnum)))
		    (-> (= (deref H V) E)
			(and (sorted_sub E 0 I)
			     (<= 0 I)))))
    (postcd (:forall ((E (array fixnum)))
		     (-> (= (deref H V) E)
			 (sorted E)))))
   (type (loc (array fixnum)) V)
   (type heap H)
   (type fixnum I))

  (let X1 (len-array-heap H V)
    (let B (< I X1)
      (case B
	((t) (f3 V I H))
	((nil) H)))))


(define f3 (V I H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I))
  (let J (- I (the fixnum 1))
    (f4 V I J H)))


(define f4 (V I J H)
  (declare
   (assertion
    (precd (:forall ((E (array fixnum)))
		    (-> (= (deref H V) E)
			(and (sorted_sub E 0 (+ J 1))
			     (sorted_sub E (+ J 1) (+ I 1))
			     (<= -1 J)
			     (<= (sel-array E (- J 1))
				 (sel-array E (+ J 1))))))))
   (type heap H)
   (type (loc (array fixnum)) V)
   (type fixnum I J))

  (let B1 (>= J (the fixnum 0))
    (case B1
      ((nil) (f6 V I H))
      ((t) (let VJ (sel-array-heap H V J)
	     (let J1 (+ J (the fixnum 1))
	       (let VJ1 (sel-array-heap H V J1)
		 (let B2 (> VJ VJ1)
		   (case B2
		     ((nil) (f6 V I H))
		     ((t) (f5 V I J H)))))))))))


(define f5 (V I J H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I J))
  (let E (sel-array-heap H V J)
    (let J1  (+ J (the fixnum 1))
      (let E2 (sel-array-heap H V J1)
	(let H1 (mod-array-heap H V J E2)
	  (let H2 (mod-array-heap H1 V J1 E)
	    (let J2 (- J (the fixnum 1))
	      (f4 V I J2 H2))))))))


;; This would just show the alternative, if it existed
;; let* can allow for multiple bindings at once,
;; flattening the otherwise nested structure.
;; The binding is sequential.
(define f5-prime (V I J H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I J))
  (let* ((E (sel-array-heap H V J))
	 (J1  (+ J (the fixnum 1)))
	 (E2 (sel-array-heap H V J1))
	 (H1 (mod-array-heap H V J E2))
	 (H2 (mod-array-heap H1 V J1 E))
	 (J2 (- J (the fixnum 1))))
    (f4 V I J2 H2)))


(define f6 (V I H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I))
  (let I1 (+ I (the fixnum 1))
    (f2 V I1 H)))


(define inssort (V H)
  (f1 V H))


;; Local Variables:
;; mode: common-lisp
;; coding: utf-8
;; End:

## inssort.lisp
(cl:in-package :cl-user)
(require "asdf")
(eval-when (:compile-toplevel :load-toplevel :execute)
  (load "builtins.lisp")

  (proclaim '(optimize ;; debug
	      ;; speed (safety 0)
	      )))

(defpackage :cavi-art.ir.unit.inssort
  (:use :cavi-art.ir.builtins))
(in-package :cavi-art.ir.unit.inssort)


;; Creator functions
(defun create-list-and-heap ()
  (let ((l '((0 . 1)
	     (1 . 2)
	     (2 . 234)
	     (3 . 23)
	     (4 . 56)
	     (5 . 41))))
    (multiple-value-bind (v h) (newptr-in-heap (new-heap) l)
      (inssort v h))))

(defun f1 (V H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V))
  (let ((I (the fixnum 0)))
    (f2 V I H)))


(defun-with-assertion f2 (V I H)
  ((precd (:forall ((E (array fixnum)))
		   (-> (= (deref H V) E)
		       (and (sorted_sub E 0 I)
			    (<= 0 I)))))
   (postcd (:forall ((E (array fixnum)))
		    (-> (= (deref H V) E)
			(sorted E)))))
  (declare (type (loc (array fixnum)) V)
	   (type heap H)
	   (type fixnum I))
  (let ((X1 (len-array-heap H V)))
    (let ((B (< I X1)))
      (case B
	(break)
	((t) (f3 V I H))
	((nil) H)))))


(defun f3 (V I H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I))
  (let ((J (- I (the fixnum 1))))
    (f4 V I J H)))


(defun-with-assertion f4 (V I J H)
  ((precd (:forall ((E (array fixnum)))
		   (-> (= (deref H V) E)
		       (and (sorted_sub E 0 (+ J 1))
			    (sorted_sub E (+ J 1) (+ I 1))
			    (<= -1 J)
			    (<= (sel-array E (- J 1))
				(sel-array E (+ J 1))))))))
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I J))
  (let ((B1 (>= J (the fixnum 0))))
    (case B1
	  ((nil) (f6 V I H))
	  ((t) (let* ((VJ (sel-array-heap H V J))
		      (J1 (+ J (the fixnum 1)))
		      (VJ1 (sel-array-heap H V J1))
		      (B2 (> VJ VJ1)))
		 (case B2
		   ((nil) (f6 V I H))
		   ((t) (f5 V I J H))))))))


(defun f5 (V I J H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I J))
  (let* ((E (sel-array-heap H V J))
	 (J1  (+ J (the fixnum 1)))
	 (E2 (sel-array-heap H V J1))
	 (H1 (mod-array-heap H V J E2))
	 (H2 (mod-array-heap H1 V J1 E))
	 (J2 (- J (the fixnum 1))))
    (f4 V I J2 H2)))


(defun f6 (V I H)
  (declare (type heap H)
	   (type (loc (array fixnum)) V)
	   (type fixnum I))
  (let ((I1 (+ I (the fixnum 1))))
    (f2 V I1 H)))


(defun inssort (V H)
  (f1 V H))


;; Local Variables:
;; mode: common-lisp
;; coding: utf-8
;; End:

## packages.lisp
(in-package :cl-user)

(defpackage :cavi-art.ir.builtins
  (:use
   :common-lisp)
  (:shadow + - * / < <= > >= 1+ 1-)
  (:export + - * / < <= > >= 1+ 1-)

  ;; Export generalized boolean constants
  (:export :t :nil)

  ;; Export our minimal core-lisp for execution
  (:export :case :declare :defun :export :format :function :lambda
	   :let :let* :multiple-value-bind :require :the :type)

  ;; Export types
  (:export :fixnum :number :real :float)

  ;; Export simulated heap and array
  (:export :assertion :defun-with-assertion)
  (:export :heap :heap-p :loc :new-heap :sel-heap :mod-heap :newptr-in-heap)
  (:export :sel-array :mod-array :sel-array-heap
	   :mod-array-heap :len-array-heap))

(provide "packages.lisp")

## rt.lisp
(cl:in-package :cl-user)
(proclaim '(optimize debug
	    ;; speed (safety 0)
	    ))

(print *load-pathname*)
(print (directory-namestring *load-pathname*))
(print (pathname (directory-namestring *load-pathname*)))

(load (merge-pathnames (directory-namestring *load-pathname*) "cl-reexport.lisp"))
(load (merge-pathnames (directory-namestring *load-pathname*) "core.lisp"))
(load (merge-pathnames (directory-namestring *load-pathname*) "builtins.lisp"))
(unless (find-package :ir)
  (defpackage :ir
    (:use :ir.core :ir.builtins)))

(in-package :ir)
(cl-reexport:reexport-from :ir.core)
(cl-reexport:reexport-from :ir.builtins)
	(cl:in-package :cl-user)
	(load (merge-pathnames (directory-namestring load-pathname) "core.lisp"))
	(defpackage :ir.builtins
	(:use :ir.core :common-lisp)
	(:shadow + - * / < <= > >= 1+ 1-)
	(:export + - * / < <= > >= 1+ 1-)

	(:shadowing-import-from :common-lisp :let :let* :case :load)

	;; Export generalized boolean constants
	(:export :t :nil)

	;; Export our minimal core-lisp for execution
	(:export :format)

	;; Export types
	(:export :fixnum :number :real :float)

	;; Export simulated heap and array
	(:export :assertion :defun-with-assertion)
	(:export :heap :heap-p :loc :new-heap :sel-heap :mod-heap :newptr-in-heap)
	(:export :sel-array :mod-array :sel-array-heap
	:mod-array-heap :len-array-heap))
	(in-package :ir.builtins)

	(eval-when (:compile-toplevel :load-toplevel :execute)
	(declaim (optimize safety)))

	;; PARAMETERS
	(defparameter assertions-executable-p nil
	"This parameter influences whether assertions are to be executable or not.")

	;; Redeclare some CL builtins so that they operate only on fixnums
	;; Do not pollute the package with define-op definitions.
	(macrolet ((define-op (opname)
	`(defun ,opname (&rest vals)
	(declare (optimize speed (safety 0)))
	(the fixnum (apply (function ,(find-symbol (symbol-name opname) "COMMON-LISP")) vals))))

	(boolean-op (opname)
	(let ((result (gensym)))
	`(defun ,opname (&rest vals)
	(declare (optimize speed (safety 0)))
	(let ((,result (apply (function ,(find-symbol (symbol-name opname) "COMMON-LISP")) vals)))
	(if ,result
	'true
	'false)))))

	(define-op1 (opname)
	`(defun ,opname (val)
	(declare (type fixnum val)
	(optimize speed (safety 0)))
	(the fixnum (funcall (function ,(find-symbol (symbol-name opname) "COMMON-LISP")) val)))))
	(define-op +)
	(define-op -)
	(define-op *)
	(define-op /)
	(boolean-op <)
	(boolean-op <=)
	(boolean-op >)
	(boolean-op >=)
	(define-op1 1+)
	(define-op1 1-))


	;;
	;; Now the assertion basics get here


	(defun assert-get (type form)
	(assoc type form))

	(defun assert-precd (form) (assert-get 'precd form))
	(defun assert-postcd (form) (assert-get 'postcd form))

	(eval-when (:compile-toplevel :execute :load-toplevel)
	;; We need these accessible on compiling so that
	;; `defun-with-assertion' can be computed in compile-time
	(defun get-decls (body)
	"Gets the `declare'-d and docstring forms (if there are any) of a
	defun-ish body"
	(let ((form (car body)))
	(if (or (and (listp form)
	(eq (car form)
	'declare))
	(stringp form))
	(cons form (get-decls (cdr body)))
	nil)))

	(defun remove-decls (body)
	"Returns the `declare'-stripped forms of a `defun'-ish body so
	that only executable things get there."
	(let ((form (car body)))
	(if (or (and (listp form)
	(eq (car form)
	'declare))
	(stringp form))
	(remove-decls (cdr body))
	body))))

	(defun assert-as-code (assertion &key fname)
	"TODO: Make it work. Now it is just returning t and printing that it should be checked"
	`(prog1 t (format t "[At ~a] Should now be checking ~a~%" ',fname ',assertion)))


	(defmacro defun-with-assertion (name args assertion-form &body full-body)
	"This macro is like a defun but it also introduces assertions as
	declarations in the function metadata as well as allows executing the
	assertions, provided a working implementation of `assert-as-code' for
	assertion formulae and a non-nil `assertions-executable-p' parameter
	value."
	(let ((body (remove-decls full-body))
	(decls (get-decls full-body)))
	(flet ((structured-body-with-postconditions-maybe (body &key postcd)
	(if (and assertions-executable-p
	postcd)
	(let ((first-forms (butlast body))
	(last-form (last body)))
	(list first-forms
	`(assert ,(assert-as-code postcd))
	last-form))
	body)
	))
	`(defun ,name ,args
	(declare (assertion ,@assertion-form))
	,@decls
	,@(when (and assertions-executable-p
	(assert-precd assertion-form))
	`((assert ,(assert-as-code (assert-precd assertion-form)))))

	,@(structured-body-with-postconditions-maybe body :postcd (assert-postcd assertion-form))))))


	;; Define the builtin functions

	(defun heap-p (h)
	"Test whether a given parameter is a heap"
	(assoc :is-heap h))

	(deftype heap () '(and list
	(satisfies heap-p)))

	;; For the while the information attached to loc is not really useful,
	;; but we should eventually annotate a loc with its associated heap
	;; and type check the value at the end.
	(deftype loc (a) 'symbol)

	(defun get-heap (H L)
	(declare (type heap H)
	(type (loc (array fixnum)) L))
	"Dereferences a pointer from a heap"
	(cdr (assoc L H)))

	(defun mod-heap (H L V)
	(declare (type heap H)
	(type (loc (array fixnum)) L)
	(type cons V))
	"Modifies a heap `H' so that the position pointed by `L' should
	point to `V' in the resulting heap. TODO: should not be fixed to fixnum"
	(cons (cons L V) (remove L H :key #'car)))

	(defun newptr-in-heap (H V)
	(declare (type heap H)
	(type cons V))
	"Creates a new pointer in the heap and returns `values' for both the
	newly allocated loc and the modified heap with such a pointer pointing
	to value `V'"
	(let ((p (gensym)))
	(values (the (loc (array fixnum)) p)
	(the heap (cons (cons p V) H)))))

	(defmacro with-pointer-in-heap (H H2 V &body body)
	(assert (and (typep H2 'atom)
	(typep V 'atom)))
	`(multiple-value-bind (,V ,H2) (newptr-in-heap ,H nil)
	,@body))

	(defun new-heap ()
	"Creates an empty heap"
	'((:is-heap . t)))

	(defun sel-array (E I)
	(declare (type cons E)
	(type fixnum I))
	"Returns a value by index in a modelled array"
	(the fixnum (cdr (assoc I E))))

	(defun mod-array (E I V)
	"Modifies an array `E' so that position `I' now points to `V'"
	(the cons (cons (cons I V) (remove I E :key #'car))))

	(defun sel-array-heap (H V I)
	"Convenience method for selecting an array without dereferencing the
	pointer to the heap before."
	(sel-array (get-heap H V) I))

	(defun mod-array-heap (H L I V)
	"Convenience method for modifying an array without dereferencing the
	pointer to the heap before."
	(the heap (mod-heap H L (mod-array (get-heap H L) I V))))

	(defun len-array-heap (H V)
	"Convenience method for getting the length of an array without
	dereferencing the pointer to the heap before."
	(the fixnum (length (the list (get-heap H V)))))

	;; END OF BUILTIN DECLS


	;; Local Variables:
	;; mode: common-lisp
	;; coding: utf-8
	;; End:
	#\|
	This file is a part of cl-reexport project.
	Taken from: https://github.com/takagi/cl-reexport/blob/master/src/cl-reexport.lisp
	Copyright (c) 2014 Masayuki Takagi (kamonama@gmail.com)
	\|#

	(in-package :cl-user)
	(defpackage cl-reexport
	(:use :cl)
	(:export :reexport-from))
	(in-package :cl-reexport)


	;;;
	;;; Helpers
	;;;

	(defun external-symbols (package)
	(let (ret)
	(do-external-symbols (var package ret)
	(push var ret))))

	(defun exclude-symbols (exclude symbols)
	(flet ((aux (symbol)
	(member symbol exclude :key #'symbol-name
	:test #'string=)))
	(remove-if #'aux symbols)))

	(defun include-symbols (include symbols)
	(flet ((aux (symbol)
	(member symbol include :key #'symbol-name
	:test #'string=)))
	(if include
	(remove-if-not #'aux symbols)
	symbols)))


	;;;
	;;; Syntax:
	;;;
	;;; REEXPORT-FROM package-from &key include exclude
	;;;
	;;; Arguments and values:
	;;;
	;;; package-from --- a package designator from which symbols are reexported
	;;;

	(defun reexport-from (package-from &key include exclude)
	(unless (not (and include exclude))
	(error "INCLUDE option and EXCLUDE option are exclusive."))
	(let ((symbols (include-symbols include
	(exclude-symbols exclude
	(external-symbols package-from)))))
	(import symbols)
	(export symbols)))
	(defsystem "clir"
	:description "Common Lisp-like Intermediate Representation for CAVI-ART"
	:version "0.0.1"
	:author "Santiago Saavedra <s.saavedra@fdi.ucm.es>"
	:licence "GPL3"
	:components ((:file "cl-reexport")
	(:file "core")
	(:file "builtins" :depends-on ("core"))
	(:file "rt" :depends-on ("cl-reexport" "core" "builtins"))
	))
	(cl:in-package :cl-user)

	(defpackage :ir.rt
	(:documentation "Runtime package. Defines no symbols a priori."))

	(defpackage :ir.core.impl
	(:use :cl)
	(:export :assertion :get-package-symbol :assertion-decl-to-code :signature-to-typedecl
	:lambda-list-type-decls :maybe-macroexpand))

	(defpackage :ir.core
	(:use :ir.core.impl)
	(:import-from :cl :nil :t)
	(:import-from :cl &allow-other-keys &body &key &rest)
	(:import-from :cl :let*)
	(:import-from :cl :declare :optimize :speed :debug :safety)
	(:import-from :cl :require :the :type)
	(:import-from :cl :defmacro :let* :cons :car :cdr :length :if :eq "=" :symbolp :first :and :or :nconc :append :consp )
	(:import-from :cl :list :funcall)

	(:export :list)
	(:export :int)
	(:export :bool :true :false)
	(:export :load :assertion :declare :the :type :optimize :speed :debug :safety)
	(:export :assume-verified :verify-only)
	(:export :define :lettype :letvar :letconst :let :let* :letfun :case "@"))

	(in-package :ir.core.impl)
	;;;; Package ir.core.impl follows.

	;; Declare that "assertion" is a valid "declare" form.
	(eval-when (:compile-toplevel :load-toplevel :execute)
	(declaim (declaration assertion)))

	(defparameter auto-macroexpand t)

	(defun get-package-symbol (input-package-symbol)
	(return-from get-package-symbol input-package-symbol)
	(flet ((get-package-name (input-package-symbol)
	(symbol-name input-package-symbol)))
	(intern (get-package-name input-package-symbol) "IR.RT")))

	(defun assertion-decl-to-code (body-forms)
	(if (assoc 'declare body-forms)
	(let ((declarations (cdr (assoc 'declare body-forms))))
	(declare (cl:ignore declarations))
	body-forms
	)
	body-forms))

	(defun maybe-macroexpand (forms)
	(if auto-macroexpand
	(mapcar #'macroexpand-1 forms)
	forms))

	(cl:defun lambda-list-type-decls (typed-lambda-list)
	(cl:mapcar
	(cl:lambda (e)
	(list 'type (cadr e) (car e)))
	typed-lambda-list))

	;;;; Package ir.core must define vars before overriding package in cl-user.
	(in-package :ir.core)

	(cl:deftype int () `(cl:integer ,cl:most-negative-fixnum ,cl:most-positive-fixnum))
	(cl:deftype bool () '(cl:member true false))

	(cl:defparameter assume-verified nil)
	(cl:defparameter verify-only nil)

	;; Override CL-USER environment to define package (CLIR entry point)
	(cl:in-package :cl-user)

	(defmacro verification-unit (package-id &key sources uses documentation verify-only assume-verified)
	(declare (ignorable sources))
	(let ((pkg (ir.core.impl:get-package-symbol package-id)))
	`(progn (when (find-package ,pkg)
	(unuse-package ,@uses ,pkg)
	(delete-package ,pkg))
	(defpackage ,pkg
	(:use ,@uses)
	(:documentation ,documentation))
	(in-package ,pkg)
	(mapcar (lambda (f) (push f ir.core:assume-verified)) ,assume-verified)
	(mapcar (lambda (f) (push f ir.core:verify-only)) ,verify-only))))

	;;;; Rest of ir.core follows.
	(cl:in-package :ir.core)

	(cl:defmacro lettype (type-symbol param-list type-boolean-expresssion optional-data)
	(declare (cl:ignore optional-data))
	"Defines a type globally in the environment."
	`(cl:deftype ,type-symbol ,param-list ,type-boolean-expresssion)
	;; TODO: Use `optional-data'
	)


	(cl:defmacro define (function-name typed-lambda-list &body full-body)
	"Defines an exportable function in the verification unit. The
	function may be mutually recursive with other DEFINE-d functions."
	(cl:let ((body
	(assertion-decl-to-code full-body)))
	`(cl:defun ,function-name ,(cl:mapcar #'cl:car typed-lambda-list)
	(declare ,@(lambda-list-type-decls typed-lambda-list))
	,@ (maybe-macroexpand body))))


	(cl:defmacro letfun (function-decls &body body)
	"Defines a lexically bound set of possibly mutually-recursive
	functions."
	(cl:assert (= 1 (length body)))
	`(cl:labels
	,(cl:mapcar (cl:lambda (f)
	(cons (car f) (cons (cl:mapcar #'car (cl:cadr f)) (maybe-macroexpand (cl:cddr f))))) function-decls)
	,@(maybe-macroexpand body)))

	(cl:defmacro let (typed-var-list val &body body)
	"Lexically binds a var, syntax is: (let var val body-form). It can
	destructure tuples as (let (a b) (list a b) a)"
	(cl:assert (= 1 (length body)))
	(cl:if (= 1 (length typed-var-list))
	`(let ,(car typed-var-list) ,val ,@(maybe-macroexpand body))
	(cl:if (and (= 2 (length typed-var-list))
	(symbolp (first typed-var-list)))

	(cl:destructuring-bind
	(var-name var-type) typed-var-list
	`(cl:let ((,var-name ,val))
	(declare (type ,var-type ,var-name))
	,@ (maybe-macroexpand body)))

	;; TODO Correctly treat constructor application
	(cl:labels
	((strip-var-types (typed-var-list)
	"Strips variable types from a let-pattern (more
	or less, a simple destructuring lambda list)"
	(cl:if (consp (car typed-var-list))
	(cons (strip-var-types (car typed-var-list))
	(strip-var-types (cdr typed-var-list)))
	(car typed-var-list)))
	(get-type-for-decl (typed-var-list)
	(cl:reduce #'get-type-for-decl-acc typed-var-list))

	(get-type-for-decl-acc (typed-var-list acc)
	(cl:if (consp (car typed-var-list))
	(nconc (get-type-for-decl typed-var-list) acc)
	(cons 'type typed-var-list))))
	`(cl:destructuring-bind ,(strip-var-types typed-var-list) ,val
	(declare ,@(get-type-for-decl typed-var-list))
	,@ (maybe-macroexpand body))))))

	(cl:defmacro case (condition &body cases)
	"Defines a case conditional."
	;; TODO The cases may be destructuring
	`(cl:case
	,condition
	,@ (cl:mapcar
	(cl:lambda (c)
	(cl:destructuring-bind
	(pattern form) c
	(list pattern (car (maybe-macroexpand (list form)))))) cases)))

	(cl:defmacro @ (fname &rest args)
	"Substitutes the @ function application form for the appropriate
	executable funcall."
	(if (eq fname :external)
	`(funcall #'call-external ,@args)
	`(funcall #',fname ,@args)))
	(cl:in-package :cl-user)
	(require "asdf")
	(push (directory-namestring load-pathname) asdf:central-registry)

	(cl:in-package :asdf-user)
	(oos 'load-op 'clir)
	;; These instructions makes the code available at any time. They can
	;; be removed, but then a Common-Lisp runtime will not know how to
	;; parse the file.
	(cl:eval-when (:compile-toplevel :load-toplevel :execute)
	(load "init.lisp"))
	;; End of bogus instruction

	(package :inssort
	:uses (:ir)
	:documentation "This is the implementation of a verified insertion sort in CLIR")


	;; Test function (outside core for the moment)
	(define create-list-and-heap ()
	(let l '((0 . 1)
	(1 . 2)
	(2 . 234)
	(3 . 23)
	(4 . 56)
	(5 . 41))
	(cl:multiple-value-bind (v h) (newptr-in-heap (new-heap) l)
	(inssort v h))))


	(define f1 (V H)
	(declare (type heap H)
	(type (loc (array int)) V))
	(let I (the int 0)
	(f2 V I H)))

	(define f2 (V I H)
	(declare
	(assertion
	(precd (:forall ((E (array fixnum)))
	(-> (= (deref H V) E)
	(and (sorted_sub E 0 I)
	(<= 0 I)))))
	(postcd (:forall ((E (array fixnum)))
	(-> (= (deref H V) E)
	(sorted E)))))
	(type (loc (array fixnum)) V)
	(type heap H)
	(type fixnum I))

	(let X1 (len-array-heap H V)
	(let B (< I X1)
	(case B
	((t) (f3 V I H))
	((nil) H)))))


	(define f3 (V I H)
	(declare (type heap H)
	(type (loc (array fixnum)) V)
	(type fixnum I))
	(let J (- I (the fixnum 1))
	(f4 V I J H)))


	(define f4 (V I J H)
	(declare
	(assertion
	(precd (:forall ((E (array fixnum)))
	(-> (= (deref H V) E)
	(and (sorted_sub E 0 (+ J 1))
	(sorted_sub E (+ J 1) (+ I 1))
	(<= -1 J)
	(<= (sel-array E (- J 1))
	(sel-array E (+ J 1))))))))
	(type heap H)
	(type (loc (array fixnum)) V)
	(type fixnum I J))

	(let B1 (>= J (the fixnum 0))
	(case B1
	((nil) (f6 V I H))
	((t) (let VJ (sel-array-heap H V J)
	(let J1 (+ J (the fixnum 1))
	(let VJ1 (sel-array-heap H V J1)
	(let B2 (> VJ VJ1)
	(case B2
	((nil) (f6 V I H))
	((t) (f5 V I J H)))))))))))


	(define f5 (V I J H)
	(declare (type heap H)
	(type (loc (array fixnum)) V)
	(type fixnum I J))
	(let E (sel-array-heap H V J)
	(let J1 (+ J (the fixnum 1))
	(let E2 (sel-array-heap H V J1)
	(let H1 (mod-array-heap H V J E2)
	(let H2 (mod-array-heap H1 V J1 E)
	(let J2 (- J (the fixnum 1))
	(f4 V I J2 H2))))))))


	;; This would just show the alternative, if it existed
	;; let* can allow for multiple bindings at once,
	;; flattening the otherwise nested structure.
	;; The binding is sequential.
	(define f5-prime (V I J H)
	(declare (type heap H)
	(type (loc (array fixnum)) V)
	(type fixnum I J))
	(let* ((E (sel-array-heap H V J))
	(J1 (+ J (the fixnum 1)))
	(E2 (sel-array-heap H V J1))
	(H1 (mod-array-heap H V J E2))
	(H2 (mod-array-heap H1 V J1 E))
	(J2 (- J (the fixnum 1))))
	(f4 V I J2 H2)))



	(define f6 (V I H)
	(declare (type heap H)
	(type (loc (array fixnum)) V)
	(type fixnum I))
	(let I1 (+ I (the fixnum 1))
	(f2 V I1 H)))


	(define inssort (V H)
	(f1 V H))



	;; Local Variables:
	;; mode: common-lisp
	;; coding: utf-8
	;; End:
	(in-package :cl-user)

	(defpackage :cavi-art.ir.builtins
	(:use
	:common-lisp)
	(:shadow + - * / < <= > >= 1+ 1-)
	(:export + - * / < <= > >= 1+ 1-)

	;; Export generalized boolean constants
	(:export :t :nil)

	;; Export our minimal core-lisp for execution
	(:export :case :declare :defun :export :format :function :lambda
	:let :let* :multiple-value-bind :require :the :type)

	;; Export types
	(:export :fixnum :number :real :float)

	;; Export simulated heap and array
	(:export :assertion :defun-with-assertion)
	(:export :heap :heap-p :loc :new-heap :sel-heap :mod-heap :newptr-in-heap)
	(:export :sel-array :mod-array :sel-array-heap
	:mod-array-heap :len-array-heap))

	(provide "packages.lisp")
	(cl:in-package :cl-user)
	(proclaim '(optimize debug
	;; speed (safety 0)
	))

	(print load-pathname)
	(print (directory-namestring load-pathname))
	(print (pathname (directory-namestring load-pathname)))

	(load (merge-pathnames (directory-namestring load-pathname) "cl-reexport.lisp"))
	(load (merge-pathnames (directory-namestring load-pathname) "core.lisp"))
	(load (merge-pathnames (directory-namestring load-pathname) "builtins.lisp"))
	(unless (find-package :ir)
	(defpackage :ir
	(:use :ir.core :ir.builtins)))

	(in-package :ir)
	(cl-reexport:reexport-from :ir.core)
	(cl-reexport:reexport-from :ir.builtins)