lenary

{-# OPTIONS --copatterns #-}

open import Agda.Builtin.Nat

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} → A → Vec A n → Vec A (suc n)

record Stream (A : Set) : Set where
  coinductive

lenary

$ racket -iq -e "(require rosette)"
Welcome to Racket v6.4.
> (define (foo) identity)
> foo
#<procedure:foo>
> identity
#<procedure:identity>
> ((foo) 3)
free-identifier=?: contract violation
  expected: identifier?

lenary

module UTLC

-- This is a terrible implementation of the Untyped Lambda Calculus,
-- using the semantics from Fig 5-3 in TAPL, amended using the changes
-- proposed in Chapter 6 of TAPL, associated with the deBruijn
-- indices.

-- This gives us the `Fin n` datatype, which is the numbers from 0 up
-- to (but not including) n. So, `Fin 0` has no inhabitants; `Fin 1`
-- has one inhabitant, namely 0; and `Fin 2` has two inhabitants,

lenary

module UTLC where

open import Data.String

Var : Set
Var = String

-- Untyped Lambda Calculus:

-- Terms:

lenary

%% So you have an aribtrary function, like so

f(A,B,C) ->
  A + B + C.


%% We want something that can be more helpful for sectioning/partial application. 
%% What about transforming that thing above to the following:

lenary

I'm currently writing an Erlang backend for the Idris compiler. Right now I've got to the internally "primitive" operations, and would like to see an increased reliance on compiling to these primitives in the Prelude rather than using the foreign function calls that are currently used.

This would probably be a breaking change for lots of backends, so I thought I'd propose it before making any major code changes.

I'm willing to do all these changes to the C and conventional backends, I'd just like to run the idea of them past a few set of eyes before I start.

Some background:

The list of current primitives (over 70) is in Lang.hs below. They cover a wide variety of functionality, most of which is mathematical operations, but there's some more important stuff about I/O: LPrintNum, LPrintStr, LReadStr, LStdIn, LStdOut, LStdErr.

lenary

Preprocessing executable 'idris-erlang' for idris-0.9.14.2...
[2 of 2] Compiling Main             ( codegen/idris-erlang/Main.hs, dist/build/idris-erlang/idris-erlang-tmp/Main.o )
Linking dist/build/idris-erlang/idris-erlang ...

lenary

Resolving dependencies...
[1 of 1] Compiling Main             ( /var/folders/kf/wlmqhdfs665cq2t28q42zx6m0000gn/T/idris-0.9.14.3-20303/idris-0.9.14.3/dist/setup/setup.hs, /var/folders/kf/wlmqhdfs665cq2t28q42zx6m0000gn/T/idris-0.9.1
4.3-20303/idris-0.9.14.3/dist/setup/Main.o )
Linking /var/folders/kf/wlmqhdfs665cq2t28q42zx6m0000gn/T/idris-0.9.14.3-20303/idris-0.9.14.3/dist/setup/setup ...
Configuring idris-0.9.14.3...
rm -f idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o idris_opts.o idris_stats.o mini-gmp.o idris_stdfgn.o idris_net.o libidris_rts.a
fatal: Not a git repository (or any of the parent directories): .git
Generating dist/build/autogen/Version_idris.hs for release
Building idris-0.9.14.3...
Preprocessing library idris-0.9.14.3...

lenary

Idris> :l VerifiedNatLattice.idr
Type checking ./VerifiedNatLattice.idr
VerifiedNatLattice.idr:6:10:
When elaborating type of Prelude.Algebra.Nat instance of Prelude.Algebra.VerifiedBoundedJoinSemilattice, method boundedJoinSemilatticeBottomIsBottom:
Can't resolve type class BoundedJoinSemilattice B
Metavariables: Nat instance of Prelude.Algebra.VerifiedBoundedJoinSemilattice

lenary

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Int) -> GCounter

gcjoin : GCounter -> GCounter -> GCounter
gcjoin l r = (MkGCounter ((value l) + (value r)))