module FStar.Tactics.CanonCommSemiring

fsdoc: no-summary-found

fsdoc: no-comment-found

let canon_attr:()

An attribute for marking definitions to unfold by the tactic

let (norm_fully (#a:Type) (x:a)):x
val spolynomial_normalize:Unidentified product: [#a:eqtype] Unidentified product: [cr a] Unidentified product: [spolynomial a] canonical_sum a

Canonize a reflected expression

val canonical_sum_simplify:Unidentified product: [#a:eqtype] Unidentified product: [cr a] Unidentified product: [canonical_sum a] canonical_sum a
val spolynomial_simplify:Unidentified product: [#a:eqtype] Unidentified product: [cr a] Unidentified product: [spolynomial a] canonical_sum a
let (vmap a):*(list (*(var, a)), a)
let ((update (#a:Type) (x:var) (xa:a) (vm:vmap a)):vmap a):let  (l, y) = vm in (FStar.Pervasives.Native.Mktuple2 (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 x xa)) l) y)

Add a new entry in a variable map

let ((quote_list (#a:Type) (ta:term) (quotea:Unidentified product: [a] (Tac term)) (xs:list a)):(Tac term)):match xs with []  -> mk_app ((`(Nil))) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 ta Q_Implicit)) (Prims.Nil )) | (Prims.Cons x xs')  -> mk_app ((`(Cons))) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 ta Q_Implicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 quotea x Q_Explicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 quote_list ta quotea xs' Q_Explicit)) (Prims.Nil ))))

Quotes a list

let ((quote_vm (#a:Type) (ta:term) (quotea:Unidentified product: [a] (Tac term)) (vm:vmap a)):(Tac term)):let  ((quote_map_entry (p:(*(nat, a)))):(Tac term)) = mk_app ((`(Mktuple2))) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 (`(nat)) Q_Implicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 ta Q_Implicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 pack ((Tv_Const ((C_Int (fst p))))) Q_Explicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 quotea (snd p) Q_Explicit)) (Prims.Nil ))))) in let  tyentry = mk_e_app ((`(tuple2))) (Prims.Cons ((`(nat))) (Prims.Cons ta (Prims.Nil ))) in let  tlist = quote_list tyentry quote_map_entry (fst vm) in let  tylist = mk_e_app ((`(list))) (Prims.Cons tyentry (Prims.Nil )) in mk_app ((`(Mktuple2))) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 tylist Q_Implicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 ta Q_Implicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 tlist Q_Explicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 quotea (snd vm) Q_Explicit)) (Prims.Nil )))))

Quotes a variable map

let (interp_var (#a:Type) (vm:vmap a) (i:index)):match List.Tot.assoc i (fst vm) with (Some x)  -> x | _  -> snd vm
let ((interp_cs (#a:Type) (r:cr a) (vm:vmap a) (s:canonical_sum a)):a):let  azero = r.cm_add.unit in match s with Nil_monom  -> azero | (Cons_varlist l t)  -> ics_aux r vm (interp_vl r vm l) t | (Cons_monom c l t)  -> ics_aux r vm (interp_m r vm c l) t

Interpretation of a canonical sum

let ((interp_sp (#a:Type) (r:cr a) (vm:vmap a) (p:spolynomial a)):a):let  aplus = r.cm_add.mult in let  amult = r.cm_mult.mult in match p with (SPconst c)  -> c | (SPvar i)  -> interp_var vm i | (SPplus p1 p2)  -> aplus (interp_sp r vm p1) (interp_sp r vm p2) | (SPmult p1 p2)  -> amult (interp_sp r vm p1) (interp_sp r vm p2)

Interpretation of a polynomial

typepolynomial = Pvar:Unidentified product: [index] polynomial a | Pconst:Unidentified product: [a] polynomial a | Pplus:Unidentified product: [polynomial a] Unidentified product: [polynomial a] polynomial a | Pmult:Unidentified product: [polynomial a] Unidentified product: [polynomial a] polynomial a | Popp:Unidentified product: [polynomial a] polynomial a 
val polynomial_normalize:Unidentified product: [#a:eqtype] Unidentified product: [cr a] Unidentified product: [polynomial a] canonical_sum a

Canonize a reflected expression

val spolynomial_of:Unidentified product: [#a:eqtype] Unidentified product: [cr a] Unidentified product: [polynomial a] spolynomial a

Translate to a representation without additive inverses

let ((interp_p (#a:Type) (r:cr a) (vm:vmap a) (p:polynomial a)):a):let  aplus = r.cm_add.mult in let  amult = r.cm_mult.mult in match p with (Pconst c)  -> c | (Pvar i)  -> interp_var vm i | (Pplus p1 p2)  -> aplus (interp_p r vm p1) (interp_p r vm p2) | (Pmult p1 p2)  -> amult (interp_p r vm p1) (interp_p r vm p2) | (Popp p)  -> r.opp (interp_p r vm p)

Interpretation of a polynomial

let ((find_aux (n:nat) (x:term) (xs:list term)):(Tot (option nat) (decreases xs))):match xs with []  -> None | (Prims.Cons x' xs')  -> if term_eq x x' then (Some n) else find_aux (+(n, 1)) x xs'
let ((reification_aux (#a:Type) (unquotea:Unidentified product: [term] (Tac a)) (ts:list term) (vm:vmap a) (add:term) (opp:term) (mone:term) (mult:term) (t:term)):(Tac (*(*(polynomial a, list term), vmap a)))):let  (hd, tl) = collect_app_ref t in match (FStar.Pervasives.Native.Mktuple2 inspect hd list_unref tl) with ((Tv_FVar fv), [(t1, _); (t2, _)])  -> let  ((binop (op:Unidentified product: [polynomial a] Unidentified product: [polynomial a] polynomial a)):(Tac (*(*(polynomial a, list term), vmap a)))) = let  (e1, ts, vm) = reification_aux unquotea ts vm add opp mone mult t1 in let  (e2, ts, vm) = reification_aux unquotea ts vm add opp mone mult t2 in ((FStar.Pervasives.Native.Mktuple3 op e1 e2 ts vm)) in if term_eq (pack ((Tv_FVar fv))) add then binop Pplus else if term_eq (pack ((Tv_FVar fv))) mult then binop Pmult else make_fvar t unquotea ts vm | ((Tv_FVar fv), [(t1, _)])  -> let  ((monop (op:Unidentified product: [polynomial a] polynomial a)):(Tac (*(*(polynomial a, list term), vmap a)))) = let  (e, ts, vm) = reification_aux unquotea ts vm add opp mone mult t1 in ((FStar.Pervasives.Native.Mktuple3 op e ts vm)) in if term_eq (pack ((Tv_FVar fv))) opp then monop Popp else make_fvar t unquotea ts vm | ((Tv_Const _), [])  -> (FStar.Pervasives.Native.Mktuple3 (Pconst (unquotea t)) ts vm) | (_, _)  -> make_fvar t unquotea ts vm

This expects that add, opp, mone mult, and t have already been normalized

let steps:(Prims.Cons primops (Prims.Cons iota (Prims.Cons zeta (Prims.Cons delta_attr (Prims.Cons `%%canon_attr (Prims.Nil )) (Prims.Cons delta_only (Prims.Cons `%%FStar.Mul.op_Star (Prims.Cons `%%FStar.Algebra.CommMonoid.int_plus_cm (Prims.Cons `%%FStar.Algebra.CommMonoid.int_multiply_cm (Prims.Cons `%%FStar.Algebra.CommMonoid.__proj__CM__item__mult (Prims.Cons `%%FStar.Algebra.CommMonoid.__proj__CM__item__unit (Prims.Cons `%%__proj__CR__item__cm_add (Prims.Cons `%%__proj__CR__item__opp (Prims.Cons `%%__proj__CR__item__cm_mult (Prims.Cons `%%FStar.List.Tot.Base.assoc (Prims.Cons `%%FStar.Pervasives.Native.fst (Prims.Cons `%%FStar.Pervasives.Native.snd (Prims.Cons `%%FStar.Pervasives.Native.__proj__Mktuple2__item___1 (Prims.Cons `%%FStar.Pervasives.Native.__proj__Mktuple2__item___2 (Prims.Cons `%%FStar.List.Tot.Base.op_At (Prims.Cons `%%FStar.List.Tot.Base.append (Prims.Nil )))))))))))))))) (Prims.Nil ))))))