val is_arith_expr : term -> tm expr
let is_arith_expr t =
  let! a = as_arith_expr t in
  match a with
  | Atom _ t -> begin
    let hd, tl = collect_app_ref t in
    match inspect_ln hd, tl with
    | Tv_FVar _, []
    | Tv_BVar _, []
    | Tv_Var _, [] -> return a
    | _ -> let! s = lift term_to_string t in
           fail ("not an arithmetic expression: (" ^ s ^ ")")
  end
  | _ -> return a
val is_arith_expr : term -> tm expr
let is_arith_expr t =
let! a = as_arith_expr t in
match a with
| Atom _ t ->
  let hd, tl = collect_app_ref t in
  (match inspect_ln hd, tl with
    | Tv_FVar _, [] | Tv_BVar _, [] | Tv_Var _, [] -> return a
    | _ ->
      let! s = lift term_to_string t in
      fail ("not an arithmetic expression: (" ^ s ^ ")"))
| _ -> return a
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.Types.term FStar.Reflection.V2.Arith.op_let_Bang FStar.Reflection.V2.Arith.expr FStar.Reflection.V2.Arith.as_arith_expr Prims.nat Prims.l_or Prims.eq2 Prims.precedes Prims.list FStar.Reflection.V2.Data.argv FStar.Pervasives.Native.fst FStar.Reflection.V2.Data.aqualv FStar.Pervasives.Native.Mktuple2 FStar.Reflection.V2.Data.term_view FStar.Reflection.V2.Builtins.inspect_ln FStar.Reflection.Types.fv FStar.Reflection.V2.Arith.return FStar.Reflection.Types.bv FStar.Reflection.Types.namedv FStar.Pervasives.Native.tuple2 Prims.string FStar.Reflection.V2.Arith.lift FStar.Tactics.V2.Builtins.term_to_string FStar.Reflection.V2.Arith.fail Prims.op_Hat FStar.Reflection.V2.Arith.tm FStar.Reflection.V2.Derived.Lemmas.collect_app_ref
(*
   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)
private 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) // why? To have a catch-all pattern and thus an easy WP

val lift : ('a -> Tac 'b) -> ('a -> tm 'b)
let lift f x st =
    Inr (f x, st)

val liftM : ('a -> 'b) -> (tm 'a -> tm 'b)
let liftM f x =
    let! xx = x in
    return (f xx)

val liftM2 : ('a -> 'b -> 'c) -> (tm 'a -> tm 'b -> tm 'c)
let liftM2 f x y =
    let! xx = x in
    let! yy = y in
    return (f xx yy)

val liftM3 : ('a -> 'b -> 'c -> 'd) -> (tm 'a -> tm 'b -> tm 'c -> tm 'd)
let liftM3 f x y z =
    let! xx = x in
    let! yy = y in
    let! zz = z in
    return (f xx yy zz)


private let rec find_idx (f : 'a -> Tac bool) (l : list 'a) : Tac (option ((n:nat{n < List.Tot.Base.length l}) * 'a)) =
    match l with
    | [] -> None
    | x::xs ->
        if f x
        then Some (0, x)
        else begin match find_idx f xs with
             | None -> None
             | Some (i, x) -> Some (i+1, x)
             end

private let atom (t:term) : tm expr = fun (n, atoms) ->
    match find_idx (term_eq_old t) atoms with
    | None -> Inr (Atom n t, (n + 1, t::atoms))
    | Some (i, t) -> Inr (Atom (n - 1 - i) t, (n, atoms))

private val fail : (#a:Type) -> string -> tm a
private let fail #a s = fun i -> Inl s

val as_arith_expr : term -> tm expr
#push-options "--initial_fuel 4 --max_fuel 4"
let rec as_arith_expr (t:term) =
    let hd, tl = collect_app_ln t in
    // Invoke [collect_app_order]: forall (arg, qual) ∈ tl, (arg, qual) << t
    collect_app_order t;
    // [precedes_fst_tl]: forall (arg, qual) ∈ tl, arg << t
    let precedes_fst_tl (arg: term) (q: aqualv)
      : Lemma (List.Tot.memP (arg, q) tl ==> arg << t)
      = let _: argv = arg, q in ()
    in Classical.forall_intro_2 (precedes_fst_tl);
    match inspect_ln hd, tl with
    | Tv_FVar fv, [(e1, Q_Implicit); (e2, Q_Explicit) ; (e3, Q_Explicit)] ->
      let qn = inspect_fv fv in
      let e2' = as_arith_expr e2 in
      let e3' = as_arith_expr e3 in
      if qn = land_qn then liftM2 Land e2' e3'
      else if qn = lxor_qn then liftM2 Lxor e2' e3'
      else if qn = lor_qn then liftM2 Lor e2' e3'
      else if qn = shiftr_qn then liftM2 Shr e2' e3'
      else if qn = shiftl_qn then liftM2 Shl e2' e3'
      else if qn = udiv_qn then liftM2 Udiv e2' e3'
      else if qn = umod_qn then liftM2 Umod e2' e3'
      else if qn = mul_mod_qn then liftM2 MulMod e2' e3'
      else if qn = ladd_qn then liftM2 Ladd e2' e3'
      else if qn = lsub_qn then liftM2 Lsub e2' e3'
      else atom t
    | Tv_FVar fv, [(l, Q_Explicit); (r, Q_Explicit)] ->
        let qn = inspect_fv fv in
        // Have to go through hoops to get F* to typecheck this.
        // Maybe the do notation is twisting the terms somehow unexpected?
        let ll = as_arith_expr l in
        let rr = as_arith_expr r in
        if      qn = add_qn   then liftM2 Plus ll rr
        else if qn = minus_qn then liftM2 Minus ll rr
        else if qn = mult_qn  then liftM2 Mult ll rr
        else if qn = mult'_qn then liftM2 Mult ll rr
        else atom t
    | Tv_FVar fv, [(l, Q_Implicit); (r, Q_Explicit)] ->
        let qn = inspect_fv fv in
        let ll = as_arith_expr l in
        let rr = as_arith_expr r in
        if qn = nat_bv_qn then liftM NatToBv rr
        else atom t
    | Tv_FVar fv, [(a, Q_Explicit)] ->
        let qn = inspect_fv fv in
        let aa = as_arith_expr a in
        if qn = neg_qn then liftM Neg aa
        else atom t
    | Tv_Const (C_Int i), _ ->
        return (Lit i)
    | _ ->
        atom t
#pop-options

val is_arith_expr : term -> tm expr
val is_arith_expr : term -> tm expr
t: FStar.Reflection.Types.term -> FStar.Reflection.V2.Arith.tm FStar.Reflection.V2.Arith.expr