anchor.diff:        raw : bool
         [<Option('s', HelpText = "The stage at which Starling should stop and output.")>]
         stage : string option
  +      [<Option('m', HelpText = "Show full model in term-refinement stages.")>]
  +      showModel: bool
         [<Option('O', HelpText = "Perform no optimisation stages.")>]
         noOptimise : bool
         [<Value(0, MetaName = "input", HelpText = "The file to load (omit, or supply -, for standard input).")>]
  
positive.code:     | HSF of Horn.Horn list
  
  /// Pretty-prints a response.
  let printResponse = 
      function 
      | Frontend f -> Lang.Frontend.printResponse f
      | Destructure f -> printModel (printPAxiom printCView) printDView f
      | Expand e -> printModel (printPAxiom printGView) printDView  e
      | Semantics e -> printModel (printSAxiom printGView) printDView  e
      | Frame {Axioms = f} -> printNumHeaderedList printFramedAxiom f
      | TermGen {Axioms = t} -> printNumHeaderedList (printSTerm printGView printView) t
      | Reify {Axioms = t} -> printNumHeaderedList (printSTerm printViewSet printView) t
      | Flatten m -> printModel (printSTerm printGView printVFunc) printDFunc m
      | Optimise {Axioms = t} -> printNumHeaderedList (printSTerm printGView printVFunc) t
      | Z3 z -> Z3.Backend.printResponse z
      | HSF h -> Starling.Pretty.Horn.printHorns h
  
  
negative.code: 
  /// Runs Starling with the given options, and outputs the results.
  let mainWithOptions opts = 
      let optimise = not opts.noOptimise
      
      let starlingR = 
          match (requestFromStage opts.stage) with
          | Some otype -> runStarling optimise otype opts.input
          | None -> fail Error.BadStage
      
      let pfn = 
          if opts.raw then (sprintf "%A" >> Starling.Pretty.Types.String)
                      else printResponse opts.showModel
      printResult pfn (List.map printError) starlingR
      |> Starling.Pretty.Types.print
      |> printfn "%s"
  