Skip to content
Permalink
Browse files

Merge PR #70: Misc cleanup

  • Loading branch information...
cwgoes committed Aug 26, 2019
1 parent ae50a73 commit a998218c8ddd597ca142b1b422dba84e89de58a6
@@ -15,6 +15,9 @@ build-opt: clean
lint:
stack exec -- hlint app src test

format:
find . -type f -name "*.hs" -exec stylish-haskell -i {} \;

test:
stack test --fast

@@ -30,4 +33,4 @@ clean:
clean-full:
stack clean --full

.PHONY: all setup build build-watch build-opt lint test repl-lib repl-exe clean clean-full
.PHONY: all setup build build-watch build-opt lint format test repl-lib repl-exe clean clean-full
@@ -1,5 +1,9 @@
# Juvix

![GitHub](https://img.shields.io/github/license/cryptiumlabs/juvix)
![Build status](https://img.shields.io/circleci/build/github/cryptiumlabs/juvix?token=abc123def456)
![GitHub issues](https://img.shields.io/github/issues/cryptiumlabs/juvix)

## Overview

Juvix synthesizes a high-level frontend syntax, dependent-linearly-typed core language, and low-level parallelisable
@@ -1,2 +1,4 @@
import Distribution.Simple
import Distribution.Simple

main IO ()
main = defaultMain
@@ -13,8 +13,6 @@ import Config
import Interactive
import Options

import qualified Juvix.EAL as Solve

context IO Context
context = do
pwd getCurrentDirectory
@@ -80,8 +78,6 @@ run ctx (Options cmd configPath) = do
Version do
putDoc versionDoc
exitSuccess
Solve -> do
print =<< Solve.computeTwo
_ -> do
putText "Not yet implemented!"
exitFailure
@@ -17,7 +17,9 @@ data Command
= Version
| Config
| Interactive
| Solve
| Init
| Plan
| Apply

options Context Parser Options
options ctx = Options <$> commandOptions <*> configOptions ctx
@@ -30,7 +32,9 @@ commandOptions = subparser (
command "version" (info versionOptions (progDesc "Display version information"))
<> command "config" (info configurationOptions (progDesc "Adjust runtime configuration or generate an example config file"))
<> command "interactive" (info interactiveOptions (progDesc "Launch interactive mode"))
<> command "solve" (info solveOptions (progDesc "Solve some equations"))
<> command "init" (info initOptions (progDesc "Initialise deployment configuration"))
<> command "plan" (info planOptions (progDesc "Plan deployment"))
<> command "apply" (info applyOptions (progDesc "Execute deployment"))
)

versionOptions Parser Command
@@ -42,5 +46,11 @@ configurationOptions = pure Config
interactiveOptions Parser Command
interactiveOptions = pure Interactive

solveOptions Parser Command
solveOptions = pure Solve
initOptions Parser Command
initOptions = pure Init

planOptions Parser Command
planOptions = pure Plan

applyOptions Parser Command
applyOptions = pure Apply
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
@@ -0,0 +1,2 @@
import Distribution.Simple
main = defaultMain
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
@@ -1,7 +1,7 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Juvix.Library hiding (link, reduce)

@@ -10,13 +10,13 @@ type family (G a b) :: Bool where
G a _ = 'False

class (Typeable a, Typeable b) Dynamical a b where
isFromA :: Proxy a Proxy b Bool
isFromA Proxy a Proxy b Bool

instance (Typeable b, Typeable a, G a b ~ flag, Dynamical' flag a b) Dynamical a b where
isFromA = isFromA' (Proxy :: Proxy flag)

class Dynamical' flag a b where
isFromA' :: Proxy flag Proxy a Proxy b Bool
isFromA' Proxy flag Proxy a Proxy b Bool

instance Dynamical' 'True (a b) a where
isFromA' _ (Proxy :: Proxy (a b)) (Proxy :: Proxy a) = True

This file was deleted.

@@ -1,13 +1,13 @@
import Juvix.Library hiding (Nat)
import Juvix.Library hiding (Nat)


inl :: t1 (t1 t2) p t2
inl t1 (t1 t2) p t2
inl = \x k _l k x

inr :: t1 p (t1 t2) t2
inr t1 p (t1 t2) t2
inr = \y _k l l y

case' :: (t1 t2 t3) t1 t2 t3
case' (t1 t2 t3) t1 t2 t3
case' = \i k l i k l


@@ -17,7 +17,7 @@ type Times x y = forall z. (x → y → z) → z

type Exists f = forall z. (forall x. f x z) z

type Mu f = (forall a. (f a -> a) -> a)
type Mu f = (forall a. (f a a) a)

type One = forall x. x x

@@ -42,7 +42,7 @@ one' = inr zero'
--succ = fix inr


newtype Huffman' b c = Huffman' (forall a. forall z. ((c -> z) -> (b -> a -> z) -> z) a)
newtype Huffman' b c = Huffman' (forall a. forall z. ((c z) (b a z) z) a)

leaf :: c Huffman b c
leaf c Huffman b c
leaf = inl
@@ -2,8 +2,8 @@
--"A tutorial implementation of a dependently typed lambda calculus"


import Control.Monad.Except --Enable throwError
import Prelude
import Control.Monad.Except
import Prelude

-- Inferable terms
data ITerm
@@ -33,7 +33,7 @@ data Type

--Values are lambda abstractions or neutral terms
data Value
= VLam (Value -> Value)
= VLam (Value Value)
| VNeutral Neutral

--A neutral term is either a variable or an application of a neutral term to a value
@@ -42,26 +42,26 @@ data Neutral
| NApp Neutral Value

--vfree creates the value corresponding to a free variable
vfree :: Name -> Value
vfree Name Value
vfree n = VNeutral (NFree n)

--Evaluation

type Env = [Value]
type NameEnv v = [(Name, v)]
iEval :: ITerm -> (NameEnv Value,Env) -> Value
iEval ITerm (NameEnv Value,Env) Value
iEval (Ann e _) d = cEval e d
iEval (Free x) d = case lookup x (fst d) of Nothing -> (vfree x); Just v -> v
iEval (Bound ii) d = (snd d) !! ii --(!!) :: [a] -> Int -> a. It's the list lookup operator.
iEval (e1 :@: e2) d = vapp (iEval e1 d) (cEval e2 d)

vapp :: Value -> Value -> Value
vapp (VLam f) v = f v
vapp (VNeutral n) v = VNeutral (NApp n v)
vapp Value Value Value
vapp (VLam f) v = f v
vapp (VNeutral n) v = VNeutral (NApp n v)

cEval :: CTerm -> (NameEnv Value,Env) -> Value
cEval (Inf ii) d = iEval ii d
cEval (Lam e) d = VLam (\ x -> cEval e (((\(e, d) -> (e, (x : d))) d)))
cEval CTerm (NameEnv Value,Env) Value
cEval (Inf ii) d = iEval ii d
cEval (Lam e) d = VLam (\ x -> cEval e (((\(e, d) -> (e, (x : d))) d)))

--Contexts

@@ -82,28 +82,28 @@ type Result a = Either String a

--Type checking

cKind :: Context -> Type -> Kind -> Result ()
cKind Context Type Kind Result ()
cKind g (TFree x) Star
= case lookup x g of
Just (HasKind Star) -> return ()
Nothing -> throwError "unknown identifier"
Just (HasKind Star) -> return ()
Nothing -> throwError "unknown identifier"
cKind g (Fun kk kk') Star
= do cKind g kk Star
cKind g kk' Star

--inferable terms returns a type.
iType0 :: Context -> ITerm -> Result Type
iType0 Context ITerm Result Type
iType0 = iType 0

iType :: Int -> Context -> ITerm -> Result Type
iType Int Context ITerm Result Type
iType ii g (Ann e ty)
= do cKind g ty Star
cType ii g e ty
return ty
iType ii g (Free x)
= case lookup x g of
Just (HasType ty) -> return ty
Nothing -> throwError "unknown identifier"
Just (HasType ty) -> return ty
Nothing -> throwError "unknown identifier"
iType ii g (e1 :@: e2)
= do si <- iType ii g e1
case si of
@@ -112,7 +112,7 @@ iType ii g (e1 :@: e2)
_ -> throwError "illegal application"

--checkable terms takes a type as input and returns ().
cType :: Int -> Context -> CTerm -> Type -> Result ()
cType Int Context CTerm Type Result ()
cType ii g (Inf e) ty
= do ty' <- iType ii g e
unless (ty == ty') (throwError "type mismatch")
@@ -125,33 +125,33 @@ cType ii g _ _
--Substitution

--substitution function for inferable terms
iSubst :: Int -> ITerm -> ITerm -> ITerm
iSubst ii r (Ann e ty) = Ann (cSubst ii r e) ty
iSubst ii r (Bound j) = if ii == j then r else Bound j
iSubst ii r (Free y) = Free y
iSubst ii r (e1 :@: e2) = iSubst ii r e1 :@: cSubst ii r e2
iSubst Int ITerm ITerm ITerm
iSubst ii r (Ann e ty) = Ann (cSubst ii r e) ty
iSubst ii r (Bound j) = if ii == j then r else Bound j
iSubst ii r (Free y) = Free y
iSubst ii r (e1 :@: e2) = iSubst ii r e1 :@: cSubst ii r e2

--substitution function for checkable terms
cSubst :: Int -> ITerm -> CTerm -> CTerm
cSubst ii r (Inf e) = Inf (iSubst ii r e)
cSubst ii r (Lam e) = Lam (cSubst (ii + 1) r e)
cSubst Int ITerm CTerm CTerm
cSubst ii r (Inf e) = Inf (iSubst ii r e)
cSubst ii r (Lam e) = Lam (cSubst (ii + 1) r e)

--Quotation: takes a value back to a term
quote0 :: Value -> CTerm
quote0 Value CTerm
quote0 = quote 0

quote :: Int -> Value -> CTerm
quote ii (VLam f) = Lam (quote (ii + 1) (f (vfree (Quote ii))))
quote ii (VNeutral n) = Inf (neutralQuote ii n)
quote Int Value CTerm
quote ii (VLam f) = Lam (quote (ii + 1) (f (vfree (Quote ii))))
quote ii (VNeutral n) = Inf (neutralQuote ii n)

neutralQuote :: Int -> Neutral -> ITerm
neutralQuote ii (NFree x) = boundfree ii x
neutralQuote ii (NApp n v) = neutralQuote ii n :@: quote ii v
neutralQuote Int Neutral ITerm
neutralQuote ii (NFree x) = boundfree ii x
neutralQuote ii (NApp n v) = neutralQuote ii n :@: quote ii v

--checks if the variable occurring at the head of the application is a bound variable or a free name
boundfree :: Int -> Name -> ITerm
boundfree ii (Quote k) = Bound (ii - k - 1)
boundfree ii x = Free x
boundfree Int Name ITerm
boundfree ii (Quote k) = Bound (ii - k - 1)
boundfree ii x = Free x

--definitions for testing
id' = Lam (Inf (Bound 0))
@@ -3,12 +3,12 @@ version: 0.0.0.0
github: "cryptiumlabs/juvix"
license: GPL-3
homepage: https://github.com/cryptiumlabs/juvix#readme
synopsis: Juvix smart contract compiler & toolkit
synopsis: Juvix smart contract language compiler, debugging toolkit, & stateful deployment system
category: Web3
description: Please see the README on GitHub at <https://github.com/cwgoes/juvix#readme>
description: Please see the README on GitHub at <https://github.com/cryptiumlabs/juvix#readme>
author: Cryptium Labs
maintainer: cwgoes@cryptium.ch, jeremy@cryptium.ch
copyright: 2018-2019 Cryptium Labs
maintainer: cwgoes@cryptium.ch, jeremy@cryptium.ch, marty@cryptium.ch, andy@cryptium.ch
copyright: 2018 Christopher Goes, 2018-2019 Cryptium Labs

extra-source-files:
- README.md
@@ -26,6 +26,8 @@ dependencies:
- fgl-visualize
- enummapset
- turtle
- directory

default-extensions:
- NoImplicitPrelude
- OverloadedStrings
@@ -55,12 +57,11 @@ ghc-options:
- -Wall
- -fno-warn-orphans
- -fno-warn-name-shadowing
- -j4
- -j6

library:
source-dirs: src
dependencies:
- directory
- z3
exposed-modules:
- Juvix
@@ -100,7 +101,6 @@ executables:
- -with-rtsopts=-N
dependencies:
- juvix
- directory
- optparse-applicative
- ansi-wl-pprint
- raw-strings-qq
@@ -1,5 +1,9 @@
#!/bin/sh

set -xe

make format

# disabled for now
# make lint

0 comments on commit a998218

Please sign in to comment.
You can’t perform that action at this time.