val op_let_Bang (m: tm 'a) (f: ('a -> tm 'b)) : tm 'b
let (let!) (m : tm 'a) (f : 'a -> tm 'b) : tm 'b =
    fun i -> match m i with
             | Inr (x, j) -> f x j
             | s -> Inl (Inl?.v s)
val op_let_Bang (m: tm 'a) (f: ('a -> tm 'b)) : tm 'b
let op_let_Bang (m: tm 'a) (f: ('a -> tm 'b)) : tm 'b =
fun i ->
  match m i with
  | Inr (x, j) -> f x j
  | s -> Inl (Inl?.v s)
FStar.Reflection.V2.Arith.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
FStar.Reflection.V2.Arith.fst
FStar.Reflection.V2.Arith.tm FStar.Reflection.V2.Arith.st FStar.Pervasives.either Prims.string FStar.Pervasives.Native.tuple2 FStar.Pervasives.Inl FStar.Pervasives.__proj__Inl__item__v
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Reflection.V2.Arith

open FStar.Tactics.V2
open FStar.Reflection.V2
module O = FStar.Order

(*
 * Simple decision procedure to decide if a term is an "arithmetic
 * proposition", by which we mean a simple relation between two
 * arithmetic expressions (each representing integers or naturals)
 *
 * Main use case: deciding, in a tactic, if a goal is an arithmetic
 * expression and applying a custom decision procedure there (instead of
 * feeding to the SMT solver)
 *)

noeq
type expr =
    | Lit     : int -> expr
    // atom, contains both a numerical ID and the actual term encountered
    | Atom    : nat -> term -> expr
    | Plus    : expr -> expr -> expr
    | Mult    : expr -> expr -> expr
    | Minus   : expr -> expr -> expr
    | Land    : expr -> expr -> expr
    | Lxor    : expr -> expr -> expr
    | Lor     : expr -> expr -> expr
    | Ladd    : expr -> expr -> expr
    | Lsub    : expr -> expr -> expr
    | Shl     : expr -> expr -> expr
    | Shr     : expr -> expr -> expr
    | Neg     : expr -> expr
    | Udiv    : expr -> expr -> expr
    | Umod    : expr -> expr -> expr
    | MulMod  : expr -> expr -> expr
    | NatToBv : expr -> expr
    // | Div   : expr -> expr -> expr // Add this one?

noeq
type connective =
    | C_Lt | C_Eq | C_Gt | C_Ne

noeq
type prop =
    | CompProp : expr -> connective -> expr -> prop
    | AndProp  : prop -> prop -> prop
    | OrProp   : prop -> prop -> prop
    | NotProp  : prop -> prop

let lt e1 e2 = CompProp e1 C_Lt e2
let le e1 e2 = CompProp e1 C_Lt (Plus (Lit 1) e2)
let eq e1 e2 = CompProp e1 C_Eq e2
let ne e1 e2 = CompProp e1 C_Ne e2
let gt e1 e2 = CompProp e1 C_Gt e2
let ge e1 e2 = CompProp (Plus (Lit 1) e1) C_Gt e2

(* Define a traversal monad! Makes exception handling and counter-keeping easy *)
private let st = p:(nat * list term){fst p == List.Tot.Base.length (snd p)}
private let tm a = st -> Tac (either string (a * st))
private let return (x:'a) : tm 'a = fun i -> Inr (x, i)
val op_let_Bang (m: tm 'a) (f: ('a -> tm 'b)) : tm 'b
m: FStar.Reflection.V2.Arith.tm 'a -> f: (_: 'a -> FStar.Reflection.V2.Arith.tm 'b)
  -> FStar.Reflection.V2.Arith.tm 'b