author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 58058  1a0b18176548 
permissions  rwrr 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

1 
(* Title: HOL/Library/Old_SMT/old_smt_translate.ML 
36898  2 
Author: Sascha Boehme, TU Muenchen 
3 

4 
Translate theorems into an SMT intermediate format and serialize them. 

5 
*) 

6 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

7 
signature OLD_SMT_TRANSLATE = 
36898  8 
sig 
41123  9 
(*intermediate term structure*) 
36898  10 
datatype squant = SForall  SExists 
11 
datatype 'a spattern = SPat of 'a list  SNoPat of 'a list 

12 
datatype sterm = 

13 
SVar of int  

14 
SApp of string * sterm list  

15 
SLet of string * sterm * sterm  

40664  16 
SQua of squant * string list * sterm spattern list * int option * sterm 
36898  17 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

18 
(*translation configuration*) 
36898  19 
type prefixes = {sort_prefix: string, func_prefix: string} 
20 
type sign = { 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

21 
header: string list, 
36898  22 
sorts: string list, 
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset

23 
dtyps: (string * (string * (string * string) list) list) list list, 
36898  24 
funcs: (string * (string list * string)) list } 
25 
type config = { 

26 
prefixes: prefixes, 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

27 
header: term list > string list, 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
41057
diff
changeset

28 
is_fol: bool, 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
41057
diff
changeset

29 
has_datatypes: bool, 
36898  30 
serialize: string list > sign > sterm list > string } 
31 
type recon = { 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

32 
context: Proof.context, 
36898  33 
typs: typ Symtab.table, 
34 
terms: term Symtab.table, 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

35 
rewrite_rules: thm list, 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset

36 
assms: (int * thm) list } 
36898  37 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

38 
(*translation*) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

39 
val add_config: Old_SMT_Utils.class * (Proof.context > config) > 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

40 
Context.generic > Context.generic 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

41 
val translate: Proof.context > string list > (int * thm) list > 
36898  42 
string * recon 
43 
end 

44 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

45 
structure Old_SMT_Translate: OLD_SMT_TRANSLATE = 
36898  46 
struct 
47 

40663  48 

36898  49 
(* intermediate term structure *) 
50 

51 
datatype squant = SForall  SExists 

52 

53 
datatype 'a spattern = SPat of 'a list  SNoPat of 'a list 

54 

55 
datatype sterm = 

56 
SVar of int  

57 
SApp of string * sterm list  

58 
SLet of string * sterm * sterm  

40664  59 
SQua of squant * string list * sterm spattern list * int option * sterm 
36898  60 

61 

62 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

63 
(* translation configuration *) 
36898  64 

65 
type prefixes = {sort_prefix: string, func_prefix: string} 

66 

67 
type sign = { 

36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

68 
header: string list, 
36898  69 
sorts: string list, 
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset

70 
dtyps: (string * (string * (string * string) list) list) list list, 
36898  71 
funcs: (string * (string list * string)) list } 
72 

73 
type config = { 

74 
prefixes: prefixes, 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

75 
header: term list > string list, 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
41057
diff
changeset

76 
is_fol: bool, 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
41057
diff
changeset

77 
has_datatypes: bool, 
36898  78 
serialize: string list > sign > sterm list > string } 
79 

80 
type recon = { 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

81 
context: Proof.context, 
36898  82 
typs: typ Symtab.table, 
83 
terms: term Symtab.table, 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

84 
rewrite_rules: thm list, 
40161
539d07b00e5f
keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
boehmes
parents:
39535
diff
changeset

85 
assms: (int * thm) list } 
36898  86 

87 

88 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

89 
(* translation context *) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

90 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

91 
fun make_tr_context {sort_prefix, func_prefix} = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

92 
(sort_prefix, 1, Typtab.empty, func_prefix, 1, Termtab.empty) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

93 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

94 
fun string_of_index pre i = pre ^ string_of_int i 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

95 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

96 
fun add_typ T proper (cx as (sp, Tidx, typs, fp, idx, terms)) = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

97 
(case Typtab.lookup typs T of 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

98 
SOME (n, _) => (n, cx) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

99 
 NONE => 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

100 
let 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

101 
val n = string_of_index sp Tidx 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

102 
val typs' = Typtab.update (T, (n, proper)) typs 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

103 
in (n, (sp, Tidx+1, typs', fp, idx, terms)) end) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

104 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

105 
fun add_fun t sort (cx as (sp, Tidx, typs, fp, idx, terms)) = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

106 
(case Termtab.lookup terms t of 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

107 
SOME (n, _) => (n, cx) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

108 
 NONE => 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

109 
let 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

110 
val n = string_of_index fp idx 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

111 
val terms' = Termtab.update (t, (n, sort)) terms 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

112 
in (n, (sp, Tidx, typs, fp, idx+1, terms')) end) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

113 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

114 
fun sign_of header dtyps (_, _, typs, _, _, terms) = { 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

115 
header = header, 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

116 
sorts = Typtab.fold (fn (_, (n, true)) => cons n  _ => I) typs [], 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

117 
dtyps = dtyps, 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

118 
funcs = Termtab.fold (fn (_, (n, SOME ss)) => cons (n,ss)  _ => I) terms []} 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

119 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

120 
fun recon_of ctxt rules thms ithms (_, _, typs, _, _, terms) = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

121 
let 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

122 
fun add_typ (T, (n, _)) = Symtab.update (n, T) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

123 
val typs' = Typtab.fold add_typ typs Symtab.empty 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

124 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

125 
fun add_fun (t, (n, _)) = Symtab.update (n, t) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

126 
val terms' = Termtab.fold add_fun terms Symtab.empty 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

127 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

128 
val assms = map (pair ~1) thms @ ithms 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

129 
in 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

130 
{context=ctxt, typs=typs', terms=terms', rewrite_rules=rules, assms=assms} 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

131 
end 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

132 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

133 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

134 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

135 
(* preprocessing *) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

136 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

137 
(** datatype declarations **) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

138 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

139 
fun collect_datatypes_and_records (tr_context, ctxt) ts = 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

140 
let 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

141 
val (declss, ctxt') = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

142 
fold (Term.fold_types Old_SMT_Datatypes.add_decls) ts ([], ctxt) 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

143 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

144 
fun is_decl_typ T = exists (exists (equal T o fst)) declss 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

145 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

146 
fun add_typ' T proper = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

147 
(case Old_SMT_Builtin.dest_builtin_typ ctxt' T of 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

148 
SOME n => pair n 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

149 
 NONE => add_typ T proper) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

150 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

151 
fun tr_select sel = 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

152 
let val T = Term.range_type (Term.fastype_of sel) 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

153 
in add_fun sel NONE ##>> add_typ' T (not (is_decl_typ T)) end 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

154 
fun tr_constr (constr, selects) = 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

155 
add_fun constr NONE ##>> fold_map tr_select selects 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

156 
fun tr_typ (T, cases) = add_typ' T false ##>> fold_map tr_constr cases 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

157 
val (declss', tr_context') = fold_map (fold_map tr_typ) declss tr_context 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

158 

09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

159 
fun add (constr, selects) = 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

160 
Termtab.update (constr, length selects) #> 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

161 
fold (Termtab.update o rpair 1) selects 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

162 
val funcs = fold (fold (fold add o snd)) declss Termtab.empty 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

163 
in ((funcs, declss', tr_context', ctxt'), ts) end 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

164 
(* FIXME: also return necessary datatype and record theorems *) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

165 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

166 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

167 
(** etaexpand quantifiers, let expressions and builtins *) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

168 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

169 
local 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

170 
fun eta f T t = Abs (Name.uu, T, f (Term.incr_boundvars 1 t $ Bound 0)) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

171 

42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

172 
fun exp f T = eta f (Term.domain_type (Term.domain_type T)) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

173 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

174 
fun exp2 T q = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

175 
let val U = Term.domain_type T 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

176 
in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

177 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

178 
fun exp2' T l = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

179 
let val (U1, U2) = Term.dest_funT T > Term.domain_type 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

180 
in Abs (Name.uu, U1, eta I U2 (l $ Bound 0)) end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

181 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

182 
fun expf k i T t = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

183 
let val Ts = drop i (fst (Old_SMT_Utils.dest_funT k T)) 
41195
f59491d56327
fixed etaexpansion: introduce a couple of abstractions at once
boehmes
parents:
41173
diff
changeset

184 
in 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

185 
Term.incr_boundvars (length Ts) t 
42321
ce83c1654b86
fixed etaexpansion: use correct order to apply new bound variables
boehmes
parents:
42319
diff
changeset

186 
> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts  1) 
41195
f59491d56327
fixed etaexpansion: introduce a couple of abstractions at once
boehmes
parents:
41173
diff
changeset

187 
> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts 
f59491d56327
fixed etaexpansion: introduce a couple of abstractions at once
boehmes
parents:
41173
diff
changeset

188 
end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

189 
in 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

190 

42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

191 
fun eta_expand ctxt is_fol funcs = 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

192 
let 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

193 
fun exp_func t T ts = 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

194 
(case Termtab.lookup funcs t of 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

195 
SOME k => 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

196 
Term.list_comb (t, ts) 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

197 
> k <> length ts ? expf k (length ts) T 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

198 
 NONE => Term.list_comb (t, ts)) 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

199 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

200 
fun expand ((q as Const (@{const_name All}, _)) $ Abs a) = q $ abs_expand a 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

201 
 expand ((q as Const (@{const_name All}, T)) $ t) = q $ exp expand T t 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

202 
 expand (q as Const (@{const_name All}, T)) = exp2 T q 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

203 
 expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

204 
 expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

205 
 expand (q as Const (@{const_name Ex}, T)) = exp2 T q 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

206 
 expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

207 
if is_fol then expand (Term.betapply (Abs a, t)) 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

208 
else l $ expand t $ abs_expand a 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

209 
 expand ((l as Const (@{const_name Let}, T)) $ t $ u) = 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

210 
if is_fol then expand (u $ t) 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

211 
else l $ expand t $ exp expand (Term.range_type T) u 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

212 
 expand ((l as Const (@{const_name Let}, T)) $ t) = 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

213 
if is_fol then 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

214 
let val U = Term.domain_type (Term.range_type T) 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

215 
in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

216 
else exp2 T (l $ expand t) 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

217 
 expand (l as Const (@{const_name Let}, T)) = 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

218 
if is_fol then 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

219 
let val U = Term.domain_type (Term.range_type T) 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

220 
in 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

221 
Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

222 
Bound 0 $ Bound 1)) 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

223 
end 
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

224 
else exp2' T l 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

225 
 expand t = 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

226 
(case Term.strip_comb t of 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

227 
(u as Const (c as (_, T)), ts) => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

228 
(case Old_SMT_Builtin.dest_builtin ctxt c ts of 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

229 
SOME (_, k, us, mk) => 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

230 
if k = length us then mk (map expand us) 
46529
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

231 
else if k < length us then 
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

232 
chop k (map expand us) >> mk > Term.list_comb 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

233 
else expf k (length ts) T (mk (map expand us)) 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

234 
 NONE => exp_func u T (map expand ts)) 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

235 
 (u as Free (_, T), ts) => exp_func u T (map expand ts) 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

236 
 (Abs a, ts) => Term.list_comb (abs_expand a, map expand ts) 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

237 
 (u, ts) => Term.list_comb (u, map expand ts)) 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

238 

679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

239 
and abs_expand (n, T, t) = Abs (n, T, expand t) 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

240 

679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

241 
in map expand end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

242 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

243 
end 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

244 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

245 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

246 
(** introduce explicit applications **) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

247 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

248 
local 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

249 
(* 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

250 
Make application explicit for functions with varying number of arguments. 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

251 
*) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

252 

43154
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

253 
fun add t i = apfst (Termtab.map_default (t, i) (Integer.min i)) 
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

254 
fun add_type T = apsnd (Typtab.update (T, ())) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

255 

41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

256 
fun min_arities t = 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

257 
(case Term.strip_comb t of 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

258 
(u as Const _, ts) => add u (length ts) #> fold min_arities ts 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

259 
 (u as Free _, ts) => add u (length ts) #> fold min_arities ts 
43154
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

260 
 (Abs (_, T, u), ts) => add_type T #> min_arities u #> fold min_arities ts 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

261 
 (_, ts) => fold min_arities ts) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

262 

43154
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

263 
fun minimize types t i = 
43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

264 
let 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

265 
fun find_min j [] _ = j 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

266 
 find_min j (U :: Us) T = 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

267 
if Typtab.defined types T then j 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

268 
else find_min (j + 1) Us (U > T) 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

269 

9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

270 
val (Ts, T) = Term.strip_type (Term.type_of t) 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

271 
in find_min 0 (take i (rev Ts)) T end 
43154
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

272 

41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

273 
fun app u (t, T) = 
58057  274 
(Const (@{const_name fun_app}, T > T) $ t $ u, Term.range_type T) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

275 

41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

276 
fun apply i t T ts = 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41281
diff
changeset

277 
let 
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41281
diff
changeset

278 
val (ts1, ts2) = chop i ts 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

279 
val (_, U) = Old_SMT_Utils.dest_funT i T 
41328
6792a5c92a58
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41281
diff
changeset

280 
in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

281 
in 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

282 

43385
9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

283 
fun intro_explicit_application ctxt funcs ts = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

284 
let 
43154
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

285 
val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty) 
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

286 
val arities' = Termtab.map (minimize types) arities 
43385
9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

287 

9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

288 
fun app_func t T ts = 
9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

289 
if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts) 
9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

290 
else apply (the (Termtab.lookup arities' t)) t T ts 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

291 

43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

292 
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t)) 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

293 

41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

294 
fun traverse Ts t = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

295 
(case Term.strip_comb t of 
43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

296 
(q as Const (@{const_name All}, _), [Abs (x, T, u)]) => 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

297 
q $ Abs (x, T, in_trigger (T :: Ts) u) 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

298 
 (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) => 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

299 
q $ Abs (x, T, in_trigger (T :: Ts) u) 
43929
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

300 
 (q as Const (@{const_name Let}, _), [u1, u2 as Abs _]) => 
43154
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

301 
q $ traverse Ts u1 $ traverse Ts u2 
72e4753a6677
made introduction of explicit application stable under removal of vacuous facts (which only lower the rank of constants but do not participate in the proof)
boehmes
parents:
42321
diff
changeset

302 
 (u as Const (c as (_, T)), ts) => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

303 
(case Old_SMT_Builtin.dest_builtin ctxt c ts of 
46529
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

304 
SOME (_, k, us, mk) => 
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

305 
let 
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

306 
val (ts1, ts2) = chop k (map (traverse Ts) us) 
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

307 
val U = Term.strip_type T >> snd o chop k > (op >) 
a018d542e0ae
corrected treatment of applications of builtin functions to higherorder terms
boehmes
parents:
43932
diff
changeset

308 
in apply 0 (mk ts1) U ts2 end 
43385
9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

309 
 NONE => app_func u T (map (traverse Ts) ts)) 
9cd4b4ecb4dd
slightly more general treatment of mutually recursive datatypes;
boehmes
parents:
43154
diff
changeset

310 
 (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts) 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

311 
 (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts) 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

312 
 (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

313 
 (u, ts) => traverses Ts u ts) 
58057  314 
and in_trigger Ts ((c as @{const trigger}) $ p $ t) = 
43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

315 
c $ in_pats Ts p $ in_weight Ts t 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

316 
 in_trigger Ts t = in_weight Ts t 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

317 
and in_pats Ts ps = 
58057  318 
in_list @{typ "pattern list"} 
319 
(in_list @{typ pattern} (in_pat Ts)) ps 

320 
and in_pat Ts ((p as Const (@{const_name pat}, _)) $ t) = 

43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

321 
p $ traverse Ts t 
58057  322 
 in_pat Ts ((p as Const (@{const_name nopat}, _)) $ t) = 
43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

323 
p $ traverse Ts t 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

324 
 in_pat _ t = raise TERM ("bad pattern", [t]) 
58057  325 
and in_weight Ts ((c as @{const weight}) $ w $ t) = 
43554
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

326 
c $ w $ traverse Ts t 
9bece8cbb5be
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 > T2 > T3 should be considered to have a rank less or equal to 1 if variables of type T2 > T3 occur bound in a problem);
boehmes
parents:
43507
diff
changeset

327 
 in_weight Ts t = traverse Ts t 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

328 
and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts) 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

329 
in map (traverse []) ts end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

330 

58057  331 
val fun_app_eq = mk_meta_eq @{thm fun_app_def} 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

332 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

333 
end 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

334 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

335 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

336 
(** map HOL formulas to FOL formulas (i.e., separate formulas froms terms) **) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

337 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

338 
local 
58057  339 
val term_bool = @{lemma "term_true ~= term_false" 
340 
by (simp add: term_true_def term_false_def)} 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

341 

41785
77dcc197df9a
wrap occurrences of quantifiers in firstorder terms (i.e., outside firstorder formulas) in Ifexpressions
boehmes
parents:
41426
diff
changeset

342 
val is_quant = member (op =) [@{const_name All}, @{const_name Ex}] 
77dcc197df9a
wrap occurrences of quantifiers in firstorder terms (i.e., outside firstorder formulas) in Ifexpressions
boehmes
parents:
41426
diff
changeset

343 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

344 
val fol_rules = [ 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

345 
Let_def, 
58057  346 
mk_meta_eq @{thm term_true_def}, 
347 
mk_meta_eq @{thm term_false_def}, 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

348 
@{lemma "P = True == P" by (rule eq_reflection) simp}, 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

349 
@{lemma "if P then True else False == P" by (rule eq_reflection) simp}] 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

350 

58057  351 
fun as_term t = @{const HOL.eq (bool)} $ t $ @{const term_true} 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

352 

47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

353 
exception BAD_PATTERN of unit 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

354 

5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

355 
fun wrap_in_if pat t = 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

356 
if pat then 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

357 
raise BAD_PATTERN () 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

358 
else 
58057  359 
@{const If (bool)} $ t $ @{const term_true} $ @{const term_false} 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

360 

679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

361 
fun is_builtin_conn_or_pred ctxt c ts = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

362 
is_some (Old_SMT_Builtin.dest_builtin_conn ctxt c ts) orelse 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

363 
is_some (Old_SMT_Builtin.dest_builtin_pred ctxt c ts) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

364 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

365 
fun builtin b ctxt c ts = 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

366 
(case (Const c, ts) of 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

367 
(@{const HOL.eq (bool)}, [t, u]) => 
58057  368 
if t = @{const term_true} orelse u = @{const term_true} then 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

369 
Old_SMT_Builtin.dest_builtin_eq ctxt t u 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

370 
else b ctxt c ts 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

371 
 _ => b ctxt c ts) 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

372 
in 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

373 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

374 
fun folify ctxt = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

375 
let 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

376 
fun in_list T f t = HOLogic.mk_list T (map_filter f (HOLogic.dest_list t)) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

377 

47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

378 
fun in_term pat t = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

379 
(case Term.strip_comb t of 
58057  380 
(@{const True}, []) => @{const term_true} 
381 
 (@{const False}, []) => @{const term_false} 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

382 
 (u as Const (@{const_name If}, _), [t1, t2, t3]) => 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

383 
if pat then raise BAD_PATTERN () 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

384 
else u $ in_form t1 $ in_term pat t2 $ in_term pat t3 
41785
77dcc197df9a
wrap occurrences of quantifiers in firstorder terms (i.e., outside firstorder formulas) in Ifexpressions
boehmes
parents:
41426
diff
changeset

385 
 (Const (c as (n, _)), ts) => 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

386 
if is_builtin_conn_or_pred ctxt c ts then wrap_in_if pat (in_form t) 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

387 
else if is_quant n then wrap_in_if pat (in_form t) 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

388 
else Term.list_comb (Const c, map (in_term pat) ts) 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

389 
 (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

390 
 _ => t) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

391 

58057  392 
and in_weight ((c as @{const weight}) $ w $ t) = c $ w $ in_form t 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

393 
 in_weight t = in_form t 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

394 

58057  395 
and in_pat ((p as Const (@{const_name pat}, _)) $ t) = 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

396 
p $ in_term true t 
58057  397 
 in_pat ((p as Const (@{const_name nopat}, _)) $ t) = 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

398 
p $ in_term true t 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

399 
 in_pat t = raise TERM ("bad pattern", [t]) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

400 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

401 
and in_pats ps = 
58057  402 
in_list @{typ "pattern list"} 
403 
(SOME o in_list @{typ pattern} (try in_pat)) ps 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

404 

58057  405 
and in_trigger ((c as @{const trigger}) $ p $ t) = 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

406 
c $ in_pats p $ in_weight t 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

407 
 in_trigger t = in_weight t 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

408 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

409 
and in_form t = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

410 
(case Term.strip_comb t of 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

411 
(q as Const (qn, _), [Abs (n, T, u)]) => 
41785
77dcc197df9a
wrap occurrences of quantifiers in firstorder terms (i.e., outside firstorder formulas) in Ifexpressions
boehmes
parents:
41426
diff
changeset

412 
if is_quant qn then q $ Abs (n, T, in_trigger u) 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

413 
else as_term (in_term false t) 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

414 
 (Const c, ts) => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

415 
(case Old_SMT_Builtin.dest_builtin_conn ctxt c ts of 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

416 
SOME (_, _, us, mk) => mk (map in_form us) 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

417 
 NONE => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

418 
(case Old_SMT_Builtin.dest_builtin_pred ctxt c ts of 
47533
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

419 
SOME (_, _, us, mk) => mk (map (in_term false) us) 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

420 
 NONE => as_term (in_term false t))) 
5afe54e05406
avoid generating syntactically invalid patterns (with "if_then_else") in SMTLIB files
blanchet
parents:
46529
diff
changeset

421 
 _ => as_term (in_term false t)) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

422 
in 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

423 
map in_form #> 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

424 
cons (Old_SMT_Utils.prop_of term_bool) #> 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

425 
pair (fol_rules, [term_bool], builtin) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

426 
end 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

427 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

428 
end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

429 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

430 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

431 
(* translation into intermediate format *) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

432 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

433 
(** utility functions **) 
36898  434 

435 
val quantifier = (fn 

436 
@{const_name All} => SOME SForall 

437 
 @{const_name Ex} => SOME SExists 

438 
 _ => NONE) 

439 

440 
fun group_quant qname Ts (t as Const (q, _) $ Abs (_, T, u)) = 

441 
if q = qname then group_quant qname (T :: Ts) u else (Ts, t) 

442 
 group_quant _ Ts t = (Ts, t) 

443 

58057  444 
fun dest_weight (@{const weight} $ w $ t) = 
41173
7c6178d45cc8
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents:
41172
diff
changeset

445 
(SOME (snd (HOLogic.dest_number w)), t) 
40664  446 
 dest_weight t = (NONE, t) 
447 

58057  448 
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true) 
449 
 dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false) 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

450 
 dest_pat t = raise TERM ("bad pattern", [t]) 
37124  451 

452 
fun dest_pats [] = I 

453 
 dest_pats ts = 

454 
(case map dest_pat ts > split_list > distinct (op =) of 

455 
(ps, [true]) => cons (SPat ps) 

456 
 (ps, [false]) => cons (SNoPat ps) 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

457 
 _ => raise TERM ("bad multipattern", ts)) 
36898  458 

58057  459 
fun dest_trigger (@{const trigger} $ tl $ t) = 
37124  460 
(rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t) 
36898  461 
 dest_trigger t = ([], t) 
462 

463 
fun dest_quant qn T t = quantifier qn > Option.map (fn q => 

464 
let 

465 
val (Ts, u) = group_quant qn [T] t 

40664  466 
val (ps, p) = dest_trigger u 
467 
val (w, b) = dest_weight p 

468 
in (q, rev Ts, ps, w, b) end) 

36898  469 

470 
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat 

471 
 fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat 

472 

473 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

474 
(** translation from Isabelle terms into SMT intermediate terms **) 
36898  475 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

476 
fun intermediate header dtyps builtin ctxt ts trx = 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
41057
diff
changeset

477 
let 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

478 
fun transT (T as TFree _) = add_typ T true 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

479 
 transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], [])) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

480 
 transT (T as Type _) = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

481 
(case Old_SMT_Builtin.dest_builtin_typ ctxt T of 
39298
5aefb5bc8a93
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
boehmes
parents:
37124
diff
changeset

482 
SOME n => pair n 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

483 
 NONE => add_typ T true) 
36898  484 

485 
fun app n ts = SApp (n, ts) 

486 

487 
fun trans t = 

488 
(case Term.strip_comb t of 

489 
(Const (qn, _), [Abs (_, T, t1)]) => 

490 
(case dest_quant qn T t1 of 

40664  491 
SOME (q, Ts, ps, w, b) => 
36898  492 
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>> 
40664  493 
trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b')) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

494 
 NONE => raise TERM ("unsupported quantifier", [t])) 
36898  495 
 (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) => 
496 
transT T ##>> trans t1 ##>> trans t2 #>> 

497 
(fn ((U, u1), u2) => SLet (U, u1, u2)) 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

498 
 (u as Const (c as (_, T)), ts) => 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

499 
(case builtin ctxt c ts of 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

500 
SOME (n, _, us, _) => fold_map trans us #>> app n 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

501 
 NONE => transs u T ts) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

502 
 (u as Free (_, T), ts) => transs u T ts 
36898  503 
 (Bound i, []) => pair (SVar i) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

504 
 _ => raise TERM ("bad SMT term", [t])) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

505 

36898  506 
and transs t T ts = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

507 
let val (Us, U) = Old_SMT_Utils.dest_funT (length ts) T 
36898  508 
in 
509 
fold_map transT Us ##>> transT U #> (fn Up => 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

510 
add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp) 
36898  511 
end 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

512 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

513 
val (us, trx') = fold_map trans ts trx 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

514 
in ((sign_of (header ts) dtyps trx', us), trx') end 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

515 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

516 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

517 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

518 
(* translation *) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

519 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

520 
structure Configs = Generic_Data 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

521 
( 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

522 
type T = (Proof.context > config) Old_SMT_Utils.dict 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

523 
val empty = [] 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

524 
val extend = I 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

525 
fun merge data = Old_SMT_Utils.dict_merge fst data 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

526 
) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

527 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

528 
fun add_config (cs, cfg) = Configs.map (Old_SMT_Utils.dict_update (cs, cfg)) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

529 

41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

530 
fun get_config ctxt = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

531 
let val cs = Old_SMT_Config.solver_class_of ctxt 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

532 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

533 
(case Old_SMT_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

534 
SOME cfg => cfg ctxt 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

535 
 NONE => error ("SMT: no translation configuration found " ^ 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

536 
"for solver class " ^ quote (Old_SMT_Utils.string_of_class cs))) 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

537 
end 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

538 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

539 
fun translate ctxt comments ithms = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

540 
let 
41232
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

541 
val {prefixes, is_fol, header, has_datatypes, serialize} = get_config ctxt 
4ea9f2a8c093
fixed lambdalifting: shift indices of bound variables correctly (after locking the required bound variables) and apply bound variables to the new function symbol in the right order;
boehmes
parents:
41198
diff
changeset

542 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

543 
val with_datatypes = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

544 
has_datatypes andalso Config.get ctxt Old_SMT_Config.datatypes 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

545 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

546 
fun no_dtyps (tr_context, ctxt) ts = 
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

547 
((Termtab.empty, [], tr_context, ctxt), ts) 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

548 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

549 
val ts1 = map (Envir.beta_eta_contract o Old_SMT_Utils.prop_of o snd) ithms 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

550 

41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41328
diff
changeset

551 
val ((funcs, dtyps, tr_context, ctxt1), ts2) = 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

552 
((make_tr_context prefixes, ctxt), ts1) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

553 
> (if with_datatypes then collect_datatypes_and_records else no_dtyps) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

554 

43929
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

555 
fun is_binder (Const (@{const_name Let}, _) $ _) = true 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

556 
 is_binder t = Lambda_Lifting.is_quantifier t 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

557 

61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

558 
fun mk_trigger ((q as Const (@{const_name All}, _)) $ Abs (n, T, t)) = 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

559 
q $ Abs (n, T, mk_trigger t) 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

560 
 mk_trigger (eq as (Const (@{const_name HOL.eq}, T) $ lhs $ _)) = 
58057  561 
Term.domain_type T > @{typ pattern} 
562 
> (fn T => Const (@{const_name pat}, T) $ lhs) 

563 
> HOLogic.mk_list @{typ pattern} o single 

564 
> HOLogic.mk_list @{typ "pattern list"} o single 

565 
> (fn t => @{const trigger} $ t $ eq) 

43929
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

566 
 mk_trigger t = t 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

567 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

568 
val (ctxt2, ts3) = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

569 
ts2 
42319
9a8ba59aed06
unfold and etacontract let expressions before lambdalifting to avoid bad terms
boehmes
parents:
41785
diff
changeset

570 
> eta_expand ctxt1 is_fol funcs 
43929
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

571 
> rpair ctxt1 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

572 
> Lambda_Lifting.lift_lambdas NONE is_binder 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

573 
> (fn (ts', defs) => fn ctxt' => 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

574 
map mk_trigger defs @ ts' 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

575 
> intro_explicit_application ctxt' funcs 
61d432e51aff
generalized lambdalifting such that it is less specifically tailored for SMT (it does not anymore dependent on any SMTspecific code)
boehmes
parents:
43928
diff
changeset

576 
> pair ctxt') 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

577 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

578 
val ((rewrite_rules, extra_thms, builtin), ts4) = 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

579 
(if is_fol then folify ctxt2 else pair ([], [], I)) ts3 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

580 

2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

581 
val rewrite_rules' = fun_app_eq :: rewrite_rules 
36898  582 
in 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

583 
(ts4, tr_context) 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

584 
> intermediate header dtyps (builtin Old_SMT_Builtin.dest_builtin) ctxt2 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41123
diff
changeset

585 
>> uncurry (serialize comments) 
41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41250
diff
changeset

586 
> recon_of ctxt2 rewrite_rules' extra_thms ithms 
36898  587 
end 
588 

589 
end 