Skip to content

Commit

Permalink
Merge branch 'master' into kwxm/BLS12_381/prototype
Browse files Browse the repository at this point in the history
  • Loading branch information
kwxm committed Mar 16, 2023
2 parents 7771982 + e714dda commit f1581d5
Show file tree
Hide file tree
Showing 382 changed files with 2,385 additions and 1,089 deletions.
4 changes: 3 additions & 1 deletion .github/workflows/check-changelog.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,8 @@ jobs:

- name: Enforce New File or 'No Changelog Required' Label
uses: actions/github-script@v6
# don't require changelogs for draft PRs
if: github.event.pull_request.draft == false
with:
script: |
function shouldCheckChangelog() {
Expand Down Expand Up @@ -49,4 +51,4 @@ jobs:
checkChangelog();
} else {
core.info("PR contains the label 'No Changelog Required', skipping changelog check.");
}
}
2 changes: 1 addition & 1 deletion .github/workflows/haddock.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ jobs:
name: github-pages
steps:
- uses: actions/checkout@v3
- uses: nixbuild/nix-quick-install-action@v21
- uses: nixbuild/nix-quick-install-action@v22
with:
nix_conf: |
experimental-features = nix-command flakes
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/hlint.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ jobs:
version: '3.4'

- name: Quick Install Nix
uses: nixbuild/nix-quick-install-action@v21
uses: nixbuild/nix-quick-install-action@v22
with:
nix_conf: |
experimental-features = nix-command flakes
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/pre-commit-check.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ jobs:
uses: actions/checkout@v3

- name: Quick Install Nix
uses: nixbuild/nix-quick-install-action@v21
uses: nixbuild/nix-quick-install-action@v22
with:
nix_conf: |
experimental-features = nix-command flakes
Expand Down
2 changes: 1 addition & 1 deletion .stylish-haskell.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ steps:
remove_redundant: false

- trailing_whitespace: {}
columns: 120
columns: 100
newline: native
language_extensions:
- DataKinds
Expand Down
22 changes: 15 additions & 7 deletions doc/notes/fomega/cek-cps-experiments/src/CekMachine.cps.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
-- editorconfig-checker-disable-file

-- This file contains a version of the CEK machine in
-- continuation-passing-style, where the frames and return
-- operation of the original version are replaced with explicit
Expand All @@ -14,7 +12,8 @@
-- This is for efficiency reasons.
-- The type checker pass is required as well (and in our case it subsumes the renamer pass).
-- Feeding ill-typed terms to the CEK machine will likely result in a 'MachineException'.
-- The CEK machine generates booleans along the way which might contain globally non-unique 'Unique's.
-- The CEK machine generates booleans along the way which might contain globally non-unique
-- 'Unique's.
-- This is not a problem as the CEK machines handles name capture by design.

module PlutusCore.Interpreter.CekMachine
Expand Down Expand Up @@ -103,15 +102,23 @@ instantiateEvaluate
instantiateEvaluate k env _ (TyAbs _ _ _ body) = computeCek k env body
instantiateEvaluate k env ty fun
| isJust $ termAsPrimIterApp fun = k env $ TyInst () fun ty
| otherwise = throw $ MachineException NonPrimitiveInstantiationMachineError fun
| otherwise =
throw $ MachineException NonPrimitiveInstantiationMachineError fun

-- | Apply a function to an argument and proceed.
-- If the function is a 'LamAbs', then extend the current environment with a new variable and proceed.
-- If the function is a 'LamAbs', then extend the current environment with a new variable and
-- proceed.
-- If the function is not a 'LamAbs', then 'Apply' it to the argument and view this
-- as an iterated application of a 'BuiltinName' to a list of 'Value's.
-- If succesful, proceed with either this same term or with the result of the computation
-- depending on whether 'BuiltinName' is saturated or not.
applyEvaluate :: Cont -> Environment -> Environment -> Plain Value -> Plain Value -> EvaluationResult
applyEvaluate ::
Cont
-> Environment
-> Environment
-> Plain Value
-> Plain Value
-> EvaluationResult
applyEvaluate k funEnv argEnv lam@(LamAbs _ name _ body) arg =
computeCek k (extendEnvironment name arg argEnv funEnv) body
applyEvaluate k funEnv _ fun arg =
Expand All @@ -124,7 +131,8 @@ applyEvaluate k funEnv _ fun arg =
ConstAppSuccess term' -> k funEnv term'
ConstAppFailure -> EvaluationFailure
ConstAppStuck -> k funEnv term
ConstAppError err -> throw $ MachineException (ConstAppMachineError err) term
ConstAppError err ->
throw $ MachineException (ConstAppMachineError err) term

-- | Evaluate a term using the CEK machine. May throw a 'MachineException'.
evaluateCek :: Term TyName Name () -> EvaluationResult
Expand Down
21 changes: 15 additions & 6 deletions doc/notes/fomega/cek-cps-experiments/src/CekMachine.original.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
-- editorconfig-checker-disable-file
-- | The CEK machine.
-- Rules are the same as for the CK machine from "PlutusCore.Evaluation.CkMachine",
-- except we do not use substitution and use environments instead.
Expand All @@ -7,7 +6,8 @@
-- This is for efficiency reasons.
-- The type checker pass is required as well (and in our case it subsumes the renamer pass).
-- Feeding ill-typed terms to the CEK machine will likely result in a 'MachineException'.
-- The CEK machine generates booleans along the way which might contain globally non-unique 'Unique's.
-- The CEK machine generates booleans along the way which might contain globally non-unique
-- 'Unique's.
-- This is not a problem as the CEK machines handles name capture by design.

module PlutusCore.Interpreter.CekMachine
Expand Down Expand Up @@ -102,15 +102,23 @@ instantiateEvaluate
instantiateEvaluate env con _ (TyAbs _ _ _ body) = computeCek env con body
instantiateEvaluate env con ty fun
| isJust $ termAsPrimIterApp fun = returnCek env con $ TyInst () fun ty
| otherwise = throw $ MachineException NonPrimitiveInstantiationMachineError fun
| otherwise =
throw $ MachineException NonPrimitiveInstantiationMachineError fun

-- | Apply a function to an argument and proceed.
-- If the function is a 'LamAbs', then extend the current environment with a new variable and proceed.
-- If the function is a 'LamAbs', then extend the current environment with a new variable and
-- proceed.
-- If the function is not a 'LamAbs', then 'Apply' it to the argument and view this
-- as an iterated application of a 'BuiltinName' to a list of 'Value's.
-- If succesful, proceed with either this same term or with the result of the computation
-- depending on whether 'BuiltinName' is saturated or not.
applyEvaluate :: Environment -> Environment -> Context -> Plain Value -> Plain Value -> EvaluationResult
applyEvaluate ::
Environment
-> Environment
-> Context
-> Plain Value
-> Plain Value
-> EvaluationResult
applyEvaluate funEnv argEnv con (LamAbs _ name _ body) arg =
computeCek (extendEnvironment name arg argEnv funEnv) con body
applyEvaluate funEnv _ con fun arg =
Expand All @@ -123,7 +131,8 @@ applyEvaluate funEnv _ con fun arg =
ConstAppSuccess term' -> returnCek funEnv con term'
ConstAppFailure -> EvaluationFailure
ConstAppStuck -> returnCek funEnv con term
ConstAppError err -> throw $ MachineException (ConstAppMachineError err) term
ConstAppError err ->
throw $ MachineException (ConstAppMachineError err) term

-- | Evaluate a term using the CEK machine. May throw a 'MachineException'.
evaluateCek :: Term TyName Name () -> EvaluationResult
Expand Down
22 changes: 14 additions & 8 deletions doc/notes/fomega/cek-cps-experiments/src/CekMachine.recursive.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
-- editorconfig-checker-disable-file
{-# LANGUAGE BangPatterns #-}

-- This file contains a version of the CEK machine in
Expand All @@ -17,7 +16,8 @@
-- This is for efficiency reasons.
-- The type checker pass is required as well (and in our case it subsumes the renamer pass).
-- Feeding ill-typed terms to the CEK machine will likely result in a 'MachineException'.
-- The CEK machine generates booleans along the way which might contain globally non-unique 'Unique's.
-- The CEK machine generates booleans along the way which might contain globally non-unique
-- 'Unique's.
-- This is not a problem as the CEK machines handles name capture by design.

module PlutusCore.Interpreter.CekMachine
Expand Down Expand Up @@ -84,12 +84,14 @@ evalCek !cl@(Closure term env) =
Unwrap _ term' ->
case evalCek $ Closure term' env of
Closure (Wrap _ _ _ t) env' -> evalCek $ Closure t env'
_ -> throw $ MachineException NonWrapUnwrappedMachineError term'
_ ->
throw $ MachineException NonWrapUnwrappedMachineError term'

Error{} -> throw $ MachineException OpenTermEvaluatedMachineError term

Var _ name -> case lookupName name env of
Nothing -> throw $ MachineException OpenTermEvaluatedMachineError term
Nothing ->
throw $ MachineException OpenTermEvaluatedMachineError term
Just cl@(Closure val7 env7) -> cl

-- | Instantiate a term with a type and proceed.
Expand All @@ -101,10 +103,12 @@ instantiateEvaluate
instantiateEvaluate _ !(Closure (TyAbs _ _ _ body) env) = evalCek (Closure body env)
instantiateEvaluate ty !(Closure fun env)
| isJust $! termAsPrimIterApp fun = Closure (TyInst () fun ty) env
| otherwise = throw $ MachineException NonPrimitiveInstantiationMachineError fun
| otherwise =
throw $ MachineException NonPrimitiveInstantiationMachineError fun

-- | Apply a function to an argument and proceed.
-- If the function is a 'LamAbs', then extend the current environment with a new variable and proceed.
-- If the function is a 'LamAbs', then extend the current environment with a new variable and
-- proceed.
-- If the function is not a 'LamAbs', then 'Apply' it to the argument and view this
-- as an iterated application of a 'BuiltinName' to a list of 'Value's.
-- If succesful, proceed with either this same term or with the result of the computation
Expand All @@ -121,9 +125,11 @@ applyEvaluate !(Closure funVal funEnv) !(Closure argVal argEnv) =
Just (IterApp headName spine) ->
case runQuote $! ((applyBuiltinName $! headName) $! spine) of
ConstAppSuccess term' -> Closure term' funEnv
ConstAppFailure -> throw $ MachineException OpenTermEvaluatedMachineError term
ConstAppFailure ->
throw $ MachineException OpenTermEvaluatedMachineError term
ConstAppStuck -> Closure term funEnv
ConstAppError err -> throw $ MachineException (ConstAppMachineError err) term
ConstAppError err ->
throw $ MachineException (ConstAppMachineError err) term

-- | Evaluate a term using the CEK machine. May throw a 'MachineException'.
evaluateCek :: Term TyName Name () -> EvaluationResult
Expand Down

0 comments on commit f1581d5

Please sign in to comment.