val reification_aux (#a: Type) (mult unit me: term) : Tac (exp a)
let rec reification_aux (#a:Type) (mult unit me : term) : Tac (exp a) =
  let hd, tl = collect_app_ref me in
  let tl = list_unref tl in
  match inspect hd, tl with
  | Tv_FVar fv, [(me1, Q_Explicit) ; (me2, Q_Explicit)] ->
    if term_eq_old (pack (Tv_FVar fv)) mult
    then Mult (reification_aux mult unit me1) (reification_aux mult unit me2)
    else Var (unquote me)
  | _, _ ->
    if term_eq_old me unit
    then Unit
    else Var (unquote me)
val reification_aux (#a: Type) (mult unit me: term) : Tac (exp a)
let rec reification_aux (#a: Type) (mult unit me: term) : Tac (exp a) =
let hd, tl = collect_app_ref me in
let tl = list_unref tl in
match inspect hd, tl with
| Tv_FVar fv, [me1, Q_Explicit ; me2, Q_Explicit] ->
  if term_eq_old (pack (Tv_FVar fv)) mult
  then Mult (reification_aux mult unit me1) (reification_aux mult unit me2)
  else Var (unquote me)
| _, _ -> if term_eq_old me unit then Unit else Var (unquote me)
FStar.Tactics.CanonMonoid.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.List.Tot.fst.checked FStar.List.fst.checked FStar.Algebra.Monoid.fst.checked
FStar.Tactics.CanonMonoid.fst
FStar.Tactics.NamedView.term FStar.Reflection.Types.term Prims.l_or Prims.eq2 Prims.precedes Prims.list FStar.Reflection.V2.Data.argv FStar.Pervasives.Native.fst FStar.Reflection.V2.Data.aqualv FStar.Reflection.Types.fv FStar.Tactics.CanonMonoid.Mult FStar.Tactics.CanonMonoid.exp FStar.Tactics.CanonMonoid.reification_aux Prims.bool FStar.Tactics.CanonMonoid.Var FStar.Tactics.V2.Builtins.unquote FStar.Tactics.V2.Builtins.term_eq_old FStar.Tactics.NamedView.pack FStar.Tactics.NamedView.Tv_FVar FStar.Tactics.NamedView.named_term_view FStar.Pervasives.Native.tuple2 FStar.Tactics.CanonMonoid.Unit FStar.Pervasives.Native.Mktuple2 FStar.Tactics.NamedView.inspect FStar.List.Tot.Base.list_unref 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.Tactics.CanonMonoid

open FStar.Algebra.Monoid
open FStar.List
open FStar.Reflection.V2
open FStar.Tactics.V2

(* Only dump when debugging is on *)
let dump m = if debugging () then dump m

(* "A Monoid Expression Simplifier" ported from
   http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html *)

type exp (a:Type) : Type =
  | Unit : exp a
  | Var : a -> exp a
  | Mult : exp a -> exp a -> exp a

let rec exp_to_string (#a:Type) (a_to_string:a->string) (e:exp a) =
  match e with
  | Unit -> "Unit"
  | Var x -> "Var " ^ a_to_string x
  | Mult e1 e2 -> "Mult (" ^ exp_to_string a_to_string e1
                   ^ ") (" ^ exp_to_string a_to_string e2 ^ ")"

let rec mdenote (#a:Type) (m:monoid a) (e:exp a) : a =
  match e with
  | Unit -> Monoid?.unit m
  | Var x -> x
  | Mult e1 e2 -> Monoid?.mult m (mdenote m e1) (mdenote m e2)

let rec mldenote (#a:Type) (m:monoid a) (xs:list a) : a =
  match xs with
  | [] -> Monoid?.unit m
  | [x] -> x
  | x::xs' -> Monoid?.mult m x (mldenote m xs')

let rec flatten (#a:Type) (e:exp a) : list a =
  match e with
  | Unit -> []
  | Var x -> [x]
  | Mult e1 e2 -> flatten e1 @ flatten e2

(* This proof internally uses the monoid laws; the SMT solver picks up
   on them because they are written as squashed formulas in the
   definition of monoid; need to be careful with this since these are
   quantified formulas without any patterns. Dangerous stuff! *)
let rec flatten_correct_aux (#a:Type) (m:monoid a) ml1 ml2 :
  Lemma (mldenote m (ml1 @ ml2) == Monoid?.mult m (mldenote m ml1)
                                                  (mldenote m ml2)) =
  match ml1 with
  | [] -> ()
  | e::es1' -> flatten_correct_aux m es1' ml2

let rec flatten_correct (#a:Type) (m:monoid a) (e:exp a) :
    Lemma (mdenote m e == mldenote m (flatten e)) =
  match e with
  | Unit | Var _ -> ()
  | Mult e1 e2 -> flatten_correct_aux m (flatten e1) (flatten e2);
                  flatten_correct m e1; flatten_correct m e2

let monoid_reflect (#a:Type) (m:monoid a) (e1 e2:exp a)
    (_ : squash (mldenote m (flatten e1) == mldenote m (flatten e2)))
    : squash (mdenote m e1 == mdenote m e2) =
  flatten_correct m e1; flatten_correct m e2
val reification_aux (#a: Type) (mult unit me: term) : Tac (exp a)

    mult: FStar.Tactics.NamedView.term ->
    unit: FStar.Tactics.NamedView.term ->
    me: FStar.Tactics.NamedView.term
  -> FStar.Tactics.Effect.Tac (FStar.Tactics.CanonMonoid.exp a)