// NOTE: this definition is not up to date with the latest version of K, as it // uses both substitution and symbolic reasoning. // It is intended for documentation and academic purposes only.

FUN — Untyped — Substitution

Author: Grigore Roșu (grosu@illinois.edu)
Organization: University of Illinois at Urbana-Champaign

Author: Traian Florin Șerbănuță (traian.serbanuta@unibuc.ro)
Organization: University of Bucharest

Abstract

This is the substitution-based definition of FUN. For additional explanations regarding the semantics of the various FUN constructs, the reader should consult the emvironment-based definition of FUN.

Syntax

k
requires "substitution.md"
//requires "modules/pattern-matching.k"

module FUN-UNTYPED-COMMON
  imports DOMAINS-SYNTAX

The Syntactic Constructs

k
  syntax Name
  syntax Names ::= List{Name,","}

  syntax Exp ::= Int | Bool | String | Name
               | "(" Exp ")"                       [bracket]
  syntax Exps  ::= List{Exp,","}                   [strict]
  syntax Val
  syntax Vals ::= List{Val,","}

  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]
               | Exp "-" Exp                       [strict, prefer, arith]
               | "-" Exp                           [strict, arith]
               > non-assoc:
                 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]

  syntax Exp ::= "if" Exp "then" Exp "else" Exp    [strict(1)]

  syntax Exp ::= "[" Exps "]"                      [strict]
               | "cons" |  "head" | "tail" | "null?"
               | "[" Exps "|" Exp "]"
  syntax Val ::= "[" Vals "]"

  syntax ConstructorName
  syntax Exp ::= ConstructorName
               | ConstructorName "(" Exps ")"      [prefer, strict(2)]
  syntax Val ::= ConstructorName "(" Vals ")"

  syntax Exp ::= "fun" Cases
               | Exp Exp                           [strict, left]
  syntax Case  ::= Exp "->" Exp                    [binder]
// NOTE: The binder attribute above is the only difference between this
// module and the syntax module of environment-based FUN.  We need
// to fix a bug in order to import modules and override the attributes
// of operations.
  syntax Cases ::= List{Case, "|"}

  syntax Exp ::= "let" Bindings "in" Exp
               | "letrec" Bindings "in" Exp                 [prefer]
  syntax Binding  ::= Exp "=" Exp
  syntax Bindings ::= List{Binding,"and"}

  syntax Exp ::= "ref"
               | "&" Name
               | "@" Exp                           [strict]
               | Exp ":=" Exp                      [strict]
               | Exp ";" Exp                       [strict(1), right]

  syntax Exp ::= "callcc"
               | "try" Exp "catch" "(" Name ")" Exp
  syntax Name ::= "throw" [token]

  syntax Exp ::= "datatype" Type "=" TypeCases Exp

  syntax TypeVar
  syntax TypeVars ::= List{TypeVar,","}

  syntax TypeName
  syntax Type ::= "int" | "bool" | "string"
                | Type "-->" Type                            [right]
                | "(" Type ")"                             [bracket]
                | TypeVar
                | TypeName             [klabel(TypeName), avoid]
                | Type TypeName   [klabel(Type-TypeName), onlyLabel]
                | "(" Types ")" TypeName                    [prefer]
  syntax Types ::= List{Type,","}
  syntax Types ::= TypeVars

  syntax TypeCase ::= ConstructorName
                    | ConstructorName "(" Types ")"
  syntax TypeCases ::= List{TypeCase,"|"}     [klabel(_|TypeCase_)]

Additional Priorities

k
  syntax priority @__FUN-UNTYPED-COMMON
                > ___FUN-UNTYPED-COMMON
                > arith
                > _:=__FUN-UNTYPED-COMMON
                > let_in__FUN-UNTYPED-COMMON
                  letrec_in__FUN-UNTYPED-COMMON
                  if_then_else__FUN-UNTYPED-COMMON
                > _;__FUN-UNTYPED-COMMON
                > fun__FUN-UNTYPED-COMMON
                > datatype_=___FUN-UNTYPED-COMMON
endmodule

module FUN-UNTYPED-MACROS
  imports FUN-UNTYPED-COMMON

Desugaring macros

k
  rule P1 P2 -> E => P1 -> fun P2 -> E                       [macro-rec]
  rule F P = E => F = fun P -> E                             [macro-rec]

  rule [E1,E2,Es:Exps|T] => [E1|[E2,Es|T]]                   [macro-rec]

//  rule 'TypeName(Tn:TypeName) => (.TypeVars) Tn              [macro]
  rule `Type-TypeName`(T:Type, Tn:TypeName) => (T) Tn          [macro]

  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]

  syntax Name ::= "$k" | "$v"
  rule try E catch(X) E'
    => callcc (fun $k -> (fun throw -> E)(fun X -> $k E'))   [macro]

  rule datatype _T = _TCs E => E                               [macro]

mu needed for letrec, but we put it here so we can also write programs with mu in them, which is particularly useful for testing.

k
  syntax Exp ::= "mu" Case

endmodule


module FUN-UNTYPED-SYNTAX
  imports FUN-UNTYPED-COMMON
  imports BUILTIN-ID-TOKENS

  syntax Name ::= r"[a-z][_a-zA-Z0-9]*"            [token, prec(2)]
                | #LowerId                         [token]
  syntax ConstructorName ::= #UpperId              [token]
  syntax TypeVar  ::= r"['][a-z][_a-zA-Z0-9]*"     [token]
  syntax TypeName ::= Name                         [token]
endmodule

Semantics

k
module FUN-UNTYPED
  imports FUN-UNTYPED-COMMON
  imports FUN-UNTYPED-MACROS
  imports DOMAINS
  imports SUBSTITUTION
  //imports PATTERN-MATCHING

  configuration <T color="yellow">
                  <k color="green"> $PGM:Exp </k>
                  <store color="white"> .Map </store>
                </T>

Both Name and functions are values now:

k
  syntax Val ::= Int | Bool | String | Name
  syntax Exp ::= Val
  syntax Exps ::= Vals
  syntax KResult ::= Val
  syntax Exps ::= Names
  syntax Vals ::= Names

  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

  rule if  true then E else _ => E
  rule if false then _ else E => E

  rule isVal(cons) => true
  rule isVal(cons _V:Val) => true
  rule cons V:Val [Vs:Vals] => [V,Vs]

  syntax Val ::= ConstructorName

  rule isVal(fun _) => true
  syntax KVar ::= Name
  syntax Name ::= freshName(Int)    [freshGenerator, function]
  rule freshName(I:Int) => {#parseToken("Name", "#" +String Int2String(I))}:>Name

  rule (. => getMatching(P, V)) ~> (fun P->_ | _) V:Val
  rule matchResult(M:Map) ~> (fun _->E | _) _ => E[M]
  rule (matchFailure => .) ~> (fun (_->_ | Cs:Cases => Cs)) _
//  rule (fun P->E | _) V:Val => E[getMatching(P,V)]  when isMatching(P,V)
//  rule (fun (P->_ | Cs:Cases => Cs)) V:Val  when notBool isMatching(P,V)

We can reduce multiple bindings to one list binding, and then apply the usual desugaring of let into function application. It is important that the rule below is a macro, so let is eliminated immediately, otherwise it may interfere in ugly ways with substitution.

k
  rule let Bs in E => ((fun [names(Bs)] -> E) [exps(Bs)])    [macro]

We only give the semantics of one-binding letrec. Multipe bindings are left as an exercise.

k
  // changed because of parsing error
  //rule mu X:Name -> E => E[(mu X -> E) / X]
  rule mu X:Name -> E => E[X |-> (mu X -> E)]
  rule letrec F:Name = E in E' => let F = (mu F -> E) in E'  [macro]

We cannot have & anymore, but we can give direct semantics to ref. We also have to declare ref to be a value, so that we will never heat on it.

k
//  rule <k> & X => L ...</k>  <env>... X |-> L </env>
  rule isVal(ref) => true
  rule <k> ref V:Val => !L:Int ...</k> <store>... .Map => !L |-> V ...</store>
  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

  syntax Val ::= cc(K)
  rule isVal(callcc) => true
  rule <k> (callcc V:Val => V cc(K)) ~> K </k>
  rule <k> cc(K) V:Val ~> _ => V ~> K </k>

Auxiliary getters

k
  syntax Names ::= names(Bindings)  [function]
  rule names(.Bindings) => .Names
  rule names(X:Name=_ and Bs) => X,names(Bs)

  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

  /* 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 [head|tail] matching for lists, so we add the following custom pattern decomposition rule:

k
  rule getMatching([H:Exp | T:Exp], [V:Val, Vs:Vals])
    => getMatchingAux((H, T), (V, [Vs]))
endmodule