From 647d66a196f0b99eee35950d0d36b6fb9bfc064a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 10 Aug 2022 22:07:54 -0400 Subject: [PATCH] feat(th-data): use lists, not iter/array; add Proof_rules --- src/th-data/Sidekick_th_data.ml | 96 +++++++++++++++++---------------- src/th-data/proof_rules.ml | 27 ++++++++++ src/th-data/proof_rules.mli | 33 ++++++++++++ src/th-data/th_intf.ml | 51 +++--------------- 4 files changed, 116 insertions(+), 91 deletions(-) create mode 100644 src/th-data/proof_rules.ml create mode 100644 src/th-data/proof_rules.mli diff --git a/src/th-data/Sidekick_th_data.ml b/src/th-data/Sidekick_th_data.ml index 956bec1b..3bf30e6c 100644 --- a/src/th-data/Sidekick_th_data.ml +++ b/src/th-data/Sidekick_th_data.ml @@ -27,8 +27,8 @@ module C = struct | Finite, Finite -> Finite | _ -> Infinite - let sum = Iter.fold ( + ) Finite - let product = Iter.fold ( * ) Finite + let sum = List.fold_left ( + ) Finite + let product = List.fold_left ( * ) Finite let to_string = function | Finite -> "finite" @@ -65,18 +65,19 @@ end = struct (* cut infinite loop *) let res = match A.as_datatype ty with - | Ty_other -> false + | Ty_other { sub = [] } -> false + | Ty_other { sub } -> List.exists is_direct_recursion sub | Ty_arrow (_, ret) -> is_direct_recursion ret - | Ty_app { args } -> Iter.exists is_direct_recursion args | Ty_data { cstors } -> - Iter.flat_map A.Cstor.ty_args cstors - |> Iter.exists is_direct_recursion + List.exists + (fun c -> List.exists is_direct_recursion @@ A.Cstor.ty_args c) + cstors in Ty_tbl.replace dr_tbl ty res; res in let is_direct_recursion_cstor (c : A.Cstor.t) : bool = - Iter.exists is_direct_recursion (A.Cstor.ty_args c) + List.exists is_direct_recursion (A.Cstor.ty_args c) in let rec get_cell (ty : ty) : ty_cell = @@ -88,20 +89,20 @@ end = struct Ty_tbl.add self.cards ty cell; let card = match A.as_datatype ty with - | Ty_other -> + | Ty_other { sub = [] } -> if A.ty_is_finite ty then C.Finite else C.Infinite - | Ty_app { args } -> Iter.map get_card args |> C.product + | Ty_other { sub } -> List.map get_card sub |> C.product | Ty_arrow (args, ret) -> - C.(get_card ret ^ C.product @@ Iter.map get_card args) + C.(get_card ret ^ C.product @@ List.map get_card args) | Ty_data { cstors } -> let c = cstors - |> Iter.map (fun c -> + |> List.map (fun c -> let card = - C.product (Iter.map get_card @@ A.Cstor.ty_args c) + C.product (List.map get_card @@ A.Cstor.ty_args c) in (* we can use [c] as base constructor if it's finite, or at least if it doesn't directly depend on [ty] in @@ -150,17 +151,17 @@ end = struct let name = "th-data.cstor" (* associate to each class a unique constructor term in the class (if any) *) - type t = { c_n: E_node.t; c_cstor: A.Cstor.t; c_args: E_node.t array } + type t = { c_n: E_node.t; c_cstor: A.Cstor.t; c_args: E_node.t list } let pp out (v : t) = Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@ :args [@[%a@]]@])" name - A.Cstor.pp v.c_cstor E_node.pp v.c_n (Util.pp_array E_node.pp) v.c_args + A.Cstor.pp v.c_cstor E_node.pp v.c_n (Util.pp_list E_node.pp) v.c_args (* attach data to constructor terms *) let of_term cc n (t : Term.t) : _ option * _ list = match A.view_as_data t with | T_cstor (cstor, args) -> - let args = CCArray.map (CC.add_term cc) args in + let args = List.map (CC.add_term cc) args in Some { c_n = n; c_cstor = cstor; c_args = args }, [] | _ -> None, [] @@ -186,20 +187,22 @@ end = struct let t1 = E_node.term c1.c_n in let t2 = E_node.term c2.c_n in mk_expl t1 t2 @@ Proof_trace.add_step proof - @@ fun () -> A.P.lemma_cstor_inj t1 t2 i + @@ fun () -> Proof_rules.lemma_cstor_inj t1 t2 i in - assert (CCArray.length c1.c_args = CCArray.length c2.c_args); + assert (List.length c1.c_args = List.length c2.c_args); let acts = ref [] in - Util.array_iteri2 c1.c_args c2.c_args ~f:(fun i u1 u2 -> - acts := CC.Handler_action.Act_merge (u1, u2, expl_merge i) :: !acts); + CCList.iteri2 + (fun i u1 u2 -> + acts := CC.Handler_action.Act_merge (u1, u2, expl_merge i) :: !acts) + c1.c_args c2.c_args; Ok (c1, !acts) ) else ( (* different function: disjointness *) let expl = let t1 = E_node.term c1.c_n and t2 = E_node.term c2.c_n in mk_expl t1 t2 @@ Proof_trace.add_step proof - @@ fun () -> A.P.lemma_cstor_distinct t1 t2 + @@ fun () -> Proof_rules.lemma_cstor_distinct t1 t2 in Error (CC.Handler_action.Conflict expl) @@ -310,7 +313,7 @@ end = struct match A.view_as_data t, A.as_datatype ty with | T_cstor _, _ -> () | _, Ty_data { cstors; _ } -> - (match Iter.take 2 cstors |> Iter.to_rev_list with + (match cstors with | [ cstor ] when not (Term.Tbl.mem self.single_cstor_preproc_done t) -> (* single cstor: assert [t = cstor (sel-c-0 t, …, sel-c n t)] *) Log.debugf 50 (fun k -> @@ -322,8 +325,7 @@ end = struct let u = let sel_args = A.Cstor.ty_args cstor - |> Iter.mapi (fun i _ty -> A.mk_sel self.tst cstor i t) - |> Iter.to_array + |> List.mapi (fun i _ty -> A.mk_sel self.tst cstor i t) in A.mk_cstor self.tst cstor sel_args in @@ -333,10 +335,11 @@ end = struct let proof = let pr_isa = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_isa_split t [ Lit.atom (A.mk_is_a self.tst cstor t) ] + Proof_rules.lemma_isa_split t + [ Lit.atom (A.mk_is_a self.tst cstor t) ] and pr_eq_sel = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_select_cstor ~cstor_t:u t + Proof_rules.lemma_select_cstor ~cstor_t:u t in Proof_trace.add_step self.proof @@ fun () -> Proof_core.proof_r1 pr_isa pr_eq_sel @@ -394,7 +397,7 @@ end = struct name Term.pp_debug t is_true E_node.pp n Monoid_cstor.pp cstor); let pr = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t + Proof_rules.lemma_isa_cstor ~cstor_t:(E_node.term cstor.c_n) t in let n_bool = CC.n_bool cc is_true in let expl = @@ -417,11 +420,11 @@ end = struct Log.debugf 5 (fun k -> k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])" name E_node.pp n i A.Cstor.pp c_t); - assert (i < CCArray.length cstor.c_args); - let u_i = CCArray.get cstor.c_args i in + assert (i < List.length cstor.c_args); + let u_i = List.nth cstor.c_args i in let pr = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t + Proof_rules.lemma_select_cstor ~cstor_t:(E_node.term cstor.c_n) t in let expl = Expl.( @@ -441,7 +444,7 @@ end = struct []) | T_cstor _ | T_other _ -> [] - let cstors_of_ty (ty : ty) : A.Cstor.t Iter.t = + let cstors_of_ty (ty : ty) : A.Cstor.t list = match A.as_datatype ty with | Ty_data { cstors } -> cstors | _ -> assert false @@ -458,7 +461,7 @@ end = struct Monoid_cstor.pp c1); let pr = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n) + Proof_rules.lemma_isa_cstor ~cstor_t:(E_node.term c1.c_n) (E_node.term is_a2.is_a_n) in let n_bool = CC.n_bool cc is_true in @@ -484,13 +487,13 @@ end = struct Log.debugf 5 (fun k -> k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])" name E_node.pp n2 sel2.sel_idx Monoid_cstor.pp c1); - assert (sel2.sel_idx < CCArray.length c1.c_args); + assert (sel2.sel_idx < List.length c1.c_args); let pr = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n) + Proof_rules.lemma_select_cstor ~cstor_t:(E_node.term c1.c_n) (E_node.term sel2.sel_n) in - let u_i = CCArray.get c1.c_args sel2.sel_idx in + let u_i = List.nth c1.c_args sel2.sel_idx in let expl = Expl.mk_theory (E_node.term sel2.sel_n) (E_node.term u_i) [ @@ -563,7 +566,7 @@ end = struct let mk_graph (self : t) cc : graph = let g : graph = N_tbl.create ~size:32 () in let traverse_sub cstor : _ list = - Util.array_to_list_map + List.map (fun sub_n -> sub_n, CC.find cc sub_n) cstor.Monoid_cstor.c_args in @@ -603,7 +606,7 @@ end = struct (fun (a, b) -> E_node.term a, E_node.term b.repr) path in - A.P.lemma_acyclicity path + Proof_rules.lemma_acyclicity path in let expl = let subs = @@ -648,8 +651,7 @@ end = struct let rhs = let args = A.Cstor.ty_args c - |> Iter.mapi (fun i _ty -> A.mk_sel self.tst c i u) - |> Iter.to_list |> CCArray.of_list + |> List.mapi (fun i _ty -> A.mk_sel self.tst c i u) in A.mk_cstor self.tst c args in @@ -657,7 +659,8 @@ end = struct k "(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])" name Term.pp_debug u Term.pp_debug rhs Lit.pp lit); let pr = - Proof_trace.add_step self.proof @@ fun () -> A.P.lemma_isa_sel t + Proof_trace.add_step self.proof @@ fun () -> + Proof_rules.lemma_isa_sel t in (* merge [u] and [rhs] *) CC.merge_t (SI.cc solver) u rhs @@ -676,19 +679,19 @@ end = struct Term.Tbl.add self.case_split_done t (); let c = cstors_of_ty (Term.ty t) - |> Iter.map (fun c -> A.mk_is_a self.tst c t) - |> Iter.map (fun t -> + |> List.map (fun c -> + let t = A.mk_is_a self.tst c t in let lit = SI.mk_lit solver t in (* TODO: set default polarity, depending on n° of args? *) lit) - |> Iter.to_rev_list in SI.add_clause_permanent solver acts c - (Proof_trace.add_step self.proof @@ fun () -> A.P.lemma_isa_split t c); + ( Proof_trace.add_step self.proof @@ fun () -> + Proof_rules.lemma_isa_split t c ); Iter.diagonal_l c (fun (l1, l2) -> let pr = Proof_trace.add_step self.proof @@ fun () -> - A.P.lemma_isa_disj (Lit.neg l1) (Lit.neg l2) + Proof_rules.lemma_isa_disj (Lit.neg l1) (Lit.neg l2) in SI.add_clause_permanent solver acts [ Lit.neg l1; Lit.neg l2 ] pr) ) @@ -752,8 +755,7 @@ end = struct let cstor_app = let args = A.Cstor.ty_args base_cstor - |> Iter.mapi (fun i _ -> A.mk_sel self.tst base_cstor i t) - |> Iter.to_array + |> List.mapi (fun i _ -> A.mk_sel self.tst base_cstor i t) in A.mk_cstor self.tst base_cstor args in @@ -776,7 +778,7 @@ end = struct | Some c -> Log.debugf 5 (fun k -> k "(@[th-data.mk-model.find-cstor@ %a@])" Monoid_cstor.pp c); - let args = CCArray.map (recurse si) c.c_args in + let args = List.map (recurse si) c.c_args in let t = A.mk_cstor self.tst c.c_cstor args in Some t diff --git a/src/th-data/proof_rules.ml b/src/th-data/proof_rules.ml new file mode 100644 index 00000000..5e65ef3c --- /dev/null +++ b/src/th-data/proof_rules.ml @@ -0,0 +1,27 @@ +open Sidekick_core + +let lemma_isa_cstor ~cstor_t t : Proof_term.t = + Proof_term.apply_rule ~terms:[ cstor_t; t ] "data.isa-cstor" + +let lemma_select_cstor ~cstor_t t : Proof_term.t = + Proof_term.apply_rule ~terms:[ cstor_t; t ] "data.select-cstor" + +let lemma_isa_split t lits : Proof_term.t = + Proof_term.apply_rule ~terms:[ t ] ~lits "data.isa-split" + +let lemma_isa_sel t : Proof_term.t = + Proof_term.apply_rule ~terms:[ t ] "data.isa-sel" + +let lemma_isa_disj l1 l2 : Proof_term.t = + Proof_term.apply_rule ~lits:[ l1; l2 ] "data.isa-disj" + +let lemma_cstor_inj t1 t2 i : Proof_term.t = + Proof_term.apply_rule ~terms:[ t1; t2 ] ~indices:[ i ] "data.cstor-inj" + +let lemma_cstor_distinct t1 t2 : Proof_term.t = + Proof_term.apply_rule ~terms:[ t1; t2 ] "data.cstor-distinct" + +let lemma_acyclicity ts : Proof_term.t = + Proof_term.apply_rule + ~terms:(CCList.flat_map (fun (t1, t2) -> [ t1; t2 ]) ts) + "data.acyclicity" diff --git a/src/th-data/proof_rules.mli b/src/th-data/proof_rules.mli new file mode 100644 index 00000000..a2010781 --- /dev/null +++ b/src/th-data/proof_rules.mli @@ -0,0 +1,33 @@ +open Sidekick_core + +val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t +(** [lemma_isa_cstor (d …) (is-c t)] returns the clause + [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *) + +val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t +(** [lemma_select_cstor (c t1…tn) (sel-c-i t)] + returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *) + +val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.t +(** [lemma_isa_split t lits] is the proof of + [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *) + +val lemma_isa_sel : Term.t -> Proof_term.t +(** [lemma_isa_sel (is-c t)] is the proof of + [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *) + +val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t +(** [lemma_isa_disj (is-c t) (is-d t)] is the proof + of [¬ (is-c t) \/ ¬ (is-c t)] *) + +val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t +(** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of + [c t1…tn = c u1…un |- ti = ui] *) + +val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t +(** [lemma_isa_distinct (c …) (d …)] is the proof + of the unit clause [|- (c …) ≠ (d …)] *) + +val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.t +(** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false] + by acyclicity. *) diff --git a/src/th-data/th_intf.ml b/src/th-data/th_intf.ml index e26304da..88369491 100644 --- a/src/th-data/th_intf.ml +++ b/src/th-data/th_intf.ml @@ -9,51 +9,16 @@ type ty = Term.t - ['t] is the representation of terms *) type ('c, 't) data_view = - | T_cstor of 'c * 't array + | T_cstor of 'c * 't list | T_select of 'c * int * 't | T_is_a of 'c * 't | T_other of 't (** View of types in a way that is directly useful for the theory of datatypes *) type ('c, 'ty) data_ty_view = - | Ty_arrow of 'ty Iter.t * 'ty - | Ty_app of { args: 'ty Iter.t } + | Ty_arrow of 'ty list * 'ty | Ty_data of { cstors: 'c } - | Ty_other - -module type PROOF_RULES = sig - val lemma_isa_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t - (** [lemma_isa_cstor (d …) (is-c t)] returns the clause - [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *) - - val lemma_select_cstor : cstor_t:Term.t -> Term.t -> Proof_term.t - (** [lemma_select_cstor (c t1…tn) (sel-c-i t)] - returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *) - - val lemma_isa_split : Term.t -> Lit.t list -> Proof_term.t - (** [lemma_isa_split t lits] is the proof of - [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *) - - val lemma_isa_sel : Term.t -> Proof_term.t - (** [lemma_isa_sel (is-c t)] is the proof of - [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *) - - val lemma_isa_disj : Lit.t -> Lit.t -> Proof_term.t - (** [lemma_isa_disj (is-c t) (is-d t)] is the proof - of [¬ (is-c t) \/ ¬ (is-c t)] *) - - val lemma_cstor_inj : Term.t -> Term.t -> int -> Proof_term.t - (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of - [c t1…tn = c u1…un |- ti = ui] *) - - val lemma_cstor_distinct : Term.t -> Term.t -> Proof_term.t - (** [lemma_isa_distinct (c …) (d …)] is the proof - of the unit clause [|- (c …) ≠ (d …)] *) - - val lemma_acyclicity : (Term.t * Term.t) list -> Proof_term.t - (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false] - by acyclicity. *) -end + | Ty_other of { sub: 'ty list } (* TODO: remove? or make compute_card use that? *) @@ -66,7 +31,7 @@ module type DATA_TY = sig val finite : t -> bool val set_finite : t -> bool -> unit val view : t -> (cstor, t) data_ty_view - val cstor_args : cstor -> t Iter.t + val cstor_args : cstor -> t list end module type ARG = sig @@ -79,20 +44,20 @@ module type ARG = sig type t (** Constructor *) - val ty_args : t -> ty Iter.t + val ty_args : t -> ty list (** Type arguments, for a polymorphic constructor *) include Sidekick_sigs.EQ with type t := t include Sidekick_sigs.PRINT with type t := t end - val as_datatype : ty -> (Cstor.t Iter.t, ty) data_ty_view + val as_datatype : ty -> (Cstor.t list, ty) data_ty_view (** Try to view type as a datatype (with its constructors) *) val view_as_data : Term.t -> (Cstor.t, Term.t) data_view (** Try to view Term.t as a datatype Term.t *) - val mk_cstor : Term.store -> Cstor.t -> Term.t array -> Term.t + val mk_cstor : Term.store -> Cstor.t -> Term.t list -> Term.t (** Make a constructor application Term.t *) val mk_is_a : Term.store -> Cstor.t -> Term.t -> Term.t @@ -110,6 +75,4 @@ module type ARG = sig val ty_set_is_finite : ty -> bool -> unit (** Modify the "finite" field (see {!ty_is_finite}) *) - - module P : PROOF_RULES end