jonsterling

{-# OPTIONS --type-in-type --cubical --rewriting --confluence-check #-}

module stc-playground where

open import Cubical.Foundations.Prelude
open import Agda.Builtin.Equality renaming (_≡_ to _≣_)
open import Agda.Builtin.Equality.Rewrite
open import Agda.Primitive

jonsterling

\RequirePackage{expl3}
\RequirePackage{xparse}

\ProvidesExplPackage {namespace} {2020/08/31} {0.1} {Compositional namespaces for labels}

\tl_new:N \l_ns_stk

\cs_new:Npn \ns_push:n #1 {
  \tl_put_right:Nn \l_ns_stk {#1}
  \tl_put_right:Nn \l_ns_stk {/}

jonsterling

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

jonsterling

\RequirePackage{expl3}
\RequirePackage{xparse}
\RequirePackage{ebproof}

%% This package is an extension and modification of code by Emmanuel Beffara

\ExplSyntaxOn

\cs_new_protected:Npn \__formulas_split: {
  $\hskip 1em plus 1fil$\displaystyle

jonsterling

\section{Focused Sequent Calculus}

Focused sequent calculus has several class of proposition\footnote{We are
writing $\Neg{a},\Pos{a}$ for negative and positive atoms respectively. You may
also see these written as $\Neg{P},\Pos{P}$.} and context. We summarize them
below, noting that $\Pos{\Omega}$ ranges over ordered lists, whereas $\Gamma$
ranges over multisets:
\begin{grammar}
  negative & \Neg{A} &

jonsterling

Core RedML is (so far) a one-sided, polarized L calculus in the style of Curien-Herbelin-Munch. 
Lambda calculus can be compiled to Core RedML through a bunch of gnarly macros. For instance, the term

    (((lam [x] (lam [y] (pair x y))) nil) nil)
    
should evaluate to a pair of nils. This term is compiled into Core RedML as the first stage of the following
computation trace, which shows how it computes to the desired pair.
    

State: (cut

jonsterling

 Flat profile:

Each sample counts as 0.01 seconds.
  %   cumulative   self              self     total           
 time   seconds   seconds    calls  ms/call  ms/call  name    
 25.18      1.76     1.76     2415     0.73     0.85  mark_slice
 10.44      2.49     0.73  4193520     0.00     0.00  camlHashtbl__insert_bucket_1371
  9.87      3.18     0.69  6306936     0.00     0.00  camlHashtbl__add_1385
  7.73      3.72     0.54 67916414     0.00     0.00  caml_page_table_lookup
  5.87      4.13     0.41     4771     0.09     0.21  caml_empty_minor_heap

jonsterling

open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where

----------------------------------------------------------------------

add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)

jonsterling

[0.066684s] Checked test/success/V-types.prl
[0.022747s] Checked test/success/bool-fhcom-without-open-eval.prl
[0.009820s] Checked test/success/bool-pair-test.prl
[0.010696s] Checked test/success/dashes-n-slashes.prl
[0.009144s] Checked test/success/decomposition.prl
[0.006263s] Checked test/success/discrete-types.prl
[0.013531s] Checked test/success/empty.prl
[0.009508s] Checked test/success/equality-elim.prl
[0.017783s] Checked test/success/equality.prl
[0.017168s] Checked test/success/fcom-types.prl

jonsterling

Nuprl_functional = 
λ _top_assumption_ : nat,
(λ (_evar_0_ : (λ n : nat, matrix_functional (Nuprl n)) 0)
 (_evar_0_0 : ∀ n : nat, (λ n0 : nat, matrix_functional (Nuprl n0)) (S n)),
 match
   _top_assumption_ as n
   return ((λ n0 : nat, matrix_functional (Nuprl n0)) n)
 with
 | 0 => _evar_0_