formatting

Author: lamg

Prover/Core.fs

@@ -317,7 +317,7 @@ and Proposition =
       | :? Integer as p ->
         match p with
         | ExtInteger m -> loop m
-        | Integer(_) -> [], []
+        | Integer _ -> [], []
         | UnaryMinus m -> loop m
         | Plus(x, y)
         | Minus(x, y)
@@ -542,14 +542,14 @@ and Sequence =
     member this.TextualSubstitution (varName: string) (expr: WExpr) : WExpr =
       match this with
       | ExtSequence e -> ExtSequence(e.TextualSubstitution varName expr) :> WExpr
-      | Empty(_) -> failwith "Not Implemented"
+      | Empty _ -> failwith "Not Implemented"
       | Cons(_, _) -> failwith "Not Implemented"
       | Concat(_, _) -> failwith "Not Implemented"
       | IsPrefix(_, _) -> failwith "Not Implemented"
       | IsSuffix(_, _) -> failwith "Not Implemented"
-      | Length(_) -> failwith "Not Implemented"
-      | Head(_) -> failwith "Not Implemented"
-      | Tail(_) -> failwith "Not Implemented"
+      | Length _ -> failwith "Not Implemented"
+      | Head _ -> failwith "Not Implemented"
+      | Tail _ -> failwith "Not Implemented"
 
 and WSort =
   | WInt
@@ -750,7 +750,7 @@ let internal checkAssuming (ctx: Context) (assumptions: Proposition list) (p: Pr
   assumptions
   |> List.iter (fun l -> solver.Assert((l :> WExpr).ToZ3Expr(ctx, Map.empty) :?> BoolExpr))
 
-  let exp = ((p :> WExpr).ToZ3Expr(ctx, Map.empty)) :?> BoolExpr
+  let exp = (p :> WExpr).ToZ3Expr(ctx, Map.empty) :?> BoolExpr
   solver.Assert(ctx.MkNot exp)
 
   match solver.Check() with

Prover/LanguageServices/Wybe/Semantics.fs

@@ -380,10 +380,10 @@ let semanticExprToWExpr (e: SemanticTree) : DomainWExpr =
       | Lit(Int i), [] -> Integer i :> WExpr
       | Unary(Op.UnaryMinus, _), [ c ] -> -(typedToWExpr c :?> Integer) :> WExpr
       | Unary(Op.Length, _), [ c ] -> len (typedToWExpr c) :> WExpr
-      | Binary(_, Op.Plus, _), [ l; r ] -> ((typedToWExpr l :?> Integer) + (typedToWExpr r :?> Integer)) :> WExpr
-      | Binary(_, Op.Minus, _), [ l; r ] -> ((typedToWExpr l :?> Integer) - (typedToWExpr r :?> Integer)) :> WExpr
-      | Binary(_, Op.Times, _), [ l; r ] -> ((typedToWExpr l :?> Integer) * (typedToWExpr r :?> Integer)) :> WExpr
-      | Binary(_, Op.Div, _), [ l; r ] -> ((typedToWExpr l :?> Integer) / (typedToWExpr r :?> Integer)) :> WExpr
+      | Binary(_, Op.Plus, _), [ l; r ] -> (typedToWExpr l :?> Integer) + (typedToWExpr r :?> Integer) :> WExpr
+      | Binary(_, Op.Minus, _), [ l; r ] -> (typedToWExpr l :?> Integer) - (typedToWExpr r :?> Integer) :> WExpr
+      | Binary(_, Op.Times, _), [ l; r ] -> (typedToWExpr l :?> Integer) * (typedToWExpr r :?> Integer) :> WExpr
+      | Binary(_, Op.Div, _), [ l; r ] -> (typedToWExpr l :?> Integer) / (typedToWExpr r :?> Integer) :> WExpr
       | Expr.Var name, [] -> mkIntVar name
       | _ -> failwith $"not implemented: {exprToTree e.Expr}"
     | Some(Type.Array inner) ->

Test/WybeLangTest.fs

@@ -115,8 +115,8 @@ let ``weakest precondition assignment`` () =
 
 [<Fact>]
 let ``weakest precondition composition`` () =
-  [ Becomes ["n", DomainWExpr(None, n + 1)],
-    Becomes ["n", DomainWExpr(None, n * 2)],
+  [ Becomes [ "n", DomainWExpr(None, n + 1) ],
+    Becomes [ "n", DomainWExpr(None, n * 2) ],
     StateSpace(vars, n > zero),
     StateSpace(vars, (n + 1) * 2 > zero) ]
   |> List.iter (fun (s, t, postcondition, expected) ->