diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-05 21:46:26 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 17:43:40 +0100 |
| commit | d6ced637d9b7acabef2ccc9e761ec149bc7c93da (patch) | |
| tree | 24b6b6c59e2e91348cc6a87071a2d75f645e8f98 | |
| parent | e1ef9491edaf8f7e6f553c49b24163b7e2a53825 (diff) | |
Mark ring morphisms as opaque.
This prevents Coq from unfolding IZR in ring_simplify and field_simplify.
This is a change of behavior for users of morphism rings, so they might have
to pass the postprocess option to Add Ring/Field if they want morphisms to be
automatically expanded.
There are two predefined morphisms in the standard library: IDphi (when
polynomial coefficients have the same type as constants) and gen_phiZ (when
the only available constants are 0 and 1). They are hardcoded as transparent.
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 2a3d66934..87ee66660 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -323,11 +323,13 @@ let _ = add_map "ring" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)]) @@ -756,12 +758,14 @@ let _ = add_map "field" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_reference "display_linear", (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); my_reference "display_pow_linear", - (function -1|9|10|11|12|14|16|18|19->Eval|17->Rec|_->Prot); + (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); @@ -778,9 +782,11 @@ let _ = add_map "field_cond" (map_without_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); - (* PCond: evaluate morphism and denum list, protect ring + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); + (* PCond: evaluate denum list, protect ring operations and make recursive call on the var map *) - my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);; let _ = Redexpr.declare_reduction "simpl_field_expr" |