author  wenzelm 
Sun, 07 Feb 2021 21:25:21 +0100  
changeset 73233  4d36070bdbf4 
parent 70308  7f568724d67e 
child 73235  4e631963fe24 
permissions  rwrr 
38073  1 
(* Title: HOL/Tools/Predicate_Compile/code_prolog.ML 
2 
Author: Lukas Bulwahn, TU Muenchen 

3 

41941  4 
Prototype of an code generator for logic programming languages 
5 
(a.k.a. Prolog). 

38073  6 
*) 
7 

8 
signature CODE_PROLOG = 

9 
sig 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

10 
type code_options = 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

11 
{ensure_groundness : bool, 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

12 
limit_globally : int option, 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

13 
limited_types : (typ * int) list, 
38959
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

14 
limited_predicates : (string list * int) list, 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

15 
replacing : ((string * string) * string) list, 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

16 
manual_reorder : ((string * int) * int list) list} 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

17 
val set_ensure_groundness : code_options > code_options 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

18 
val map_limit_predicates : ((string list * int) list > (string list * int) list) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

19 
> code_options > code_options 
55437  20 
val code_options_of : theory > code_options 
38950
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

21 
val map_code_options : (code_options > code_options) > theory > theory 
55437  22 

59156  23 
val prolog_system: string Config.T 
24 
val prolog_timeout: real Config.T 

25 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

26 
datatype arith_op = Plus  Minus 
38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

27 
datatype prol_term = Var of string  Cons of string  AppF of string * prol_term list 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

28 
 Number of int  ArithOp of arith_op * prol_term list; 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

29 
datatype prem = Conj of prem list 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

30 
 Rel of string * prol_term list  NotRel of string * prol_term list 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

31 
 Eq of prol_term * prol_term  NotEq of prol_term * prol_term 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

32 
 ArithEq of prol_term * prol_term  NotArithEq of prol_term * prol_term 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

33 
 Ground of string * typ; 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

34 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

35 
type clause = ((string * prol_term list) * prem); 
38073  36 
type logic_program = clause list; 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

37 
type constant_table = (string * string) list 
55437  38 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

39 
val generate : Predicate_Compile_Aux.mode option * bool > 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

40 
Proof.context > string > (logic_program * constant_table) 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

41 
val write_program : logic_program > string 
59156  42 
val run : Proof.context > logic_program > (string * prol_term list) > 
43885  43 
string list > int option > prol_term list list 
55437  44 

43885  45 
val active : bool Config.T 
46 
val test_goals : 

45442  47 
Proof.context > bool > (string * typ) list > (term * term list) list > 
43885  48 
Quickcheck.result list 
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

49 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

50 
val trace : bool Unsynchronized.ref 
55437  51 

38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

52 
val replace : ((string * string) * string) > logic_program > logic_program 
38073  53 
end; 
54 

55 
structure Code_Prolog : CODE_PROLOG = 

56 
struct 

57 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

58 
(* diagnostic tracing *) 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

59 

7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

60 
val trace = Unsynchronized.ref false 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

61 

55437  62 
fun tracing s = if !trace then Output.tracing s else () 
63 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

64 

c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

65 
(* code generation options *) 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

66 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

67 
type code_options = 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

68 
{ensure_groundness : bool, 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

69 
limit_globally : int option, 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

70 
limited_types : (typ * int) list, 
38959
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

71 
limited_predicates : (string list * int) list, 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

72 
replacing : ((string * string) * string) list, 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

73 
manual_reorder : ((string * int) * int list) list} 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

74 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

75 

39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

76 
fun set_ensure_groundness {ensure_groundness, limit_globally, limited_types, limited_predicates, 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

77 
replacing, manual_reorder} = 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

78 
{ensure_groundness = true, limit_globally = limit_globally, limited_types = limited_types, 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

79 
limited_predicates = limited_predicates, replacing = replacing, 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

80 
manual_reorder = manual_reorder} 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

81 

39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

82 
fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates, 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

83 
replacing, manual_reorder} = 
55437  84 
{ensure_groundness = ensure_groundness, limit_globally = limit_globally, 
85 
limited_types = limited_types, limited_predicates = f limited_predicates, 

86 
replacing = replacing, manual_reorder = manual_reorder} 

39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

87 

9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

88 
fun merge_global_limit (NONE, NONE) = NONE 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

89 
 merge_global_limit (NONE, SOME n) = SOME n 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

90 
 merge_global_limit (SOME n, NONE) = SOME n 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41307
diff
changeset

91 
 merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m)) (* FIXME odd merge *) 
55437  92 

38950
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

93 
structure Options = Theory_Data 
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

94 
( 
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

95 
type T = code_options 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

96 
val empty = {ensure_groundness = false, limit_globally = NONE, 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

97 
limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []} 
38950
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

98 
val extend = I; 
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

99 
fun merge 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

100 
({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1, 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

101 
limited_types = limited_types1, limited_predicates = limited_predicates1, 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

102 
replacing = replacing1, manual_reorder = manual_reorder1}, 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

103 
{ensure_groundness = ensure_groundness2, limit_globally = limit_globally2, 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

104 
limited_types = limited_types2, limited_predicates = limited_predicates2, 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

105 
replacing = replacing2, manual_reorder = manual_reorder2}) = 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41307
diff
changeset

106 
{ensure_groundness = ensure_groundness1 orelse ensure_groundness2 (* FIXME odd merge *), 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

107 
limit_globally = merge_global_limit (limit_globally1, limit_globally2), 
38950
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

108 
limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2), 
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

109 
limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2), 
38960
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

110 
manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2), 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

111 
replacing = Library.merge (op =) (replacing1, replacing2)}; 
38950
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

112 
); 
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

113 

62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

114 
val code_options_of = Options.get 
62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

115 

62578950e748
storing options for prolog code generation in the theory
bulwahn
parents:
38948
diff
changeset

116 
val map_code_options = Options.map 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

117 

55437  118 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

119 
(* system configuration *) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

120 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

121 
datatype prolog_system = SWI_PROLOG  YAP 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

122 

39462
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

123 
fun string_of_system SWI_PROLOG = "swiprolog" 
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

124 
 string_of_system YAP = "yap" 
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

125 

69593  126 
val prolog_system = Attrib.setup_config_string \<^binding>\<open>prolog_system\<close> (K "swiprolog") 
55437  127 

59156  128 
fun get_prolog_system ctxt = 
129 
(case Config.get ctxt prolog_system of 

130 
"swiprolog" => SWI_PROLOG 

131 
 "yap" => YAP 

132 
 name => error ("Bad prolog system: " ^ quote name ^ " (\"swiprolog\" or \"yap\" expected)")) 

133 

134 

69593  135 
val prolog_timeout = Attrib.setup_config_real \<^binding>\<open>prolog_timeout\<close> (K 10.0) 
59156  136 

137 
fun get_prolog_timeout ctxt = seconds (Config.get ctxt prolog_timeout) 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

138 

55437  139 

38073  140 
(* internal program representation *) 
141 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

142 
datatype arith_op = Plus  Minus 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

143 

38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

144 
datatype prol_term = Var of string  Cons of string  AppF of string * prol_term list 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

145 
 Number of int  ArithOp of arith_op * prol_term list; 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

146 

38735  147 
fun dest_Var (Var v) = v 
148 

149 
fun add_vars (Var v) = insert (op =) v 

150 
 add_vars (ArithOp (_, ts)) = fold add_vars ts 

151 
 add_vars (AppF (_, ts)) = fold add_vars ts 

152 
 add_vars _ = I 

153 

154 
fun map_vars f (Var v) = Var (f v) 

155 
 map_vars f (ArithOp (opr, ts)) = ArithOp (opr, map (map_vars f) ts) 

156 
 map_vars f (AppF (fs, ts)) = AppF (fs, map (map_vars f) ts) 

157 
 map_vars f t = t 

55437  158 

38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

159 
fun maybe_AppF (c, []) = Cons c 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

160 
 maybe_AppF (c, xs) = AppF (c, xs) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

161 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

162 
fun is_Var (Var _) = true 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

163 
 is_Var _ = false 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

164 

81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

165 
fun is_arith_term (Var _) = true 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

166 
 is_arith_term (Number _) = true 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

167 
 is_arith_term (ArithOp (_, operands)) = forall is_arith_term operands 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

168 
 is_arith_term _ = false 
38073  169 

38081
8b02ce312893
removing pointless type information in internal prolog terms
bulwahn
parents:
38080
diff
changeset

170 
fun string_of_prol_term (Var s) = "Var " ^ s 
38075  171 
 string_of_prol_term (Cons s) = "Cons " ^ s 
55437  172 
 string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

173 
 string_of_prol_term (Number n) = "Number " ^ string_of_int n 
38075  174 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

175 
datatype prem = Conj of prem list 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

176 
 Rel of string * prol_term list  NotRel of string * prol_term list 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

177 
 Eq of prol_term * prol_term  NotEq of prol_term * prol_term 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

178 
 ArithEq of prol_term * prol_term  NotArithEq of prol_term * prol_term 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

179 
 Ground of string * typ; 
38735  180 

38073  181 
fun dest_Rel (Rel (c, ts)) = (c, ts) 
38735  182 

183 
fun map_term_prem f (Conj prems) = Conj (map (map_term_prem f) prems) 

184 
 map_term_prem f (Rel (r, ts)) = Rel (r, map f ts) 

185 
 map_term_prem f (NotRel (r, ts)) = NotRel (r, map f ts) 

186 
 map_term_prem f (Eq (l, r)) = Eq (f l, f r) 

187 
 map_term_prem f (NotEq (l, r)) = NotEq (f l, f r) 

188 
 map_term_prem f (ArithEq (l, r)) = ArithEq (f l, f r) 

189 
 map_term_prem f (NotArithEq (l, r)) = NotArithEq (f l, f r) 

190 
 map_term_prem f (Ground (v, T)) = Ground (dest_Var (f (Var v)), T) 

191 

192 
fun fold_prem_terms f (Conj prems) = fold (fold_prem_terms f) prems 

193 
 fold_prem_terms f (Rel (_, ts)) = fold f ts 

194 
 fold_prem_terms f (NotRel (_, ts)) = fold f ts 

195 
 fold_prem_terms f (Eq (l, r)) = f l #> f r 

196 
 fold_prem_terms f (NotEq (l, r)) = f l #> f r 

197 
 fold_prem_terms f (ArithEq (l, r)) = f l #> f r 

198 
 fold_prem_terms f (NotArithEq (l, r)) = f l #> f r 

199 
 fold_prem_terms f (Ground (v, T)) = f (Var v) 

55437  200 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

201 
type clause = ((string * prol_term list) * prem); 
38073  202 

203 
type logic_program = clause list; 

55437  204 

205 

38073  206 
(* translation from introduction rules to internal representation *) 
207 

38958
08eb0ffa2413
improving clashfree naming of variables and preds in code_prolog
bulwahn
parents:
38956
diff
changeset

208 
fun mk_conform f empty avoid name = 
38956  209 
let 
210 
fun dest_Char (Symbol.Char c) = c 

211 
val name' = space_implode "" (map (dest_Char o Symbol.decode) 

212 
(filter (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) 

213 
(Symbol.explode name))) 

38958
08eb0ffa2413
improving clashfree naming of variables and preds in code_prolog
bulwahn
parents:
38956
diff
changeset

214 
val name'' = f (if name' = "" then empty else name') 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
42489
diff
changeset

215 
in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end 
38956  216 

55437  217 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

218 
(** constant table **) 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

219 

7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

220 
type constant_table = (string * string) list 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

221 

7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

222 
fun declare_consts consts constant_table = 
38956  223 
let 
224 
fun update' c table = 

225 
if AList.defined (op =) table c then table else 

226 
let 

56812  227 
val c' = mk_conform (Name.enforce_case false) "pred" (map snd table) (Long_Name.base_name c) 
38956  228 
in 
229 
AList.update (op =) (c, c') table 

230 
end 

231 
in 

232 
fold update' consts constant_table 

233 
end 

55437  234 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

235 
fun translate_const constant_table c = 
55437  236 
(case AList.lookup (op =) constant_table c of 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

237 
SOME c' => c' 
55437  238 
 NONE => error ("No such constant: " ^ c)) 
38073  239 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

240 
fun inv_lookup _ [] _ = NONE 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

241 
 inv_lookup eq ((key, value)::xs) value' = 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

242 
if eq (value', value) then SOME key 
55445
a76c679c0218
static repair of ML file  untested (!) by default since 76965c356d2a;
wenzelm
parents:
55440
diff
changeset

243 
else inv_lookup eq xs value' 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

244 

7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

245 
fun restore_const constant_table c = 
55437  246 
(case inv_lookup (op =) constant_table c of 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

247 
SOME c' => c' 
55437  248 
 NONE => error ("No constant corresponding to " ^ c)) 
249 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

250 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

251 
(** translation of terms, literals, premises, and clauses **) 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

252 

69593  253 
fun translate_arith_const \<^const_name>\<open>Groups.plus_class.plus\<close> = SOME Plus 
254 
 translate_arith_const \<^const_name>\<open>Groups.minus_class.minus\<close> = SOME Minus 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

255 
 translate_arith_const _ = NONE 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

256 

38734
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

257 
fun mk_nat_term constant_table n = 
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

258 
let 
69593  259 
val zero = translate_const constant_table \<^const_name>\<open>Groups.zero_class.zero\<close> 
260 
val Suc = translate_const constant_table \<^const_name>\<open>Suc\<close> 

38734
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

261 
in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end 
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

262 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

263 
fun translate_term ctxt constant_table t = 
55437  264 
(case try HOLogic.dest_number t of 
69593  265 
SOME (\<^typ>\<open>int\<close>, n) => Number n 
266 
 SOME (\<^typ>\<open>nat\<close>, n) => mk_nat_term constant_table n 

38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

267 
 NONE => 
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

268 
(case strip_comb t of 
55437  269 
(Free (v, T), []) => Var v 
38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

270 
 (Const (c, _), []) => Cons (translate_const constant_table c) 
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

271 
 (Const (c, _), args) => 
55437  272 
(case translate_arith_const c of 
273 
SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args) 

274 
 NONE => 

275 
AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)) 

276 
 _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))) 

38073  277 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

278 
fun translate_literal ctxt constant_table t = 
55437  279 
(case strip_comb t of 
69593  280 
(Const (\<^const_name>\<open>HOL.eq\<close>, _), [l, r]) => 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

281 
let 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

282 
val l' = translate_term ctxt constant_table l 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

283 
val r' = translate_term ctxt constant_table r 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

284 
in 
55437  285 
(if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) 
286 
(l', r') 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

287 
end 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

288 
 (Const (c, _), args) => 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

289 
Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args) 
55437  290 
 _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)) 
38073  291 

292 
fun NegRel_of (Rel lit) = NotRel lit 

293 
 NegRel_of (Eq eq) = NotEq eq 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

294 
 NegRel_of (ArithEq eq) = NotArithEq eq 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

295 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

296 
fun mk_groundness_prems t = map Ground (Term.add_frees t []) 
55437  297 

298 
fun translate_prem ensure_groundness ctxt constant_table t = 

299 
(case try HOLogic.dest_not t of 

300 
SOME t => 

301 
if ensure_groundness then 

302 
Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)]) 

303 
else 

304 
NegRel_of (translate_literal ctxt constant_table t) 

305 
 NONE => translate_literal ctxt constant_table t) 

306 

38114
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

307 
fun imp_prems_conv cv ct = 
55437  308 
(case Thm.term_of ct of 
69593  309 
Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => 
56245  310 
Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct 
55437  311 
 _ => Conv.all_conv ct) 
38114
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

312 

0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

313 
fun preprocess_intro thy rule = 
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

314 
Conv.fconv_rule 
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

315 
(imp_prems_conv 
51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
51126
diff
changeset

316 
(HOLogic.Trueprop_conv (Conv.try_conv (Conv.rewr_conv @{thm Predicate.eq_is_eq})))) 
38114
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

317 
(Thm.transfer thy rule) 
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

318 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

319 
fun translate_intros ensure_groundness ctxt gr const constant_table = 
38073  320 
let 
42361  321 
val intros = map (preprocess_intro (Proof_Context.theory_of ctxt)) (Graph.get_node gr const) 
59582  322 
val (intros', ctxt') = Variable.import_terms true (map Thm.prop_of intros) ctxt 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

323 
val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table 
38073  324 
fun translate_intro intro = 
325 
let 

326 
val head = HOLogic.dest_Trueprop (Logic.strip_imp_concl intro) 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

327 
val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems intro) 
38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

328 
val prems' = Conj (map (translate_prem ensure_groundness ctxt' constant_table') prems) 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

329 
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems') 
38073  330 
in clause end 
39724  331 
in 
332 
(map translate_intro intros', constant_table') 

333 
end 

38073  334 

38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

335 
fun depending_preds_of (key, intros) = 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

336 
fold Term.add_const_names (map Thm.prop_of intros) [] 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

337 

2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

338 
fun add_edges edges_of key G = 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

339 
let 
55437  340 
fun extend' key (G, visited) = 
341 
(case try (Graph.get_node G) key of 

342 
SOME v => 

343 
let 

344 
val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v)) 

345 
val (G', visited') = fold extend' 

346 
(subtract (op =) (key :: visited) new_edges) (G, key :: visited) 

347 
in 

348 
(fold (Graph.add_edge o (pair key)) new_edges G', visited') 

349 
end 

350 
 NONE => (G, visited)) 

38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

351 
in 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

352 
fst (extend' key (G, [])) 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

353 
end 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

354 

39183
512c10416590
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents:
38961
diff
changeset

355 
fun print_intros ctxt gr consts = 
512c10416590
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents:
38961
diff
changeset

356 
tracing (cat_lines (map (fn const => 
512c10416590
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents:
38961
diff
changeset

357 
"Constant " ^ const ^ "has intros:\n" ^ 
61268  358 
cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts)) 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

359 

55437  360 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

361 
(* translation of moded predicates *) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

362 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

363 
(** generating graph of moded predicates **) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

364 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

365 
(* could be moved to Predicate_Compile_Core *) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

366 
fun requires_modes polarity cls = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

367 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

368 
fun req_mode_of pol (t, derivation) = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

369 
(case fst (strip_comb t) of 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

370 
Const (c, _) => SOME (c, (pol, Predicate_Compile_Core.head_mode_of derivation)) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

371 
 _ => NONE) 
55437  372 
fun req (Predicate_Compile_Aux.Prem t, derivation) = 
373 
req_mode_of polarity (t, derivation) 

374 
 req (Predicate_Compile_Aux.Negprem t, derivation) = 

375 
req_mode_of (not polarity) (t, derivation) 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

376 
 req _ = NONE 
55437  377 
in 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

378 
maps (fn (_, prems) => map_filter req prems) cls 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

379 
end 
55437  380 

381 
structure Mode_Graph = 

382 
Graph( 

383 
type key = string * (bool * Predicate_Compile_Aux.mode) 

384 
val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord) 

385 
) 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

386 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

387 
fun mk_moded_clauses_graph ctxt scc gr = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

388 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

389 
val options = Predicate_Compile_Aux.default_options 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

390 
val mode_analysis_options = 
39761
c2a76ec6e2d9
renaming use_random to use_generators in the predicate compiler
bulwahn
parents:
39724
diff
changeset

391 
{use_generators = true, reorder_premises = true, infer_pos_and_neg_modes = true} 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

392 
fun infer prednames (gr, (pos_modes, neg_modes, random)) = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

393 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

394 
val (lookup_modes, lookup_neg_modes, needs_random) = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

395 
((fn s => the (AList.lookup (op =) pos_modes s)), 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

396 
(fn s => the (AList.lookup (op =) neg_modes s)), 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

397 
(fn s => member (op =) (the (AList.lookup (op =) random s)))) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

398 
val (preds, all_vs, param_vs, all_modes, clauses) = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

399 
Predicate_Compile_Core.prepare_intrs options ctxt prednames 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39798
diff
changeset

400 
(maps (Core_Data.intros_of ctxt) prednames) 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

401 
val ((moded_clauses, random'), _) = 
55437  402 
Mode_Inference.infer_modes mode_analysis_options options 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

403 
(lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

404 
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

405 
val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m  _ => NONE))) modes 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

406 
val neg_modes' = map (apsnd (map_filter (fn (false, m) => SOME m  _ => NONE))) modes 
55437  407 
val _ = 
408 
tracing ("Inferred modes:\n" ^ 

409 
cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map 

410 
(fn (p, m) => 

411 
Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes)) 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

412 
val gr' = gr 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

413 
> fold (fn (p, mps) => fold (fn (mode, cls) => 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

414 
Mode_Graph.new_node ((p, mode), cls)) mps) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

415 
moded_clauses 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

416 
> fold (fn (p, mps) => fold (fn (mode, cls) => fold (fn req => 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

417 
Mode_Graph.add_edge ((p, mode), req)) (requires_modes (fst mode) cls)) mps) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

418 
moded_clauses 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

419 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

420 
(gr', (AList.merge (op =) (op =) (pos_modes, pos_modes'), 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

421 
AList.merge (op =) (op =) (neg_modes, neg_modes'), 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

422 
AList.merge (op =) (op =) (random, random'))) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

423 
end 
55437  424 
in 
425 
fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], []))) 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

426 
end 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

427 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

428 
fun declare_moded_predicate moded_preds table = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

429 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

430 
fun update' (p as (pred, (pol, mode))) table = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

431 
if AList.defined (op =) table p then table else 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

432 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

433 
val name = Long_Name.base_name pred ^ (if pol then "p" else "n") 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

434 
^ Predicate_Compile_Aux.ascii_string_of_mode mode 
56812  435 
val p' = mk_conform (Name.enforce_case false) "pred" (map snd table) name 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

436 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

437 
AList.update (op =) (p, p') table 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

438 
end 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

439 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

440 
fold update' moded_preds table 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

441 
end 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

442 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

443 
fun mk_program ctxt moded_gr moded_preds (prog, (moded_pred_table, constant_table)) = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

444 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

445 
val moded_pred_table' = declare_moded_predicate moded_preds moded_pred_table 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

446 
fun mk_literal pol derivation constant_table' t = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

447 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

448 
val (p, args) = strip_comb t 
55437  449 
val mode = Predicate_Compile_Core.head_mode_of derivation 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

450 
val name = fst (dest_Const p) 
55437  451 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

452 
val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode))) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

453 
val args' = map (translate_term ctxt constant_table') args 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

454 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

455 
Rel (p', args') 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

456 
end 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

457 
fun mk_prem pol (indprem, derivation) constant_table = 
55437  458 
(case indprem of 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

459 
Predicate_Compile_Aux.Generator (s, T) => (Ground (s, T), constant_table) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

460 
 _ => 
55437  461 
declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) []) 
462 
constant_table 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

463 
> (fn constant_table' => 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

464 
(case indprem of Predicate_Compile_Aux.Negprem t => 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

465 
NegRel_of (mk_literal (not pol) derivation constant_table' t) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

466 
 _ => 
55437  467 
mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem), 
468 
constant_table'))) 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

469 
fun mk_clause pred_name pol (ts, prems) (prog, constant_table) = 
55437  470 
let 
471 
val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table 

472 
val args = map (translate_term ctxt constant_table') ts 

473 
val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table' 

474 
in 

475 
(((pred_name, args), Conj prems') :: prog, constant_table'') 

476 
end 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

477 
fun mk_clauses (pred, mode as (pol, _)) = 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

478 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

479 
val clauses = Mode_Graph.get_node moded_gr (pred, mode) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

480 
val pred_name = the (AList.lookup (op =) moded_pred_table' (pred, mode)) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

481 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

482 
fold (mk_clause pred_name pol) clauses 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

483 
end 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

484 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

485 
apsnd (pair moded_pred_table') (fold mk_clauses moded_preds (prog, constant_table)) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

486 
end 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

487 

0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

488 
fun generate (use_modes, ensure_groundness) ctxt const = 
55437  489 
let 
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

490 
fun strong_conn_of gr keys = 
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
45750
diff
changeset

491 
Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr) 
40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39798
diff
changeset

492 
val gr = Core_Data.intros_graph_of ctxt 
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

493 
val gr' = add_edges depending_preds_of const gr 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

494 
val scc = strong_conn_of gr' [const] 
55437  495 
val initial_constant_table = 
69593  496 
declare_consts [\<^const_name>\<open>Groups.zero_class.zero\<close>, \<^const_name>\<open>Suc\<close>] [] 
38073  497 
in 
55437  498 
(case use_modes of 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

499 
SOME mode => 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

500 
let 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

501 
val moded_gr = mk_moded_clauses_graph ctxt scc gr 
46614
165886a4fe64
clarified Graph.restrict (formerly Graph.subgraph) based on public graph operations;
wenzelm
parents:
45750
diff
changeset

502 
val moded_gr' = Mode_Graph.restrict 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

503 
(member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr 
55437  504 
val scc = Mode_Graph.strong_conn moded_gr' 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

505 
in 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

506 
apfst rev (apsnd snd 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

507 
(fold (mk_program ctxt moded_gr') (rev scc) ([], ([], initial_constant_table)))) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

508 
end 
55437  509 
 NONE => 
510 
let 

39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

511 
val _ = print_intros ctxt gr (flat scc) 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

512 
val constant_table = declare_consts (flat scc) initial_constant_table 
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

513 
in 
55437  514 
apfst flat 
515 
(fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table) 

516 
end) 

38073  517 
end 
55437  518 

519 

38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

520 
(* implementation for fully enumerating predicates and 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

521 
for sizelimited predicates for enumerating the values of a datatype upto a specific size *) 
38073  522 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

523 
fun add_ground_typ (Conj prems) = fold add_ground_typ prems 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

524 
 add_ground_typ (Ground (_, T)) = insert (op =) T 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

525 
 add_ground_typ _ = I 
38073  526 

38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

527 
fun mk_relname (Type (Tcon, Targs)) = 
56812  528 
Name.enforce_case false (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs) 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

529 
 mk_relname _ = raise Fail "unexpected type" 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

530 

38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

531 
fun mk_lim_relname T = "lim_" ^ mk_relname T 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

532 

d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

533 
fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T 
55437  534 

38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

535 
fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) = 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

536 
if member (op =) seen T then ([], (seen, constant_table)) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

537 
else 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

538 
let 
55437  539 
val (limited, size) = 
540 
(case AList.lookup (op =) limited_types T of 

541 
SOME s => (true, s) 

542 
 NONE => (false, 0)) 

38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

543 
val rel_name = (if limited then mk_lim_relname else mk_relname) T 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

544 
fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) = 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

545 
let 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

546 
val constant_table' = declare_consts [constr_name] constant_table 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

547 
val Ts = binder_types cT 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

548 
val (rec_clauses, (seen', constant_table'')) = 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

549 
fold_map (mk_ground_impl ctxt limited_types) Ts (seen, constant_table') 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

550 
val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts)) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

551 
val lim_var = 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

552 
if limited then 
55437  553 
if recursive then [AppF ("suc", [Var "Lim"])] 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

554 
else [Var "Lim"] 
55437  555 
else [] 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

556 
fun mk_prem v T' = 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

557 
if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v]) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

558 
else Rel (mk_relname T', [v]) 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

559 
val clause = 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

560 
((rel_name, lim_var @ [maybe_AppF (translate_const constant_table'' constr_name, vars)]), 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

561 
Conj (map2 mk_prem vars Ts)) 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

562 
in 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

563 
(clause :: flat rec_clauses, (seen', constant_table'')) 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

564 
end 
55445
a76c679c0218
static repair of ML file  untested (!) by default since 76965c356d2a;
wenzelm
parents:
55440
diff
changeset

565 
val constrs = Function_Lib.inst_constrs_of ctxt T 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

566 
val constrs' = (constrs ~~ map (is_recursive_constr T) constrs) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

567 
> (fn cs => filter_out snd cs @ filter snd cs) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

568 
val (clauses, constant_table') = 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

569 
apfst flat (fold_map mk_impl constrs' (T :: seen, constant_table)) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

570 
val size_term = funpow size (fn t => AppF ("suc", [t])) (Cons "zero") 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

571 
in 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

572 
((if limited then 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

573 
cons ((mk_relname T, [Var "x"]), Rel (mk_lim_relname T, [size_term, Var "x"])) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

574 
else I) clauses, constant_table') 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

575 
end 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

576 
 mk_ground_impl ctxt _ T (seen, constant_table) = 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

577 
raise Fail ("unexpected type :" ^ Syntax.string_of_typ ctxt T) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

578 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

579 
fun replace_ground (Conj prems) = Conj (map replace_ground prems) 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

580 
 replace_ground (Ground (x, T)) = 
55437  581 
Rel (mk_relname T, [Var x]) 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

582 
 replace_ground p = p 
55437  583 

38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

584 
fun add_ground_predicates ctxt limited_types (p, constant_table) = 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

585 
let 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

586 
val ground_typs = fold (add_ground_typ o snd) p [] 
55437  587 
val (grs, (_, constant_table')) = 
588 
fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table) 

38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

589 
val p' = map (apsnd replace_ground) p 
38073  590 
in 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

591 
((flat grs) @ p', constant_table') 
38073  592 
end 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

593 

55437  594 

38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

595 
(* make depthlimited version of predicate *) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

596 

6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

597 
fun mk_lim_rel_name rel_name = "lim_" ^ rel_name 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

598 

38959
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

599 
fun mk_depth_limited rel_names ((rel_name, ts), prem) = 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

600 
let 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

601 
fun has_positive_recursive_prems (Conj prems) = exists has_positive_recursive_prems prems 
38959
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

602 
 has_positive_recursive_prems (Rel (rel, ts)) = member (op =) rel_names rel 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

603 
 has_positive_recursive_prems _ = false 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

604 
fun mk_lim_prem (Conj prems) = Conj (map mk_lim_prem prems) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

605 
 mk_lim_prem (p as Rel (rel, ts)) = 
67405
e9ab4ad7bd15
uniform use of Standard ML opinfix  eliminated warnings;
wenzelm
parents:
67399
diff
changeset

606 
if member (op =) rel_names rel then Rel (mk_lim_rel_name rel, Var "Lim" :: ts) else p 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

607 
 mk_lim_prem p = p 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

608 
in 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

609 
if has_positive_recursive_prems prem then 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

610 
((mk_lim_rel_name rel_name, (AppF ("suc", [Var "Lim"])) :: ts), mk_lim_prem prem) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

611 
else 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

612 
((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

613 
end 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

614 

39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

615 
fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero") 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

616 

9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

617 
fun add_limited_predicates limited_predicates (p, constant_table) = 
55437  618 
let 
619 
fun add (rel_names, limit) p = 

38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

620 
let 
38959
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

621 
val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

622 
val clauses' = map (mk_depth_limited rel_names) clauses 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

623 
fun mk_entry_clause rel_name = 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

624 
let 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

625 
val nargs = length (snd (fst 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

626 
(the (find_first (fn ((rel, _), _) => rel = rel_name) clauses)))) 
55437  627 
val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs) 
38959
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

628 
in 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

629 
(("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars)) 
706ab66e3464
towards support of limited predicates for mutually recursive predicates
bulwahn
parents:
38958
diff
changeset

630 
end 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

631 
in (p @ (map mk_entry_clause rel_names) @ clauses') end 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

632 
in 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

633 
(fold add limited_predicates p, constant_table) 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

634 
end 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

635 

6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

636 

6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

637 
(* replace predicates in clauses *) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

638 

6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

639 
(* replace (A, B, C) p = replace A by B in clauses of C *) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

640 
fun replace ((from, to), location) p = 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

641 
let 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

642 
fun replace_prem (Conj prems) = Conj (map replace_prem prems) 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

643 
 replace_prem (r as Rel (rel, ts)) = 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

644 
if rel = from then Rel (to, ts) else r 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

645 
 replace_prem r = r 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

646 
in 
55437  647 
map 
648 
(fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) 

649 
p 

38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

650 
end 
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

651 

55437  652 

38960
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

653 
(* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *) 
38947
6ed1cffd9d4e
added quite adhoc logic program transformations limited_predicates and replacements of predicates
bulwahn
parents:
38864
diff
changeset

654 

38960
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

655 
fun reorder_manually reorder p = 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

656 
let 
55445
a76c679c0218
static repair of ML file  untested (!) by default since 76965c356d2a;
wenzelm
parents:
55440
diff
changeset

657 
fun reorder' ((rel, args), prem) seen = 
38960
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

658 
let 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

659 
val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

660 
val i = the (AList.lookup (op =) seen' rel) 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

661 
val perm = AList.lookup (op =) reorder (rel, i) 
55437  662 
val prem' = 
663 
(case perm of 

664 
SOME p => (case prem of Conj prems => Conj (map (nth prems) p)  _ => prem) 

665 
 NONE => prem) 

38960
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

666 
in (((rel, args), prem'), seen') end 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

667 
in 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

668 
fst (fold_map reorder' p []) 
363bfb245917
adding manual reordering of premises to prolog generation
bulwahn
parents:
38959
diff
changeset

669 
end 
39462
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

670 

55437  671 

38735  672 
(* rename variables to prologfriendly names *) 
673 

674 
fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) 

675 

676 
fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming) 

677 

678 
fun mk_renaming v renaming = 

56812  679 
(v, mk_conform (Name.enforce_case true) "Var" (map snd renaming) v) :: renaming 
38735  680 

681 
fun rename_vars_clause ((rel, args), prem) = 

682 
let 

683 
val vars = fold_prem_terms add_vars prem (fold add_vars args []) 

684 
val renaming = fold mk_renaming vars [] 

685 
in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end 

55437  686 

687 

39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

688 
(* limit computation globally by some threshold *) 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

689 

55445
a76c679c0218
static repair of ML file  untested (!) by default since 76965c356d2a;
wenzelm
parents:
55440
diff
changeset

690 
fun limit_globally limit const_name (p, constant_table) = 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

691 
let 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

692 
val rel_names = fold (fn ((r, _), _) => insert (op =) r) p [] 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

693 
val p' = map (mk_depth_limited rel_names) p 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

694 
val rel_name = translate_const constant_table const_name 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

695 
val nargs = length (snd (fst 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

696 
(the (find_first (fn ((rel, _), _) => rel = rel_name) p)))) 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

697 
val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs) 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

698 
val entry_clause = ((rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars)) 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

699 
val p'' = filter_out (fn ((rel, _), _) => rel = rel_name) p 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

700 
in 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

701 
(entry_clause :: p' @ p'', constant_table) 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

702 
end 
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

703 

55437  704 

39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

705 
(* post processing of generated prolog program *) 
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

706 

55537  707 
fun post_process ctxt (options: code_options) const_name (p, constant_table) = 
39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

708 
(p, constant_table) 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

709 
> (case #limit_globally options of 
55445
a76c679c0218
static repair of ML file  untested (!) by default since 76965c356d2a;
wenzelm
parents:
55440
diff
changeset

710 
SOME limit => limit_globally limit const_name 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

711 
 NONE => I) 
39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

712 
> (if #ensure_groundness options then 
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

713 
add_ground_predicates ctxt (#limited_types options) 
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

714 
else I) 
39724  715 
> tap (fn _ => tracing "Adding limited predicates...") 
39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

716 
> add_limited_predicates (#limited_predicates options) 
39724  717 
> tap (fn _ => tracing "Replacing predicates...") 
39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

718 
> apfst (fold replace (#replacing options)) 
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

719 
> apfst (reorder_manually (#manual_reorder options)) 
55537  720 
> apfst (map rename_vars_clause) 
39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

721 

55437  722 

38073  723 
(* code printer *) 
724 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

725 
fun write_arith_op Plus = "+" 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

726 
 write_arith_op Minus = "" 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

727 

38735  728 
fun write_term (Var v) = v 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

729 
 write_term (Cons c) = c 
55437  730 
 write_term (AppF (f, args)) = 
731 
f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 

732 
 write_term (ArithOp (oper, [a1, a2])) = 

733 
write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2 

38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

734 
 write_term (Number n) = string_of_int n 
38073  735 

736 
fun write_rel (pred, args) = 

55437  737 
pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
38073  738 

739 
fun write_prem (Conj prems) = space_implode ", " (map write_prem prems) 

55437  740 
 write_prem (Rel p) = write_rel p 
38073  741 
 write_prem (NotRel p) = "not(" ^ write_rel p ^ ")" 
742 
 write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r 

743 
 write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r 

38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

744 
 write_prem (ArithEq (l, r)) = write_term l ^ " is " ^ write_term r 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

745 
 write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

746 
 write_prem _ = raise Fail "Not a valid prolog premise" 
38073  747 

748 
fun write_clause (head, prem) = 

749 
write_rel head ^ (if prem = Conj [] then "." else " : " ^ write_prem prem ^ ".") 

750 

751 
fun write_program p = 

55437  752 
cat_lines (map write_clause p) 
753 

38073  754 

38790  755 
(* query templates *) 
38078  756 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

757 
(** query and prelude for swiprolog **) 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

758 

39464
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

759 
fun swi_prolog_query_first (rel, args) vnames = 
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

760 
"eval : once(" ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^ 
38082  761 
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ 
762 
"\\n', [" ^ space_implode ", " vnames ^ "]).\n" 

55437  763 

39464
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

764 
fun swi_prolog_query_firstn n (rel, args) vnames = 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

765 
"eval : findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^ 
39464
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

766 
rel ^ "(" ^ space_implode ", " (map write_term args) ^ "), Sols), writelist(Sols).\n" ^ 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

767 
"writelist([]).\n" ^ 
39546
bfe10da7d764
renaming variable name to decrease likelyhood of nameclash
bulwahn
parents:
39542
diff
changeset

768 
"writelist([(" ^ space_implode ", " vnames ^ ")SolutionTail]) : " ^ 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

769 
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ 
39546
bfe10da7d764
renaming variable name to decrease likelyhood of nameclash
bulwahn
parents:
39542
diff
changeset

770 
"\\n', [" ^ space_implode ", " vnames ^ "]), writelist(SolutionTail).\n" 
55437  771 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

772 
val swi_prolog_prelude = 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

773 
": use_module(library('dialect/ciao/aggregates')).\n" ^ 
38729
9c9d14827380
improving output of set comprehensions; adding style_check flags
bulwahn
parents:
38728
diff
changeset

774 
": style_check(singleton).\n" ^ 
41067  775 
": style_check(discontiguous).\n" ^ 
38729
9c9d14827380
improving output of set comprehensions; adding style_check flags
bulwahn
parents:
38728
diff
changeset

776 
": style_check(atom).\n\n" ^ 
38073  777 
"main : catch(eval, E, (print_message(error, E), fail)), halt.\n" ^ 
778 
"main : halt(1).\n" 

38075  779 

55437  780 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

781 
(** query and prelude for yap **) 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

782 

39464
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

783 
fun yap_query_first (rel, args) vnames = 
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

784 
"eval : once(" ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^ 
38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

785 
"format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^ 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

786 
"\\n', [" ^ space_implode ", " vnames ^ "]).\n" 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

787 

970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

788 
val yap_prelude = 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

789 
": initialization(eval).\n" 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

790 

55437  791 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

792 
(* systemdependent query, prelude and invocation *) 
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

793 

55437  794 
fun query system nsols = 
795 
(case system of 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

796 
SWI_PROLOG => 
55437  797 
(case nsols of 
798 
NONE => swi_prolog_query_first 

799 
 SOME n => swi_prolog_query_firstn n) 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

800 
 YAP => 
55437  801 
(case nsols of 
802 
NONE => yap_query_first 

803 
 SOME n => 

804 
error "No support for querying multiple solutions in the prolog system yap")) 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

805 

970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

806 
fun prelude system = 
55437  807 
(case system of 
808 
SWI_PROLOG => swi_prolog_prelude 

809 
 YAP => yap_prelude) 

38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

810 

41940  811 
fun invoke system file = 
38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

812 
let 
41940  813 
val (env_var, cmd) = 
814 
(case system of 

51709
19b47bfac6ef
proper prolog commandline instead of hashbang, which might switch to invalid executable and thus fail (notably on lxbroy2);
wenzelm
parents:
51704
diff
changeset

815 
SWI_PROLOG => ("ISABELLE_SWIPL", "\"$ISABELLE_SWIPL\" q t main f ") 
41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP  discontinued implicit detection;
wenzelm
parents:
41941
diff
changeset

816 
 YAP => ("ISABELLE_YAP", "\"$ISABELLE_YAP\" L ")) 
39462
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

817 
in 
41940  818 
if getenv env_var = "" then 
39462
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

819 
(warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "") 
51704
0b0fc7dc4ce4
actually fail on prolog errors  such as swipl startup failure due to missing shared libraries  assuming it normally produces clean return code 0;
wenzelm
parents:
51314
diff
changeset

820 
else 
62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62519
diff
changeset

821 
(case Isabelle_System.bash_output (cmd ^ File.bash_path file) of 
51704
0b0fc7dc4ce4
actually fail on prolog errors  such as swipl startup failure due to missing shared libraries  assuming it normally produces clean return code 0;
wenzelm
parents:
51314
diff
changeset

822 
(out, 0) => out 
0b0fc7dc4ce4
actually fail on prolog errors  such as swipl startup failure due to missing shared libraries  assuming it normally produces clean return code 0;
wenzelm
parents:
51314
diff
changeset

823 
 (_, rc) => 
0b0fc7dc4ce4
actually fail on prolog errors  such as swipl startup failure due to missing shared libraries  assuming it normally produces clean return code 0;
wenzelm
parents:
51314
diff
changeset

824 
error ("Error caused by prolog system " ^ env_var ^ 
0b0fc7dc4ce4
actually fail on prolog errors  such as swipl startup failure due to missing shared libraries  assuming it normally produces clean return code 0;
wenzelm
parents:
51314
diff
changeset

825 
": return code " ^ string_of_int rc)) 
39462
3a86194d1534
registering code_prolog as component; using environment variable; adding settings file for prolog code generation
bulwahn
parents:
39461
diff
changeset

826 
end 
38792
970508a5119f
added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory
bulwahn
parents:
38790
diff
changeset

827 

41952
c7297638599b
cleanup of former settings GHC_PATH, EXEC_GHC, EXEC_OCAML, EXEC_SWIPL, EXEC_YAP  discontinued implicit detection;
wenzelm
parents:
41941
diff
changeset

828 

38075  829 
(* parsing prolog solution *) 
38790  830 

38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

831 
val scan_number = 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

832 
Scan.many1 Symbol.is_ascii_digit 
38075  833 

834 
val scan_atom = 

55437  835 
Scan.many1 
836 
(fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) 

38075  837 

838 
val scan_var = 

38078  839 
Scan.many1 
840 
(fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) 

38075  841 

842 
fun dest_Char (Symbol.Char s) = s 

843 

43735
9b88fd07b912
standardized String.concat towards implode (cf. c37a1f29bbc0)
bulwahn
parents:
43324
diff
changeset

844 
val string_of = implode o map (dest_Char o Symbol.decode) 
38075  845 

38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

846 
fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x  ord "0")) xs 0 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

847 

38078  848 
fun scan_terms xs = (((scan_term  $$ ",") ::: scan_terms) 
849 
 (scan_term >> single)) xs 

850 
and scan_term xs = 

38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

851 
((scan_number >> (Number o int_of_symbol_list)) 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

852 
 (scan_var >> (Var o string_of)) 
38078  853 
 ((scan_atom  ($$ "("  scan_terms  $$ ")")) 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

854 
>> (fn (f, ts) => AppF (string_of f, ts))) 
38078  855 
 (scan_atom >> (Cons o string_of))) xs 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

856 

38075  857 
val parse_term = fst o Scan.finite Symbol.stopper 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

858 
(Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term) 
40924  859 
o raw_explode 
55437  860 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

861 
fun parse_solutions sol = 
38075  862 
let 
55437  863 
fun dest_eq s = 
864 
(case space_explode "=" s of 

38075  865 
(l :: r :: []) => parse_term (unprefix " " r) 
55437  866 
 _ => raise Fail "unexpected equation in prolog output") 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

867 
fun parse_solution s = map dest_eq (space_explode ";" s) 
73233
4d36070bdbf4
more robust: accommodate output lines produced by Scala "bash_process";
wenzelm
parents:
70308
diff
changeset

868 
val sols = (case Library.trim_split_lines sol of [] => []  s => fst (split_last s)) 
38075  869 
in 
38961
8c2f59171647
handling the quickcheck result no counterexample more correctly
bulwahn
parents:
38960
diff
changeset

870 
map parse_solution sols 
55437  871 
end 
872 

873 

38073  874 
(* calling external interpreter and getting results *) 
875 

59156  876 
fun run ctxt p (query_rel, args) vnames nsols = 
38073  877 
let 
59156  878 
val timeout = get_prolog_timeout ctxt 
879 
val system = get_prolog_system ctxt 

55437  880 
val renaming = fold mk_renaming (fold add_vars args vnames) [] 
38735  881 
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames 
39464
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

882 
val args' = map (rename_vars_term renaming) args 
39542
a50c0ae2312c
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
bulwahn
parents:
39541
diff
changeset

883 
val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

884 
val _ = tracing ("Generated prolog program:\n" ^ prog) 
62519  885 
val solution = Timeout.apply timeout (fn prog => 
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42111
diff
changeset

886 
Isabelle_System.with_tmp_file "prolog_file" "" (fn prolog_file => 
41940  887 
(File.write prolog_file prog; invoke system prolog_file))) prog 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

888 
val _ = tracing ("Prolog returned solution(s):\n" ^ solution) 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

889 
val tss = parse_solutions solution 
38073  890 
in 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

891 
tss 
38073  892 
end 
893 

55437  894 

38790  895 
(* restoring types in terms *) 
38075  896 

38081
8b02ce312893
removing pointless type information in internal prolog terms
bulwahn
parents:
38080
diff
changeset

897 
fun restore_term ctxt constant_table (Var s, T) = Free (s, T) 
69593  898 
 restore_term ctxt constant_table (Number n, \<^typ>\<open>int\<close>) = HOLogic.mk_number \<^typ>\<open>int\<close> n 
55437  899 
 restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number") 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

900 
 restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T) 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

901 
 restore_term ctxt constant_table (AppF (f, args), T) = 
55437  902 
let 
903 
val thy = Proof_Context.theory_of ctxt 

904 
val c = restore_const constant_table f 

905 
val cT = Sign.the_const_type thy c 

906 
val (argsT, resT) = strip_type cT 

907 
val subst = Sign.typ_match thy (resT, T) Vartab.empty 

908 
val argsT' = map (Envir.subst_type subst) argsT 

909 
in 

910 
list_comb (Const (c, Envir.subst_type subst cT), 

911 
map (restore_term ctxt constant_table) (args ~~ argsT')) 

912 
end 

38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

913 

55437  914 

39465
fcff6903595f
adding restoring of numerals for natural numbers for values command
bulwahn
parents:
39464
diff
changeset

915 
(* restore numerals in natural numbers *) 
fcff6903595f
adding restoring of numerals for natural numbers for values command
bulwahn
parents:
39464
diff
changeset

916 

fcff6903595f
adding restoring of numerals for natural numbers for values command
bulwahn
parents:
39464
diff
changeset

917 
fun restore_nat_numerals t = 
69593  918 
if fastype_of t = \<^typ>\<open>nat\<close> andalso is_some (try HOLogic.dest_nat t) then 
919 
HOLogic.mk_number \<^typ>\<open>nat\<close> (HOLogic.dest_nat t) 

39465
fcff6903595f
adding restoring of numerals for natural numbers for values command
bulwahn
parents:
39464
diff
changeset

920 
else 
fcff6903595f
adding restoring of numerals for natural numbers for values command
bulwahn
parents:
39464
diff
changeset

921 
(case t of 
55437  922 
t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2 
923 
 t => t) 

924 

925 

38790  926 
(* values command *) 
927 

928 
val preprocess_options = Predicate_Compile_Aux.Options { 

929 
expected_modes = NONE, 

39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39187
diff
changeset

930 
proposed_modes = [], 
38790  931 
proposed_names = [], 
932 
show_steps = false, 

933 
show_intermediate_results = false, 

934 
show_proof_trace = false, 

935 
show_modes = false, 

936 
show_mode_inference = false, 

937 
show_compilation = false, 

938 
show_caught_failures = false, 

39383
ddfafa97da2f
adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents:
39187
diff
changeset

939 
show_invalid_clauses = false, 
38790  940 
skip_proof = true, 
941 
no_topmost_reordering = false, 

942 
function_flattening = true, 

943 
specialise = false, 

944 
fail_safe_function_flattening = false, 

945 
no_higher_order_predicate = [], 

946 
inductify = false, 

947 
detect_switches = true, 

40054
cd7b1fa20bce
adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents:
39798
diff
changeset

948 
smart_depth_limiting = true, 
38790  949 
compilation = Predicate_Compile_Aux.Pred 
950 
} 

951 

38075  952 
fun values ctxt soln t_compr = 
953 
let 

42361  954 
val options = code_options_of (Proof_Context.theory_of ctxt) 
55437  955 
val split = 
956 
(case t_compr of 

69593  957 
(Const (\<^const_name>\<open>Collect\<close>, _) $ t) => t 
55437  958 
 _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr)) 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset

959 
val (body, Ts, fp) = HOLogic.strip_ptupleabs split 
38075  960 
val output_names = Name.variant_list (Term.add_free_names body []) 
961 
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) 

38080
8c20eb9a388d
cleaning example file; more natural ordering of variable names
bulwahn
parents:
38079
diff
changeset

962 
val output_frees = rev (map2 (curry Free) output_names Ts) 
38075  963 
val body = subst_bounds (output_frees, body) 
964 
val (pred as Const (name, T), all_args) = 

55437  965 
(case strip_comb body of 
38075  966 
(Const (name, T), all_args) => (Const (name, T), all_args) 
55437  967 
 (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)) 
38732
3371dbc806ae
moving preprocessing to values in prolog generation
bulwahn
parents:
38731
diff
changeset

968 
val _ = tracing "Preprocessing specification..." 
42361  969 
val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name 
38732
3371dbc806ae
moving preprocessing to values in prolog generation
bulwahn
parents:
38731
diff
changeset

970 
val t = Const (name, T) 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

971 
val thy' = 
52788  972 
Proof_Context.theory_of ctxt 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

973 
> Predicate_Compile.preprocess preprocess_options t 
42361  974 
val ctxt' = Proof_Context.init_global thy' 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

975 
val _ = tracing "Generating prolog program..." 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

976 
val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *) 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

977 
> post_process ctxt' options name 
39464
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

978 
val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table 
13493d3c28d0
values command for prolog supports complex terms and not just variables
bulwahn
parents:
39462
diff
changeset

979 
val args' = map (translate_term ctxt constant_table') all_args 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

980 
val _ = tracing "Running prolog program..." 
59156  981 
val tss = run ctxt p (translate_const constant_table' name, args') output_names soln 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

982 
val _ = tracing "Restoring terms..." 
69593  983 
val empty = Const(\<^const_name>\<open>bot\<close>, fastype_of t_compr) 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

984 
fun mk_insert x S = 
69593  985 
Const (\<^const_name>\<open>Set.insert\<close>, fastype_of x > fastype_of S > fastype_of S) $ x $ S 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

986 
fun mk_set_compr in_insert [] xs = 
42489
db9b9e46131c
some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);
wenzelm
parents:
42361
diff
changeset

987 
rev ((Free ("dots", fastype_of t_compr)) :: (* FIXME proper name!? *) 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

988 
(if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)) 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

989 
 mk_set_compr in_insert (t :: ts) xs = 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

990 
let 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

991 
val frees = Term.add_frees t [] 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

992 
in 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

993 
if null frees then 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

994 
mk_set_compr (t :: in_insert) ts xs 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

995 
else 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

996 
let 
55437  997 
val uu as (uuN, uuT) = 
998 
singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t) 

38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

999 
val set_compr = 
55437  1000 
HOLogic.mk_Collect (uuN, uuT, 
1001 
fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) 

69593  1002 
frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), \<^term>\<open>True\<close>))) 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

1003 
in 
38729
9c9d14827380
improving output of set comprehensions; adding style_check flags
bulwahn
parents:
38728
diff
changeset

1004 
mk_set_compr [] ts 
55437  1005 
(set_compr :: 
1006 
(if null in_insert then xs else (fold mk_insert in_insert empty) :: xs)) 

38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

1007 
end 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

1008 
end 
38075  1009 
in 
69593  1010 
foldl1 (HOLogic.mk_binop \<^const_name>\<open>sup\<close>) (mk_set_compr [] 
55437  1011 
(map (fn ts => HOLogic.mk_tuple 
1012 
(map (restore_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) []) 

38075  1013 
end 
1014 

1015 
fun values_cmd print_modes soln raw_t state = 

1016 
let 

1017 
val ctxt = Toplevel.context_of state 

1018 
val t = Syntax.read_term ctxt raw_t 

1019 
val t' = values ctxt soln t 

1020 
val ty' = Term.type_of t' 

70308  1021 
val ctxt' = Proof_Context.augment t' ctxt 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

1022 
val _ = tracing "Printing terms..." 
55437  1023 
in 
1024 
Print_Mode.with_modes print_modes (fn () => 

38075  1025 
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, 
55437  1026 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) () 
55445
a76c679c0218
static repair of ML file  untested (!) by default since 76965c356d2a;
wenzelm
parents:
55440
diff
changeset

1027 
end > Pretty.writeln 
38075  1028 

1029 

55447  1030 
(* values command for Prolog queries *) 
38075  1031 

1032 
val opt_print_modes = 

69593  1033 
Scan.optional (\<^keyword>\<open>(\<close>  Parse.!!! (Scan.repeat1 Parse.name  \<^keyword>\<open>)\<close>)) [] 
38075  1034 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

1035 
val _ = 
69593  1036 
Outer_Syntax.command \<^command_keyword>\<open>values_prolog\<close> 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

1037 
"enumerate and print comprehensions" 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

1038 
(opt_print_modes  Scan.optional (Parse.nat >> SOME) NONE  Parse.term 
55447  1039 
>> (fn ((print_modes, soln), t) => Toplevel.keep (values_cmd print_modes soln t))) 
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

1040 

38075  1041 

38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1042 
(* quickcheck generator *) 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1043 

39541
6605c1e87c7f
removing clone in code_prolog and predicate_compile_quickcheck
bulwahn
parents:
39465
diff
changeset

1044 
(* FIXME: a small clone of Predicate_Compile_Quickcheck  maybe refactor out commons *) 
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1045 

69593  1046 
val active = Attrib.setup_config_bool \<^binding>\<open>quickcheck_prolog_active\<close> (K true) 
43885  1047 

45442  1048 
fun test_term ctxt (t, eval_terms) = 
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1049 
let 
44241  1050 
val t' = fold_rev absfree (Term.add_frees t []) t 
42361  1051 
val options = code_options_of (Proof_Context.theory_of ctxt) 
52788  1052 
val thy = Proof_Context.theory_of ctxt 
39541
6605c1e87c7f
removing clone in code_prolog and predicate_compile_quickcheck
bulwahn
parents:
39465
diff
changeset

1053 
val ((((full_constname, constT), vs'), intro), thy1) = 
42091  1054 
Predicate_Compile_Aux.define_quickcheck_predicate t' thy 
57962  1055 
val thy2 = 
69593  1056 
Context.theory_map (Named_Theorems.add_thm \<^named_theorems>\<open>code_pred_def\<close> intro) thy1 
39541
6605c1e87c7f
removing clone in code_prolog and predicate_compile_quickcheck
bulwahn
parents:
39465
diff
changeset

1057 
val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2 
42361  1058 
val ctxt' = Proof_Context.init_global thy3 
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1059 
val _ = tracing "Generating prolog program..." 
39461
0ed0f015d140
adding mode inference to prolog compilation; separate between (adhoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents:
39383
diff
changeset

1060 
val (p, constant_table) = generate (NONE, true) ctxt' full_constname 
39798
9e7a0a9d194e
adding option to globally limit the prolog execution
bulwahn
parents:
39761
diff
changeset

1061 
> post_process ctxt' (set_ensure_groundness options) full_constname 
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1062 
val _ = tracing "Running prolog program..." 
59156  1063 
val tss = 
1064 
run ctxt p (translate_const constant_table full_constname, map (Var o fst) vs') 

1065 
(map fst vs') (SOME 1) 

38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1066 
val _ = tracing "Restoring terms..." 
43885  1067 
val counterexample = 
55437  1068 
(case tss of 
39541
6605c1e87c7f
removing clone in code_prolog and predicate_compile_quickcheck
bulwahn
parents:
39465
diff
changeset

1069 
[ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs')) 
55437  1070 
 _ => NONE) 
38733
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

1071 
in 
43885  1072 
Quickcheck.Result 
55437  1073 
{counterexample = 
1074 
Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample, 

1075 
evaluation_terms = Option.map (K []) counterexample, 

1076 
timings = [], 

1077 
reports = []} 

1078 
end 

38732
3371dbc806ae
moving preprocessing to values in prolog generation
bulwahn
parents:
38731
diff
changeset

1079 

45442  1080 
fun test_goals ctxt _ insts goals = 
43885  1081 
let 
45226  1082 
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals 
43885  1083 
in 
45442  1084 
Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) [] 
43885  1085 
end 
55437  1086 

1087 
end 