bmmoore

Set Implicit Arguments.
Unset Strict Implicit.

(*
The first example from the paper
"How to make ad hoc proof automation less ad hoc",
don't work as expected with the non-ssreflect apply.
 *)

(* The example works over separation logic heaps

bmmoore

(* Attempting to generalize the Gallina side of rtauto over the logic *)

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)

bmmoore

Require Import String.
Require Import ZArith.
Require Import imp.

Local Open Scope Z.
Import List.ListNotations.
Local Open Scope list.
Local Open Scope string.

(** An execution trace is a sequence of zero or more steps.

bmmoore

import java.util.ArrayDeque;
import java.util.Deque;

class Test {
  static final int LIMIT = 10000;
  static final int BATCH = 100;
  static final int ITERS = 1000;
  public static void main(String[] args) {
    for (int i = 0; i < 20000; ++i) {
       testDLL();

bmmoore

diff no-error_kool-untyped.k error_kool-untyped.k
534c534
< /*   */
---
> 

bmmoore

{-# LANGUAGE
  MultiParamTypeClasses,
  TypeFamilies #-}

class Field f where
  type FType f :: *

class (Field field) => Has field o where
  get :: field -> o -> FType field

bmmoore

(defn repeated-until* [element done]
  (reify
    Reader
    (read-bytes [this b]
      (loop [b b, result []]
        (let [[success x b] (read-bytes element b)]
          (if success
            (if (= x done)
              [true result b]
              (recur b (conj result x)))

bmmoore

; using clojure.tools.macro

(defmacro mu [self body]
  `(let [self# (promise)
         impl# (symbol-macrolet [~self @self#] ~body)]
     (deliver self# impl#)
     impl#))

bmmoore

(def empty-frame (compile-frame []))

(defn repeated-until [element done]
  (let [element* (compile-frame element (fn [v] (if (nil? v) done)) (fn [v] (if (= v done) nil v)))
        self (promise)
        impl (header element* (fn [elt] (if (nil? elt) empty-frame (compile-frame @self rest (partial cons elt)))) first)]
    (deliver self impl)
    impl))

bmmoore

{-# OPTIONS --universe-polymorphism #-}
module match where
open import Data.List hiding (or)
open import Category.Monad
open import Category.Functor
open import Function
open import Data.Maybe
open import Data.Bool
open import Data.Nat
open import Relation.Binary.PropositionalEquality