AlecsFerra

{-# LANGUAGE GADTs #-}

{-@ LIQUID "--ple"           @-}
{-@ LIQUID "--etabeta"       @-}
{-@ LIQUID "--reflection"    @-}
{-@ LIQUID "--dependantcase" @-}

module ExprCompiler where

import Language.Haskell.Liquid.ProofCombinators

AlecsFerra

-- Implementation in LH of Calculating Dependently-Typed Compilers
-- https://people.cs.nott.ac.uk/pszgmh/well-typed.pdf

{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

{-@ LIQUID "--ple"               @-}
{-@ LIQUID "--reflection"        @-}
{-@ LIQUID "--max-case-expand=4" @-}

AlecsFerra

Local Definitions Proposal

The Issue

Suppose we are working with the following Liquid Haskell code:

{-@ LIQUID "--ple" @-}
{-@ LIQUID "--reflection" @-}

AlecsFerra

// Implementation in LH of A correct-by-construction conversion from lambda calculus to combinatory logic
// https://webspace.science.uu.nl/~swier004/publications/2023-jfp.pdf

{-# Language GADTs #-}

{-@ LIQUID "--reflection"        @-}
{-@ LIQUID "--ple"               @-}
{-@ LIQUID "--full"              @-}
{-@ LIQUID "--max-case-expand=4" @-}
{-@ LIQUID "--etabeta"           @-}

AlecsFerra

nix-shell -p "python3.withPackages (ps: with ps; [ dbus-python distro ])" --run "python3 <your-eduroam.py>"

AlecsFerra

#! /usr/bin/env python3

# flatten.py
# Copyright (C) 2024 Alessio Ferrarini <github.com/alecsferra>
# 
# This program is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
# 

AlecsFerra

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Data (Proxy (Proxy))
import Data.Kind (Type)
import Text.Printf (printf)

AlecsFerra

module AxiomK where

open import Relation.Binary.PropositionalEquality using (_≡_)
open _≡_

-- All the equality proofs are the same ⁾
-- Unless we use the `--without-K` option ⁾
same-≡ : ∀ {l} {A : Set l} {a b : A} → (p₁ p₂ : a ≡ b) → p₁ ≡ p₂
same-≡ refl refl = refl

AlecsFerra

module RewriteAbuse where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p rewrite (sym (+-assoc m n p))
             |       (+-comm m n)
             |       (+-assoc n m p)

AlecsFerra

;; Some proofs about pairs
;; ∀ a b c. a = b → (a, c) = (b, c)
(claim a=b→ac=bc
  (Π ([T U]
      [K U]
      [a T]
      [b T]
      [c K]
      [_ (= T a b)])
    (= (Pair T K) (cons a c) (cons b c))))