HasCal — A promising embedding of pluscal in haskell.

A very bad example of a simple Nat div2 check in TLA+
A neat embedding of PlusCal in haskell
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}
import Control.Monad (when)
import HasCal
data Global = Global
{ _number :: Int
, _output :: Int
} deriving (Eq, Generic, Hashable, Show)
instance Pretty Global where pretty = unsafeViaShowmakeLenses ‘’GlobaltestNatDivision :: IO ()
testNatDivision = do
let startingLabel = ()
let startingLocals = pure ()
let nd2 = do
while (do v <- use (global.number) ; return (v >= 2)) do
global.output += 1
global.number -= 2
let process = do
initial_n <- use (global.number)
initial_o <- use (global.output)
global.output -= initial_o
nd2 my_output <- use (global.output)
assert (initial_n `div` 2 == my_output)
model defaultOptions { debug = True } Begin {..} (pure True) do
_number <- [ 1 .. 1000 ]
_output <- [ 0 ]
return Global {..}
main :: IO ()
main = do
testNatDivision

--

--

--

An old programmer learning new tricks.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Why Windows 10 Won’t Start

Flutter with Digital Ocean Spaces

Automate CloudFront Catch Invalidation Using CodePipeline and Lambda

Exploring Blockchain Development — Day 2

SpringBoot and Rest APIs in Java

Web Based Integration Solution for Remote OSCE/MMI

{UPDATE} MMX Masters Hack Free Resources Generator

Say no to messy code

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
art yerkes

art yerkes

An old programmer learning new tricks.

More from Medium

Coordinating Addressable LED Light Effects

A new phase for the Rustc Reading Club

The best RUST furnace replica