gallais

{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds      #-}

import Data.Constraint
import Data.Function

gallais

module Zippy where

data Desc : Set₁ where
  `σ : (A : Set) (d : A → Desc) → Desc
  `r : Desc → Desc
  `q : Desc

open import Size
open import Data.Unit
open import Data.Product

gallais

module Printf

import Lightyear.Char
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings

%access public export
%default total

gallais

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE ScopedTypeVariables  #-}
-- We need undecidable instances for the definition of @Foldr@,
-- and @Domains@ and @CoDomain@ using @If@ for instance.

gallais

module Subst1 where
open import Term

infixl 20 _-_
_-_ : {σ : Ty} → (Γ : Con) → Var Γ σ → Con
ε - ()
(Γ , σ) - vz = Γ
(Γ , τ) - vs x = (Γ - x) , τ

gallais

record Default {ℓ} (A : Set ℓ) (a : A) : Set ℓ where
  constructor _!
  field value : A

instance

  default : ∀ {ℓ} {A : Set ℓ} a → Default A a
  default a = record { value = a }

open import Agda.Builtin.Nat

gallais

open List

let bind (xs : 'a list) (f : 'a -> 'b list) : 'b list =
  concat (map f xs)

let rec parts : 'a list -> 'a list list list = function
  | []      -> [[]]
  | [c]     -> [[[c]]]
  | c :: cs ->
    bind (parts cs) (fun (p :: ps) ->

gallais

module Compiled-252 where

data U : Set where
  z : U
  s : U → U

{-# IMPORT Compiled.URaw #-}
{-# COMPILED_DATA U Compiled.URaw.U Compiled.URaw.Z Compiled.URaw.S #-}

gallais

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds      #-}
{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE RankNTypes     #-}

module ModularParser3 where

import Data.Function

gallais

{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}