Merge PR #11906: [micromega] native support for boolean operators

Reviewed-by: maximedenes
Reviewed-by: pi8027
Reviewed-by: vbgl

1 files changed, 91 insertions, 37 deletions

diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 41579d5792..4e1f9a66ac 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.
@@ -248,10 +246,12 @@ module EBinOpT = struct
       source1 : EConstr.t
     ; source2 : EConstr.t
     ; source3 : EConstr.t
-    ; target : EConstr.t
-    ; inj1 : EInjT.t (* InjTyp source1 target *)
-    ; inj2 : EInjT.t (* InjTyp source2 target *)
-    ; inj3 : EInjT.t (* InjTyp source3 target *)
+    ; target1 : EConstr.t
+    ; target2 : EConstr.t
+    ; target3 : EConstr.t
+    ; inj1 : EInjT.t (* InjTyp source1 target1 *)
+    ; inj2 : EInjT.t (* InjTyp source2 target2 *)
+    ; inj3 : EInjT.t (* InjTyp source3 target3 *)
     ; bop : EConstr.t (* BOP *)
     ; tbop : EConstr.t (* TBOP *)
     ; tbopinj : EConstr.t (* TBOpInj *)
@@ -272,7 +272,8 @@ module EUnOpT = struct
   type t =
     { source1 : EConstr.t
     ; source2 : EConstr.t
-    ; target : EConstr.t
+    ; target1 : EConstr.t
+    ; target2 : EConstr.t
     ; uop : EConstr.t
     ; inj1_t : EInjT.t
     ; inj2_t : EInjT.t
@@ -319,7 +320,8 @@ type decl_kind =
   | UnOp of EUnOpT.t decl
   | CstOp of ECstOpT.t decl
   | Saturate of ESatT.t decl
-  | Spec of ESpecT.t decl
+  | UnOpSpec of ESpecT.t decl
+  | BinOpSpec of ESpecT.t decl
 
 type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr
 
@@ -353,6 +355,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
 
@@ -363,6 +366,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
@@ -370,7 +378,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
@@ -383,6 +391,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
 
@@ -392,24 +422,28 @@ module EBinOp = struct
   let table = table
 
   let mk_elt evd i a =
-    let i1 = get_inj evd a.(5) in
-    let i2 = get_inj evd a.(6) in
-    let i3 = get_inj evd a.(7) in
-    let tbop = a.(8) in
+    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)
-    ; target = a.(3)
+    ; target1 = a.(3)
+    ; target2 = a.(4)
+    ; target3 = a.(5)
     ; inj1 = i1
     ; inj2 = i2
     ; inj3 = i3
-    ; bop = a.(4)
-    ; tbop = a.(8)
-    ; tbopinj = a.(9)
+    ; bop
+    ; tbop
+    ; tbopinj = a.(11)
     ; classify_binop =
-        classify_op (mkconvert_binop i1 i2 i3) i1.EInjT.inj a.(4) tbop }
+        classify_op (mkconvert_binop i1 i2 i3) i3.EInjT.inj a.(6) tbop }
 
-  let get_key = 4
+  let get_key = 6
   let cast x = BinOp x
   let dest = function BinOp x -> Some x | _ -> None
 end
@@ -452,23 +486,25 @@ module EUnOp = struct
   let dest = function UnOp x -> Some x | _ -> None
 
   let mk_elt evd i a =
-    let i1 = get_inj evd a.(4) in
-    let i2 = get_inj evd a.(5) in
-    let uop = a.(3) in
-    let tuop = a.(6) in
+    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)
-    ; target = a.(2)
+    ; target1 = a.(2)
+    ; target2 = a.(3)
     ; uop
     ; inj1_t = i1
     ; inj2_t = i2
     ; tuop
-    ; tuopinj = a.(7)
+    ; tuopinj = a.(8)
     ; is_construct = EConstr.isConstruct evd uop
-    ; classify_unop = classify_op (mkconvert_unop i1 i2) i1.EInjT.inj uop tuop
+    ; classify_unop = classify_op (mkconvert_unop i1 i2) i2.EInjT.inj uop tuop
     }
 
-  let get_key = 3
+  let get_key = 4
 end
 
 module EBinRel = struct
@@ -485,6 +521,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)
@@ -621,19 +658,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 cast x = UnOpSpec x
+  let dest = function UnOpSpec x -> Some x | _ -> None
+  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 = BinOpSpec x
+  let dest = function BinOpSpec 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)
@@ -641,7 +691,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;
@@ -788,7 +839,8 @@ let app_unop evd src unop arg prf =
             ( force mkapp
             , [| unop.source1
                ; unop.source2
-               ; unop.target
+               ; unop.target1
+               ; unop.target2
                ; unop.uop
                ; unop.inj1_t.EInjT.inj
                ; unop.inj2_t.EInjT.inj
@@ -859,7 +911,9 @@ let app_binop evd src binop arg1 prf1 arg2 prf2 =
             , [| binop.source1
                ; binop.source2
                ; binop.source3
-               ; binop.target
+               ; binop.target1
+               ; binop.target2
+               ; binop.target3
                ; binop.bop
                ; binop.inj1.EInjT.inj
                ; binop.inj2.EInjT.inj
@@ -1366,7 +1420,7 @@ let rec spec_of_term env evd (senv : spec_env) t =
     with Not_found -> (
       try
         match snd (HConstr.find c !specs_cache) with
-        | Spec s ->
+        | UnOpSpec s | BinOpSpec s ->
           let thm = EConstr.mkApp (s.deriv.ESpecT.spec, a') in
           register_constr senv' t' thm
         | _ -> (get_name t' senv', senv')