ETCSprover/term.sig at master · u5943321/ETCSprover · GitHub

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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
signature term =
sig
eqtype sort
eqtype term

datatype sort_view =
         vo
         | va of term * term

datatype term_view =
    vVar of string * sort
  | vB of int
  | vFun of string * sort * term list

val view_sort: sort -> sort_view
val view_term: term -> (*term*) term_view


val eq_term: term * term -> bool
val eq_sort: sort * sort -> bool

exception TER of string * sort list * term list

val mk_ob_sort: sort
val mk_ar_sort: term -> term -> sort

val mk_var: string -> sort -> term
val var: string * sort -> term
val mk_fun: string -> term list -> term
val mk_bound: int -> term

val sort_of: term -> sort

val mk_ob: string -> term
val mk_ar:string -> term -> term -> term
val mk_ar0: string -> string -> string -> term

val mk_const: string -> sort -> term

val is_var: term -> bool

val dest_fun: term -> string * sort * term list
val dest_var: term -> string * sort
val dest_ar: sort -> term * term

(*
val dest_pair: term -> term * term
val dest_o: term -> term * term
*)


val one: term
val s: term
val z: term
val zero: term
val N: term

(*
val to1: term -> term
val tp: term -> term
val id: term -> term

val p1: term -> term -> term
val p2: term -> term -> term
val pa: term -> term -> term
val po: term -> term -> term
val i1: term -> term -> term
val i2: term -> term -> term

val O: term * term -> term
val cod: sort -> term
val coeqa: term -> term -> term
val coeqo: term -> term -> term
val copa: term -> term -> term
val copo: term -> term -> term
*)

val replaces: term * term -> sort -> sort
val replacet: term * term -> term -> term

val substs: (string * sort) * term -> sort -> sort
val substt: (string * sort) * term -> term -> term

val fvt: term -> (string * sort) set
val fvtl: term list -> (string * sort) set
val fvs: sort -> (string * sort) set

val pair_compare: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
val sort_compare: sort * sort -> order
val term_compare: term * term -> order
val essps: (string * sort) set
val pvariantt: (string * sort) set -> term -> term

val fsymss: sort -> string set
val fsymst: term -> string set

(*
datatype ForP = fsym | psym
*)

val fxty: string -> int
val is_const: string -> bool

(*
val fpdict: (string, ForP) Binarymap.dict ref
val fpdict0: (string, ForP) Binarymap.dict

val insert_fsym: string -> unit
val insert_psym: string -> unit
*)

type fsymd = (string, sort * (string * sort) list) Binarymap.dict
val fsyms0: fsymd
val fsyms: fsymd ref
val lookup_fun: fsymd -> string -> (sort * (string * sort) list) option
val is_fun: string -> bool
val new_fun:
   string -> sort * (string * sort) list -> unit


type psymd = (string, (string * sort) list) Binarymap.dict
val psyms0: psymd
val psyms: psymd ref
val lookup_pred: psymd -> string -> (string * sort) list option
val is_pred: string -> bool
val new_pred:
   string -> (string * sort) list -> unit

type vd
val emptyvd:vd
val mk_tenv: ((string * sort) * term) list -> vd
val v2t: string * sort -> term -> vd -> vd
val lookup_t: vd -> string * sort -> term option
val match_term: (string * sort) set -> term -> term -> vd -> vd
val match_sort: (string * sort) set -> sort -> sort -> vd -> vd
val match_tl: (string * sort) set -> term list -> term list -> vd -> vd
val pvd: vd -> ((string * sort) * term) list

val inst_sort: vd -> sort -> sort
val inst_term: vd -> term -> term

val ill_formed_fv: string * sort -> bool

val ob_sort: sort
val ar_sort: term -> term -> sort

end