Skip to content

Commit

Permalink
Port to Hierarchy Builder
Browse files Browse the repository at this point in the history
  • Loading branch information
@proux01
proux01 committed Nov 16, 2022
1 parent d4de5a2 commit 1a4efa1
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 24 deletions.
9 changes: 7 additions & 2 deletions examples/zmodule.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -399,6 +399,11 @@ Ltac morph_zmodule_reflection V VarMap ME1 ME2 ZE1 ZE2 :=
apply: (@AG_correct V VarMap ZE1 ZE2);
[vm_compute; reflexivity].

Module MorphSort.
Import GRing.
Definition Additive U V := @Additive.apply U V (Phant (U -> V)).
End MorphSort.

Elpi Tactic morph_zmodule.
Elpi Accumulate lp:{{

Expand All @@ -423,8 +428,8 @@ quote V F {{ @subr lp:V' lp:In1 lp:In2 }}
coq.unify-eq V V' ok, !,
quote V F In1 OutM1 Out1 VarMap, quote V F In2 OutM2 Out2 VarMap.
quote V F In {{ @MMorph lp:U lp:V lp:G lp:OutM }} Out VarMap :-
coq.unify-eq {{ @GRing.Additive.apply lp:U lp:V lp:Ph lp:G lp:In1 }} In ok, !,
quote U (x\ F {{ @GRing.Additive.apply lp:U lp:V lp:Ph lp:G lp:x }})
coq.unify-eq {{ @MorphSort.Additive lp:U lp:V lp:G lp:In1 }} In ok, !,
quote U (x\ F {{ @MorphSort.Additive lp:U lp:V lp:G lp:x }})
In1 OutM Out VarMap.
quote V F In {{ @MX lp:V lp:In }} {{ AGX lp:N }} VarMap :- !,
mem VarMap (F In) N.
Expand Down
44 changes: 22 additions & 22 deletions theories/common.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ quote.nat _ {{ Nat.of_num_uint lp:In }} {{ NC lp:OutM }} Out _ :-
n-constant N OutM,
quote.expr.constant { z-constant N } Out.
quote.nat R In {{ NX lp:In }} Out VarMap :- !,
Zmodule = {{ GRing.Ring.zmodType lp:R }},
Zmodule = {{ GRing_Ring__to__GRing_Zmodule lp:R }},
mem VarMap {{ @GRing.natmul lp:Zmodule (@GRing.one lp:R) lp:In }} N, !,
quote.expr.variable { positive-constant {calc (N + 1)} } Out.

Expand Down Expand Up @@ -193,13 +193,13 @@ quote.zmod U R Morph {{ @intmul lp:U' lp:In1 lp:In2 }}
quote.zmod U R Morph In1 OutM1 Out1 VarMap, !,
quote.ring
{{ int_Ring }} none R
(n\ {{ @intmul (GRing.Ring.zmodType lp:R) (@GRing.one lp:R) lp:n }})
(n\ {{ @intmul (GRing_Ring__to__GRing_Zmodule lp:R) (@GRing.one lp:R) lp:n }})
In2 OutM2 Out2 VarMap, !,
quote.expr.mul Out1 Out2 Out.
% additive functions
quote.zmod U R Morph In
{{ @ZMMorph lp:V lp:U lp:NewMorphInst lp:OutM }} Out VarMap :-
NewMorph = (x\ {{ @GRing.Additive.apply lp:V lp:U _ lp:NewMorphInst lp:x }}),
NewMorph = (x\ {{ @MorphSort.Additive lp:V lp:U lp:NewMorphInst lp:x }}),
coq.unify-eq In (NewMorph In1) ok,
!,
% TODO: for concrete additive functions, should we unpack [NewMorph]?
Expand All @@ -223,63 +223,63 @@ pred quote.ring i:term, i:option term, i:term, i:(term -> term),
i:term, o:term, o:term, o:list term.
% 0%R
quote.ring R _ _ _ {{ @GRing.zero lp:V }} {{ @R0 lp:R }} Out _ :-
coq.unify-eq V {{ GRing.Ring.zmodType lp:R }} ok, !,
coq.unify-eq V {{ GRing_Ring__to__GRing_Zmodule lp:R }} ok, !,
quote.expr.zero Out.
% -%R
quote.ring R F TR Morph {{ @GRing.opp lp:V lp:In1 }}
{{ @ROpp lp:R lp:OutM1 }} Out VarMap :-
coq.unify-eq V {{ GRing.Ring.zmodType lp:R }} ok,
coq.unify-eq V {{ GRing_Ring__to__GRing_Zmodule lp:R }} ok,
!,
quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !,
quote.expr.opp Out1 Out.
% Z.opp
quote.ring R none TR Morph
{{ Z.opp lp:In1 }} {{ @RZOpp lp:OutM1 }} Out VarMap :-
coq.unify-eq {{ ZInstances.Z_ringType }} R ok,
coq.unify-eq {{ Z_ringType }} R ok,
!,
quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !,
quote.expr.opp Out1 Out.
% +%R
quote.ring R F TR Morph {{ @GRing.add lp:V lp:In1 lp:In2 }}
{{ @RAdd lp:R lp:OutM1 lp:OutM2 }} Out VarMap :-
coq.unify-eq V {{ GRing.Ring.zmodType lp:R }} ok,
coq.unify-eq V {{ GRing_Ring__to__GRing_Zmodule lp:R }} ok,
!,
quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !,
quote.ring R F TR Morph In2 OutM2 Out2 VarMap, !,
quote.expr.add Out1 Out2 Out.
% Z.add
quote.ring R none TR Morph {{ Z.add lp:In1 lp:In2 }}
{{ @RZAdd lp:OutM1 lp:OutM2 }} Out VarMap :-
coq.unify-eq {{ ZInstances.Z_ringType }} R ok,
coq.unify-eq {{ Z_ringType }} R ok,
!,
quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !,
quote.ring R none TR Morph In2 OutM2 Out2 VarMap, !,
quote.expr.add Out1 Out2 Out.
% Z.sub
quote.ring R none TR Morph {{ Z.sub lp:In1 lp:In2 }}
{{ @RZSub lp:OutM1 lp:OutM2 }} Out VarMap :-
coq.unify-eq {{ ZInstances.Z_ringType }} R ok,
coq.unify-eq {{ Z_ringType }} R ok,
!,
quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !,
quote.ring R none TR Morph In2 OutM2 Out2 VarMap, !,
quote.expr.sub Out1 Out2 Out.
% (_ *+ _)%R
quote.ring R F TR Morph {{ @GRing.natmul lp:V lp:In1 lp:In2 }}
{{ @RMuln lp:R lp:OutM1 lp:OutM2 }} Out VarMap :-
coq.unify-eq V {{ @GRing.Ring.zmodType lp:R }} ok,
coq.unify-eq V {{ @GRing_Ring__to__GRing_Zmodule lp:R }} ok,
!,
quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !,
quote.nat TR In2 OutM2 Out2 VarMap, !,
quote.expr.mul Out1 Out2 Out.
% (_ *~ _)%R
quote.ring R F TR Morph {{ @intmul lp:V lp:In1 lp:In2 }}
{{ @RMulz lp:R lp:OutM1 lp:OutM2 }} Out VarMap :-
coq.unify-eq V {{ @GRing.Ring.zmodType lp:R }} ok,
coq.unify-eq V {{ @GRing_Ring__to__GRing_Zmodule lp:R }} ok,
!,
quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !,
quote.ring
{{ int_Ring }} none TR
(n\ {{ @intmul (GRing.Ring.zmodType lp:TR) (@GRing.one lp:TR) lp:n }})
(n\ {{ @intmul (GRing_Ring__to__GRing_Zmodule lp:TR) (@GRing.one lp:TR) lp:n }})
In2 OutM2 Out2 VarMap, !,
quote.expr.mul Out1 Out2 Out.
% 1%R
Expand All @@ -298,7 +298,7 @@ quote.ring R F TR Morph {{ @GRing.mul lp:R' lp:In1 lp:In2 }}
% Z.mul
quote.ring R none TR Morph {{ Z.mul lp:In1 lp:In2 }}
{{ @RZMul lp:OutM1 lp:OutM2 }} Out VarMap :-
coq.unify-eq {{ ZInstances.Z_ringType }} R ok,
coq.unify-eq {{ Z_ringType }} R ok,
!,
quote.ring R none TR Morph In1 OutM1 Out1 VarMap, !,
quote.ring R none TR Morph In2 OutM2 Out2 VarMap, !,
Expand All @@ -317,15 +317,15 @@ quote.ring R F TR Morph {{ @exprz lp:R' lp:In1 lp:In2 }}
z-constant Exp { coq.reduction.vm.norm {{ Z_of_int lp:In2 }} {{ Z }} },
if (Exp >= 0)
(CONT =
(coq.unify-eq {{ GRing.UnitRing.ringType lp:R' }} R ok, !,
(coq.unify-eq {{ GRing_UnitRing__to__GRing_Ring lp:R' }} R ok, !,
quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !,
n-constant Exp Out2, !,
OutM = {{ @RExpPosz lp:R' lp:OutM1 lp:Out2 }}, !,
quote.expr.exp Out1 Out2 Out))
(CONT =
(field-mode,
F = some F',
coq.unify-eq R' {{ GRing.Field.unitRingType lp:F' }} ok, !,
coq.unify-eq R' {{ GRing_Field__to__GRing_UnitRing lp:F' }} ok, !,
quote.ring R F TR Morph In1 OutM1 Out1 VarMap, !,
n-constant { calc (~ (Exp + 1)) } Out2, !,
OutM = {{ @RExpNegz lp:F' lp:OutM1 lp:Out2 }}, !,
Expand All @@ -334,7 +334,7 @@ quote.ring R F TR Morph {{ @exprz lp:R' lp:In1 lp:In2 }}
% Z.pow
quote.ring R none TR Morph {{ Z.pow lp:In1 lp:In2 }}
{{ @RZExp lp:OutM1 lp:In2' }} Out VarMap :-
coq.unify-eq {{ ZInstances.Z_ringType }} R ok,
coq.unify-eq {{ Z_ringType }} R ok,
coq.reduction.vm.norm In2 {{ Z }} In2',
z-constant Exp In2',
!,
Expand All @@ -347,7 +347,7 @@ quote.ring R none TR Morph {{ Z.pow lp:In1 lp:In2 }}
quote.ring R (some F) TR Morph {{ @GRing.inv lp:R' lp:In1 }}
{{ @RInv lp:F lp:OutM1 }} {{ @FEinv Z lp:Out1 }} VarMap :-
field-mode,
coq.unify-eq R' {{ GRing.Field.unitRingType lp:F }} ok,
coq.unify-eq R' {{ GRing_Field__to__GRing_UnitRing lp:F }} ok,
!,
quote.ring R (some F) TR Morph In1 OutM1 Out1 VarMap.
% Posz
Expand All @@ -363,14 +363,14 @@ quote.ring R _ TR _ {{ Negz lp:In }} {{ @RNegz lp:OutM1 }} Out VarMap :-
quote.expr.opp { quote.expr.add { quote.expr.one } Out1 } Out.
% Z constants
quote.ring R _ _ _ In {{ @RZC lp:In }} Out _ :-
coq.unify-eq {{ ZInstances.Z_ringType }} R ok,
coq.unify-eq {{ int_Ring }} R ok,
z-constant _ In, !,
quote.expr.constant In Out.
% morphisms
quote.ring R _ TR Morph In
{{ @RMorph lp:Q lp:R lp:NewMorphInst lp:OutM }} Out VarMap :-
NewMorph = (x\ {{ @GRing.RMorphism.apply
lp:Q lp:R _ lp:NewMorphInst lp:x }}),
NewMorph = (x\ {{ @MorphSort.RMorphism
lp:Q lp:R lp:NewMorphInst lp:x }}),
coq.unify-eq In (NewMorph In1) ok,
!,
% TODO: for concrete morphisms, should we unpack [NewMorph]?
Expand All @@ -379,8 +379,8 @@ quote.ring R _ TR Morph In
quote.ring R _ TR Morph In
{{ @RMorph' lp:V lp:R lp:NewMorphInst lp:OutM }} Out VarMap :-
NewMorph =
(x\ {{ @GRing.Additive.apply
lp:V (GRing.Ring.zmodType lp:R) _ lp:NewMorphInst lp:x }}),
(x\ {{ @MorphSort.Additive
lp:V (GRing_Ring__to__GRing_Zmodule lp:R) lp:NewMorphInst lp:x }}),
coq.unify-eq In (NewMorph In1) ok,
!,
% TODO: for concrete additive functions, should we unpack [NewMorph]?
Expand Down
13 changes: 13 additions & 0 deletions theories/ring.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -691,6 +691,19 @@ Strategy expand
[addn_expand nat_of_pos_rec_expand nat_of_pos_expand nat_of_N_expand
int_of_Z_expand Neval Reval Nnorm Rnorm Fnorm PEeval FEeval].

Definition int_Ring := Eval hnf in [the ringType of int : Type].
Definition Z_ringType := Eval hnf in [the ringType of Z : Type].

Definition GRing_Ring__to__GRing_Zmodule : ringType -> zmodType := id.
Definition GRing_UnitRing__to__GRing_Ring : unitRingType -> ringType := id.
Definition GRing_Field__to__GRing_UnitRing : fieldType -> unitRingType := id.

Module MorphSort.
Import GRing.
Definition Additive U V := @Additive.apply U V (Phant (U -> V)).
Definition RMorphism U V := @RMorphism.apply U V (Phant (U -> V)).
End MorphSort.

Elpi Tactic ring.
Elpi Accumulate File "theories/common.elpi".
Elpi Accumulate File "theories/ring.elpi".
Expand Down

0 comments on commit 1a4efa1

Please sign in to comment.