;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -*- Mode: Lisp -*- ;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Practicals: Proof Tacticals for the PVS Proof Assistant
;;
;; Author          : Florent Kirchner (fkirchne@nianet.org)
;; Created On      : Mon Jun 16 17:18:37 2003
;; Last Modified By: Florent Kirchner (fkirchne@nianet.org)
;; Last Modified On: Thu Sep 30 06:26:58 2005
;; Update Count    : 3
;; Status          : Experimental
;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; This is a U.S. Government work and thus not protected by U.S.
;; copyright. As a courtesy, please retain the header lines and
;; introductory comments in any derivative works. Problem reports,
;; suggestions and enhancements are encouraged. Send them to the
;; address above.
;;
;; ---------------------------------------------------------------------------
;;
;; This file implements various PVS strategies.  
;;
;; As a convention, the identifier 'dy' is used wherever a dummy variable
;; affectation needs to be done.
;; The PVS function names will be written in uppercase, and the lisp functions
;; in lowercase
;;
;; =============================== End of preamble ===========================


;; ========================================================== Global variables

(defvar *practicals-debug-flag* nil
  "[Practicals Package] Triggers the printing of debugging messages in the Practicals strategies.")

(defvar *error-tag* nil
  "[Practicals Package] The current error name: used for naming exceptions.")

(defvar *suppress-prac-messages* nil
  "[Practicals Package] Governs the printing of the package's messages.")

(defvar *thesis-symbol* '(/-)
  "[Practicals Package] List of all the thesis symbols, used when parsing sequent patterns.")

(defvar *do-symbol* '(->)
  "[Practicals Package] List of all the do symbols, used when parsing sequent patterns.")


;; =================================================== Developper's lil helper

(defun gen-prac-response (name msg &optional (force-printing? t))
  (declare (string name msg))
  (if *suppress-prac-messages*
      '(skip)
    `(skip-msg ,(format nil "[Practicals.~A]  ~A" name msg)
	       ,force-printing?)))

(defstrat RELOAD-PRACTICALS ()
  (LET ((dy (libload "/home/flo/beta/pvs/packages/Practicals/practicals"))
	(msg (gen-prac-response "reload" "Loading: Practicals.")) )
    msg)
  "[Practicals Package] Reloads the Practicals package."
  )

(defstrat PRACTICALS-DEBUG-MODE (b)
  (LET ((dy (setq *practicals-debug-flag* b))
	(msg (gen-prac-response "practicals-debug-mode" 
				(format nil "Setting debug mode to ~A" b))))
    msg)
    "[Practicals Package] Sets the debug mode on/off."
    )

(defun print-debug (str)
  (declare (string str))
  (when *practicals-debug-flag* (pprint str) ) )

(defstrat foo () (skip-msg "foo" T) "[Practicals Package]")
(defstrat bar () (skip-msg "bar" T) "[Practicals Package]")


;; =================================================== Proof monad contructors

;; piks can be interpreted as "do something but don't mess everything
;; up". It is useful to lure a progress-testing tactical rule like
;; (try...) into thinking that the proof has made some progress.
(defstrat PIKS ()
  (APPLY (SKIP) :save? t)
  "[Practicals Package] The inverse of skip. Does nothing to the proof, but does not count as a skip either."
  )

;; This generate the backtrack event. Since backtracking ultimately
;; evaluates to skip, the effect of this tactic is invisible on the
;; toplevel. This only makes sense as a glassbox.
(defstrat BACKTRACK ()
  (TRY (PIKS) (FAIL) (SKIP-MSG "[Practicals.backtrack] This shouldn't occur: please report." t))
  "[Practicals Package] This generates a backtracking value. On toplevel, it will return skip."
  "Backtracking"
  )


;; ==================================================== Proof monad destructor

(defstruct flag
  "[Practicals package] The set of flags reflecting a tactic's outcome."
  (success nil)
  (subgoal nil)
  (skip nil)
  (backtrack nil)
  (fail nil)
  )

(defstruct var
  "[Practicals package] Miscellaneous counters and flags."
  (fnum nil)
  )

;; This is the de-constructor. 'figure' figures out the outcome of
;; step on the current goal, and fills the values of otc depending on
;; it.
(defhelper FIGURE (STEP otc)
  (let ((dy (print-debug (format nil "[fig0] otc: ~A." otc)))) ;DEBUG
    (TRY				;2 - analyze the result of 1
     (TRY				;1 - differenciate backtrack and skip.
      (PIKS)
      (TRY				;0 - the subgoal case
       STEP
       (LET ((dy (setf (flag-subgoal otc) t)) ;STEP generated subgoals
	     (dy (print-debug (format nil "[fig1] otc: ~A." otc)))) ;DEBUG
	    (SKIP))
       (LET ((dy (setf (flag-backtrack otc) t (flag-skip otc) t)) ;STEP might be either skip or backtrack
	     (dy (print-debug (format nil "[fig2] otc: ~A." otc)))) ;DEBUG
	    (TRY (PIKS) STEP (SKIP-MSG "[Practicals.figure1] This shouldn't occur: please report." t)))
       )				; /0
      (skip-msg "[Practicals.figure2] This shouldn't occur: please report." t)
      )					; /1
     (IF (flag-subgoal otc)
	 (LET ((dy (print-debug (format nil "[fig3] otc: ~A." otc)))) ;DEBUG
	      (SKIP))			;step was a subgoal
	 (LET ((dy (setf (flag-backtrack otc) nil)) ;step was a skip
	       (dy (print-debug (format nil "[fig3'] otc: ~A." otc)))) ;DEBUG
	      (FAIL)))
     (IF (flag-backtrack otc) 
	 (LET ((dy (setf (flag-skip otc) nil)) ;step was a backtrack
	       (dy (print-debug (format nil "[fig4] otc: ~A." otc)))) ;DEBUG
	      (BACKTRACK))
	 (LET ((dy (setf (flag-fail otc) t)) ;step was a fail
	       (dy (print-debug (format nil "[fig4'] otc: ~A." otc)))) ;DEBUG
	      (BACKTRACK)))
     )					; /2
    ) ; from this try only success (STEP=success), backtrack (STEP=skip,backtrack,fail), subgoal (STEP=subgoal) can arise
  "[Practicals Package] Filter the result of a step -without backtracking"
  "Testing ~A"
  )

;; This helper simulates the application of step1 on a dummy goal and
;; modifies the flags (in otc) accordingly to the result.
(defhelper INSPECT (STEP otc)
  (LET ((lvar (make-var))		;misc. local variables
	(dy (print-debug (format nil "[init] lvar: ~A, ~% otc: ~A." lvar otc)))) ;DEBUG
       (THEN (SPREAD (CASE "FORALL (x:real): x=x") ;create a copy of the goal
		     ((DELETE -1)       ;store away the original
		      (THEN@ (HIDE 1)	;and work on the duplicate
			     (LET ((dy (setf (var-fnum lvar) (label *ps*)))
				   (dy (print-debug (format nil "[s1] lvar: ~A, ~% otc: ~A." lvar otc)))) ;DEBUG
				  (FIGURE$ STEP otc)
				  )))
		     )			; end of the spread. 
	     (IF (equal (var-fnum lvar) (label *ps*)) ;3 - test: has step proven the goal ? Delete the possible remaining copy of the goal
		 (THEN@ (LET ((dy (setf (flag-success otc) nil))
			      (dy (print-debug (format nil "[s4] lvar: ~A, ~% otc: ~A." lvar otc)))) ;DEBUG
			     (REVEAL *)) 
			(GRIND)) ;step didn't prove the goal, delete the duplicate
		 (LET ((dy (setf (flag-success otc) t))
		       (dy (print-debug (format nil "[s5] lvar: ~A, ~% otc: ~A." lvar otc))))	;DEBUG
		      (SKIP))		;step proved the goal
		 )			; /3
	     )
       )
  "[Practicals Package] This helper simulates the application of step1 on a dummy goal and fills the fields in otc depending on the outcome."
  "Inspecting ~A"
  )

;; Prints out some info on the possible outcome of step
(defstep INFO (STEP)
  (LET ((otc (make-flag)))
       (THEN@ (INSPECT$ STEP otc)
	      (LISP (pprint otc))))
  "[Practicals Package] Prints out information on the eventual outcome of the application of step"
  "Testing ~A"
  )

;; The test strategy. Uses the 'inspect' helper to analyze step and
;; applies one of the step-* on that account. Note that the glassbox
;; version of this strategy should be used to enable failure in the
;; step-*
(defstep TEST-CASE (STEP STEP-SUCCESS STEP-SUBGOAL STEP-SKIP STEP-BACKTRACK STEP-FAIL) 
  (LET ((otc (make-flag)))
       (TRY
	(TRY (INSPECT$ STEP otc) (FAIL) (SKIP-MSG "[Practicals.test-case1] This shouldn't happen: please report." t))
	(SKIP-MSG "[Practicals.test-case2] This shouldn't happen: please report." t)
	(LET ((res 
	       (cond ((flag-subgoal otc) STEP-SUBGOAL)
		     ((flag-skip otc) STEP-SKIP)
		     ((flag-success otc) STEP-SUCCESS)
		     ((flag-fail otc) STEP-FAIL)
		     ((flag-backtrack otc) STEP-BACKTRACK)
		     (t '(SKIP-MSG "[Practicals.test-case3] This shouldn't occur: please report." t)) ) ))
	     res) )
       )
  "[Practicals Package] Test the result of a step, apply one of the arguments in consequence."
  "Testing ~A"
  )

;; Instances of 'test-case'. Easier to use for end-users.
(defstep TESTSUCCESS (STEP STEP1 STEP2)
  (TEST-CASE$ STEP STEP1 STEP2 STEP2 STEP2 STEP2)
  "[Practicals] Test for success in step."
  "Testing success in ~A"
  )

(defstep TESTSUBGOAL (STEP STEP1 STEP2)
  (TEST-CASE$ STEP STEP2 STEP1 STEP2 STEP2 STEP2)
  "[Practicals] Test for subgoals in step."
  "Testing subgoals in ~A"
  )

(defstep TESTSKIP (STEP STEP1 STEP2)
  (TEST-CASE$ STEP STEP2 STEP2 STEP1 STEP2 STEP2)
  "[Practicals] Test for skip in step."
  "Testing skip in ~A"
  )

(defstep TESTBACKTRACK (STEP STEP1 STEP2)
  (TEST-CASE$ STEP STEP2 STEP2 STEP2 STEP1 STEP2)
  "[Practicals] Test for backtracking in step."
  "Testing backtracking in ~A"
  )

(defstep TESTFAIL (STEP STEP1 STEP2)
  (TEST-CASE$ STEP STEP2 STEP2 STEP2 STEP2 STEP1)
  "[Practicals] Test for failure in step."
  "Testing failure in ~A"
  )


;; ================================================================= Sharp PVS

;; Note that the following strategies are part of the 'sharp' fragment
;; of the strategy language, and therefore we cannot guarantee a
;; result if 'fail' is used instead of the 'throw' mechanism.

;; Nomenclature: 
;; #tactic is a tactic that applies its n>1 th
;; arguments on all of the subgoals previously generated.
;; #tactic@ applies its n>1 th arguments along the main 
;; branch of the proof (only the first of the first of the 
;; subgoals previously generated)

;; Instances of 'FIGURE'. Subsumes the old PROGRESS practical.
(defstrat #IFSUBGOAL (STEP STEP1 STEP2)
  (LET ((otc (make-flag)))
       (TRY (FIGURE$ STEP otc) 
	    STEP1 ;if step1 = fail, #IFSUBGOAL backtracks. Shouldn't happen, though.
	  (IF (flag-backtrack otc)
	      (BACKTRACK)
	    (IF (flag-fail otc)
		(FAIL)
	      (IF (flag-skip otc)
		  STEP2
		  (SKIP-MSG "[Practicals.ifsubgoal] This shouldn't happen: please report." t)
		  ) ) )
	    ) )
  "[Practicals] Applies step. If it generates subgoals, apply step1 to these subgoals, else apply step2"
  )

;; #THEN is an (unbugged) synonym of THEN; it uses 'FIGURE' to monitor the
;; outcome of step1 and then applies step2 if step1 has subgoal'ed or skip'ed.
(defstrat #THEN (STEP1 &rest STEPS)
  (LET ((otc (make-flag))
	(STEP2 (if STEPS 
		   (cons '#THEN STEPS)
		 '(SKIP)
		 )) )
       (TRY (FIGURE$ STEP1 otc) 
	    STEP2	  ;note : if step2 = fail, #THEN backtracks
	    (IF (flag-backtrack otc)
		(BACKTRACK)
		(IF (flag-fail otc)
		    (FAIL)
		    (IF (flag-skip otc)
			STEP2
			(SKIP-MSG "[Practicals.then] This shouldn't happen: please report." t)
			) ) )
	    ) )
  "The sharp-level branching sequence strategy"
  )

;; #BRANCH is to BRANCH what #THEN is to THEN.
(defstrat #BRANCH (STEP STEPLIST)
  (SKIP)
  "The sharp-level branching strategy"
  )

;; == Conditionals and Loops 

;; When evaluates its first argument; if it results in nil then
;; nothing is done and the result of this strategy is a (SKIP). Else
;; the strategy applies the following steps to all subgoals in
;; sequence.
(defstrat #WHEN (term &rest STEPS)
  (LET ((trm (eval term)))
       (IF (and trm STEPS)
	   (LET ((STEP (cons '#THEN STEPS)))
		STEP)
	   (SKIP)))
  "[Practicals Package] Applies the steps if the term is non nil, skip else.
 (<when# flag step1 ... stepn) is an abbreviation for 
 (if flag (<then# step1 .. stepn) (skip))."
  )

;; When evaluates its first argument; if it results in nil then
;; nothing is done and the result of this strategy is a (SKIP). Else
;; the strategy applies the following steps in sequence to the main
;; branch of the proof.
(defstrat #WHEN@ (term &rest STEPS)
  (LET ((trm (eval term)))
       (IF (and trm STEPS) 
	   (LET ((STEP (cons 'THEN@ STEPS)))
		STEP)
	   (SKIP)))
  "[Practicals Package] Applies the steps if the term is non nil, skip else. This is an 
 abbreviation for (if flag (then@ step1 .. stepn) (skip))."
  )

;; This strategy repeats a list of steps along the main proof branch,
;; while a given lisp condition holds.
(defstrat #WHILE@ (term &rest STEPS)
  (REPEAT (#WHEN@ term STEPS))
  "[Practicals Package] Repeat the arguments while a lisp condition holds. The iteration takes
 place along the main proof branch (repeat)."
  )

;; This is the same as the (while...) tactical, but repeats its
;; arguments along all branches.
(defstrat #WHILE (term &rest STEPS)
  (REPEAT* (#WHEN term STEPS))
  "[Practicals Package] Repeat the arguments while a lisp condition holds. The iteration takes
 place along all branches (repeat*)."
  )

(defstrat #FOR (n STEP)
  (IF (or (not (numberp n)) (= n 0))
      (SKIP)
      (IF (< n 0) (REPEAT STEP)
	  (LET ((m (- n 1)))
	       (#THEN STEP
		     (FOR m STEP)))))
  "[Practicals Package] Repeats N times STEP, or until it does nothing if N < 0, in all the branches."
  )

(defstrat #FOR@ (n STEP)
  (IF (or (not (numberp n)) (= n 0))
      (SKIP)
      (IF (< n 0) (REPEAT@ STEP)
	  (let ((m (- n 1)))
	    (THEN@ STEP
		   (FOR m STEP)))))
  "[Practicals Package] Repeats N times STEP, or until it does nothing if N < 0, in the main branch."
  )

;; == Exception Handling

;; This is a named fail. The strategy backtracks and sets the global
;; variable *error-tag* to its given value. 
(defstrat #THROW (tag) 
  (let ((dy (setq *error-tag* tag)))
    (BACKTRACK) ) 
  "[Practicals Package] Throw a named error."
  )

;; Catch is the counterpart of the (throw...) strategy. It evaluates
;; its first argument; if the result is an exception or a named
;; exception which tag corresponds to the argument provided, then it
;; returns (STEP2). If the tag does not correspond to the name of the
;; exception, then it is propagated. If the tag is nil (or
;; unspecified) then all errors are caught.
(defstrat #CATCH (STEP1 &optional (tag nil) (STEP2 (SKIP)))
  (LET ((otc (make-flag)))
       (TRY (FIGURE$ STEP1 otc)
	    (SKIP)			; step was a subgoal
	    (IF (flag-backtrack otc)
		(IF (or (not tag) (equal *error-tag* tag))
		    (LET ((dy (setq *error-tag* nil))) STEP2) ;catch the exception
		    (BACKTRACK))	;propagate the exception
		(IF (flag-fail otc)
		    (SKIP-MSG "[Practicals.catch] Unexpected fail here. Make sure you are not using the pvs (FAIL) rule, if this is not the case please report." T)
		    (IF (flag-skip otc)
			(SKIP)
			(SKIP-MSG "[Practicals.catch] This shouldn't happen: please report." t))))
	    )
       )
  "[Practicals Package] Catch a named error. If the error with name 'tag' is catched then execute step2."
  )

;; Example of exception programming --this is actually a synonym of
;; #ifsubgoal...
(defstep PROGRESS? (STEP STEP-PROGRESS STEP-SKIP)
  (#CATCH (#CATCH (#IFSUBGOAL STEP (#THROW "sg") (#THROW "skorbt"))
		  "sg"
		  STEP-PROGRESS )
	  "skorbt"
	  STEP-SKIP
	  )
  "[Practicals Package] Test case for #-programming."
  "Testing progress"
  )

;;; == First to apply / to solve 

(defstrat #FIRST (SLIST) 
  (#WHEN@ 'SLIST
	  (LET ((STEP1 (car SLIST))
		(NEWSLIST (cdr SLIST)))
	       (#CATCH STEP1 nil (#FIRST NEWSLIST)))
	  )
  "[Practicals Package] Applies the first tactic that does not throw an exception."
  )

(defstrat #SOLVE (SLIST)
  (#WHEN@ 'SLIST
	  (LET ((STEP1 (car SLIST))
		(NEWSLIST (cdr SLIST)))
	       (#CATCH (#THEN STEP1 (#THROW "exn"))
		       "exn"
		       (#SOLVE newsList) )
	       )
	  )
  "[Practicals Package] Applies the first tactic that solves the current goal"
  )


;;; ========================================================= Pattern matching

(defstruct abstract-pattern 
  "[Practicals Package] This is the structure filled in by the sequent pattern parsing function."
  (antecedent nil)
  (consequent nil)
  (step nil)
  )

;; Parse a pattern such as (A \- B -> (C)) into an abstract pattern construct.
;; Flag indicates the position in the pattern (0 is the antecedent, 1 the
;; consequent, 2 the tactic).
(defun parse-screen-item (in-list)
  (let ((result (make-abstract-pattern)))
    (defun parse-screen-item-rec (in-list symbol-flag)
      (let ((in-list-elt (car in-list)))
	(cond
	 ((null in-list)
	  (write-string "[Practicals.screen] Syntax error in pattern: ill-formed pattern. You need to specify at least \"-> (STEP)\""))
	 ((find in-list-elt *thesis-symbol*) 
	  (if (< symbol-flag 1) 
	      (parse-screen-item-rec (cdr in-list) 1)
	    (print "[Practicals.screen] Syntax error in pattern: too many /-'s.") ) )
	 ((find in-list-elt *do-symbol*)
	  (if (< symbol-flag 2)
	      (parse-screen-item-rec (cdr in-list) 2) 
	    (print "[Practicals.screen] Syntax error in pattern: too many ->'s.") ) )
	 ((eql symbol-flag 0)
	  (setf (abstract-pattern-antecedent result) 
		(append (abstract-pattern-antecedent result) (list in-list-elt)))
	  (parse-screen-item-rec (cdr in-list) symbol-flag) )
	 ((eql symbol-flag 1)
	  (setf (abstract-pattern-consequent result) 
		(append (abstract-pattern-consequent result) (list in-list-elt)))
	  (parse-screen-item-rec (cdr in-list) symbol-flag) )
	 ((eql symbol-flag 2)
	  (setf (abstract-pattern-step result) in-list-elt) 
	  result )
	 (t (print "[Practicals.screen] Syntax error in pattern: this is a bug. Please report."))
	 ) ) )	
    (parse-screen-item-rec in-list 0) ) )

;; Flatten a list of abstract pattern constructs into a Manip-compatible list
;; (((- A) (+ B) step (C)) ... ((- An) (+ Bn) step Cn)
(defun make-spec-item (ap)
  (let ((ante (abstract-pattern-antecedent ap))
	(conse (abstract-pattern-consequent ap))
	(stp (abstract-pattern-step ap)))
    (cond ((and (null ante) (null conse))
	   (list "%"
		 'step
		 stp) )
	  ((null ante) 
	   (list (append '(+) conse)
		 'step
		 stp) )
	  ((null conse) 
	   (list (append '(-) ante)
		 'step
		 stp) )
	  (t 
	   (list (append '(-) ante)
		 (append '(+) conse)
		 'step
		 stp) ))))

;; Parse a list of patterns into a list of spec items
(defun format-screen-items (in-list)
  (mapcar #'make-spec-item (mapcar #'parse-screen-item in-list))
  )

;; This function does the actual job of SCREEN: parse the arguments, do the
;; matching, and the correct instantiation of the corresponding step. This
;; heavily relies on the syntactic matching functions defined by the Manip
;; package.
(defun screen-syntax-step (spec-items print-flag)
  (let* ((match-items (parse-match-items (car spec-items))) ;Manip function
	 (error-msg (match-items-error-msg match-items))
	 (action-targets-steps (match-items-action-targets-steps match-items))
	 (next-spec-items (cdr spec-items)))
    (if error-msg
	(gen-prac-response 'screen (format nil "~A~%" error-msg))
      (let* ((fnum-patterns (normalize-patterns match-items)) ;Manip function
	     (vars-instances-fnums (match-instances fnum-patterns))) ;Manip function
	(cond ((>= (length (cadr vars-instances-fnums))
		   (length fnum-patterns))
	       (if print-flag
		   `(match-syntax-show$ ,@vars-instances-fnums
					,@action-targets-steps) ;Manip function
		 (apply #'match-syntax-rule 	;Manip function
			(append vars-instances-fnums action-targets-steps))))
	      ((consp next-spec-items) 
	       (match-syntax-step2 next-spec-items print-flag))
	      (t (gen-prac-response 'screen 
				    (format nil "No pattern matches found.~%") 
		  )))))))

;; The strategy is pretty much just a function call.
(defstep SCREEN (args &optional (print-only? nil))
  (let ((spec-list (format-screen-items args))
	(step (screen-syntax-step spec-list print-only?)) )
    step)
  "[Practicals Package] Matches the current proof sequent against one or more sequent patterns, and applies the proof step that is associated with the first matching pattern."
  "~%Screening..."
  )