feat lib/mir: add Decl, Db_op, make Db_ser a list of ops

Author: c-cube

src/lib/common/db_op.ml

@@ -0,0 +1,25 @@
+(** Operations that modify {!Db.t}. These can be sent on the network. *)
+type ('term, 'ty) t_poly =
+  | Op_enable of Imandrax_api.Uid.t list
+  | Op_disable of Imandrax_api.Uid.t list
+  | Op_add_decls of ('term, 'ty) Decl.t_poly list
+  | Op_add_rw of 'ty Pattern_head.t_poly * ('term, 'ty) Rewrite_rule.t_poly
+  | Op_add_fc_trigger of 'ty Pattern_head.t_poly * 'ty Trigger.t_poly
+  | Op_add_elim of
+      'ty Pattern_head.t_poly * ('term, 'ty) Elimination_rule.t_poly
+  | Op_add_gen_trigger of 'ty Pattern_head.t_poly * 'ty Trigger.t_poly
+  | Op_add_count_fun of Imandrax_api.Uid.t * ('term, 'ty) Fun_def.t_poly
+  | Op_set_admission of Imandrax_api.Uid.t * Admission.t
+  | Op_set_thm_as_rw of
+      Imandrax_api.Uid.t * ('term, 'ty) Rewrite_rule.t_poly list
+  | Op_set_thm_as_fc of
+      Imandrax_api.Uid.t * ('term, 'ty) Instantiation_rule.t_poly list
+  | Op_set_thm_as_elim of
+      Imandrax_api.Uid.t * ('term, 'ty) Elimination_rule.t_poly list
+  | Op_set_thm_as_gen of
+      Imandrax_api.Uid.t * ('term, 'ty) Instantiation_rule.t_poly
+  | Op_add_instantiation_rule of ('term, 'ty) Instantiation_rule.t_poly
+  | Op_add_rule_spec_fc_triggers of Imandrax_api.Uid.t * 'ty Trigger.t_poly list
+  | Op_add_rule_spec_rw of
+      Imandrax_api.Uid.t * ('term, 'ty) Rewrite_rule.t_poly list
+[@@deriving show { with_path = false }, twine, map, iter]

src/lib/common/db_ser.ml

@@ -1,41 +1,12 @@
 (** A serializable logic database. It contains all relevant context for proof
     obligations. *)
 
-type 'a uid_map = (Imandrax_api.Uid.t * 'a) list
-[@@deriving show, twine, typereg]
-
-type ('ty, 'a) ph_map = ('ty Pattern_head.t_poly * 'a) list
-[@@deriving show, twine, typereg, map, iter]
-
 type 'a ca_ptr = 'a Imandrax_api_ca_store.Ca_ptr.t [@@deriving twine, typereg]
 
 open struct
   let pp_ca_ptr _ out c = Imandrax_api_ca_store.Ca_ptr.pp out c
 end
 
-type ('term, 'ty) t_poly = {
-  cname_decls: Imandrax_api.Uid_set.t;  (** declarations by cname/cptr *)
-  local_tys: 'ty Imandrax_api.Ty_view.def_poly list;
-      (** type declarations included here *)
-  local_funs: ('term, 'ty) Fun_def.t_poly list;
-      (** function declarations included here *)
-  rw_rules: ('ty, ('term, 'ty) Rewrite_rule.t_poly ca_ptr list) ph_map;
-  inst_rules: ('term, 'ty) Instantiation_rule.t_poly ca_ptr uid_map;
-  rule_spec_fc: 'ty Trigger.t_poly ca_ptr list uid_map;
-  rule_spec_rw_rules: ('term, 'ty) Rewrite_rule.t_poly ca_ptr list uid_map;
-  fc: ('ty, 'ty Trigger.t_poly ca_ptr list) ph_map;
-  elim: ('ty, ('term, 'ty) Elimination_rule.t_poly ca_ptr list) ph_map;
-  gen: ('ty, 'ty Trigger.t_poly ca_ptr list) ph_map;
-  thm_as_rw: ('term, 'ty) Rewrite_rule.t_poly ca_ptr list uid_map;
-  thm_as_fc: ('term, 'ty) Instantiation_rule.t_poly ca_ptr list uid_map;
-  thm_as_elim: ('term, 'ty) Elimination_rule.t_poly ca_ptr list uid_map;
-  thm_as_gen: ('term, 'ty) Instantiation_rule.t_poly ca_ptr list uid_map;
-  admission: Admission.t ca_ptr uid_map;
-  count_funs_of_ty: Imandrax_api.Uid.t uid_map;
-      (** Type -> count function for it *)
-  disabled: Imandrax_api.Uid_set.t;
-}
+type ('term, 'ty) t_poly = { ops: ('term, 'ty) Db_op.t_poly ca_ptr list }
 [@@deriving show { with_path = false }, twine, typereg]
 (** A serializable logic database. *)
-
-(* NOTE: this is not deriving map because we can't map through a ca_ptr. *)

src/lib/common/decl.ml

@@ -0,0 +1,7 @@
+type ('term, 'ty) t_poly =
+  | Fun of ('term, 'ty) Fun_def.t_poly
+  | Ty of 'ty Imandrax_api.Ty_view.def_poly
+  | Theorem of ('term, 'ty) Theorem.t_poly
+  | Rule_spec of ('term, 'ty) Rule_spec.t_poly
+  | Verify of ('term, 'ty) Verify.t_poly
+[@@deriving show { with_path = false }, map, iter, twine]

src/lib/common/rule_spec.ml

@@ -0,0 +1,15 @@
+type ('term, 'ty) t_poly = {
+  rule_spec_fc: bool;  (** forward chaining rule? *)
+  rule_spec_rewriting: bool;  (** rewrite rule? *)
+  rule_spec_perm_restrict: bool;
+      (** apply permutative rewrite rule restrictions? *)
+  rule_spec_link: ('term, 'ty) Fun_def.t_poly;
+      (** corresponding (boolean) function *)
+  rule_spec_triggers: 'term Pre_trigger.t_poly list;
+      (** explicit rule triggers *)
+}
+[@@deriving twine, map, iter, show { with_path = false }]
+(** A rule_spec_spec, entered with
+    [rule_spec_spec foo x y = <formula using x,y>] *)
+
+let name self = self.rule_spec_link.f_name

src/lib/common/verify.ml

@@ -0,0 +1,14 @@
+type ('term, 'ty) t_poly = {
+  verify_link: ('term, 'ty) Fun_def.t_poly;
+      (** nameless function representing the property to check *)
+  verify_simplify: bool;  (** simplify first? *)
+  verify_nonlin: bool;  (** nonlinear real arithmetic? *)
+  verify_upto: Imandrax_api.Upto.t option;
+  verify_is_instance: bool;
+  verify_minimize: 'term list;  (** arithmetic terms to minimize in models *)
+  verify_by: ('ty Var.t_poly list * 'term) option;
+}
+[@@deriving twine, iter, map, show { with_path = false }]
+(** A [verify (fun x y -> <formula using x,y>)] event, for nameless theorems. *)
+
+let name self = self.verify_link.f_name