{-# OPTIONS --without-K #-}
open import foundation.functions using (_∘_)
open import foundation.identity-types using (refl; ap) renaming (Id to _≡_)
We think of contexts as snoc lists of types
{-# OPTIONS --without-K #-} | |
import Relation.Binary.PropositionalEquality as Eq | |
open Eq using (_≡_; refl) | |
pattern erefl x = refl {x = x} | |
--- path induction --- | |
J : ∀ {A : Set} → |
%{ | |
(** the [Surface] module contains our AST. *) | |
open Surface | |
(** exception raised when a [nonempty_list] returns an empty list. *) | |
exception EmptyUnfolding | |
(** desugars `(x y z : a) -> b` into `(x : a) -> (y : a) -> (z : a) -> b`. *) | |
let rec unfoldPi (xs : string list) (dom : expr) (cod : expr) : expr = | |
match xs with |
{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-} | |
{- | |
(compiled with GHC 9.4.2) | |
-} | |
{- | |
HEADS UP | |
this is an example implementation of a non-trivial type system using bidirectional type checking. | |
it is... |
(* language definition *) | |
type nom = string | |
type bop = Add | Sub | Mul | |
type typ = | |
| Int | Arrow of typ * typ | Meta of meta | |
and meta = meta_state ref | |
and meta_state = | |
| Solved of typ | |
| Unsolved of nom (* keep name for pretty printing *) |
module natcomp where
open import Data.Nat using (ℕ; _+_)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Properties using (++-assoc)
open import Data.Maybe using (Maybe; just; nothing; _>>=_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open Relation.Binary.PropositionalEquality.≡-Reasoning
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} | |
{-# HLINT ignore "Use list comprehension" #-} | |
import Data.IORef ( IORef, newIORef, readIORef, writeIORef ) | |
import GHC.IO ( unsafePerformIO ) | |
import Control.Applicative ( Alternative(..) ) | |
import Control.Monad ( when ) | |
import Debug.Trace | |