1signature Absyn = 2sig 3 type term = Term.term 4 type pretype = Pretype.pretype 5 type 'a quotation = 'a Portable.quotation 6 7 datatype vstruct = datatype Absyn_dtype.vstruct 8 datatype absyn = datatype Absyn_dtype.absyn 9 10 val locn_of_absyn : absyn -> locn.locn 11 val locn_of_vstruct : vstruct -> locn.locn 12 13 val traverse : (absyn -> bool) -> 14 ((absyn -> absyn) -> (absyn -> absyn)) -> 15 absyn -> absyn 16 17 val to_vstruct : absyn -> vstruct 18 19 val mk_AQ : term -> absyn 20 val mk_ident : string -> absyn 21 val mk_app : absyn * absyn -> absyn 22 val mk_lam : vstruct * absyn -> absyn 23 val mk_typed : absyn * pretype -> absyn 24 25 val mk_eq : absyn * absyn -> absyn 26 val mk_conj : absyn * absyn -> absyn 27 val mk_disj : absyn * absyn -> absyn 28 val mk_imp : absyn * absyn -> absyn 29 val mk_pair : absyn * absyn -> absyn 30 val mk_forall : vstruct * absyn -> absyn 31 val mk_exists : vstruct * absyn -> absyn 32 val mk_exists1 : vstruct * absyn -> absyn 33 val mk_select : vstruct * absyn -> absyn 34 val mk_binder : string -> vstruct * absyn -> absyn 35 36 val dest_AQ : absyn -> term 37 val dest_ident : absyn -> string 38 val dest_app : absyn -> absyn * absyn 39 val dest_lam : absyn -> vstruct * absyn 40 val dest_typed : absyn -> absyn * pretype 41 val dest_eq : absyn -> absyn * absyn 42 val dest_conj : absyn -> absyn * absyn 43 val dest_disj : absyn -> absyn * absyn 44 val dest_imp : absyn -> absyn * absyn 45 val dest_pair : absyn -> absyn * absyn 46 val dest_forall : absyn -> vstruct * absyn 47 val dest_exists : absyn -> vstruct * absyn 48 val dest_exists1 : absyn -> vstruct * absyn 49 val dest_select : absyn -> vstruct * absyn 50 val dest_binder : string -> absyn -> vstruct * absyn 51 val dest_binop : string -> absyn -> absyn * absyn 52 53 val list_mk_app : absyn * absyn list -> absyn 54 val list_mk_lam : vstruct list * absyn -> absyn 55 val list_mk_conj : absyn list -> absyn 56 val list_mk_disj : absyn list -> absyn 57 val list_mk_imp : absyn list -> absyn 58 val list_mk_pair : absyn list -> absyn 59 val list_mk_forall : vstruct list * absyn -> absyn 60 val list_mk_exists : vstruct list * absyn -> absyn 61 val list_mk_exists1 : vstruct list * absyn -> absyn 62 val list_mk_select : vstruct list * absyn -> absyn 63 64 val strip_app : absyn -> absyn * absyn list 65 val strip_lam : absyn -> vstruct list * absyn 66 val strip_conj : absyn -> absyn list 67 val strip_disj : absyn -> absyn list 68 val strip_imp : absyn -> absyn list 69 val strip_pair : absyn -> absyn list 70 val strip_forall : absyn -> vstruct list * absyn 71 val strip_exists : absyn -> vstruct list * absyn 72 val strip_exists1 : absyn -> vstruct list * absyn 73 val strip_select : absyn -> vstruct list * absyn 74 75 val is_ident : absyn -> bool 76 val is_app : absyn -> bool 77 val is_lam : absyn -> bool 78 val is_AQ : absyn -> bool 79 val is_typed : absyn -> bool 80 val is_eq : absyn -> bool 81 val is_conj : absyn -> bool 82 val is_disj : absyn -> bool 83 val is_imp : absyn -> bool 84 val is_pair : absyn -> bool 85 val is_forall : absyn -> bool 86 val is_exists : absyn -> bool 87 val is_exists1 : absyn -> bool 88 val is_select : absyn -> bool 89end 90