1 files changed, 110 insertions, 0 deletions
diff --git a/contrib/jprover/jterm.mli b/contrib/jprover/jterm.mli
new file mode 100644
index 00000000..0bc42010
--- /dev/null
+++ b/contrib/jprover/jterm.mli
@@ -0,0 +1,110 @@
+(* This module is modified and extracted from Meta-Prl. *)
+
+(* Definitions of [jterm]: *)
+type param = param'
+and operator = operator'
+and term = term'
+and bound_term = bound_term'
+and param' =
+  | Number of int
+  | String of string
+  | Token of string
+  | Var of string
+  | ParamList of param list
+and operator' = { op_name : Opname.opname; op_params : param list; } 
+and term' = { term_op : operator; term_terms : bound_term list; } 
+and bound_term' = { bvars : string list; bterm : term; } 
+type term_subst = (string * term) list
+
+type error_msg = TermMatchError of term * string | StringError of string
+
+exception RefineError of string * error_msg
+
+(* Collect free variables: *)
+val free_vars_list : term -> string list
+
+(* Substitutions: *)
+val subst_term : term list -> string list list -> string list -> term -> term
+val subst : term -> string list -> term list -> term
+val subst1 : term -> string -> term -> term
+val var_subst : term -> term -> string -> term
+val apply_subst : term -> (string * term) list -> term
+
+(* Unification: *)
+val unify_mm : term -> term -> 'a -> (string * term) list
+
+val xnil_term : term'
+
+(* Testing functions: *)
+val is_xnil_term : term' -> bool
+val is_var_term : term' -> bool
+val is_true_term : term' -> bool
+val is_false_term : term' -> bool
+val is_all_term : term' -> bool
+val is_exists_term : term' -> bool
+val is_or_term : term' -> bool
+val is_and_term : term' -> bool
+val is_cor_term : term' -> bool
+val is_cand_term : term' -> bool
+val is_implies_term : term' -> bool
+val is_iff_term : term' -> bool
+val is_not_term : term' -> bool
+val is_fun_term : term -> bool
+val is_const_term : term -> bool
+
+
+(* Constructors for [jterms]: *)
+val var_ : string -> term'
+val fun_ : string -> term list -> term'
+val const_ : string -> term'
+val pred_ : string -> term list -> term'
+val not_ : term -> term'
+val and_ : term -> term -> term'
+val or_ : term -> term -> term'
+val imp_ : term -> term -> term'
+val cand_ : term -> term -> term'
+val cor_ : term -> term -> term'
+val iff_ : term -> term -> term'
+val false_ : term'
+val true_ : term'
+val nil_term : term'
+val forall : string -> term -> term'
+val exists : string -> term -> term'
+
+
+(* Destructors for [jterm]: *)
+val dest_var : term -> string
+val dest_fun : term -> string * term list
+val dest_const : term -> string
+val dest_not : term -> term
+val dest_iff : term -> term * term
+val dest_implies : term -> term * term
+val dest_cand : term -> term * term
+val dest_cor : term -> term * term
+val dest_and : term -> term * term
+val dest_or : term -> term * term
+val dest_exists : term -> string * term * term
+val dest_all : term -> string * term * term
+
+(* Wide-logical connectives: *)
+val wand_ : term list -> term
+val wor_ : term list -> term
+val wimp_ : term list -> term
+
+(* Printing and debugging tools: *)
+val fprint_str_list : out_channel -> string list -> unit
+val mbreak : string -> unit
+val print_strs : string list -> unit
+val print_term : out_channel -> term -> unit
+val print_error_msg : exn -> unit
+
+(* Other exported functions for [jall.ml]: *)
+val make_term : 'a -> 'a
+val dest_term : 'a -> 'a
+val make_op : 'a -> 'a
+val dest_op : 'a -> 'a
+val make_bterm : 'a -> 'a
+val dest_bterm : 'a -> 'a
+val dest_param : 'a -> 'a
+val mk_var_term : string -> term'
+val mk_string_term : Opname.opname -> string -> term'