From d6ced637d9b7acabef2ccc9e761ec149bc7c93da Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sun, 5 Mar 2017 21:46:26 +0100
Subject: 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.
---
 plugins/setoid_ring/newring.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 2a3d66934b..87ee666605 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"
-- 
cgit v1.2.3