Convert to axiom maps throughout.

This makes debugging slightly easier, as one can sort-of eyeball
where the failures are coming from and map them to the graph.

Some more automation might be nice, though.

Flattener.fs

@@ -48,7 +48,7 @@ let addGlobalsToViewSet gs =
     Multiset.map (addGlobalsToGuarded gs)
 
 /// Adds the globals in gs to the argument list of the assertions in a term.
-let addGlobalsToTerm gs =
+let addGlobalsToTerm gs _ =
     mapTerm id
             (addGlobalsToViewSet (gs Before))
             (funcOfView (gs After))
@@ -90,6 +90,6 @@ let flatten (mdl: Model<PTerm<ViewSet, View>, DView>) =
 
     {Globals = mdl.Globals
      Locals = mdl.Locals
-     Axioms = List.map (addGlobalsToTerm gargs) mdl.Axioms
+     Axioms = Map.map (addGlobalsToTerm gargs) mdl.Axioms
      ViewDefs = List.map (addGlobalsToViewDef gpars) mdl.ViewDefs
      Semantics = mdl.Semantics}

Framer.fs

@@ -22,15 +22,26 @@ let instantiateFrame fg dvs =
 
 /// Converts an axiom into a list of framed axioms, by combining it with the
 /// defining views of a model.
-let frameAxiom ds fg axiom = 
-    List.map (fun { View = vs } -> 
-        { Axiom = axiom
-          Frame = instantiateFrame fg vs }) ds
+let frameAxiom ds fg (name, axiom) =
+    // Each axiom comes in with a name like method_0,
+    // where the 0 is the edge number.
+    // This appends the viewdef number after the edge number.
+    List.mapi
+        (fun i { View = vs } -> 
+              (sprintf "%s_%d" name i,
+               { Axiom = axiom
+                 Frame = instantiateFrame fg vs }))
+         ds
 
 /// Converts a model into a set of framed axioms.
 let frameAxioms {ViewDefs = ds; Axioms = xs} =
     // We use a fresh variable generator to ensure every frame variable is unique.
-    concatMap (frameAxiom ds (freshGen ())) xs
+    let fg = freshGen ()
+
+    xs
+    |> Map.toList
+    |> concatMap (frameAxiom ds fg)
+    |> Map.ofList
 
 /// Converts a model into one over framed axioms.
 let frame mdl = withAxioms (frameAxioms mdl) mdl

Graph.fs

@@ -288,16 +288,16 @@ let combine { Nodes = ans ; Edges = aes }
 ///     The graph whose axioms are to be given.
 /// </param>
 /// <returns>
-///     The edges of <paramref name="_arg1" />
+///     The edges of <paramref name="_arg1" />, as name-edge pairs.
 ///     This is wrapped in a Chessie result over <c>Error</c>.
 /// </returns>
 let axiomatiseGraph { Name = name; Contents = { Nodes = nodes; Edges = edges } } =
     edges
     |> Map.toList
     |> Seq.map
-           (fun (_, { Pre = s; Post = t; Cmd = c }) ->
+           (fun (name, { Pre = s; Post = t; Cmd = c }) ->
                 match (Map.tryFind s nodes, Map.tryFind t nodes) with
-                | Some sn, Some tn -> ok { Pre = sn; Post = tn; Cmd = c }
+                | Some sn, Some tn -> ok (name, { Pre = sn; Post = tn; Cmd = c })
                 | _ -> { Pre = s; Post = t; Cmd = c } |> EdgeOutOfBounds |> fail)
     |> collect
 
@@ -313,15 +313,17 @@ let axiomatiseGraph { Name = name; Contents = { Nodes = nodes; Edges = edges } }
 ///     Such graphs typically represent one method.
 /// </param>
 /// <returns>
-///     A list of axioms characterising <paramref name="graph" />,
+///     A map of axioms characterising <paramref name="graphs" />,
 ///     wrapped in a Chessie result.
 /// </returns>
-let axiomatiseGraphs (graphs: Graph seq)
-                     : Result<Axiom<GView, VFunc> seq, Error> =
+let axiomatiseGraphs graphs =
+    // The map key is redundant, as we already have it inside the
+    // graph iself.
     graphs
-    |> Seq.map axiomatiseGraph
+    |> Map.toSeq
+    |> Seq.map (snd >> axiomatiseGraph)
     |> collect
-    |> lift Seq.concat
+    |> lift (Seq.concat >> Map.ofSeq)
 
 /// <summary>
 ///     Converts a CFG-based model into an axiom-based model.
@@ -338,5 +340,5 @@ let axiomatiseGraphs (graphs: Graph seq)
 ///     wrapped in a Chessie result.
 /// </returns>
 let axiomatise model =
-    lift (fun xs -> withAxioms (Seq.toList xs) model)
+    lift (fun xs -> withAxioms xs model)
          (axiomatiseGraphs model.Axioms)

Horn.fs

@@ -340,16 +340,17 @@ let hsfConditionBody dvs env ps sem =
 
 /// Constructs a series of Horn clauses for a term.
 /// Takes the environment of active global variables.
-let hsfTerm dvs env num {Cmd = c; WPre = w ; Goal = g} =
+let hsfTerm dvs env (name, {Cmd = c; WPre = w ; Goal = g}) =
     lift2 (fun head body ->
-           [ Comment (sprintf "term %d" num)
+           [ Comment (sprintf "term %s" name)
              Clause (head, body) ])
           (Option.get (hsfFunc dvs env g))
           (hsfConditionBody dvs env w c)
 
 /// Constructs a set of Horn clauses for all terms associated with a model.
 let hsfModelTerms gs dvs =
-    Seq.mapi (hsfTerm dvs gs)
+    Map.toSeq
+    >> Seq.map (hsfTerm dvs gs)
     >> collect
     >> lift List.concat
 

Main.fs

@@ -19,7 +19,7 @@ type Options =
       [<Option('s', HelpText = "The stage at which Starling should stop and output.")>]
       stage : string option
       [<Option('t', HelpText = "Show specific axiom or term in term-refinement stages.")>]
-      term : int option
+      term : string option
       [<Option('m', HelpText = "Show full model in term-refinement stages.")>]
       showModel: bool
       [<Option('O', HelpText = "Perform no optimisation stages.")>]

Model.fs

@@ -157,7 +157,7 @@ module Types =
     type Model<'axiom, 'dview> = 
         { Globals : VarMap
           Locals : VarMap
-          Axioms : 'axiom list
+          Axioms : Map<string, 'axiom>
           /// <summary>
           ///   The semantic function for this model.
           /// </summary>
@@ -232,17 +232,24 @@ module Pretty =
                    printType ty ]
 
     /// Pretty-prints a model constraint.
-    let printViewDef pView { View = vs; Def = e } = 
-        keyMap [ ("View", pView vs)
-                 ("Def", withDefault (String "?") (Option.map printBoolExpr e)) ]
+    let printViewDef pView { View = vs; Def = e } =
+        printAssoc Inline
+            [ (String "View", pView vs)
+              (String "Def", withDefault (String "?") (Option.map printBoolExpr e)) ]
+
+    /// Pretty-prints the axiom map for a model.
+    let printModelAxioms pAxiom model =
+        printMap Indented String pAxiom model.Axioms
 
     /// Pretty-prints a model given axiom and defining-view printers.
     let printModel pAxiom pDView model = 
         headed "Model" 
-            [ headed "Shared variables" <| List.map printModelVar (Map.toList model    .Globals)
-              headed "Thread variables" <| List.map printModelVar (Map.toList model    .Locals)
+            [ headed "Shared variables" <|
+                  Seq.singleton (printMap Inline String printType model.Globals)
+              headed "Thread variables" <|
+                  Seq.singleton (printMap Inline String printType model.Locals)
               headed "ViewDefs" <| List.map (printViewDef pDView) model.ViewDefs
-              headed "Axioms" <| List.map pAxiom model.Axioms ]
+              headed "Axioms" <| Seq.singleton (printModelAxioms pAxiom model) ]
 
     /// <summary>
     ///     Enumerations of ways to view part or all of a <c>Model</c>.
@@ -259,7 +266,7 @@ module Pretty =
         /// <summary>
         ///     View a specific term.
         /// </summary>
-        | Term of int
+        | Term of string
 
     /// <summary>
     ///     Prints a model using the <c>ModelView</c> given.
@@ -285,11 +292,11 @@ module Pretty =
     let printModelView mView pAxiom pViewDef m =
         match mView with
         | ModelView.Model -> printModel pAxiom pViewDef m
-        | ModelView.Terms -> printNumHeaderedList pAxiom m.Axioms
-        | ModelView.Term i when 0 < i && i <= List.length m.Axioms ->
-            pAxiom m.Axioms.[i - 1]
-        | ModelView.Term i ->
-            sprintf "no term #%d" i |> String
+        | ModelView.Terms -> printModelAxioms pAxiom m
+        | ModelView.Term termstr ->
+            Map.tryFind termstr m.Axioms
+            |> Option.map pAxiom
+            |> withDefault (termstr |> sprintf "no term '%s'" |> String)
 
 
 /// Rewrites a Term by transforming its Cmd with fC, its WPre with fW,
@@ -313,7 +320,7 @@ let axioms {Axioms = xs} = xs
 
 /// Creates a new model that is the input model with a different axiom set.
 /// The axiom set may be of a different type.
-let withAxioms (xs : 'y list) (model : Model<'x, 'dview>) : Model<'y, 'dview> = 
+let withAxioms (xs : Map<string, 'y>) (model : Model<'x, 'dview>) : Model<'y, 'dview> = 
     { Globals = model.Globals
       Locals = model.Locals
       ViewDefs = model.ViewDefs
@@ -322,9 +329,14 @@ let withAxioms (xs : 'y list) (model : Model<'x, 'dview>) : Model<'y, 'dview> =
 
 /// Maps a pure function f over the axioms of a model.
 let mapAxioms (f : 'x -> 'y) (model : Model<'x, 'dview>) : Model<'y, 'dview> =
-    withAxioms (model |> axioms |> List.map f) model
+    withAxioms (model |> axioms |> Map.map (fun _ -> f)) model
 
 /// Maps a failing function f over the axioms of a model.
 let tryMapAxioms (f : 'x -> Result<'y, 'e>) (model : Model<'x, 'dview>) : Result<Model<'y, 'dview>, 'e> =
     lift (fun x -> withAxioms x model)
-         (model |> axioms |> List.map f |> collect)
+         (model
+          |> axioms
+          |> Map.toSeq
+          |> Seq.map (fun (k, v) -> v |> f |> lift (mkPair k))
+          |> collect
+          |> lift Map.ofList)

Modeller.fs

@@ -812,14 +812,14 @@ let modelMethod gs ls { Signature = sg ; Body = b } =
     // TODO(CaptainHayashi): method parameters
     b
     |> modelBlock gs ls
-    |> lift (fun c -> { Signature = sg ; Body = c })
+    |> lift (fun c -> (sg.Name, { Signature = sg ; Body = c }))
     |> mapMessages (curry MEAxiom sg.Name)
 
 /// Converts a list of methods.
-/// The list is enclosed in a Chessie result.
+/// The resulting map is enclosed in a Chessie result.
 let modelMethods gs ls = 
     // TODO(CaptainHayashi): method parameters
-    List.map (modelMethod gs ls) >> collect
+    Seq.map (modelMethod gs ls) >> collect >> lift Map.ofSeq
 
 /// Checks a view prototype to see if it contains duplicate parameters.
 let checkViewProtoDuplicates (proto : ViewProto) = 

Pretty.fs

@@ -95,12 +95,6 @@ let cmdHeaded header cmds =
 
 let headed name = cmdHeaded (String name)
 
-let keyMap = 
-    List.map (fun (k, v) -> 
-        colonSep [ String k
-                   v ])
-    >> vsep
-
 let ssurround left right mid = Surround((String left), mid, (String right))
 let braced = ssurround "{" "}"
 let angled = ssurround "<" ">"
@@ -113,21 +107,54 @@ let func f xs = hjoin [String f; commaSep xs |> parened]
 /// Pretty-prints Funcs using pxs to print parameters.
 let printFunc pxs { Starling.Collections.Func.Name = f; Params = xs } = func f (Seq.map pxs xs)
 
-/// Pretty-prints a list by headering each by its number.
-let printNumHeaderedList pp = 
-    Seq.ofList
-    >> Seq.mapi (fun i x -> headed (sprintf "%d" (i + 1)) (x |> pp |> Seq.singleton))
-    >> Seq.toList
+/// <summary>
+///    Whether to separate keys and values by colons, or by indentation.
+/// </summary>
+type MapSep =
+    | Inline
+    | Indented
+
+/// <summary>
+///     Pretty-prints an association list of Commands.
+/// </summary>
+/// <param name="mapSep">
+///     The <c>MapSep</c> to use when joining the key and value.
+/// </param>
+/// <param name="_arg1">
+///     An association list, as a sequence,to print using <paramref name="pK" />
+///     and <paramref name="pV" />.
+/// </param>
+/// <returns>
+///     A printer for the given association list.
+/// </returns>
+let printAssoc mapSep = 
+    Seq.map
+        (fun (k, v) ->
+             match mapSep with
+             | Inline -> colonSep [ k; v ]
+             | Indented -> cmdHeaded k [ v ])
     >> vsep
 
-/// Pretty-prints a list by preceding each by its number.
-let printNumPrecList pp = 
-    Seq.ofList
-    >> Seq.mapi (fun i x -> 
-           hsep [ sprintf "%d" (i + 1) |> String
-                  pp x ])
-    >> Seq.toList
-    >> vsep
+/// <summary>
+///     Pretty-prints a map, given printers for keys and values.
+/// </summary>
+/// <param name="mapSep">
+///     The <c>MapSep</c> to use when joining the key and value.
+/// </param>
+/// <param name="pK">
+///     A printer for keys.
+/// </param>
+/// <param name="pV">
+///     A printer for values.
+/// </param>
+/// <param name="_arg1">
+///     A map to print using <paramref name="pK" /> and <paramref name="pV" />.
+/// </param>
+/// <returns>
+///     A printer for the given map.
+/// </returns>
+let printMap mapSep pK pV =
+    Map.toSeq >> Seq.map (pairMap pK pV) >> printAssoc mapSep
 
 /// Formats an error that is wrapping another error.
 let wrapped wholeDesc whole err =

TestStudies.fs

@@ -142,8 +142,8 @@ let holdLock =
 let holdTick =
     func "holdTick" [AExpr (aUnmarked "t")] |> Func |> Multiset.singleton
 
-/// The axioms of the ticketed lock.
-let ticketLockMethods = [
+/// The ticketed lock's lock method.
+let ticketLockLock =
     { Signature = func "lock" []
       Body =
           { Pre = Multiset.empty()
@@ -172,14 +172,22 @@ let ticketLockMethods = [
                                                  |> CFunc.ITE
                                                  |> Multiset.singleton } ] } )
                     Post = holdLock } ] } }
+
+/// The ticket lock's unlock method.
+let ticketLockUnlock =
     { Signature = func "unlock" []
       Body =
           { Pre = holdLock
             Contents =
                 [ { Command =
                         func "!I++" [ AExpr (aBefore "serving"); AExpr (aAfter "serving") ]
                         |> Prim
-                    Post = Multiset.empty() }]}}]
+                    Post = Multiset.empty() }]}}
+
+/// The methods of the ticketed lock.
+let ticketLockMethods =
+    [ ("lock", ticketLockLock)
+      ("unlock", ticketLockUnlock) ] |> Map.ofList
 
 /// The view definitions of the ticketed lock model.
 let ticketLockViewDefs =

Z3.fs

@@ -38,7 +38,7 @@ module Types =
         /// Output of the final Z3 terms only.
         | Combine of Model<Microsoft.Z3.BoolExpr, DFunc>
         /// Output of satisfiability reports for the Z3 terms.
-        | Sat of Microsoft.Z3.Status list
+        | Sat of Map<string, Microsoft.Z3.Status>
 
     /// A Z3 translation error.
     type Error =
@@ -69,9 +69,6 @@ module Pretty =
         | _ -> "unknown"
         >> String
 
-    /// Pretty-prints a list of satisfiability results.
-    let printSats = printNumPrecList printSat
-
     /// Pretty-prints a response.
     let printResponse mview =
         function
@@ -87,7 +84,7 @@ module Pretty =
                 printZ3Exp
                 printDFunc
                 m
-        | Response.Sat s -> printSats s
+        | Response.Sat s -> printMap Inline String printSat s
 
     /// Pretty-prints Z3 translation errors.
     let printError =
@@ -225,13 +222,13 @@ module Translator =
 /// </summary>
 module Run =
     /// Runs Z3 on a single term, given the context in `model`.
-    let runTerm (ctx: Z3.Context) term =
+    let runTerm (ctx: Z3.Context) _ term =
         let solver = ctx.MkSimpleSolver()
         solver.Assert [| term |]
         solver.Check [||]
 
     /// Runs Z3 on a model.
-    let run ctx {Axioms = ts} = List.map (runTerm ctx) ts
+    let run ctx = axioms >> Map.map (runTerm ctx)
 
 
 /// Shorthand for the parser stage of the frontend pipeline.