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 ))))))