osa1

import Prelude.Vect

%default total

sumPairs : Vect (S n) Nat -> Vect n Nat
sumPairs (h1 :: h2 :: tl) = (h1 + h2) :: sumPairs (h2 :: tl)
sumPairs [h]              = []

-- try to show how non-top-level pattern matching won't work

osa1

Require Import Omega.
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.VectorDef.
Open Scope vector_scope.
Require Import List.
Require Import Arith.

CoInductive triangle_t (T : Type) : nat -> Type :=
| triangle : forall (n : nat), Vector.t T n -> triangle_t T (S n) -> triangle_t T n.

osa1

Require Import List.
Import ListNotations.
Open Scope list_scope.
Require Import Arith.
Require Import Omega.
Require Import Permutation.

Inductive sorted : list nat -> Prop :=
| Sorted_nil : sorted []
| Sorted_singleton : forall e, sorted [e]

osa1

Require Import List.
Import ListNotations.

Open Scope list_scope.

Inductive semigroup (A : Type) (Op : A -> A -> A) : Prop :=
| Semigroup_intro :
    (forall (a1 a2 a3 : A), Op a1 (Op a2 a3) = Op (Op a1 a2) a3) -> semigroup A Op.

osa1

module Main where

import GHC.Stack

newtype M s a = M { unM :: s -> (s, a) }

instance Monad (M s) where
    (M m) >>= k = M $ \s -> case m s of
                              (s', a) -> unM (k a) s'
    return a = M $ \s -> (s, a)

osa1

diff --git a/src/Compiler/Settings.hs b/src/Compiler/Settings.hs
index 55c3472..f340cee 100644
--- a/src/Compiler/Settings.hs
+++ b/src/Compiler/Settings.hs
@@ -50,3 +50,6 @@ newGhcjsEnv = GhcjsEnv <$> newMVar M.empty
 buildingDebug :: DynFlags -> Bool
 buildingDebug dflags = WayDebug `elem` ways dflags
 
+buildingProf :: DynFlags -> Bool
+buildingProf dflags = WayProf `elem` ways dflags

osa1

{-# LANGUAGE LambdaCase #-}

fib :: Integer -> Integer
fib 0 = 1
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

fib' :: Integer -> Integer
fib' = \case
         0 -> 1

osa1

How to run/test PureScript Lua backend

• Clone my fork of PureScript and switch to lua branch:

➜  ~  git clone https://github.com/osa1/purescript.git purescript_lua_test
Cloning into 'purescript_lua_test'...
remote: Counting objects: 9089, done.
remote: Compressing objects: 100% (3362/3362), done.
remote: Total 9089 (delta 5625), reused 8886 (delta 5517)
Receiving objects: 100% (9089/9089), 1.75 MiB | 86.00 KiB/s, done.

osa1

vblank_mode=0 optirun -b primus %command% +net_graph 1 +net_graphheight 64 +net_graphinsetbottom 437 +net_graphinsetleft 0 +net_graphinsetright -83 +net_graphpos 1 +net_graphproportionalfont 0 +net_graphtext 1

osa1

Require Import Omega.
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.VectorDef.
Open Scope vector_scope.
Require Import Bool.
Require Import List.
Require Import Arith.
Require Import Arith.EqNat.
Require Import Program.