VictorTaelin

Implement a λ-Term named `rotL` that, when applied to a function F, a Church Nat
N, and a Church N-Tuple, returns the same Church N-Tuple, but with elements
shifted left. In other words, create a generic 'rotL<N,F,t>' function for
N-tuples. Example:
- (rotL λf.λx.(f (f x))     λt.(t 1 2))   == λt.(t 2 1)
- (rotL λf.λx.(f (f (f x))) λt.(t 1 2 3)) == λt.(t 2 3 1)
Your final answer must be a λ-Term that implements `rotL` correctly, as follows:
@rotL = term_here

NOTE: Don't omit parenthesis. Each application requires them. Example:

VictorTaelin

module Main where

import Unsafe.Coerce (unsafeCoerce)

data Term
  = App Term Term
  | Var String
  | Ct0
  | Ct1 Term
  | Ct2 Term Term

VictorTaelin

{-# LANGUAGE MultilineStrings #-}

import Data.IORef
import Debug.Trace
import System.IO.Unsafe
import Text.ParserCombinators.ReadP
import qualified Data.Map as M

type Lab   = String
type Name  = String

VictorTaelin

{-# LANGUAGE MultilineStrings #-}

import Data.IORef
import Debug.Trace
import System.IO.Unsafe
import Text.ParserCombinators.ReadP
import qualified Data.Map as M

type Lab   = String
type Name  = String

VictorTaelin

TIMELINE DE EVENTOS:

000000000011111                                                                   
012345678901234                                                                   
____d_D____d_D____________________________________________________________________ A
     \ \  / /                                                                      
      \ \/ /                                                                       
_______\/\/_______________________________________________________________________ Server
        \ \                                                                         
         \ \                                                                        

VictorTaelin

// Enumerating Binary Trees with 1 label
// -------------------------------------

data Tree { #L #N{a b} }

// Recursive: requires label forking

@sp0(x) = (+ 0 (* x 2))
@sp1(x) = (+ 1 (* x 2))

VictorTaelin

// https://github.com/MaisaMilena/kaelin/blob/db1eff57aaca6d0936e1a9210da0855c5d17d45a/formality/stdlib/kaelin.fmc

// ## Kaelin
// 
// A simple, blockhain-enabled MOBA implemented in Formality-Core.
// 
// Kaelin aims to capture some of the spirit of a MOBA, inluding map awareness,
// micro and macro strategies, resource control, team-fights, skillshots and so
// on, while aiming blockchain-compatible by being very lightweight (the entire
// game state has only 8192 bits) and based on ~20 second turns. This allows it

VictorTaelin

# ./HVM.hs #

# HVM

HVM is functional language and prover based on the Interaction Calculus.

It is a pure functional runtime like Haskell's GHC, with some peculiarities:
- Variables are affine, meaning they can only occur, at most, once.
- To copy values, linear thunks are used, where 2 vars refer to the same value.
- Accessing a thunk triggers an incremental, layer-by-layer copy of the value.

VictorTaelin

#include <ctype.h>
#include <stdbool.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

typedef struct {
  const char* input;
  size_t index;

VictorTaelin

-- TASK: create a Parser for Kind7.
-- - don't be inventive, just use a simple approach that is guaranteed to work
-- - keep it simple and idiomatic
-- - include nice error messages

-- On the 'parseApp parser:
-- - support (f x y z) as an alias to (((f x) y) z)
-- - do so by parsing '(', then terms until you hit a ')', then foldl to build the App

-- Note on operators: