Skip to content

Commit

Permalink
Refactoring of ring tactic:
Browse files Browse the repository at this point in the history 
  - Allows to deal with boolean ring (like word)
  - More flexibility on the required arguments (some functions are
    now optionals).
  - Use the previous modification to in AWord.
  • Loading branch information
@bgregoir
bgregoir committed Jan 22, 2014
1 parent a2a2df6 commit 4e98b4f
Show file tree
Hide file tree
Showing 12 changed files with 731 additions and 500 deletions.
75 changes: 47 additions & 28 deletions src/ecAlgTactic.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,12 @@ module Axioms = struct
let expr = "expr"
let embed = "ofint"

let core = ["oner_neq0"; "addr0"; "addrA"; "addrC"; "addrN";
"mulr1"; "mulrA"; "mulrC"; "mulrDl"]
let core_add = ["oner_neq0"; "addr0"; "addrA"; "addrC";]
let core_mul = [ "mulr1"; "mulrA"; "mulrC"; "mulrDl"]
let core = core_add @ "addrN" :: core_mul
let core_bool = core_add @ "addrrN" :: "bmulrI" :: core_mul

let ofoppbool = ["oppE"]
let intpow = ["expr0"; "exprS"]
let ofint = ["ofint0"; "ofint1"; "ofintS"; "ofintN"]
let ofsub = ["subrE"]
Expand All @@ -34,40 +38,46 @@ module Axioms = struct
let ty1 ty = tfun ty (ty0 ty)
let ty2 ty = tfun ty (ty1 ty)

let ring_symbols env ty =
let ring_symbols env boolean ty =
let symbols =
[(zero, (true , ty0 ty));
(one , (true , ty0 ty));
(add , (true , ty2 ty));
(opp , (true , ty1 ty));
(opp , (not boolean, ty1 ty));
(sub , (false, ty2 ty));
(mul , (true , ty2 ty));
(expr, (true , toarrow [ty; tint] ty))]
(expr, (false, toarrow [ty; tint] ty))]
in
if EcReduction.EqTest.for_type env ty tint
then symbols
else symbols @ [(embed, (true, tfun tint ty))]
else symbols @ [(embed, (false, tfun tint ty))]

let field_symbols env ty =
(ring_symbols env ty)
(ring_symbols env false ty)
@ [(inv, (true , ty1 ty));
(div, (false, ty2 ty))]

let subst_of_ring (cr : ring) =
let crcore = [(zero, cr.r_zero);
(one , cr.r_one );
(add , cr.r_add );
(opp , cr.r_opp );
(mul , cr.r_mul );
(expr, cr.r_exp )] in
(mul , cr.r_mul ); ] in

let xpath = fun x -> EcPath.pqname tmod x in
let add = fun subst x p -> EcSubst.add_path subst (xpath x) p in

let subst = EcSubst.add_tydef EcSubst.empty (xpath tname) ([], cr.r_type) in
let subst = List.fold_left (fun subst (x, p) -> add subst x p) subst crcore in

let subst =
EcSubst.add_tydef EcSubst.empty (xpath tname) ([], cr.r_type) in
let subst =
List.fold_left (fun subst (x, p) -> add subst x p) subst crcore in
let subst = odfl subst (cr.r_opp |> omap (fun p -> add subst opp p)) in
let subst = odfl subst (cr.r_sub |> omap (fun p -> add subst sub p)) in
let subst = cr.r_embed |> (function `Direct -> subst | `Embed p -> add subst embed p) in
let subst = odfl subst (cr.r_exp |> omap (fun p -> add subst expr p)) in

let subst =
cr.r_embed |>
(function `Direct | `Default -> subst | `Embed p -> add subst embed p)
in
subst

let subst_of_field (cr : field) =
Expand All @@ -80,7 +90,7 @@ module Axioms = struct
subst

(* FIXME: should use operators inlining when available *)
let get axs env cr =
let get cr env axs =
let subst =
match cr with
| `Ring cr -> subst_of_ring cr
Expand All @@ -94,24 +104,33 @@ module Axioms = struct
in
List.map for1 axs

let get_core = fun env cr -> get core env (`Ring cr)
let get_expr = fun env cr -> get intpow env (`Ring cr)
let get_ofint = fun env cr -> get ofint env (`Ring cr)
let get_ofsub = fun env cr -> get ofsub env (`Ring cr)
let get_field = fun env cr -> get field env (`Field cr)
let get_ofdiv = fun env cr -> get ofdiv env (`Field cr)
let getr env cr axs = get (`Ring cr) env axs
let getf env cr axs = get (`Field cr) env axs

let ring_axioms env (cr : ring) =
let axcore = (get_core env cr) @ (get_expr env cr) in
let axint = match cr.r_embed with `Direct -> [] | `Embed _ -> get_ofint env cr in
let axsub = match cr.r_sub with None -> [] | Some _ -> get_ofsub env cr in
List.flatten [axcore; axint; axsub]
let axcore =
if cr.r_bool then getr env cr core_bool
else getr env cr core in
let axint =
match cr.r_embed with
| `Direct | `Default -> [] | `Embed _ -> getr env cr ofint in
let axopp =
match cr.r_opp with
| Some _ when cr.r_bool -> getr env cr ofoppbool
| _ -> [] in
let axsub =
match cr.r_sub with None -> [] | Some _ -> getr env cr ofsub in
let axexp =
match cr.r_exp with None -> [] | Some _ -> getr env cr intpow in

List.flatten [axcore; axopp; axexp; axint; axsub]

let field_axioms env (cr : field) =
let axring = ring_axioms env cr.f_ring in
let axcore = get_field env cr in
let axdiv = match cr.f_div with None -> [] | Some _ -> get_ofdiv env cr in
List.flatten [axring; axcore; axdiv]
let axcore = getf env cr field in
let axdiv = match cr.f_div with None -> [] | Some _ -> getf env cr ofdiv in
List.flatten [axring; axcore; axdiv]

end

let ring_symbols = Axioms.ring_symbols
Expand Down
2 changes: 1 addition & 1 deletion src/ecAlgTactic.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ open EcAlgebra
val is_module_loaded : EcEnv.env -> bool

(* -------------------------------------------------------------------- *)
val ring_symbols : EcEnv.env -> ty -> (symbol * (bool * ty)) list
val ring_symbols : EcEnv.env -> bool -> ty -> (symbol * (bool * ty)) list
val field_symbols : EcEnv.env -> ty -> (symbol * (bool * ty)) list

val ring_axioms : EcEnv.env -> ring -> (symbol * form) list
Expand Down
88 changes: 55 additions & 33 deletions src/ecAlgebra.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,25 +42,28 @@ type ring = {
r_zero : EcPath.path;
r_one : EcPath.path;
r_add : EcPath.path;
r_opp : EcPath.path;
r_opp : EcPath.path option;
r_mul : EcPath.path;
r_exp : EcPath.path;
r_exp : EcPath.path option;
r_sub : EcPath.path option;
r_embed : [ `Direct | `Embed of EcPath.path ];
r_embed : [ `Direct | `Embed of EcPath.path | `Default];
r_bool : bool (* true means boolean ring *)
}

let ring_equal r1 r2 =
EcTypes.ty_equal r1.r_type r2.r_type &&
EcPath.p_equal r1.r_zero r2.r_zero &&
EcPath.p_equal r1.r_one r2.r_one &&
EcPath.p_equal r1.r_add r2.r_add &&
EcPath.p_equal r1.r_opp r2.r_opp &&
EcUtils.oall2 EcPath.p_equal r1.r_opp r2.r_opp &&
EcPath.p_equal r1.r_mul r2.r_mul &&
EcPath.p_equal r1.r_exp r2.r_exp &&
EcUtils.oall2 EcPath.p_equal r1.r_exp r2.r_exp &&
EcUtils.oall2 EcPath.p_equal r1.r_sub r2.r_sub &&
r1.r_bool = r2.r_bool &&
match r1.r_embed, r2.r_embed with
| `Direct, `Direct -> true
| `Embed p1, `Embed p2 -> EcPath.p_equal p1 p2
| `Default, `Default -> true
| _, _ -> false


Expand Down Expand Up @@ -88,9 +91,19 @@ let rzero r = rapp r r.r_zero []
let rone r = rapp r r.r_one []

let radd r e1 e2 = rapp r r.r_add [e1; e2]
let ropp r e = rapp r r.r_opp [e]
let ropp r e =
match r.r_opp with
| Some opp -> rapp r opp [e]
| None -> assert r.r_bool; e

let rmul r e1 e2 = rapp r r.r_mul [e1; e2]
let rexp r e i = rapp r r.r_exp [e; f_int i]
let rexp r e i =
match r.r_exp with
| Some r_exp -> rapp r r_exp [e; f_int i]
| None ->
assert (1 <= i);
let rec aux exp i = if i = 1 then exp else aux (rmul r exp e) (i-1) in
aux e i

let rsub r e1 e2 =
match r.r_sub with
Expand All @@ -101,6 +114,12 @@ let rofint r i =
match r.r_embed with
| `Direct -> f_int i
| `Embed p -> rapp r p [f_int i]
| `Default ->
let one = rone r in
let rec aux i = if i = 1 then one else radd r (aux (i-1)) one in
if i = 0 then rzero r
else if 1 <= i then aux i
else ropp r (aux i)

(* -------------------------------------------------------------------- *)
let fzero f = rzero f.f_ring
Expand Down Expand Up @@ -142,14 +161,15 @@ let cring_of_ring (r : ring) : cring =
let cr = [(r.r_zero, `Zero);
(r.r_one , `One );
(r.r_add , `Add );
(r.r_opp , `Opp );
(r.r_mul , `Mul );
(r.r_exp , `Exp )]
(r.r_mul , `Mul );]
in

let cr = List.fold_left (fun m (p, op) -> Mp.add p op m) Mp.empty cr in
let cr = odfl cr (r.r_opp |> omap (fun p -> Mp.add p `Opp cr)) in
let cr = odfl cr (r.r_sub |> omap (fun p -> Mp.add p `Sub cr)) in
let cr = r.r_embed |> (function `Direct -> cr | `Embed p -> Mp.add p `OfInt cr) in
let cr = odfl cr (r.r_exp |> omap (fun p -> Mp.add p `Exp cr)) in
let cr = r.r_embed |>
(function (`Direct | `Default) -> cr | `Embed p -> Mp.add p `OfInt cr) in
(r, cr)

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -194,7 +214,7 @@ let toring ((r, cr) : cring) (rmap : RState.rstate) (form : form) =
and of_int f =
let abstract () =
match r.r_embed with
| `Direct -> abstract f
| `Direct | `Default -> abstract f
| `Embed p -> abstract (rapp r p [f])
in
match f.f_node with
Expand Down Expand Up @@ -259,7 +279,7 @@ let tofield ((r, cr) : cfield) (rmap : RState.rstate) (form : form) =
and of_int f =
let abstract () =
match r.f_ring.r_embed with
| `Direct -> abstract f
| `Direct | `Default -> abstract f
| `Embed p -> abstract (rapp r.f_ring p [f])
in

Expand Down Expand Up @@ -289,23 +309,18 @@ let tofield ((r, cr) : cfield) (rmap : RState.rstate) (form : form) =
let form = doit form in (form, !rmap)

(* -------------------------------------------------------------------- *)
let ofring (r : ring) (rmap : RState.rstate) (e : pol) : form =
let rec doit idx e =
match e with
| Pc c when ceq c c0 -> emb_rzero r
| Pc c when ceq c c1 -> emb_rone r
| Pc c -> rofint r (Big_int.int_of_big_int c)

| Pinj (j, e) -> doit (idx+j) e

| PX (p, i, q) ->
let f = oget (RState.get idx rmap) in
let f = match i with 1 -> f | _ -> rexp r f i in
let f = if peq p (Pc c1) then f else rmul r (doit idx p) f in
let f = if peq q (Pc c0) then f else radd r f (doit (idx+1) q) in
f
in
doit 1 e
let rec ofring (r:ring) (rmap:RState.rstate) (e:pexpr) : form =
match e with
| PEc c ->
if ceq c c0 then emb_rzero r
else if ceq c c1 then emb_rone r
else rofint r (Big_int.int_of_big_int c)
| PEX idx -> oget (RState.get idx rmap)
| PEadd(p1,p2) -> radd r (ofring r rmap p1) (ofring r rmap p2)
| PEsub(p1,p2) -> rsub r (ofring r rmap p1) (ofring r rmap p2)
| PEmul(p1,p2) -> rmul r (ofring r rmap p1) (ofring r rmap p2)
| PEopp p1 -> ropp r (ofring r rmap p1)
| PEpow(p1,i) -> rexp r (ofring r rmap p1) i

(* -------------------------------------------------------------------- *)
let ring_simplify (cr : cring) (eqs : eqs) (form : form) =
Expand All @@ -314,7 +329,10 @@ let ring_simplify (cr : cring) (eqs : eqs) (form : form) =

let form = toring form in
let eqs = List.map (fun (f1, f2) -> (toring f1, toring f2)) eqs in
ofring (fst cr) !map (norm form eqs)
let norm =
if (fst cr).r_bool then Bring.norm_pe form eqs
else Iring.norm_pe form eqs in
ofring (fst cr) !map norm

(* -------------------------------------------------------------------- *)
let ring_eq (cr : cring) (eqs : eqs) (f1 : form) (f2 : form) =
Expand All @@ -341,6 +359,9 @@ let field_eq (cr : cfield) (eqs : eqs) (f1 : form) (f2 : form) =
let eqs = List.map (fun (f1, f2) -> (tofield f1, tofield f2)) eqs in
let eqs = List.pmap get_field_equation eqs in


let norm =
if (fst cr).f_ring.r_bool then Bring.norm_pe else Iring.norm_pe in
let norm form = ofring (norm form eqs) in

let num1 = norm num1 in
Expand All @@ -363,6 +384,7 @@ let field_simplify (cr : cfield) (eqs : eqs) (f : form) =
let eqs = List.map (fun (f1, f2) -> (tofield f1, tofield f2)) eqs in
let eqs = List.pmap get_field_equation eqs in

let norm =
if (fst cr).f_ring.r_bool then Bring.norm_pe else Iring.norm_pe in
let norm form = ofring (norm form eqs) in

(List.map norm cond, norm num, norm denum)
(List.map norm cond, norm num, norm denum)
7 changes: 4 additions & 3 deletions src/ecAlgebra.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,12 @@ type ring = {
r_zero : EcPath.path;
r_one : EcPath.path;
r_add : EcPath.path;
r_opp : EcPath.path;
r_opp : EcPath.path option;
r_mul : EcPath.path;
r_exp : EcPath.path;
r_exp : EcPath.path option;
r_sub : EcPath.path option;
r_embed : [ `Direct | `Embed of EcPath.path ];
r_embed : [ `Direct | `Embed of EcPath.path | `Default];
r_bool : bool; (* true means boolean ring *)
}

val ring_equal : ring -> ring -> bool
Expand Down
Loading

0 comments on commit 4e98b4f

Please sign in to comment.