Update theories/micromega/ZifyBool.v

Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>

- insert boolean constraint (b = true \/ b = false)
- add specs for b2z
- zify_post_hook performs a case-analysis over boolean constraints
- Stricter typing constraints for `zify` declared operators
  The type is syntactically checked against the declaration of injections.
  Some explicit casts may need to be inserted.

3 files changed, 58 insertions, 14 deletions

diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index ab0c3bed26..c00c9ecad4 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -28,9 +28,8 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
 | ["Add" "PropOp"    constr(t) ] -> { Zify.PropBinOp.register t }
 | ["Add" "PropBinOp"    constr(t) ] -> { Zify.PropBinOp.register t }
 | ["Add" "PropUOp"   constr(t) ] -> { Zify.PropUnOp.register t }
-| ["Add" "Spec"      constr(t) ] -> { Zify.Spec.register t }
-| ["Add" "BinOpSpec" constr(t) ] -> { Zify.Spec.register t }
-| ["Add" "UnOpSpec"  constr(t) ] -> { Zify.Spec.register t }
+| ["Add" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
+| ["Add" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
 | ["Add" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
 END
 
@@ -51,5 +50,5 @@ VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
 |[ "Show" "Zify" "UnOp" ]   -> { Zify.UnOp.print () }
 |[ "Show" "Zify" "CstOp"]   -> { Zify.CstOp.print () }
 |[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
-|[ "Show" "Zify" "Spec"]    -> { Zify.Spec.print () }
+|[ "Show" "Zify" "Spec"]    -> { Zify.BinOpSpec.print () ; Zify.UnOpSpec.print()}
 END
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index fa7b4aa480..ec0f278326 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -45,9 +45,7 @@ let op_iff = lazy (zify "iff")
 let op_iff_morph = lazy (zify "iff_morph")
 let op_not = lazy (zify "not")
 let op_not_morph = lazy (zify "not_morph")
-
-(* identity function *)
-(*let identity = lazy (zify "identity")*)
+let op_True = lazy (zify "True")
 let whd = Reductionops.clos_whd_flags CClosure.all
 
 (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
@@ -356,6 +354,7 @@ let specs_cache = ref HConstr.empty
 
 (** Each type-class gives rise to a different table.
     They only differ on how projections are extracted.  *)
+
 module EInj = struct
   open EInjT
 
@@ -366,6 +365,11 @@ module EInj = struct
   let cast x = InjTyp x
   let dest = function InjTyp x -> Some x | _ -> None
 
+  let is_cstr_true evd c =
+    match EConstr.kind evd c with
+    | Lambda (_, _, c) -> EConstr.eq_constr_nounivs evd c (Lazy.force op_True)
+    | _ -> false
+
   let mk_elt evd i (a : EConstr.t array) =
     let isid = EConstr.eq_constr_nounivs evd a.(0) a.(1) in
     { isid
@@ -373,7 +377,7 @@ module EInj = struct
     ; target = a.(1)
     ; inj = a.(2)
     ; pred = a.(3)
-    ; cstr = (if isid then None else Some a.(4)) }
+    ; cstr = (if is_cstr_true evd a.(3) then None else Some a.(4)) }
 
   let get_key = 0
 end
@@ -386,6 +390,28 @@ let get_inj evd c =
     failwith ("Cannot register term " ^ t)
   | Some a -> EInj.mk_elt evd c a
 
+let rec decomp_type evd ty =
+  match EConstr.kind_of_type evd ty with
+  | EConstr.ProdType (_, t1, rst) -> t1 :: decomp_type evd rst
+  | _ -> [ty]
+
+let pp_type env evd l =
+  Pp.prlist_with_sep (fun _ -> Pp.str " -> ") (pr_constr env evd) l
+
+let check_typ evd expty op =
+  let env = Global.env () in
+  let ty = Retyping.get_type_of env evd op in
+  let ty = decomp_type evd ty in
+  if List.for_all2 (EConstr.eq_constr_nounivs evd) ty expty then ()
+  else
+    raise
+      (CErrors.user_err
+         Pp.(
+           str ": Cannot register operator "
+           ++ pr_constr env evd op ++ str ". It has type " ++ pp_type env evd ty
+           ++ str " instead of expected type "
+           ++ pp_type env evd expty))
+
 module EBinOp = struct
   type elt = EBinOpT.t
 
@@ -398,7 +424,9 @@ module EBinOp = struct
     let i1 = get_inj evd a.(7) in
     let i2 = get_inj evd a.(8) in
     let i3 = get_inj evd a.(9) in
+    let bop = a.(6) in
     let tbop = a.(10) in
+    check_typ evd EInjT.[i1.source; i2.source; i3.source] bop;
     { source1 = a.(0)
     ; source2 = a.(1)
     ; source3 = a.(2)
@@ -408,7 +436,7 @@ module EBinOp = struct
     ; inj1 = i1
     ; inj2 = i2
     ; inj3 = i3
-    ; bop = a.(6)
+    ; bop
     ; tbop
     ; tbopinj = a.(11)
     ; classify_binop =
@@ -460,6 +488,7 @@ module EUnOp = struct
     let i1 = get_inj evd a.(5) in
     let i2 = get_inj evd a.(6) in
     let uop = a.(4) in
+    check_typ evd EInjT.[i1.source; i2.source] uop;
     let tuop = a.(7) in
     { source1 = a.(0)
     ; source2 = a.(1)
@@ -491,6 +520,7 @@ module EBinRel = struct
     let i = get_inj evd a.(3) in
     let brel = a.(2) in
     let tbrel = a.(4) in
+    check_typ evd EInjT.[i.source; i.source; EConstr.mkProp] brel;
     { source = a.(0)
     ; target = a.(1)
     ; inj = get_inj evd a.(3)
@@ -627,19 +657,32 @@ module ESat = struct
   let get_key = 1
 end
 
-module ESpec = struct
+module EUnopSpec = struct
   open ESpecT
 
   type elt = ESpecT.t
 
-  let name = "Spec"
+  let name = "UnopSpec"
   let table = specs
   let cast x = Spec x
   let dest = function Spec x -> Some x | _ -> None
-  let mk_elt evd i a = {spec = a.(5)}
+  let mk_elt evd i a = {spec = a.(4)}
   let get_key = 2
 end
 
+module EBinOpSpec = struct
+  open ESpecT
+
+  type elt = ESpecT.t
+
+  let name = "BinOpSpec"
+  let table = specs
+  let cast x = Spec x
+  let dest = function Spec x -> Some x | _ -> None
+  let mk_elt evd i a = {spec = a.(5)}
+  let get_key = 3
+end
+
 module BinOp = MakeTable (EBinOp)
 module UnOp = MakeTable (EUnOp)
 module CstOp = MakeTable (ECstOp)
@@ -647,7 +690,8 @@ module BinRel = MakeTable (EBinRel)
 module PropBinOp = MakeTable (EPropBinOp)
 module PropUnOp = MakeTable (EPropUnOp)
 module Saturate = MakeTable (ESat)
-module Spec = MakeTable (ESpec)
+module UnOpSpec = MakeTable (EUnopSpec)
+module BinOpSpec = MakeTable (EBinOpSpec)
 
 let init_cache () =
   table_cache := !table;
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 7960475def..537e652fd0 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -21,7 +21,8 @@ module CstOp : S
 module BinRel : S
 module PropBinOp : S
 module PropUnOp : S
-module Spec : S
+module BinOpSpec : S
+module UnOpSpec : S
 module Saturate : S
 
 val zify_tac : unit Proofview.tactic