let permute_correct (#b:Type) (p:permute b) =
  #a:Type -> m:cm a -> vm:vmap a b -> xs:list var ->
    Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs))
let permute_correct (#b: Type) (p: permute b) =
#a: Type -> m: cm a -> vm: vmap a b -> xs: list var
  -> Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs))
FStar.Tactics.CanonCommMonoid.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Util.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSwaps.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Classical.fsti.checked FStar.Algebra.CommMonoid.fst.checked
FStar.Tactics.CanonCommMonoid.fst
FStar.Tactics.CanonCommMonoid.permute FStar.Algebra.CommMonoid.cm FStar.Tactics.CanonCommMonoid.vmap Prims.list FStar.Tactics.CanonCommMonoid.var Prims.unit Prims.l_True Prims.squash Prims.eq2 FStar.Tactics.CanonCommMonoid.xsdenote Prims.Nil FStar.Pervasives.pattern
(*
   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.CanonCommMonoid

open FStar.Algebra.CommMonoid
open FStar.List
open FStar.Reflection.V2
open FStar.Tactics.V2
open FStar.Classical
open FStar.Tactics.CanonCommSwaps

(* An expression canonizer for commutative monoids.
   Inspired by:
   - http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html
   - http://poleiro.info/posts/2015-04-13-writing-reflective-tactics.html
*)

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

(***** Expression syntax *)

let var : eqtype = nat

type exp : Type =
  | Unit : exp
  | Var : var -> exp
  | Mult : exp -> exp -> exp

let rec exp_to_string (e:exp) : string =
  match e with
  | Unit -> "Unit"
  | Var x -> "Var " ^ string_of_int (x <: var)
  | Mult e1 e2 -> "Mult (" ^ exp_to_string e1
                   ^ ") (" ^ exp_to_string e2 ^ ")"

(***** Expression denotation *)

// Use a map that stores for each variable
// (1) its denotation that should be treated abstractly (type a) and
// (2) user-specified extra information depending on its term (type b)

let vmap (a b:Type) = list (var * (a*b)) * (a * b)
let const (#a #b:Type) (xa:a) (xb:b) : vmap a b = [], (xa,xb)
let select (#a #b:Type) (x:var) (vm:vmap a b) : Tot a =
  match assoc #var #(a * b) x (fst vm) with
  | Some (a, _) -> a
  | _ -> fst (snd vm)
let select_extra (#a #b:Type) (x:var) (vm:vmap a b) : Tot b =
  match assoc #var #(a * b) x (fst vm) with
  | Some (_, b) -> b
  | _ -> snd (snd vm)
let update (#a #b:Type) (x:var) (xa:a) (xb:b) (vm:vmap a b) : vmap a b =
  (x, (xa, xb))::fst vm, snd vm

let rec mdenote (#a #b:Type) (m:cm a) (vm:vmap a b) (e:exp) : Tot a =
  match e with
  | Unit -> CM?.unit m
  | Var x -> select x vm
  | Mult e1 e2 -> CM?.mult m (mdenote m vm e1) (mdenote m vm e2)

let rec xsdenote (#a #b:Type) (m:cm a) (vm:vmap a b) (xs:list var) : Tot a =
  match xs with
  | [] -> CM?.unit m
  | [x] -> select x vm
  | x::xs' -> CM?.mult m (select x vm) (xsdenote m vm xs')

(***** Flattening expressions to lists of variables *)

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

let rec flatten_correct_aux (#a #b:Type) (m:cm a) (vm:vmap a b)
                                                  (xs1 xs2:list var) :
    Lemma (xsdenote m vm (xs1 @ xs2) == CM?.mult m (xsdenote m vm xs1)
                                                   (xsdenote m vm xs2)) =
  match xs1 with
  | [] -> CM?.identity m (xsdenote m vm xs2)
  | [x] -> if (Nil? xs2) then right_identity m (select x vm)
  | x::xs1' -> (CM?.associativity m (select x vm)
                      (xsdenote m vm xs1') (xsdenote m vm xs2);
                flatten_correct_aux m vm xs1' xs2)

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

(***** Permuting the lists of variables
       by swapping adjacent elements *)

(* The user has control over the permutation. He can store extra
   information in the vmap and use that for choosing the
   permutation. This means that permute has access to the vmap. *)

let permute (b:Type) = a:Type -> vmap a b -> list var -> list var

// high-level correctness criterion for permutations
val permute_correct : p: FStar.Tactics.CanonCommMonoid.permute b -> Type
p: FStar.Tactics.CanonCommMonoid.permute b -> Type