Add fix for issue SRI-CSL/PVS#68.

pvs-patches/patch-20191217-fix-14.lisp

@@ -0,0 +1,71 @@
+;; Provided by Shankar
+(defmethod typecheck* ((decl def-decl) expected kind arguments)
+  (declare (ignore expected kind arguments))
+  (typecheck* (formals decl) nil nil nil)
+  (set-formals-types (apply #'append (formals decl)))
+  (let* ((*bound-variables* (apply #'append (formals decl)))
+     (rtype (let ((*generate-tccs* 'none))
+          (typecheck* (declared-type decl) nil nil nil)))
+     (*recursive-subtype-term* nil))
+    (set-type rtype nil);;NSH(12/17/19): was (defined-type decl)
+                        ;;same fix as const-decl
+    (setf (type decl)
+      (make-formals-funtype (formals decl) rtype))
+    (assert (fully-instantiated? (type decl)))
+    #+pvsdebug (assert (null (freevars (type decl))))
+    (check-duplication decl)
+    (unless (funtype? (find-supertype (type decl)))
+      (type-error decl "Recursive definition must be a function type"))
+    (unless (typep decl 'adt-def-decl)
+      (typecheck-measure decl)
+      (assert (fully-instantiated? (measure decl)))
+      (setf (recursive-signature decl) (compute-recursive-signature decl)))
+    ;;(assert (null (freevars (recursive-signature decl))))
+    (set-nonempty-type rtype decl)
+    (put-decl decl)
+    (let ((*tcc-conditions* (add-formals-to-tcc-conditions (formals decl)))
+      (*added-recursive-defn-conversions* nil))
+      ;; See check-set-type-recursive-operator for how recursive conversions
+      ;; are generated.
+      (typecheck* (definition decl) rtype nil nil)
+      (when *added-recursive-defn-conversions*
+    (remove-recursive-defn-conversions *added-recursive-defn-conversions*)
+    (mapobject #'(lambda (ex) (progn (when (typep ex '(or expr type-expr))
+                       (setf (free-variables ex) 'unbound))
+                     nil))
+           (definition decl))))
+    (assert (fully-instantiated? (definition decl)))
+    (check-positive-types decl)
+    (make-def-axiom decl))
+  decl)
+
+(defmethod typecheck* ((decl fixpoint-decl) expected kind arguments)
+  (declare (ignore expected kind arguments))
+  (typecheck* (formals decl) nil nil nil)
+  (set-formals-types (apply #'append (formals decl)))
+  (let* ((*bound-variables* (apply #'append (formals decl)))
+     (*tcc-conditions* (add-formals-to-tcc-conditions (formals decl)))
+     (rtype (let ((*generate-tccs* 'none))
+          (typecheck* (declared-type decl) nil nil nil))))
+    (set-type rtype nil);;NSH(12/17/19): same fix as const-decl/def-decl
+    (setf (type decl)
+      (make-formals-funtype (formals decl) rtype))
+    (check-duplication decl)
+    (unless (funtype? (find-supertype (type decl)))
+      (type-error decl "(Co)Inductive definition must be a function type"))
+    (unless (tc-eq (find-supertype (range* (type decl))) *boolean*)
+      (type-error decl
+    "(Co)Inductive definitions must have (eventual) range type boolean"))
+    (set-nonempty-type rtype decl)
+    (put-decl decl)
+    (typecheck* (definition decl) rtype nil nil)
+    (let* ((all-vars (ind-def-formals decl))
+       (fixed-vars (fixed-inductive-variables decl all-vars))
+       (rem-vars (remove-if #'(lambda (avar) (memq avar fixed-vars))
+               all-vars))
+       (pred-type (inductive-pred-type decl fixed-vars)))
+      (check-inductive-occurrences decl pred-type fixed-vars rem-vars)
+      (make-def-axiom decl)
+      (make-inductive-def-inductions decl pred-type fixed-vars rem-vars))
+    (check-positive-types decl))
+  decl)