Lysxia

module CoDebruijn where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)

data Context : Set where
  O : Context
  1+_ : Context → Context

data Singleton : Context → Set where

Lysxia

#!/usr/bin/env cabal
{- cabal:
build-depends:
  base,
  generic-data
-}

{-# LANGUAGE ScopedTypeVariables, TypeApplications, DeriveGeneric, FlexibleContexts, UndecidableInstances, ConstraintKinds, DerivingVia #-}

import GHC.Generics (Rep, Generic)

Lysxia

-- Algebraic effects using threads

{-# LANGUAGE BlockArguments, GADTs, RankNTypes, EmptyCase, LambdaCase #-}
import Control.Concurrent
import Control.Applicative
import Control.Monad

-- Free monad as a threaded computation
-- The `forall` guarantees that `Return` can't be emitted in the middle of
-- a computation, only at the end, in a wrapper defined by `interpret`.

Lysxia

(* The SC monad (a hybrid of continuation and selection monads), monad laws, and a monad morphism from S (the selection monad) *)

Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Strict Implicit.

Record SC (s a : Type) := MkSC {
  runS : (a -> s) -> a;
  runC : (a -> s) -> s }.

Lysxia

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}

Lysxia

{-# LANGUAGE
  AllowAmbiguousTypes,
  DeriveGeneric,
  EmptyCase,
  TypeOperators,
  FlexibleInstances,
  FlexibleContexts,
  MultiParamTypeClasses,
  PolyKinds,
  TypeApplications,

Lysxia

#![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]

use ::std::vec;

extern crate creusot_contracts;
use creusot_contracts::*;

#[requires([email protected]() == n@)]
#[ensures(result ==> exists<i0: Int> exists<j0: Int> 0 <= i0 && i0 < j0 && j0 < n@ && t@[i0] == t@[j0])]
#[ensures(!result ==> forall<i0 : Int> forall<j0 : Int> 0 <= i0 && i0 < n@ && i0 < j0 && j0 < n@ ==> t@[i0] != t@[j0])]

Lysxia

From Coq Require Import List.

Fixpoint map_In {A B : Type} (xs : list A) : (forall x, In x xs -> B) -> list B :=
  match xs return (forall x, In x xs -> B) -> list B with
  | nil => fun _ => nil
  | cons x xs' => fun f => cons (f x (or_introl eq_refl)) (map_In xs' (fun x' In_x'_xs' => f x' (or_intror In_x'_xs')))
  end.

Lysxia

{-# LANGUAGE
  RankNTypes,
  TypeOperators #-}

-- | User-defined handlers.

module Bluefin.Handlers
  ( Sig
  , Handler
  , with

Lysxia

(* formalization attached to my answer to https://cstheory.stackexchange.com/questions/53855/can-we-use-relational-parametricity-to-simplify-the-type-forall-a-a-to-a *)
From Coq Require Import Lia.

Definition U : Type := forall A : Type, ((A -> A) -> A) -> A.

(* Try enumerating solutions by hand. After the initial [intros],
   we can either complete the term with [exact xi],
   or continue deeper with [apply f; intros xi]. *)
Goal U.
Proof.