From 8b8a3858f34782eeb489c43c758e8c8c1f75c108 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Dec 2019 15:41:53 +0100 Subject: [micromega] Enable ocamlformat. --- plugins/micromega/zify.ml | 821 ++++++++++++++++++++-------------------------- 1 file changed, 357 insertions(+), 464 deletions(-) (limited to 'plugins/micromega/zify.ml') diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 0a57677220..5d8ae83853 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -27,10 +27,7 @@ let pr_constr env evd e = Printer.pr_econstr_env env evd e let rec find_option pred l = match l with | [] -> raise Not_found - | e::l -> match pred e with - | Some r -> r - | None -> find_option pred l - + | e :: l -> ( match pred e with Some r -> r | None -> find_option pred l ) (** [HConstr] is a map indexed by EConstr.t. It should only be used using closed terms. @@ -39,8 +36,7 @@ module HConstr = struct module M = Map.Make (struct type t = EConstr.t - let compare c c' = - Constr.compare (unsafe_to_constr c) (unsafe_to_constr c') + let compare c c' = Constr.compare (unsafe_to_constr c) (unsafe_to_constr c') end) type 'a t = 'a list M.t @@ -52,91 +48,89 @@ module HConstr = struct M.add h (e :: l) m let empty = M.empty - let find h m = match lfind h m with e :: _ -> e | [] -> raise Not_found - let find_all = lfind let fold f m acc = M.fold (fun k l acc -> List.fold_left (fun acc e -> f k e acc) acc l) m acc - end - (** [get_projections_from_constant (evd,c) ] returns an array of constr [| a1,.. an|] such that [c] is defined as Definition c := mk a1 .. an with mk a constructor. ai is therefore either a type parameter or a projection. *) - let get_projections_from_constant (evd, i) = - match EConstr.kind evd (Reductionops.clos_whd_flags CClosure.all (Global.env ()) evd i) with + match + EConstr.kind evd + (Reductionops.clos_whd_flags CClosure.all (Global.env ()) evd i) + with | App (c, a) -> Some a | _ -> - raise (CErrors.user_err Pp.(str "The hnf of term " ++ pr_constr (Global.env ()) evd i - ++ str " should be an application i.e. (c a1 ... an)")) + raise + (CErrors.user_err + Pp.( + str "The hnf of term " + ++ pr_constr (Global.env ()) evd i + ++ str " should be an application i.e. (c a1 ... an)")) (** An instance of type, say T, is registered into a hashtable, say TableT. *) type 'a decl = - { decl: EConstr.t + { decl : EConstr.t ; (* Registered type instance *) - deriv: 'a - (* Projections of insterest *) } - + deriv : 'a (* Projections of insterest *) } module EInjT = struct type t = - { isid: bool + { isid : bool ; (* S = T -> inj = fun x -> x*) - source: EConstr.t + source : EConstr.t ; (* S *) - target: EConstr.t + target : EConstr.t ; (* T *) (* projections *) - inj: EConstr.t + inj : EConstr.t ; (* S -> T *) - pred: EConstr.t + pred : EConstr.t ; (* T -> Prop *) - cstr: EConstr.t option - (* forall x, pred (inj x) *) } + cstr : EConstr.t option (* forall x, pred (inj x) *) } end module EBinOpT = struct type t = { (* Op : source1 -> source2 -> source3 *) - source1: EConstr.t - ; source2: EConstr.t - ; source3: EConstr.t - ; target: EConstr.t - ; inj1: EConstr.t + source1 : EConstr.t + ; source2 : EConstr.t + ; source3 : EConstr.t + ; target : EConstr.t + ; inj1 : EConstr.t ; (* InjTyp source1 target *) - inj2: EConstr.t + inj2 : EConstr.t ; (* InjTyp source2 target *) - inj3: EConstr.t + inj3 : EConstr.t ; (* InjTyp source3 target *) - tbop: EConstr.t - (* TBOpInj *) } + tbop : EConstr.t (* TBOpInj *) } end module ECstOpT = struct - type t = {source: EConstr.t; target: EConstr.t; inj: EConstr.t} + type t = {source : EConstr.t; target : EConstr.t; inj : EConstr.t} end module EUnOpT = struct type t = - { source1: EConstr.t - ; source2: EConstr.t - ; target: EConstr.t - ; inj1_t: EConstr.t - ; inj2_t: EConstr.t - ; unop: EConstr.t } + { source1 : EConstr.t + ; source2 : EConstr.t + ; target : EConstr.t + ; inj1_t : EConstr.t + ; inj2_t : EConstr.t + ; unop : EConstr.t } end module EBinRelT = struct type t = - {source: EConstr.t; target: EConstr.t; inj: EConstr.t; brel: EConstr.t} + {source : EConstr.t; target : EConstr.t; inj : EConstr.t; brel : EConstr.t} end module EPropBinOpT = struct @@ -147,37 +141,32 @@ module EPropUnOpT = struct type t = EConstr.t end - module ESatT = struct - type t = {parg1: EConstr.t; parg2: EConstr.t; satOK: EConstr.t} + type t = {parg1 : EConstr.t; parg2 : EConstr.t; satOK : EConstr.t} end (* Different type of declarations *) type decl_kind = | PropOp of EPropBinOpT.t decl - | PropUnOp of EPropUnOpT.t decl - | InjTyp of EInjT.t decl - | BinRel of EBinRelT.t decl - | BinOp of EBinOpT.t decl - | UnOp of EUnOpT.t decl - | CstOp of ECstOpT.t decl - | Saturate of ESatT.t decl - - -let get_decl = function + | PropUnOp of EPropUnOpT.t decl + | InjTyp of EInjT.t decl + | BinRel of EBinRelT.t decl + | BinOp of EBinOpT.t decl + | UnOp of EUnOpT.t decl + | CstOp of ECstOpT.t decl + | Saturate of ESatT.t decl + +let get_decl = function | PropOp d -> d.decl - | PropUnOp d -> d.decl - | InjTyp d -> d.decl - | BinRel d -> d.decl - | BinOp d -> d.decl - | UnOp d -> d.decl - | CstOp d -> d.decl - | Saturate d -> d.decl - -type term_kind = - | Application of EConstr.constr - | OtherTerm of EConstr.constr + | PropUnOp d -> d.decl + | InjTyp d -> d.decl + | BinRel d -> d.decl + | BinOp d -> d.decl + | UnOp d -> d.decl + | CstOp d -> d.decl + | Saturate d -> d.decl +type term_kind = Application of EConstr.constr | OtherTerm of EConstr.constr module type Elt = sig type elt @@ -185,11 +174,9 @@ module type Elt = sig val name : string (** name *) - val table : (term_kind * decl_kind) HConstr.t ref - + val table : (term_kind * decl_kind) HConstr.t ref val cast : elt decl -> decl_kind - - val dest : decl_kind -> (elt decl) option + val dest : decl_kind -> elt decl option val get_key : int (** [get_key] is the type-index used as key for the instance *) @@ -199,19 +186,14 @@ module type Elt = sig built from the type-instance i and the arguments (type indexes and projections) of the type-class constructor. *) - (* val arity : int*) - + (* val arity : int*) end - -let table = Summary.ref ~name:("zify_table") HConstr.empty - -let saturate = Summary.ref ~name:("zify_saturate") HConstr.empty - +let table = Summary.ref ~name:"zify_table" HConstr.empty +let saturate = Summary.ref ~name:"zify_saturate" HConstr.empty let table_cache = ref HConstr.empty let saturate_cache = ref HConstr.empty - (** Each type-class gives rise to a different table. They only differ on how projections are extracted. *) module EInj = struct @@ -220,186 +202,129 @@ module EInj = struct type elt = EInjT.t let name = "EInj" - let table = table - let cast x = InjTyp x - - let dest = function - | InjTyp x -> Some x - | _ -> None - + let dest = function InjTyp x -> Some x | _ -> None let mk_elt evd i (a : EConstr.t array) = let isid = EConstr.eq_constr evd a.(0) a.(1) in { isid - ; source= a.(0) - ; target= a.(1) - ; inj= a.(2) - ; pred= a.(3) - ; cstr= (if isid then None else Some a.(4)) } + ; source = a.(0) + ; target = a.(1) + ; inj = a.(2) + ; pred = a.(3) + ; cstr = (if isid then None else Some a.(4)) } let get_key = 0 - end module EBinOp = struct type elt = EBinOpT.t + open EBinOpT let name = "BinOp" - let table = table let mk_elt evd i a = - { source1= a.(0) - ; source2= a.(1) - ; source3= a.(2) - ; target= a.(3) - ; inj1= a.(5) - ; inj2= a.(6) - ; inj3= a.(7) - ; tbop= a.(9) } + { source1 = a.(0) + ; source2 = a.(1) + ; source3 = a.(2) + ; target = a.(3) + ; inj1 = a.(5) + ; inj2 = a.(6) + ; inj3 = a.(7) + ; tbop = a.(9) } let get_key = 4 - - let cast x = BinOp x - - let dest = function - | BinOp x -> Some x - | _ -> None - + let dest = function BinOp x -> Some x | _ -> None end module ECstOp = struct type elt = ECstOpT.t + open ECstOpT let name = "CstOp" - let table = table - let cast x = CstOp x - - let dest = function - | CstOp x -> Some x - | _ -> None - - - let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3)} - + let dest = function CstOp x -> Some x | _ -> None + let mk_elt evd i a = {source = a.(0); target = a.(1); inj = a.(3)} let get_key = 2 - end module EUnOp = struct type elt = EUnOpT.t + open EUnOpT let name = "UnOp" - let table = table - let cast x = UnOp x - - let dest = function - | UnOp x -> Some x - | _ -> None - + let dest = function UnOp x -> Some x | _ -> None let mk_elt evd i a = - { source1= a.(0) - ; source2= a.(1) - ; target= a.(2) - ; inj1_t= a.(4) - ; inj2_t= a.(5) - ; unop= a.(6) } + { source1 = a.(0) + ; source2 = a.(1) + ; target = a.(2) + ; inj1_t = a.(4) + ; inj2_t = a.(5) + ; unop = a.(6) } let get_key = 3 - end module EBinRel = struct type elt = EBinRelT.t + open EBinRelT let name = "BinRel" - let table = table - let cast x = BinRel x + let dest = function BinRel x -> Some x | _ -> None - let dest = function - | BinRel x -> Some x - | _ -> None - - let mk_elt evd i a = {source= a.(0); target= a.(1); inj= a.(3); brel= a.(4)} + let mk_elt evd i a = + {source = a.(0); target = a.(1); inj = a.(3); brel = a.(4)} let get_key = 2 - end module EPropOp = struct type elt = EConstr.t let name = "PropBinOp" - let table = table - let cast x = PropOp x - - let dest = function - | PropOp x -> Some x - | _ -> None - + let dest = function PropOp x -> Some x | _ -> None let mk_elt evd i a = i - let get_key = 0 - end module EPropUnOp = struct type elt = EConstr.t let name = "PropUnOp" - let table = table - let cast x = PropUnOp x - - let dest = function - | PropUnOp x -> Some x - | _ -> None - + let dest = function PropUnOp x -> Some x | _ -> None let mk_elt evd i a = i - let get_key = 0 - end - - -let constr_of_term_kind = function - | Application c -> c - | OtherTerm c -> c - - +let constr_of_term_kind = function Application c -> c | OtherTerm c -> c let fold_declared_const f evd acc = HConstr.fold - (fun _ (_,e) acc -> f (fst (EConstr.destConst evd (get_decl e))) acc) - (!table_cache) acc - - + (fun _ (_, e) acc -> f (fst (EConstr.destConst evd (get_decl e))) acc) + !table_cache acc module type S = sig val register : Constrexpr.constr_expr -> unit - val print : unit -> unit end - module MakeTable (E : Elt) = struct (** Given a term [c] and its arguments ai, we construct a HConstr.t table that is @@ -410,33 +335,34 @@ module MakeTable (E : Elt) = struct let make_elt (evd, i) = match get_projections_from_constant (evd, i) with | None -> - let env = Global.env () in - let t = string_of_ppcmds (pr_constr env evd i) in - failwith ("Cannot register term " ^ t) + let env = Global.env () in + let t = string_of_ppcmds (pr_constr env evd i) in + failwith ("Cannot register term " ^ t) | Some a -> E.mk_elt evd i a - let register_hint evd t elt = + let register_hint evd t elt = match EConstr.kind evd t with - | App(c,_) -> - E.table := HConstr.add c (Application t, E.cast elt) !E.table - | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table - - - + | App (c, _) -> + E.table := HConstr.add c (Application t, E.cast elt) !E.table + | _ -> E.table := HConstr.add t (OtherTerm t, E.cast elt) !E.table let register_constr env evd c = let c = EConstr.of_constr c in let t = get_type_of env evd c in match EConstr.kind evd t with | App (intyp, args) -> - let styp = args.(E.get_key) in - let elt = {decl= c; deriv= (make_elt (evd, c))} in - register_hint evd styp elt + let styp = args.(E.get_key) in + let elt = {decl = c; deriv = make_elt (evd, c)} in + register_hint evd styp elt | _ -> - let env = Global.env () in - raise (CErrors.user_err Pp. - (str ": Cannot register term "++pr_constr env evd c++ - str ". It has type "++pr_constr env evd t++str " which should be of the form [F X1 .. Xn]")) + let env = Global.env () in + raise + (CErrors.user_err + Pp.( + str ": Cannot register term " + ++ pr_constr env evd c ++ str ". It has type " + ++ pr_constr env evd t + ++ str " which should be of the form [F X1 .. Xn]")) let register_obj : Constr.constr -> Libobject.obj = let cache_constr (_, c) = @@ -447,7 +373,7 @@ module MakeTable (E : Elt) = struct let subst_constr (subst, c) = Mod_subst.subst_mps subst c in Libobject.declare_object @@ Libobject.superglobal_object_nodischarge - ("register-zify-" ^ E.name) + ("register-zify-" ^ E.name) ~cache:cache_constr ~subst:(Some subst_constr) (** [register c] is called from the VERNACULAR ADD [name] constr(t). @@ -455,52 +381,40 @@ module MakeTable (E : Elt) = struct registered as a [superglobal_object_nodischarge]. TODO: pre-compute [get_type_of] - [cache_constr] is using another environment. *) - let register = fun c -> + let register c = let env = Global.env () in let evd = Evd.from_env env in let evd, c = Constrintern.interp_open_constr env evd c in let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in () - let pp_keys () = let env = Global.env () in let evd = Evd.from_env env in HConstr.fold - (fun _ (k,d) acc -> + (fun _ (k, d) acc -> match E.dest d with | None -> acc | Some _ -> - Pp.(pr_constr env evd (constr_of_term_kind k) ++ str " " ++ acc)) - (!E.table) (Pp.str "") - - - let print () = Feedback.msg_info (pp_keys ()) + Pp.(pr_constr env evd (constr_of_term_kind k) ++ str " " ++ acc)) + !E.table (Pp.str "") + let print () = Feedback.msg_info (pp_keys ()) end - module InjTable = MakeTable (EInj) - module ESat = struct type elt = ESatT.t + open ESatT let name = "Saturate" - let table = saturate - let cast x = Saturate x - - let dest = function - | Saturate x -> Some x - | _ -> None - - let mk_elt evd i a = {parg1= a.(2); parg2= a.(3); satOK= a.(5)} - + let dest = function Saturate x -> Some x | _ -> None + let mk_elt evd i a = {parg1 = a.(2); parg2 = a.(3); satOK = a.(5)} let get_key = 1 - end module BinOp = MakeTable (EBinOp) @@ -512,10 +426,9 @@ module PropUnOp = MakeTable (EPropUnOp) module Saturate = MakeTable (ESat) let init_cache () = - table_cache := !table; + table_cache := !table; saturate_cache := !saturate - (** The module [Spec] is used to register the instances of [BinOpSpec], [UnOpSpec]. They are not indexed and stored in a list. *) @@ -556,7 +469,6 @@ module Spec = struct Feedback.msg_notice l end - let unfold_decl evd = let f cst acc = cst :: acc in fold_declared_const f evd [] @@ -578,33 +490,19 @@ let locate_const str = (* The following [constr] are necessary for constructing the proof terms *) let mkapp2 = lazy (zify "mkapp2") - let mkapp = lazy (zify "mkapp") - let mkapp0 = lazy (zify "mkapp0") - let mkdp = lazy (zify "mkinjterm") - let eq_refl = lazy (zify "eq_refl") - let mkrel = lazy (zify "mkrel") - let mkprop_op = lazy (zify "mkprop_op") - let mkuprop_op = lazy (zify "mkuprop_op") - let mkdpP = lazy (zify "mkinjprop") - let iff_refl = lazy (zify "iff_refl") - let q = lazy (zify "target_prop") - let ieq = lazy (zify "injprop_ok") - let iff = lazy (zify "iff") - - (* A super-set of the previous are needed to unfold the generated proof terms. *) let to_unfold = @@ -631,7 +529,6 @@ let to_unfold = ; "mkapp0" ; "mkprop_op" ]) - (** Module [CstrTable] records terms [x] injected into [inj x] together with the corresponding type constraint. The terms are stored by side-effect during the traversal @@ -644,17 +541,15 @@ module CstrTable = struct type t = EConstr.t let hash c = Constr.hash (unsafe_to_constr c) - let equal c c' = Constr.equal (unsafe_to_constr c) (unsafe_to_constr c') end) let table : EConstr.t HConstr.t = HConstr.create 10 - let register evd t (i : EConstr.t) = HConstr.add table t i let get () = let l = HConstr.fold (fun k i acc -> (k, i) :: acc) table [] in - HConstr.clear table ; l + HConstr.clear table; l (** [gen_cstr table] asserts (cstr k) for each element of the table (k,cstr). NB: the constraint is only asserted if it does not already exist in the context. @@ -667,7 +562,7 @@ module CstrTable = struct let hyps_table = HConstr.create 20 in List.iter (fun (_, (t : EConstr.types)) -> HConstr.add hyps_table t ()) - (Tacmach.New.pf_hyps_types gl) ; + (Tacmach.New.pf_hyps_types gl); fun c -> HConstr.mem hyps_table c in (* Add the constraint (cstr k) if it is not already present *) @@ -683,17 +578,16 @@ module CstrTable = struct (Names.Id.of_string "cstr") env in - Tactics.pose_proof (Names.Name n) term ) + Tactics.pose_proof (Names.Name n) term) in List.fold_left (fun acc (k, i) -> Tacticals.New.tclTHEN (gen k i) acc) - Tacticals.New.tclIDTAC table ) + Tacticals.New.tclIDTAC table) end let mkvar red evd inj v = ( if not red then - match inj.cstr with None -> () | Some ctr -> CstrTable.register evd v ctr - ) ; + match inj.cstr with None -> () | Some ctr -> CstrTable.register evd v ctr ); let iv = EConstr.mkApp (inj.inj, [|v|]) in let iv = if red then Tacred.compute (Global.env ()) evd iv else iv in EConstr.mkApp @@ -724,11 +618,8 @@ let inj_term_of_texpr evd = function | Var (inj, e) -> mkvar false evd inj e | Constant (inj, e) -> mkvar true evd inj e -let mkapp2_id evd i (* InjTyp S3 T *) - inj (* deriv i *) - t (* S1 -> S2 -> S3 *) - b (* Binop S1 S2 S3 t ... *) - dbop (* deriv b *) e1 e2 = +let mkapp2_id evd i (* InjTyp S3 T *) inj (* deriv i *) t (* S1 -> S2 -> S3 *) b + (* Binop S1 S2 S3 t ... *) dbop (* deriv b *) e1 e2 = let default () = let e1' = inj_term_of_texpr evd e1 in let e2' = inj_term_of_texpr evd e2 in @@ -755,15 +646,16 @@ let mkapp2_id evd i (* InjTyp S3 T *) |Var (_, e1), Var (_, e2) |Constant (_, e1), Var (_, e2) |Var (_, e1), Constant (_, e2) -> - Var (inj, EConstr.mkApp (t, [|e1; e2|])) + Var (inj, EConstr.mkApp (t, [|e1; e2|])) | _, _ -> default () let mkapp_id evd i inj (unop, u) f e1 = - EUnOpT.(if EConstr.eq_constr evd u.unop f then - (* Injection does nothing *) - match e1 with - | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|])) - | Injterm e1 -> + EUnOpT.( + if EConstr.eq_constr evd u.unop f then + (* Injection does nothing *) + match e1 with + | Constant (_, e) | Var (_, e) -> Var (inj, EConstr.mkApp (f, [|e|])) + | Injterm e1 -> Injterm (EConstr.mkApp ( force mkapp @@ -775,124 +667,128 @@ let mkapp_id evd i inj (unop, u) f e1 = ; u.inj2_t ; unop ; e1 |] )) - else - let e1 = inj_term_of_texpr evd e1 in - Injterm - (EConstr.mkApp - ( force mkapp - , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|] - ))) - -type typed_constr = {constr: EConstr.t; typ: EConstr.t} - + else + let e1 = inj_term_of_texpr evd e1 in + Injterm + (EConstr.mkApp + ( force mkapp + , [|u.source1; u.source2; u.target; f; u.inj1_t; u.inj2_t; unop; e1|] + ))) +type typed_constr = {constr : EConstr.t; typ : EConstr.t} let get_injection env evd t = match snd (HConstr.find t !table_cache) with | InjTyp i -> i - | _ -> raise Not_found - - - (* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *) - let arrow = - let name x = - Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant in - EConstr.mkLambda - ( name "x" - , EConstr.mkProp - , EConstr.mkLambda - ( name "y" - , EConstr.mkProp - , EConstr.mkProd - ( Context.make_annot Names.Anonymous Sorts.Relevant - , EConstr.mkRel 2 - , EConstr.mkRel 2 ) ) ) - - - let is_prop env sigma term = - let sort = Retyping.get_sort_of env sigma term in + | _ -> raise Not_found + +(* [arrow] is the term (fun (x:Prop) (y : Prop) => x -> y) *) +let arrow = + let name x = + Context.make_annot (Name.mk_name (Names.Id.of_string x)) Sorts.Relevant + in + EConstr.mkLambda + ( name "x" + , EConstr.mkProp + , EConstr.mkLambda + ( name "y" + , EConstr.mkProp + , EConstr.mkProd + ( Context.make_annot Names.Anonymous Sorts.Relevant + , EConstr.mkRel 2 + , EConstr.mkRel 2 ) ) ) + +let is_prop env sigma term = + let sort = Retyping.get_sort_of env sigma term in Sorts.is_prop sort - (** [get_application env evd e] expresses [e] as an application (c a) +(** [get_application env evd e] expresses [e] as an application (c a) where c is the head symbol and [a] is the array of arguments. The function also transforms (x -> y) as (arrow x y) *) - let get_operator env evd e = - let is_arrow a p1 p2 = - is_prop env evd p1 && is_prop (EConstr.push_rel (Context.Rel.Declaration.LocalAssum(a,p1)) env) evd p2 - && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) in - match EConstr.kind evd e with - | Prod (a, p1, p2) when is_arrow a p1 p2 -> - (arrow,[|p1 ;p2|]) - | App(c,a) -> (c,a) - | _ -> (e,[||]) - +let get_operator env evd e = + let is_arrow a p1 p2 = + is_prop env evd p1 + && is_prop + (EConstr.push_rel (Context.Rel.Declaration.LocalAssum (a, p1)) env) + evd p2 + && (a.Context.binder_name = Names.Anonymous || EConstr.Vars.noccurn evd 1 p2) + in + match EConstr.kind evd e with + | Prod (a, p1, p2) when is_arrow a p1 p2 -> (arrow, [|p1; p2|]) + | App (c, a) -> (c, a) + | _ -> (e, [||]) - let is_convertible env evd k t = - Reductionops.check_conv env evd k t +let is_convertible env evd k t = Reductionops.check_conv env evd k t - (** [match_operator env evd hd arg (t,d)] +(** [match_operator env evd hd arg (t,d)] - hd is head operator of t - If t = OtherTerm _, then t = hd - If t = Application _, then we extract the relevant number of arguments from arg and check for convertibility *) - let match_operator env evd hd args (t, d) = - let decomp t i = - let n = Array.length args in - let t' = EConstr.mkApp(hd,Array.sub args 0 (n-i)) in - if is_convertible env evd t' t - then Some (d,t) - else None in - - match t with - | OtherTerm t -> Some(d,t) - | Application t -> - match d with - | CstOp _ -> decomp t 0 - | UnOp _ -> decomp t 1 - | BinOp _ -> decomp t 2 - | BinRel _ -> decomp t 2 - | PropOp _ -> decomp t 2 - | PropUnOp _ -> decomp t 1 - | _ -> None - - - let rec trans_expr env evd e = +let match_operator env evd hd args (t, d) = + let decomp t i = + let n = Array.length args in + let t' = EConstr.mkApp (hd, Array.sub args 0 (n - i)) in + if is_convertible env evd t' t then Some (d, t) else None + in + match t with + | OtherTerm t -> Some (d, t) + | Application t -> ( + match d with + | CstOp _ -> decomp t 0 + | UnOp _ -> decomp t 1 + | BinOp _ -> decomp t 2 + | BinRel _ -> decomp t 2 + | PropOp _ -> decomp t 2 + | PropUnOp _ -> decomp t 1 + | _ -> None ) + +let rec trans_expr env evd e = (* Get the injection *) - let {decl= i; deriv= inj} = get_injection env evd e.typ in + let {decl = i; deriv = inj} = get_injection env evd e.typ in let e = e.constr in if EConstr.isConstruct evd e then Constant (inj, e) (* Evaluate later *) else - let (c,a) = get_operator env evd e in + let c, a = get_operator env evd e in try - let (k,t) = find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) in + let k, t = + find_option + (match_operator env evd c a) + (HConstr.find_all c !table_cache) + in let n = Array.length a in - match k with - | CstOp {decl = c'} -> - Injterm (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c'|])) - | UnOp {decl = unop ; deriv = u} -> - let a' = trans_expr env evd {constr= a.(n-1); typ= u.EUnOpT.source1} in - if is_constant a' && EConstr.isConstruct evd t then - Constant (inj, e) - else mkapp_id evd i inj (unop, u) t a' - | BinOp {decl = binop ; deriv = b} -> - let a0 = trans_expr env evd {constr= a.(n-2); typ= b.EBinOpT.source1} in - let a1 = trans_expr env evd {constr= a.(n-1); typ= b.EBinOpT.source2} in - if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t - then Constant (inj, e) - else mkapp2_id evd i inj t binop b a0 a1 - | d -> - Var (inj,e) - with Not_found -> Var (inj,e) + match k with + | CstOp {decl = c'} -> + Injterm + (EConstr.mkApp (force mkapp0, [|inj.source; inj.target; e; i; c'|])) + | UnOp {decl = unop; deriv = u} -> + let a' = + trans_expr env evd {constr = a.(n - 1); typ = u.EUnOpT.source1} + in + if is_constant a' && EConstr.isConstruct evd t then Constant (inj, e) + else mkapp_id evd i inj (unop, u) t a' + | BinOp {decl = binop; deriv = b} -> + let a0 = + trans_expr env evd {constr = a.(n - 2); typ = b.EBinOpT.source1} + in + let a1 = + trans_expr env evd {constr = a.(n - 1); typ = b.EBinOpT.source2} + in + if is_constant a0 && is_constant a1 && EConstr.isConstruct evd t then + Constant (inj, e) + else mkapp2_id evd i inj t binop b a0 a1 + | d -> Var (inj, e) + with Not_found -> Var (inj, e) let trans_expr env evd e = - try trans_expr env evd e with Not_found -> + try trans_expr env evd e + with Not_found -> raise (CErrors.user_err ( Pp.str "Missing injection for type " ++ Printer.pr_leconstr_env env evd e.typ )) - type tprop = | TProp of EConstr.t (** Transformed proposition *) | IProp of EConstr.t (** Identical proposition *) @@ -903,72 +799,72 @@ let mk_iprop e = let inj_prop_of_tprop = function TProp p -> p | IProp e -> mk_iprop e let rec trans_prop env evd e = - let (c,a) = get_operator env evd e in + let c, a = get_operator env evd e in try - let (k,t) = find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) in + let k, t = + find_option (match_operator env evd c a) (HConstr.find_all c !table_cache) + in let n = Array.length a in match k with - | PropOp {decl= rop} -> - begin - try - let t1 = trans_prop env evd a.(n-2) in - let t2 = trans_prop env evd a.(n-1) in - match (t1, t2) with - | IProp _, IProp _ -> IProp e - | _, _ -> - let t1 = inj_prop_of_tprop t1 in - let t2 = inj_prop_of_tprop t2 in - TProp (EConstr.mkApp (force mkprop_op, [|t; rop; t1; t2|])) - with Not_found -> IProp e - end - | BinRel {decl = br ; deriv = rop} -> - begin - try - let a1 = trans_expr env evd {constr = a.(n-2) ; typ = rop.EBinRelT.source} in - let a2 = trans_expr env evd {constr = a.(n-1) ; typ = rop.EBinRelT.source} in - if EConstr.eq_constr evd t rop.EBinRelT.brel then - match (constr_of_texpr a1, constr_of_texpr a2) with - | Some e1, Some e2 -> IProp (EConstr.mkApp (t, [|e1; e2|])) - | _, _ -> - let a1 = inj_term_of_texpr evd a1 in - let a2 = inj_term_of_texpr evd a2 in - TProp - (EConstr.mkApp - ( force mkrel - , [| rop.EBinRelT.source - ; rop.EBinRelT.target - ; t - ; rop.EBinRelT.inj - ; br - ; a1 - ; a2 |] )) - else - let a1 = inj_term_of_texpr evd a1 in - let a2 = inj_term_of_texpr evd a2 in - TProp - (EConstr.mkApp - ( force mkrel - , [| rop.EBinRelT.source - ; rop.EBinRelT.target - ; t - ; rop.EBinRelT.inj - ; br - ; a1 - ; a2 |] )) - with Not_found -> IProp e - end - | PropUnOp {decl = rop} -> - begin - try - let t1 = trans_prop env evd a.(n-1) in - match t1 with - | IProp _ -> IProp e - | _ -> - let t1 = inj_prop_of_tprop t1 in - TProp (EConstr.mkApp (force mkuprop_op, [|t; rop; t1|])) - with Not_found -> IProp e - end - | _ -> IProp e + | PropOp {decl = rop} -> ( + try + let t1 = trans_prop env evd a.(n - 2) in + let t2 = trans_prop env evd a.(n - 1) in + match (t1, t2) with + | IProp _, IProp _ -> IProp e + | _, _ -> + let t1 = inj_prop_of_tprop t1 in + let t2 = inj_prop_of_tprop t2 in + TProp (EConstr.mkApp (force mkprop_op, [|t; rop; t1; t2|])) + with Not_found -> IProp e ) + | BinRel {decl = br; deriv = rop} -> ( + try + let a1 = + trans_expr env evd {constr = a.(n - 2); typ = rop.EBinRelT.source} + in + let a2 = + trans_expr env evd {constr = a.(n - 1); typ = rop.EBinRelT.source} + in + if EConstr.eq_constr evd t rop.EBinRelT.brel then + match (constr_of_texpr a1, constr_of_texpr a2) with + | Some e1, Some e2 -> IProp (EConstr.mkApp (t, [|e1; e2|])) + | _, _ -> + let a1 = inj_term_of_texpr evd a1 in + let a2 = inj_term_of_texpr evd a2 in + TProp + (EConstr.mkApp + ( force mkrel + , [| rop.EBinRelT.source + ; rop.EBinRelT.target + ; t + ; rop.EBinRelT.inj + ; br + ; a1 + ; a2 |] )) + else + let a1 = inj_term_of_texpr evd a1 in + let a2 = inj_term_of_texpr evd a2 in + TProp + (EConstr.mkApp + ( force mkrel + , [| rop.EBinRelT.source + ; rop.EBinRelT.target + ; t + ; rop.EBinRelT.inj + ; br + ; a1 + ; a2 |] )) + with Not_found -> IProp e ) + | PropUnOp {decl = rop} -> ( + try + let t1 = trans_prop env evd a.(n - 1) in + match t1 with + | IProp _ -> IProp e + | _ -> + let t1 = inj_prop_of_tprop t1 in + TProp (EConstr.mkApp (force mkuprop_op, [|t; rop; t1|])) + with Not_found -> IProp e ) + | _ -> IProp e with Not_found -> IProp e let unfold n env evd c = @@ -984,14 +880,14 @@ let unfold n env evd c = match n with | None -> c | Some n -> - Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c + Tacred.unfoldn [(Locus.AllOccurrences, Names.EvalVarRef n)] env evd c in (* Reduce the term *) - let c = cbv (List.rev_append (force to_unfold) unfold_decl) env evd c in + let c = cbv (List.rev_append (force to_unfold) unfold_decl) env evd c in c let trans_check_prop env evd t = - if is_prop env evd t then + if is_prop env evd t then (*let t = Tacred.unfoldn [Locus.AllOccurrences, Names.EvalConstRef coq_not] env evd t in*) match trans_prop env evd t with IProp e -> None | TProp e -> Some e else None @@ -1001,7 +897,7 @@ let trans_hyps env evd l = (fun acc (h, p) -> match trans_check_prop env evd p with | None -> acc - | Some p' -> (h, p, p') :: acc ) + | Some p' -> (h, p, p') :: acc) [] (List.rev l) (* Only used if a direct rewrite fails *) @@ -1016,7 +912,7 @@ let trans_hyp h t = let h' = fresh_id_in_env Id.Set.empty h env in tclTHENLIST [ letin_tac None (Names.Name n) t None - Locus.{onhyps= None; concl_occs= NoOccurrences} + Locus.{onhyps = None; concl_occs = NoOccurrences} ; assert_by (Name.Name h') (EConstr.mkApp (force q, [|EConstr.mkVar n|])) (tclTHEN @@ -1027,19 +923,19 @@ let trans_hyp h t = (h', Locus.InHyp) ; clear [n] ; (* [clear H] may fail if [h] has dependencies *) - tclTRY (clear [h]) ] ))) + tclTRY (clear [h]) ]))) let is_progress_rewrite evd t rew = match EConstr.kind evd rew with | App (c, [|lhs; rhs|]) -> - if EConstr.eq_constr evd (force iff) c then - (* This is a successful rewriting *) - not (EConstr.eq_constr evd lhs rhs) - else - CErrors.anomaly - Pp.( - str "is_progress_rewrite: not a rewrite" - ++ pr_constr (Global.env ()) evd rew) + if EConstr.eq_constr evd (force iff) c then + (* This is a successful rewriting *) + not (EConstr.eq_constr evd lhs rhs) + else + CErrors.anomaly + Pp.( + str "is_progress_rewrite: not a rewrite" + ++ pr_constr (Global.env ()) evd rew) | _ -> failwith "is_progress_rewrite: not even an application" let trans_hyp h t0 t = @@ -1050,10 +946,10 @@ let trans_hyp h t0 t = let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in if is_progress_rewrite evd t0 (get_type_of env evd t') then tclFIRST - [ Equality.general_rewrite_in true Locus.AllOccurrences true false - h t' false + [ Equality.general_rewrite_in true Locus.AllOccurrences true false h + t' false ; trans_hyp h t ] - else tclIDTAC )) + else tclIDTAC)) let trans_concl t = Tacticals.New.( @@ -1064,15 +960,15 @@ let trans_concl t = let t' = unfold None env evd (EConstr.mkApp (force ieq, [|t|])) in if is_progress_rewrite evd concl (get_type_of env evd t') then Equality.general_rewrite true Locus.AllOccurrences true false t' - else tclIDTAC )) + else tclIDTAC)) let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' let zify_tac = Proofview.Goal.enter (fun gl -> - Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"] ; - Coqlib.check_required_library ["Coq"; "micromega"; "ZifyInst"] ; + Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"]; + Coqlib.check_required_library ["Coq"; "micromega"; "ZifyInst"]; init_cache (); let evd = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in @@ -1083,15 +979,16 @@ let zify_tac = (Tacticals.New.tclTHEN (Tacticals.New.tclTHENLIST (List.rev_map (fun (h, p, t) -> trans_hyp h p t) hyps)) - (CstrTable.gen_cstr l)) ) + (CstrTable.gen_cstr l))) let iter_specs tac = Tacticals.New.tclTHENLIST - (List.fold_left (fun acc d -> tac d :: acc) [] (Spec.get ())) + (List.fold_left (fun acc d -> tac d :: acc) [] (Spec.get ())) - -let iter_specs (tac: Ltac_plugin.Tacinterp.Value.t) = - iter_specs (fun c -> Ltac_plugin.Tacinterp.Value.apply tac [Ltac_plugin.Tacinterp.Value.of_constr c]) +let iter_specs (tac : Ltac_plugin.Tacinterp.Value.t) = + iter_specs (fun c -> + Ltac_plugin.Tacinterp.Value.apply tac + [Ltac_plugin.Tacinterp.Value.of_constr c]) let find_hyp evd t l = try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)) @@ -1104,39 +1001,37 @@ let sat_constr c d = let hyps = Tacmach.New.pf_hyps_types gl in match EConstr.kind evd c with | App (c, args) -> - if Array.length args = 2 then ( - let h1 = - Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) + if Array.length args = 2 then + let h1 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|])) + in + let h2 = + Tacred.cbv_beta env evd + (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) + in + match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with + | Some h1, Some h2 -> + let n = + Tactics.fresh_id_in_env Id.Set.empty + (Names.Id.of_string "__sat") + env in - let h2 = - Tacred.cbv_beta env evd - (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|])) + let trm = + EConstr.mkApp + ( d.ESatT.satOK + , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] ) in - match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with - | Some h1, Some h2 -> - let n = - Tactics.fresh_id_in_env Id.Set.empty - (Names.Id.of_string "__sat") - env - in - let trm = - EConstr.mkApp - ( d.ESatT.satOK - , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] - ) - in - Tactics.pose_proof (Names.Name n) trm - | _, _ -> Tacticals.New.tclIDTAC ) - else Tacticals.New.tclIDTAC - | _ -> Tacticals.New.tclIDTAC ) - + Tactics.pose_proof (Names.Name n) trm + | _, _ -> Tacticals.New.tclIDTAC + else Tacticals.New.tclIDTAC + | _ -> Tacticals.New.tclIDTAC) let get_all_sat env evd c = - List.fold_left (fun acc e -> - match e with - | (_,Saturate s) -> s::acc - | _ -> acc) [] (HConstr.find_all c !saturate_cache ) + List.fold_left + (fun acc e -> match e with _, Saturate s -> s :: acc | _ -> acc) + [] + (HConstr.find_all c !saturate_cache) let saturate = Proofview.Goal.enter (fun gl -> @@ -1149,21 +1044,19 @@ let saturate = let rec sat t = match EConstr.kind evd t with | App (c, args) -> - sat c ; - Array.iter sat args ; - if Array.length args = 2 then - let ds = get_all_sat env evd c in - if ds = [] then () - else ( - List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds ) - else () + sat c; + Array.iter sat args; + if Array.length args = 2 then + let ds = get_all_sat env evd c in + if ds = [] then () + else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds + else () | Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous -> - sat t1 ; sat t2 + sat t1; sat t2 | _ -> () in (* Collect all the potential saturation lemma *) - sat concl ; - List.iter (fun (_, t) -> sat t) hyps ; + sat concl; + List.iter (fun (_, t) -> sat t) hyps; Tacticals.New.tclTHENLIST - (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []) - ) + (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table [])) -- cgit v1.2.3