1 (* Title: TFL/usyntax |
1 (* Title: TFL/usyntax.sml |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
3 Author: Konrad Slind, Cambridge University Computer Laboratory |
4 Copyright 1997 University of Cambridge |
4 Copyright 1997 University of Cambridge |
5 |
5 |
6 Emulation of HOL's abstract syntax functions |
6 Emulation of HOL's abstract syntax functions. |
7 *) |
7 *) |
|
8 |
|
9 signature USyntax_sig = |
|
10 sig |
|
11 structure Utils : Utils_sig |
|
12 |
|
13 datatype lambda = VAR of {Name : string, Ty : typ} |
|
14 | CONST of {Name : string, Ty : typ} |
|
15 | COMB of {Rator: term, Rand : term} |
|
16 | LAMB of {Bvar : term, Body : term} |
|
17 |
|
18 val alpha : typ |
|
19 |
|
20 (* Types *) |
|
21 val type_vars : typ -> typ list |
|
22 val type_varsl : typ list -> typ list |
|
23 val mk_vartype : string -> typ |
|
24 val is_vartype : typ -> bool |
|
25 val strip_prod_type : typ -> typ list |
|
26 |
|
27 (* Terms *) |
|
28 val free_vars_lr : term -> term list |
|
29 val type_vars_in_term : term -> typ list |
|
30 val dest_term : term -> lambda |
|
31 |
|
32 (* Prelogic *) |
|
33 val inst : (typ*typ) list -> term -> term |
|
34 |
|
35 (* Construction routines *) |
|
36 val mk_abs :{Bvar : term, Body : term} -> term |
|
37 |
|
38 val mk_imp :{ant : term, conseq : term} -> term |
|
39 val mk_select :{Bvar : term, Body : term} -> term |
|
40 val mk_forall :{Bvar : term, Body : term} -> term |
|
41 val mk_exists :{Bvar : term, Body : term} -> term |
|
42 val mk_conj :{conj1 : term, conj2 : term} -> term |
|
43 val mk_disj :{disj1 : term, disj2 : term} -> term |
|
44 val mk_pabs :{varstruct : term, body : term} -> term |
|
45 |
|
46 (* Destruction routines *) |
|
47 val dest_const: term -> {Name : string, Ty : typ} |
|
48 val dest_comb : term -> {Rator : term, Rand : term} |
|
49 val dest_abs : term -> {Bvar : term, Body : term} |
|
50 val dest_eq : term -> {lhs : term, rhs : term} |
|
51 val dest_imp : term -> {ant : term, conseq : term} |
|
52 val dest_forall : term -> {Bvar : term, Body : term} |
|
53 val dest_exists : term -> {Bvar : term, Body : term} |
|
54 val dest_neg : term -> term |
|
55 val dest_conj : term -> {conj1 : term, conj2 : term} |
|
56 val dest_disj : term -> {disj1 : term, disj2 : term} |
|
57 val dest_pair : term -> {fst : term, snd : term} |
|
58 val dest_pabs : term -> {varstruct : term, body : term} |
|
59 |
|
60 val lhs : term -> term |
|
61 val rhs : term -> term |
|
62 val rand : term -> term |
|
63 |
|
64 (* Query routines *) |
|
65 val is_imp : term -> bool |
|
66 val is_forall : term -> bool |
|
67 val is_exists : term -> bool |
|
68 val is_neg : term -> bool |
|
69 val is_conj : term -> bool |
|
70 val is_disj : term -> bool |
|
71 val is_pair : term -> bool |
|
72 val is_pabs : term -> bool |
|
73 |
|
74 (* Construction of a term from a list of Preterms *) |
|
75 val list_mk_abs : (term list * term) -> term |
|
76 val list_mk_imp : (term list * term) -> term |
|
77 val list_mk_forall : (term list * term) -> term |
|
78 val list_mk_conj : term list -> term |
|
79 |
|
80 (* Destructing a term to a list of Preterms *) |
|
81 val strip_comb : term -> (term * term list) |
|
82 val strip_abs : term -> (term list * term) |
|
83 val strip_imp : term -> (term list * term) |
|
84 val strip_forall : term -> (term list * term) |
|
85 val strip_exists : term -> (term list * term) |
|
86 val strip_disj : term -> term list |
|
87 |
|
88 (* Miscellaneous *) |
|
89 val mk_vstruct : typ -> term list -> term |
|
90 val gen_all : term -> term |
|
91 val find_term : (term -> bool) -> term -> term option |
|
92 val dest_relation : term -> term * term * term |
|
93 val is_WFR : term -> bool |
|
94 val ARB : typ -> term |
|
95 end; |
|
96 |
8 |
97 |
9 structure USyntax : USyntax_sig = |
98 structure USyntax : USyntax_sig = |
10 struct |
99 struct |
11 |
100 |
12 structure Utils = Utils; |
101 structure Utils = Utils; |