Lay groundwork for atomic conditionals.

This still needs two more changes:

1) Making microcode conditionals sequentially composed instead of
   parallel composed;
2) Exposing the syntax.

AST.fs

@@ -73,6 +73,10 @@ module Types =
         | Assume of Expression // <assume(e)>
         | SymAtomic of symbol : Symbolic<Expression> // %{xyz}(x, y)
         | Havoc of var : string // havoc var
+        | ACond of
+            cond : Expression
+            * trueBranch : Atomic list
+            * falseBranch : (Atomic list) option
     and Atomic = Node<Atomic'>
 
     /// <summary>
@@ -240,6 +244,43 @@ module Pretty =
     open Starling.Core.TypeSystem.Pretty
     open Starling.Core.Var.Pretty
 
+    /// <summary>
+    ///     Hidden building-blocks for AST pretty-printers.
+    /// </summary>
+    module private Helpers =
+        /// Pretty-prints blocks with the given indent level (in spaces).
+        let printBlock (pCmd : 'Cmd -> Doc) (c : 'Cmd list) : Doc =
+            braced (ivsep (List.map (pCmd >> Indent) c))
+
+        /// <summary>
+        ///     Pretty-prints an if-then-else.
+        /// </summary>
+        /// <param name="pCond">Pretty-printer for conditionals.</param>
+        /// <param name="pLeg">Pretty-printer for 'then'/'else' legs.</param>
+        /// <param name="cond">The conditional to print.</param>
+        /// <param name="thenLeg">The 'then' leg to print.</param>
+        /// <param name="elseLeg">The optional 'else' leg to print.</param>
+        /// <typeparam name="Cond">Type of conditionals.</typeparam>
+        /// <typeparam name="Leg">Type of 'then'/'else' leg items.</typeparam>
+        /// <returns>
+        ///     A <see cref="Doc"/> capturing the if-then-else form.
+        /// </returns>
+        let printITE
+          (pCond : 'Cond -> Doc)
+          (pLeg : 'Leg -> Doc)
+          (cond : 'Cond)
+          (thenLeg : 'Leg list)
+          (elseLeg : ('Leg list) option)
+          : Doc =
+            syntaxStr "if"
+            <+> parened (pCond cond)
+            <+> printBlock pLeg thenLeg
+            <+> (maybe
+                    Nop
+                    (fun e -> syntaxStr "else" <+> printBlock pLeg e)
+                    elseLeg)
+
+
     /// Pretty-prints Boolean operations.
     let printBinOp : BinOp -> Doc =
         function
@@ -290,7 +331,7 @@ module Pretty =
     /// <param name="s">The symbolic to print.</param>
     /// <returns>
     ///     The <see cref="Doc"/> resulting from printing <paramref name="s"/>.
-    /// </returns> 
+    /// </returns>
     and printSymbolic (s : Symbolic<Expression>) : Doc =
         String "%"
         <->
@@ -360,7 +401,7 @@ module Pretty =
         equality (printExpression dest) (printExpression src)
 
     /// Pretty-prints atomic actions.
-    let printAtomic' : Atomic' -> Doc =
+    let rec printAtomic' : Atomic' -> Doc =
         function
         | CompareAndSwap(l, f, t) ->
             func "CAS" [ printExpression l
@@ -376,13 +417,9 @@ module Pretty =
         | Assume e -> func "assume" [ printExpression e ]
         | SymAtomic sym -> printSymbolic sym
         | Havoc var -> String "havoc" <+> String var
-    let printAtomic (x : Atomic) : Doc = printAtomic' x.Node
-
-    /// Pretty-prints blocks with the given indent level (in spaces).
-    let printBlock (pCmd : 'cmd -> Doc)
-                   (c : 'cmd list)
-                   : Doc =
-        braced (ivsep (List.map (pCmd >> Indent) c))
+        | ACond (cond = c; trueBranch = t; falseBranch = f) ->
+            Helpers.printITE printExpression printAtomic c t f
+    and printAtomic (x : Atomic) : Doc = printAtomic' x.Node
 
     /// Pretty-prints commands.
     let rec printCommand' (cmd : Command') : Doc =
@@ -397,33 +434,33 @@ module Pretty =
                          |> semiSep |> withSemi |> braced |> angled)
                   yield! Seq.map (uncurry printAssign) qs }
             |> semiSep |> withSemi
-        | Command'.If(c, t, fo) ->
-            hsep [ "if" |> String |> syntax
-                   c |> printExpression |> parened
-                   t |> printBlock printCommand
-                   (maybe Nop
-                        (fun f ->
-                            hsep
-                                [ "else" |> String |> syntax
-                                  printBlock printCommand f ])
-                        fo) ]
+        | Command'.If(c, t, f) ->
+            Helpers.printITE printExpression printCommand c t f
         | Command'.While(c, b) ->
             hsep [ "while" |> String |> syntax
                    c |> printExpression |> parened
-                   b |> printBlock printCommand ]
+                   b |> Helpers.printBlock printCommand ]
         | Command'.DoWhile(b, c) ->
             hsep [ "do" |> String |> syntax
-                   b |> printBlock printCommand
+                   b |> Helpers.printBlock printCommand
                    "while" |> String |> syntax
                    c |> printExpression |> parened ]
             |> withSemi
         | Command'.Blocks bs ->
             bs
-            |> List.map (printBlock printCommand)
+            |> List.map (Helpers.printBlock printCommand)
             |> hsepStr "||"
         | Command'.ViewExpr v -> printMarkedView printView v
     and printCommand (x : Command) : Doc = printCommand' x.Node
 
+    /// <summary>
+    ///     Prints a command block.
+    /// </summary>
+    /// <param name="block">The block to print.</param>
+    /// <returns>A <see cref="Doc"/> capturing <paramref name="block"/>.
+    let printCommandBlock (block : Command list) : Doc =
+        Helpers.printBlock printCommand block
+
     /// <summary>
     ///     Pretty-prints a type literal.
     /// </summary>
@@ -454,7 +491,7 @@ module Pretty =
                     : Doc =
         hsep [ "method" |> String |> syntax
                printFunc (printParam >> syntaxIdent) s
-               printBlock pCmd b ]
+               Helpers.printBlock pCmd b ]
 
     /// Pretty-prints a general view prototype.
     let printGeneralViewProto (pParam : 'Param -> Doc)(vp : GeneralViewProto<'Param>) : Doc =

Collator.fs

@@ -80,7 +80,7 @@ module Pretty =
               vsep <| Seq.map (printScriptVar "shared") cs.SharedVars
               vsep <| Seq.map (printScriptVar "thread") cs.ThreadVars
               vsep <| Seq.map (uncurry printConstraint) cs.Constraints
-              printMap Indented String (printBlock printCommand) cs.Methods ]
+              printMap Indented String printCommandBlock cs.Methods ]
 
         // Add in search, but only if it actually exists.
         let all =
@@ -188,7 +188,7 @@ module ParamDesugar =
         let rewriteAFunc { Name = n; Params = ps } =
             { Name = n; Params = List.map rewriteExpression ps }
 
-        let rewriteAtomic atom =
+        let rec rewriteAtomic atom =
             let rewriteAtomic' =
                 function
                 | CompareAndSwap (src, test, dest) ->
@@ -202,6 +202,11 @@ module ParamDesugar =
                 | SymAtomic sym ->
                     SymAtomic (rewriteSymbolic sym)
                 | Havoc v -> Havoc (rewriteVar v)
+                | ACond (cond = c; trueBranch = t; falseBranch = f) ->
+                    ACond
+                        (rewriteExpression c,
+                         List.map rewriteAtomic t,
+                         Option.map (List.map rewriteAtomic) f)
             { atom with Node = rewriteAtomic' atom.Node }
 
         let rewritePrimSet { PreAssigns = ps; Atomics = ts; PostAssigns = qs } =

Command.fs

@@ -107,6 +107,11 @@ module Types =
         | Stored of StoredCommand
         /// <summary>An entirely symbolic command.</summary>
         | SymC of Symbolic<Expr<Sym<Var>>>
+        /// <summary>A branching command.</summary>
+        | PrimBranch of
+            cond : BoolExpr<Sym<Var>>
+            * trueBranch : PrimCommand list
+            * falseBranch : (PrimCommand list) option
         override this.ToString() = sprintf "%A" this
 
     /// <summary>
@@ -186,12 +191,14 @@ module Queries =
     ///     <c>true</c> if the command is a no-op;
     ///     <c>false</c> otherwise.
     /// </returns>
-    let isNop (prim : PrimCommand) : bool =
+    let rec isNop (prim : PrimCommand) : bool =
         match prim with
         // No Intrinsic commands are no-ops at the moment.
         | Intrinsic _ -> false
         | Stored { Results = ps } -> List.isEmpty ps
         | SymC _ -> false
+        | PrimBranch (trueBranch = t; falseBranch = f) ->
+            List.forall isNop t && maybe true (List.forall isNop) f
 
     /// <summary>
     ///     Active pattern matching no-operation commands.
@@ -237,14 +244,17 @@ module Queries =
 
     /// Combines the results of each command into a list of all results
     let commandResults cs =
-        // TODO(CaptainHayashi): are sym working variables really results?
-        let primResults prim =
+        let rec primResults prim =
             match prim with
             | Intrinsic (IAssign r) -> [ Expr.Int (r.TypeRec, r.LValue) ]
             | Intrinsic (BAssign r) -> [ Expr.Bool (r.TypeRec, r.LValue) ]
             | Intrinsic (Havoc v) -> [ mkVarExp (mapCTyped Reg v) ]
             | Stored { Results = rs } -> rs
             | SymC _ -> []
+            // TODO(MattWindsor91): is this correct?
+            | PrimBranch (trueBranch = t; falseBranch = f) ->
+                concatMap primResults t
+                @ maybe [] (concatMap primResults) f
 
         List.fold (fun a c -> a @ primResults c) [] cs
 
@@ -272,14 +282,18 @@ module Queries =
             | SymArg a -> Some a
             | _ -> None
 
-        let f prim =
+        let rec f prim =
             match prim with
             // TODO(CaptainHayashi): is this sensible!?
             | Stored { Args = xs } -> List.map symExprVars xs
             | SymC s -> List.map symExprVars (List.choose argsOnly s)
             | Intrinsic (IAssign { RValue = y } ) -> [ symExprVars (indefIntExpr y) ]
             | Intrinsic (BAssign { RValue = y } ) -> [ symExprVars (indefBoolExpr y) ]
             | Intrinsic (Havoc _) -> []
+            // TODO(CaptainHayashi): is this sensible!?
+            | PrimBranch (trueBranch = t; falseBranch = fb) ->
+                concatMap f t @ maybe [] (concatMap f) fb
+
         let vars = collect (concatMap f cmd)
         lift Set.unionMany vars
 
@@ -454,11 +468,19 @@ module Pretty =
         <-> String "}"
 
     /// Pretty-prints a PrimCommand.
-    let printPrimCommand (prim : PrimCommand) : Doc =
+    let rec printPrimCommand (prim : PrimCommand) : Doc =
         match prim with
         | Intrinsic s -> printIntrinsicCommand s
         | Stored s -> printStoredCommand s
         | SymC s -> printSymCommand s
+        | PrimBranch (cond = c; trueBranch = t; falseBranch = f) ->
+            vsep
+                [ String "if" <+> printBoolExpr (printSym printVar) c
+                  headed "then" (List.map printPrimCommand t)
+                  maybe
+                    Nop
+                    (fun x -> headed "else" (List.map printPrimCommand x))
+                    f ]
 
     /// Pretty-prints a Command.
     let printCommand : Command -> Doc = List.map printPrimCommand >> semiSep

Modeller.fs

@@ -166,6 +166,8 @@ module Types =
         | PrimNotImplemented of what : string
         /// <summary>Handling variables in symbolic prims caused an error.</summary>
         | SymVarError of err : VarMapError
+        /// <summary>An atomic branch contains a bad if-then-else condition.</summary>
+        | BadAtomicITECondition of expr: AST.Types.Expression * err: ExprError
 
     /// Represents an error when converting a method.
     type MethodError =
@@ -378,6 +380,9 @@ module Pretty =
         | SymVarError err ->
             errorStr "error in translating symbolic command"
             <&> printVarMapError err
+        | BadAtomicITECondition (expr, err) ->
+            wrapped "if-then-else condition" (printExpression expr)
+                                             (printExprError err)
 
     /// Pretty-prints method errors.
     let printMethodError (err : MethodError) : Doc =
@@ -1721,8 +1726,8 @@ let modelPostfix (ctx : MethodContext) (operand : Expression) (mode : FetchMode)
 /// Converts a single atomic command from AST to part-commands.
 let rec modelAtomic
   (ctx : MethodContext) (a : Atomic) : Result<PrimCommand, PrimError> =
-    let prim =
-        match a.Node with
+    let rec prim n =
+        match n.Node with
         | CompareAndSwap(dest, test, set) -> modelCAS ctx dest test set
         | Fetch(dest, src, mode) -> modelFetch ctx dest src mode
         | Postfix(operand, mode) -> modelPostfix ctx operand mode
@@ -1734,21 +1739,32 @@ let rec modelAtomic
         | Havoc var ->
             let varMR = mapMessages SymVarError (Env.lookup ctx.Env Full var)
             lift (fun varM -> Intrinsic (IntrinsicCommand.Havoc varM)) varMR
-
-
         | SymAtomic sym ->
             // TODO(CaptainHayashi): split out.
             let symMR =
                 (tryMapSym
                     (wrapMessages BadExpr (modelExpr ctx.Env Full id))
                          sym)
             lift SymC symMR
+        | ACond (cond = c; trueBranch = t; falseBranch = f) ->
+            let cTMR =
+                wrapMessages BadExpr (modelBoolExpr ctx.Env Full id) c
+            // An if condition needs to be of type 'bool', not a subtype.
+            let cMR =
+                bind
+                    (checkBoolIsNormalType
+                     >> mapMessages (fun m -> BadAtomicITECondition (c, ExprBadType m)))
+                    cTMR
+            let tMR = collect (List.map prim t)
+            let fMR = maybe (ok None) (List.map prim >> collect >> lift Some) f
+            lift3 (curry3 PrimBranch) cMR tMR fMR
+
 
     lift
         (function
          | Stored cmd -> Stored { cmd with Node = Some a }
          | x -> x)
-        prim
+        (prim a)
 
 /// Converts a local variable assignment to a Prim.
 and modelAssign

Optimiser.fs

@@ -576,7 +576,7 @@ module Graph =
                     | Ok (pvars, _) ->
                         Seq.forall typedVarIsThreadLocal (Set.toSeq pvars)
 
-        let isLocalPrim prim =
+        let rec isLocalPrim prim =
             match prim with
             | // TODO(CaptainHayashi): too conservative?
               SymC _ -> false
@@ -585,6 +585,10 @@ module Graph =
             | // TODO(CaptainHayashi): is this correct?
               Intrinsic (Havoc v) -> typedVarIsThreadLocal v
             | Stored { Args = ps } -> Seq.forall isLocalArg ps
+            | PrimBranch (trueBranch = t; falseBranch = f) ->
+                List.forall isLocalPrim t
+                && maybe true (List.forall isLocalPrim) f
+
 
         List.forall isLocalPrim cmd
 

Pretty.fs

@@ -57,6 +57,7 @@ let warning d = Styled([Yellow], d)
 let success d = Styled([Green], d)
 let inconclusive d = Styled([Blue], d)
 
+let syntaxStr s = syntax (String s)
 let errorStr s = error (String s)
 let errorContextStr s = errorContext (String s)
 let errorInfoStr s = errorInfo (String s)

Semantics.fs

@@ -617,10 +617,10 @@ let microcodeRoutineToBool
 /// <param name="semantics">The map from command to microcode schemata.</param>
 /// <param name="prim">The primitive command to instantiate.</param>
 /// <returns>
-///     If the instantiation succeeded, the resulting list of parallel-composed
+///     If the instantiation succeeded, the resulting list of
 ///     <see cref="Microcode"/> instructions.
 /// </returns>
-let instantiateToMicrocode
+let rec instantiateToMicrocode
   (semantics : PrimSemanticsMap)
   (prim : PrimCommand)
   : Result<Microcode<Expr<Sym<Var>>, Sym<Var>> list, Error> =
@@ -650,6 +650,16 @@ let instantiateToMicrocode
             mapMessages Traversal (mapTraversal subInMCode s.Body)
 
         bind instantiate typeCheckedDefR
+    | PrimBranch (cond = c; trueBranch = t; falseBranch = f) ->
+        let inst =
+            List.map (instantiateToMicrocode semantics)
+            >> collect
+            >> lift List.concat
+
+        lift2 
+            (fun tM fM -> [ Branch (c, tM, fM) ])
+            (inst t)
+            (maybe (ok []) inst f)
 
 /// <summary>
 ///     Translates a command to a multi-state Boolean expression.