pedrominicz

:- ensure_loaded(library(aggregate)).

% Generate typable SK-combinator calculus terms of a given size.
%
% Based on Paul Tarau's paper A Hiking Trip Through the Orders of Magnitude:
% Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal
% Forms.
%
% The paper:
% https://arxiv.org/pdf/1608.03912.pdf

pedrominicz

{-# OPTIONS_GHC -Wno-type-defaults #-}

module CountSK where

import Memo

import Data.Foldable

data Term = S | K | App Term Term

pedrominicz

:- ensure_loaded(library(apply)).
:- ensure_loaded(library(random)).

:- set_prolog_flag(optimise, true).
:- set_prolog_flag(optimise_unify, true).

% Randomly generate simply-typed lambda calculus terms using Boltzmann
% samplers.
%
% Based on the paper Random generation of closed simply-typed λ-terms: a

pedrominicz

:- ensure_loaded(library(aggregate)).
:- ensure_loaded(library(lists)).

% Generate simply-typed lambda calculus terms of a given size.
%
% Based on Paul Tarau's paper A Hiking Trip Through the Orders of Magnitude:
% Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal
% Forms.
%
% The paper:

pedrominicz

{-# OPTIONS_GHC -Wno-type-defaults #-}

module Count where

import Memo

import Data.Foldable

-- Based on section 3.1 of the paper Generating Random Lambda Calculus Terms by
-- Jue Wang.

pedrominicz

module Memo where

import Data.IORef
import System.IO.Unsafe
import qualified Data.Map as M

memoIO :: (Ord a) => (a -> b) -> IO (a -> IO b)
memoIO f = do
  v <- newIORef M.empty
  return $ \x -> do

pedrominicz

import logic.equiv.basic

universes u v

section

parameters {l r : Type u}

mutual inductive P₁, P₂ (l r : Type u)
with P₁ : Type u

pedrominicz

{
module Lex where

import Data.Bits
import Data.Char
import Data.Word

import Data.Text (Text)
import qualified Data.Text as T
}

pedrominicz

{
module Lex where
}

%wrapper "basic"

tokens :-
  $white+       ;
  [^ $white]+   { id }

pedrominicz

{
module Lazy where

import Data.ByteString (ByteString)
import qualified Data.ByteString.Lazy as B
}

%wrapper "monadUserState-bytestring"

$alpha = [A-Za-z]