Code Templates

This page contains code templates and an example of an sp-program that can be copied to get started. The example contains a bit of code to serve as a quick refresher on the basic syntax and semantics.

Empty (minimal)

Barebone template containing all required sections and the #FUNCTIONS- and #PREDICATES-section, which one usually wants as well.

#NAME
#FUNCTIONS
#VARIABLES
#OPERATIONS
#PREDICATES
#FLOW

Empty (full)

Barebone template containing all possible sections. Remove the optional ones as needed.

#NAME
#OPTIONS
#FUNCTIONS
#VARIABLES
#CONSTRAINTS
#OPERATIONS
#PREDICATES
#FLOW
#VERBATIM

Example

Some code to show off the basic syntax. The code does not have any meaning.

#NAME
programName

-- single line comment
{-
  multi-line
  comment
-}

#FUNCTIONS
f1 var1 var2 = var3
f2 var2 var1 = (var3,var4) --returns tuple with var3 and var4

#VARIABLES
var1 :: Int
var2 :: Int
var3 :: Bool
var4 :: String
?var5 :: a -> b
 {-
   the prefix ? hides var5 from the traces
   this is required for variables whose type
   is not a member of Show
 -}

#CONSTRAINTS
Ord a  
Show b

#OPERATIONS
init: --first op is used as entry point for the program
  var3' = (var1 /= var2')
  var2' = g helperVar z2 --multi-line expression
    where
      z1 = 1
      z2 = z1
  (var5,[var1,_,_]) = undefined  --using a pattern
  helperVar = undefined --local variable only visible in init

op1 SAMEAS init --same assignments as init
op2 SAMEAS op1

#PREDICATES
pred1 = undefined
pred2 = f var1 var2 z1
  where
    z1 = 1337

#FLOW
init = (pred1 nop HALT) -- continues with nop if pred1 is true
                        -- stops execution otherwise
op1 = op2
op2 = HALT
.nop = --phantom operation, use to compress common sub-BDTs
  (pred1
    (pred2 op1 op2)
    (pred3 HALT init)
  )

#VERBATIM
--plain Haskell code which is inserted at global level
f = undefined
g = undefined

Subprogram Pattern

The purpose of the subprogram pattern is to keep the number of variables and operations in a program to a minimum. For example, if you notice that a certain subset of variables is only used in a specific part of the program then it might be a good idea to subsume this part of the program in a subprogram. Then this subset of variables can be removed from the main program. Below is an example of how such a subprogram call looks like:

#NAME
mainProgram

#VARIABLES
x1 :: Int
x2 :: Int
x3 :: Bool

#OPERATIONS
someOp: --subprogram is called
  (x1',x2',x3') = subProgram x1 x2 x3 --only a single assignment is required

#FLOW
someOp = HALT

#NAME
subProgram

#FUNCTIONS
subProgram x1 x2 x3 = (x1,x2,x3)

#VARIABLES
x1 :: Int
x2 :: Int
x3 :: Bool

--variables only used in the subprogram 
y1 :: Int 
y2 :: Int

#OPERATIONS
init: --do something here...

#FLOW
init = HALT