FUN — Untyped — Environment
Author: Grigore Roșu (grosu@illinois.edu)
Organization: University of Illinois at UrbanaChampaign
Author: Traian Florin Șerbănuță (traian.serbanuta@unibuc.ro)
Organization: University of Bucharest
Abstract
This is the K semantic definition of the untyped FUN language. FUN is a pedagogical and research language that captures the essence of the functional programming paradigm, extended with several features often encountered in functional programming languages. Like many functional languages, FUN is an expression language, that is, everything, including the main program, is an expression. Functions can be declared anywhere and are first class values in the language. FUN is callbyvalue here, but it has been extended (as student homework assignments) with other parameterpassing styles. To make it more interesting and to highlight some of K's strengths, FUN includes the following features:

The basic builtin datatypes of integers, booleans and strings.

Builtin lists, which can hold any elements, including other lists. Lists are enclosed in square brackets and their elements are commaseparated; e.g.,
[1,2,3]
. 
Userdefined datatypes, by means of constructor terms. Constructor names start with a capital letter (while any other identifier in the language starts with a lowercase letter), and they can be followed by an arbitrary number of commaseparated arguments enclosed in parentheses; parentheses are not needed when the constructor takes no arguments. For example,
Pair(5,7)
is a constructor term holding two numbers,Cons(1,Cons(2,Cons(3,Nil)))
is a listlike constructor term holding 3 elements, andTree(Tree(Leaf(1), Leaf(2)), Leaf(3))
is a treelike constructor term holding 3 elements. In the untyped version of the FUN language, no type checking or inference is performed to ensure that the data constructors are used correctly. The execution will simply get stuck when they are misused. Moreover, since no type checking is performed, the datatypes are not even declared in the untyped version of FUN. 
Functions and
let
/letrec
binders can take multiple spaceseparated arguments, but these are desugared to ones that only take one argument, by currying. For example, the expressionsfun x y > x y let x y = y in x
are desugared, respectively, into the following expressions:
fun x > fun y > x y let x = fun y > y in x

Functions can be defined using pattern matching over the available datatypes. For example, the program
letrec max = fun [h] > h  [ht] > let x = max t in if h > x then h else x in max [1, 3, 5, 2, 4, 0, 1, 5]
defines a function
max
that calculates the maximum element of a nonempty list, and the functionletrec ack = fun Pair(0,n) > n + 1  Pair(m,0) > ack Pair(m  1, 1)  Pair(m,n) > ack Pair(m  1, ack Pair(m, n  1)) in ack Pair(2,3)
calculates the Ackermann function applied to a particular pair of numbers. Patterns can be nested. Patterns can currently only be used in function definitions, and not directly in
let
/letrec
binders. For example, this is not allowed:letrec Pai(x,y) = Pair(1,2) in x+y
But this is allowed:
let f Pair(x,y) = x+y in f Pair(1,2)
because it is first reduced to
let f = fun Pair(x,y) > x+y in f Pair(1,2)
by uncurrying of the
let
binder, and pattern matching is allowed in function arguments. 
We include a
callcc
construct, for two reasons: first, several functional languages support this construct; second, some semantic frameworks have difficulties defining it. Not K. 
Finally, we include mutables by means of referencing an expression, getting the reference of a variable, dereferencing and assignment. We include these for the same reasons as above: there are languages which have them, and they are not easy to define in some semantic frameworks.
Like in many other languages, some of FUN's constructs can be desugared into a smaller set of basic constructs. We do that as usual, using macros, and then we only give semantics to the core constructs.
Note:
We recommend the reader to first consult the dynamic semantics of the
LAMBDA++ language in the first part of the K Tutorial.
To keep the comments below small and focused, we will not reexplain
functional or K features that have already been explained in there.
Syntax
//require "modules/patternmatching.k"
module FUNUNTYPEDCOMMON
imports DOMAINSSYNTAX
FUN is an expression language. The constructs below fall into several categories: names, arithmetic constructs, conventional functional constructs, patterns and pattern matching, data constructs, lists, references, and callwithcurrentcontinuation (callcc). The arithmetic constructs are standard; they are present in almost all our K language definitions. The meaning of FUN's constructs are discussed in more depth when we define their semantics in the next module.
The Syntactic Constructs
We start with the syntactic definition of FUN names. We have several categories of names: ones to be used for functions and variables, others to be used for data constructors, others for types and others for type variables. We will introduce them as needed, starting with the former category. We prefer the names of variables and functions to start with lower case letters. We take the freedom to tacitly introduce syntactic lists/sequences for each nonterminal for which we need them:
syntax Name
syntax Names ::= List{Name,","}
Expression constructs will be defined throughtout the syntax module. Below are the very basic ones, namely the builtins, the names, and the parentheses used as brackets for grouping. Lists of expressions are declared strict, so all expressions in the list get evaluated whenever the list is on a position which can be evaluated:
syntax Exp ::= Int  Bool  String  Name
 "(" Exp ")" [bracket]
syntax Exps ::= List{Exp,","} [strict]
syntax Val
syntax Vals ::= List{Val,","}
syntax Bottom
syntax Bottoms ::= List{Bottom,","}
We next define the syntax of arithmetic constructs, together with their relative priorities and left/nonassociativities. We also tag all these rules with a new tag, "arith", so we can more easily define global syntax priirities later (at the end of the syntax module).
syntax Exp ::= left:
Exp "*" Exp [strict, arith]
 Exp "/" Exp [strict, arith]
 Exp "%" Exp [strict, arith]
> left:
Exp "+" Exp [strict, left, arith]
 Exp "^" Exp [strict, left, arith]
// left attribute should not be necessary; currently a parsing bug
 Exp "" Exp [strict, prefer, arith]
// the "prefer" attribute above is to not parse x1 as x(1)
// Due to some parsing problems, we currently cannot add unary minus:
 "" Exp [strict, arith]
> nonassoc:
Exp "<" Exp [strict, arith]
 Exp "<=" Exp [strict, arith]
 Exp ">" Exp [strict, arith]
 Exp ">=" Exp [strict, arith]
 Exp "==" Exp [strict, arith]
 Exp "!=" Exp [strict, arith]
> "!" Exp [strict, arith]
> Exp "&&" Exp [strict(1), left, arith]
> Exp "" Exp [strict(1), left, arith]
The conditional construct has the expected evaluation strategy, stating that only the first argument is evaluate:
syntax Exp ::= "if" Exp "then" Exp "else" Exp [strict(1)]
FUN's builtin lists are formed by enclosing commaseparated
sequences of expressions (i.e., terms of sort Exps
) in square
brackets. The list constructor cons
adds a new element to the
top of the list, head
and tail
get the first element
and the tail sublist of a list if they exist, respectively, and get
stuck otherwise, and null??
tests whether a list is empty or
not; syntactically, these are just expression constants.
In function patterns, we are also going to allow patterns following the
usual head/tail notation; for example, the pattern [x_1,...,x_nt]
binds x_1
, ..., x_n
to the first elements of the matched list,
and t
to the list formed with the remaining elements. We define list
patterns as ordinary expression constructs, although we will make sure that
we do not give them semantics if they appear in any other place then in a
function case pattern.
syntax Exp ::= "[" Exps "]" [strict]
 "cons"  "head"  "tail"  "null?"
 "[" Exps "" Exp "]"
syntax Val ::= "[" Vals "]"
Data constructors start with capital letters and they may or may
not have arguments. We need to use the attribute "prefer" to make
sure that, e.g., Cons(a)
parses as constructor Cons
with
argument a
, and not as the expression Cons
(because
constructor names are also expressions) regarded as a function applied
to the expression a
. Also, note that the constructor is strict
in its second argument, because we want to evaluate its arguments but
not the constuctor name itsef.
syntax ConstructorName
syntax Exp ::= ConstructorName
 ConstructorName "(" Exps ")" [prefer, strict(2)]
syntax Val ::= ConstructorName "(" Vals ")"
A function is essentially a 
separated ordered
sequence of cases, each case of the form pattern > expression
,
preceded by the language construct fun
. Patterns will be defined
shortly, both for the builtin lists and for userdefined constructors.
Recall that the syntax we define in K is not meant to serve as a
ultimate parser for the defined language, but rather as a convenient
notation for K abstract syntax trees, which we prefer when we write
the semantic rules. It is therefore often the case that we define a
more ``generous'' syntax than we want to allow programs to use.
We do it here, too. Specifically, the syntax of Cases
below allows any expressions to appear as pattern. This syntactic
relaxation permits many wrong programs to be parsed, but that is not a
problem because we are not going to give semantics to wrong combinations,
so those programs will get stuck; moreover, our type inferencer will reject
those programs anyway. Function application is just concatenation of
expressions, without worrying about type correctness. Again, the type
system will reject typeincorrect programs.
syntax Exp ::= "fun" Cases
 Exp Exp [strict, left]
// NOTE: We would like eventually to also have Exp "(" Exps ")
syntax Case ::= Exp ">" Exp
syntax Cases ::= List{Case, ""}
The let
and letrec
binders have the usual syntax
and functional meaning. We allow multiple and
separated bindings.
Like for the function cases above, we allow a more generous syntax for
the lefthand sides of bindings, noting that the semantics will get stuck
on incorrect bindings and that the type system will reject those programs.
syntax Exp ::= "let" Bindings "in" Exp
 "letrec" Bindings "in" Exp [prefer]
// The "prefer" attribute for letrec currently needed due to tool bug,
// to make sure that "letrec" is not parsed as "let rec".
syntax Binding ::= Exp "=" Exp
syntax Bindings ::= List{Binding,"and"}
References are first class values in FUN. The construct ref
takes an expression, evaluates it, and then it stores the resulting value
at a fresh location in the store and returns that reference. Syntactically,
ref
is just an expression constant. The construct &
takes a name as argument and evaluates to a reference, namely the store
reference where the variable passed as argument stores its value; this
construct is a bit controversial and is further discussed in the
environmentbased semantics of the FUN language, where we desugar
ref
to it. The construct @
takes a reference
and evaluates to the value stored there. The construct :=
takes
two expressions, the first expected to evaluate to a reference; the value
of its second argument will be stored at the location to which the first
points (the old value is thus lost). Finally, since expression evaluation
now has side effects, it makes sense to also add a sequential composition
construct, which is sequentially strict. This evaluates to the value of
its second argument; the value of the first argument is lost (which has
therefore been evaluated only for its side effects.
syntax Exp ::= "ref"
 "&" Name
 "@" Exp [strict]
 Exp ":=" Exp [strict]
 Exp ";" Exp [strict(1), right]
Callwithcurrentcontinuation, named callcc
in FUN, is a
powerful control operator that originated in the Scheme programming
language, but it now exists in many other functional languages. It works
by evaluating its argument, expected to evaluate to a function, and by
passing the current continuation, or evaluation context (or computation,
in K terminology), as a special value to it. When/If this special value
is invoked, the current context is discarded and replaced with the one
held by the special value and the computation continues from there.
It is like taking a snapshot of the execution context at some moment
in time and then, when desired, being able to get back in time to that
point. If you like games, it is like saving the game now (so you can
work on your homework!) and then continuing the game tomorrow or whenever
you wish. To issustrate the strength of callcc
, we also
allow exceptions in FUN by means of a conventional trycatch
construct, which will desugar to callcc
. We also need to
introduce the special expression contant throw
, but we need to
use it as a function argument name in the desugaring macro, so we define
it as a name instead of as an expression constant:
syntax Exp ::= "callcc"
 "try" Exp "catch" "(" Name ")" Exp
syntax Name ::= "throw" [token]
Finally, FUN also allows polymorphic datatype declarations. These will be useful when we define the type system later on.
syntax Exp ::= "datatype" Type "=" TypeCases Exp
// NOTE: In a future version of K, we want the datatype declaration
// to be a construct by itself, but that is not possible currently
// because K's parser wronly identifies the __ operation allowing
// a declaration to appear in front of an expression with the function
// application construct, giving ambiguous parsing errors.
We next need to define the syntax of types and type cases that appear in datatype declarations.
Like in many functional languages, type parameters/variables in userdefined types are quoted identifiers.
syntax TypeVar
syntax TypeVars ::= List{TypeVar,","}
Types can be basic types, function types, or userdefined
parametric types. In the dynamic semantics we are going to simply ignore
all the type declations, so here the syntax of types below is only useful
for generating the desired parser. To avoid syntactic ambiguities with
the arrow construct for function cases, we use the symbol >
as
a constructor for function types:
syntax TypeName
syntax Type ::= "int"  "bool"  "string"
 Type ">" Type [right]
 "(" Type ")" [bracket]
 TypeVar
 TypeName [klabel(TypeName), avoid]
 Type TypeName [klabel(TypeTypeName)]
 "(" Types ")" TypeName [prefer]
syntax Types ::= List{Type,","}
syntax Types ::= TypeVars
syntax TypeCase ::= ConstructorName
 ConstructorName "(" Types ")"
syntax TypeCases ::= List{TypeCase,""} [klabel(_TypeCase_)]
Additional Priorities
syntax priorities @__FUNUNTYPEDCOMMON
> ___FUNUNTYPEDCOMMON
> arith
> _:=__FUNUNTYPEDCOMMON
> let_in__FUNUNTYPEDCOMMON
letrec_in__FUNUNTYPEDCOMMON
if_then_else__FUNUNTYPEDCOMMON
> _;__FUNUNTYPEDCOMMON
> fun__FUNUNTYPEDCOMMON
> datatype_=___FUNUNTYPEDCOMMON
endmodule
module FUNUNTYPEDMACROS
imports FUNUNTYPEDCOMMON
Desugaring macros
We desugar the list nonconstructor operations to functions matching
over list patterns. In order to do that we need some new variables; for
those, we follow the same convention like in the K tutorial, where we
added them as new identifier constructs starting with the character $
,
so we can easily recognize them when we debug or trace the semantics.
syntax Name ::= "$h"  "$t"
rule head => fun [$h$t] > $h [macro]
rule tail => fun [$h$t] > $t [macro]
rule null? => fun [.Exps] > true  [$h$t] > false [macro]
Multiplehead list patterns desugar into successive onehead patterns:
rule [E1,E2,Es:ExpsT] => [E1[E2,EsT]] [macrorec]
Uncurrying of multiple arguments in functions and binders:
rule P1 P2 > E => P1 > fun P2 > E [macrorec]
rule F P = E => F = fun P > E [macrorec]
We desugar the trycatch
construct into callcc:
syntax Name ::= "$k"  "$v"
rule try E catch(X) E'
=> callcc (fun $k > (fun throw > E)(fun X > $k E')) [macro]
For uniformity, we reduce all types to their general form:
// rule TypeName(Tn:TypeName) => (.TypeVars) Tn [macro]
rule `TypeTypeName`(T:Type, Tn:TypeName) => (T) Tn [macro]
The dynamic semantics ignores all the type declarations:
rule datatype _T = _TCs E => E [macro]
endmodule
module FUNUNTYPEDSYNTAX
imports FUNUNTYPEDCOMMON
imports BUILTINIDTOKENS
syntax Name ::= r"[az][_azAZ09]*" [token, prec(2)]
 #LowerId [token]
syntax ConstructorName ::= #UpperId [token]
syntax TypeVar ::= r"['][az][_azAZ09]*" [token]
syntax TypeName ::= Name [token]
endmodule
Semantics
The semantics below is environmentbased. A substitutionbased
definition of FUN is also available, but that drops the &
construct as explained above.
module FUNUNTYPED
imports FUNUNTYPEDCOMMON
imports FUNUNTYPEDMACROS
imports DOMAINS
//imports PATTERNMATCHING
Configuration
The k
, env
, and store
cells are standard
(see, for example, the definition of LAMBDA++ or IMP++ in the first
part of the K tutorial).
configuration <T color="yellow">
<k color="green"> $PGM:Exp </k>
<env color="violet"> .Map </env>
<store color="white"> .Map </store>
</T>
Values and results
We only define integers, Booleans and strings as values here, but will add more values later.
syntax Val ::= Int  Bool  String
syntax Exp ::= Val
syntax Exps ::= Vals
syntax Vals ::= Bottoms
syntax KResult ::= Val
Lookup
rule <k> X:Name => V ...</k>
<env>... X > L ...</env>
<store>... L > V ...</store>
Arithmetic expressions
rule I1 * I2 => I1 *Int I2
rule I1 / I2 => I1 /Int I2 when I2 =/=K 0
rule I1 % I2 => I1 %Int I2 when I2 =/=K 0
rule I1 + I2 => I1 +Int I2
rule S1 ^ S2 => S1 +String S2
rule I1  I2 => I1 Int I2
rule  I => 0 Int I
rule I1 < I2 => I1 <Int I2
rule I1 <= I2 => I1 <=Int I2
rule I1 > I2 => I1 >Int I2
rule I1 >= I2 => I1 >=Int I2
rule V1:Val == V2:Val => V1 ==K V2
rule V1:Val != V2:Val => V1 =/=K V2
rule ! T => notBool(T)
rule true && E => E
rule false && _ => false
rule true  _ => true
rule false  E => E
Conditional
rule if true then E else _ => E
rule if false then _ else E => E
Lists
We have already declared the syntactic list of expressions strict, so
we can assume that all the elements that appear in a FUN list are
evaluated. The only thing left to do is to state that a list of
values is a value itself, that is, that the list squarebracket
construct is indeed a constructor, and to give the semantics of
cons
. Since cons
is a builtin function and is
expected to take two arguments, we have to also state that
cons
itself is a value (specifically, a function/closure
value, but we do not need that level of detail here), and also that
cons
applied to a value is a value (specifically, it would be
a function/closure value that expects the second, list argument):
rule isVal(cons) => true
rule isVal(cons _V:Val) => true
rule cons V:Val [Vs:Vals] => [V,Vs]
Data Constructors
Constructors take values as arguments and produce other values:
syntax Val ::= ConstructorName
Functions and Closures
Like in the environmentbased semantics of LAMBDA++ in the first part of the K tutorial, functions evaluate to closures. A closure includes the current environment besides the function contents; the environment will be used at execution time to lookup all the variables that appear free in the function body (we want static scoping in FUN).
syntax Val ::= closure(Map,Cases)
rule <k> fun Cases => closure(Rho,Cases) ...</k> <env> Rho </env>
Note: The reader may want to get familiar with
how the predefined pattern matching works before proceeding.
The best way to do that is to consult
k/include/modules/patternmatching.k
.
We distinguish two cases when the closure is applied. If the first pattern matches, then we pick the first case: switch to the closed environment, get the matching map and bind all its variables, and finally evaluate the function body of the first case, making sure that the environment is properly recovered afterwards. If the first pattern does not match, then we drop it and thus move on to the next one.
rule (. => getMatching(P, V)) ~> closure(_, P>_  _) V:Val
rule <k> matchResult(M:Map) ~> closure(Rho, _>E  _) _
=> bindMap(M) ~> E ~> setEnv(Rho') ...</k>
<env> Rho' => Rho </env>
rule (matchFailure => .) ~> closure(_, (_>_  Cs:Cases => Cs)) _
// rule <k> closure(Rho, P>E  _) V:Val
// => bindMap(getMatching(P,V)) ~> E ~> setEnv(Rho') ...</k>
// <env> Rho' => Rho </env> when isMatching(P,V)
// rule closure(_, (P>_  Cs:Cases => Cs)) V:Val when notBool isMatching(P,V)
Let and Letrec
To highlight the similarities and differences between let
and
letrec
, we prefer to give them direct semantics instead of
to desugar them like in LAMBDA. See the formal definitions of
bindTo
, bind
, and assignTo
at the end of
this module. Informally, bindTo(Xs, Es)
first
evaluates the expressions Es
in Exps
in the current
environment (i.e., it is strict in its second argument), then it binds
the variables in Xs
in Names
to new locations and adds
those bindings to the environment, and finally writes the values
previously obtained after evaluating the expressions Es
to those
new locations; bind(Xs)
does only the bindings of
Xs
to new locations and adds those bindings to the environment;
and assignTo(Xs,Es)
evaluates the expressions
Es
in the current environment and then it writes the resulting
values to the locations to which the variables Xs
are already
bound to in the environment.
Therefore, let Xs = Es in E
first
evaluates Es
in the current environment, then adds new
bindings for Xs
to fresh locations in the environment, then
writes the values of Es
to those locations, and finally
evaluates E
in the new environment, making sure that the
environment is properly recovered after the evaluation of E
.
On the other hand, letrec
does the same things but in a
different order: it first adds new bindings for Xs
to fresh
locations in the environment, then it evaluates Es
in the new
environment, then it writes the resulting values to their
corresponding locations, and finally it evaluates E
and
recovers the environment. The crucial difference is that the
expressions Es
now see the locations of the variables Xs
in the environment, so if they are functions, which is typically the
case with letrec
, their closures will encapsulate in their
environments the bindings of all the bound variables, including
themselves (thus, we may have a closure value stored at location
L
, whose environment contains a binding of the form
F ↦ L
; this way, the closure can invoke
itself).
rule <k> let Bs in E
=> bindTo(names(Bs),exps(Bs)) ~> E ~> setEnv(Rho) ...</k>
<env> Rho </env>
rule <k> letrec Bs in E
=> bind(names(Bs))~>assignTo(names(Bs),exps(Bs))~>E~>setEnv(Rho)...</k>
<env> Rho </env>
Recall that our syntax allows let
and letrec
to
take any expression in place of its binding. This allows us to use
the already existing function application construct to bind names to
functions, such as, e.g., let x y = y in ...
.
The desugaring macro in the syntax module uncurries such declarations,
and then the semantic rules above only work when the remaining
bindings are identifiers, so the semantics will get stuck on programs
that misuse the let
and letrec
binders.
References
The semantics of references is selfexplanatory, except maybe for the
desugaring rule of ref
, which is further discussed. Note
that &X
grabs the location of X
from the environment.
Sequential composition, which is needed only to accumulate the
side effects due to assignments, was strict in the first argument.
Once evaluated, its first argument is simply discarded:
syntax Name ::= "$x"
rule ref => fun $x > & $x [macro]
rule <k> & X => L ...</k> <env>... X > L ...</env>
rule <k> @ L:Int => V:Val ...</k> <store>... L > V ...</store>
rule <k> L:Int := V:Val => V ...</k> <store>... L > (_=>V) ...</store>
rule _V:Val; E => E
The desugaring rule of ref
(first rule above) works
because &
takes a variable and returns its location (like in C).
Note that some ``pure'' functional programming researchers strongly dislike
the &
construct, but favor ref
. We refrain from having
a personal opinion on this issue here, but support &
in the
environmentbased definition of FUN because it is, technically speaking,
more powerful than ref
. From a language design perspective, it
would be equally easy to drop &
and instead give a direct
semantics to ref
. In fact, this is precisely what we do in the
substitutionbased definition of FUN, because there appears to be no way
to give a substitutionbased definition to the &
construct.
Callcc
As we know it from the LAMBDA++ tutorial, callwithcurrentcontinuation
is quite easy to define in K. We first need to define a special
value wrapping an execution context, that is, an environment saying
where the variables should be looked up, and a computation structure
saying what is left to execute (in a substitutionbased definition,
this special value would be even simpler, as it would only need to
wrap the computation structuresee, for example, the
substitutionbased semantics of LAMBDA++ in the the first part of the
K tutorial, or the substitutionbased definition of FUN). Then
callcc
creates such a value containing the current
environment and the current remaining computation, and passes it to
its argument function. When/If invoked, the special value replaces
the current execution context with its own and continues the execution
normally.
syntax Val ::= cc(Map,K)
rule isVal(callcc) => true
rule <k> (callcc V:Val => V cc(Rho,K)) ~> K </k> <env> Rho </env>
rule <k> cc(Rho,K) V:Val ~> _ => V ~> K </k> <env> _ => Rho </env>
Auxiliary operations
Environment recovery
The environment recovery operation is the same as for the LAMBDA++ language in the K tutorial and many other languages provided with the K distribution. The first ``anywhere'' rule below shows an elegant way to achieve the benefits of tail recursion in K.
syntax KItem ::= setEnv(Map) // TODO: get rid of env
//rule (setEnv(_) => .) ~> setEnv(_) [anywhere]
rule <k> _:Val ~> (setEnv(Rho) => .) ...</k> <env> _ => Rho </env>
[structural]
bindTo
, bind
and assignTo
The meaning of these operations has already been explained when we
discussed the let
and letrec
language constructs
above.
syntax KItem ::= bindTo(Names,Exps) [strict(2)]
 bindMap(Map)
 bind(Names)
rule (. => getMatchingAux(Xs,Vs)) ~> bindTo(Xs:Names,Vs:Vals)
rule matchResult(M:Map) ~> bindTo(_:Names, _:Vals) => bindMap(M)
rule bindMap(.Map) => . [structural]
rule <k> bindMap((X:Name > V:Val => .Map) _:Map) ...</k>
<env> Rho => Rho[X < !L:Int] </env>
<store>... .Map => !L > V ...</store>
[structural]
rule bind(.Names) => . [structural]
rule <k> bind(X:Name,Xs => Xs) ...</k>
<env> Rho => Rho[X < !_L:Int] </env>
[structural]
syntax KItem ::= assignTo(Names,Exps) [strict(2)]
rule <k> assignTo(.Names,.Vals) => . ...</k> [structural]
rule <k> assignTo((X:Name,Xs => Xs),(V:Val,Vs:Vals => Vs)) ...</k>
<env>... X > L ...</env>
<store>... .Map => L > V ...</store> [structural]
Getters
The following auxiliary operations extract the list of identifiers and of expressions in a binding, respectively.
syntax Names ::= names(Bindings) [function]
rule names(.Bindings) => .Names
rule names(X:Name=_ and Bs) => (X,names(Bs))::Names
syntax Exps ::= exps(Bindings) [function]
rule exps(.Bindings) => .Exps
rule exps(_:Name=E and Bs) => E,exps(Bs)
/* Extra kore stuff */
syntax KResult ::= Vals
syntax Exps ::= Names
syntax Names ::= Bottoms
/* Matching */
syntax MatchResult ::= getMatching(Exp, Val) [function]
 getMatchingAux(Exps, Vals) [function]
 mergeMatching(MatchResult, MatchResult) [function]
 matchResult(Map)
 "matchFailure"
rule getMatching(C:ConstructorName(Es:Exps), C(Vs:Vals)) => getMatchingAux(Es, Vs)
rule getMatching([Es:Exps], [Vs:Vals]) => getMatchingAux(Es, Vs)
rule getMatching(C:ConstructorName, C) => matchResult(.Map)
rule getMatching(B:Bool, B) => matchResult(.Map)
rule getMatching(I:Int, I) => matchResult(.Map)
rule getMatching(S:String, S) => matchResult(.Map)
rule getMatching(N:Name, V:Val) => matchResult(N > V)
rule getMatching(_, _) => matchFailure [owise]
rule getMatchingAux((E:Exp, Es:Exps), (V:Val, Vs:Vals)) => mergeMatching(getMatching(E, V), getMatchingAux(Es, Vs))
rule getMatchingAux(.Exps, .Vals) => matchResult(.Map)
rule getMatchingAux(_, _) => matchFailure [owise]
rule mergeMatching(matchResult(M1:Map), matchResult(M2:Map)) => matchResult(M1 M2)
requires intersectSet(keys(M1), keys(M2)) ==K .Set
//rule mergeMatching(_, _) => matchFailure [owsie]
rule mergeMatching(matchResult(_:Map), matchFailure) => matchFailure
rule mergeMatching(matchFailure, matchResult(_:Map)) => matchFailure
rule mergeMatching(matchFailure, matchFailure) => matchFailure
Besides the generic decomposition rules for patterns and values,
we also want to allow [headtail]
matching for lists, so we add
the following custom pattern decomposition rule:
rule getMatching([H:Exp  T:Exp], [V:Val, Vs:Vals])
=> getMatchingAux((H, T), (V, [Vs]))
endmodule