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

--

--

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.