blob: 0bc42010d1f1fb4e0b9409d617fe3e7c312b3f2a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
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'
|
