From f8e91cb0a227a2d0423412e7533163568e1e9fdf Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Mon, 11 May 2020 11:59:42 +0200 Subject: [micromega] native support for boolean operators The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb. --- plugins/micromega/zify.ml | 59 +++++++++++++++++++++++++++-------------------- 1 file changed, 34 insertions(+), 25 deletions(-) (limited to 'plugins/micromega/zify.ml') diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 41579d5792..fa7b4aa480 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -248,10 +248,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 +274,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 @@ -392,24 +395,26 @@ 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 tbop = a.(10) in { 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 = a.(6) + ; 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 +457,24 @@ 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 + 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 @@ -788,7 +794,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 +866,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 -- cgit v1.2.3 From 13f09096c1dc75898e32e915161b928a68b45346 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Sun, 17 May 2020 19:48:58 +0200 Subject: Update theories/micromega/ZifyBool.v Co-authored-by: Kazuhiko Sakaguchi - 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. --- plugins/micromega/zify.ml | 62 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 53 insertions(+), 9 deletions(-) (limited to 'plugins/micromega/zify.ml') 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; -- cgit v1.2.3 From 12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Mon, 25 May 2020 17:28:53 +0200 Subject: Update zify documentation Add Zify are documented. Add is deprecated as it clashed with the standard Add command --- plugins/micromega/zify.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'plugins/micromega/zify.ml') diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index ec0f278326..4e1f9a66ac 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -320,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 @@ -664,8 +665,8 @@ module EUnopSpec = struct let name = "UnopSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None + 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 @@ -677,8 +678,8 @@ module EBinOpSpec = struct let name = "BinOpSpec" let table = specs - let cast x = Spec x - let dest = function Spec x -> Some x | _ -> None + 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 @@ -1419,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') -- cgit v1.2.3