author  wenzelm 
Fri, 27 Aug 2010 12:57:55 +0200  
changeset 38797  abe92b33ac9f 
parent 38793  eba0175d4cd1 
parent 38755  a37d39fe32f8 
child 38864  4abe644fcea5 
permissions  rwrr 
38073  1 
(* Title: HOL/Tools/Predicate_Compile/code_prolog.ML 
2 
Author: Lukas Bulwahn, TU Muenchen 

3 

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

5 
*) 

6 

7 
signature CODE_PROLOG = 

8 
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

9 
datatype prolog_system = SWI_PROLOG  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

10 
type code_options = 
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

11 
{ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system} 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

12 
val options : code_options ref 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

13 

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

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

15 
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

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

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

18 
 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

19 
 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

20 
 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

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

22 

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

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

25 
type constant_table = (string * string) list 
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

26 

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

27 
val generate : bool > 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

28 
val write_program : logic_program > string 
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

29 
val run : prolog_system > logic_program > string > string list > int option > prol_term list list 
38073  30 

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

31 
val quickcheck : Proof.context > bool > term > int > term list option * (bool list * bool) 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

32 

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

33 
val trace : bool Unsynchronized.ref 
38073  34 
end; 
35 

36 
structure Code_Prolog : CODE_PROLOG = 

37 
struct 

38 

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

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

40 

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

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

42 

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

43 
fun tracing s = if !trace then Output.tracing s else () 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

44 

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

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

46 

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

47 
datatype prolog_system = SWI_PROLOG  YAP 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

48 

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

49 
type code_options = 
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

50 
{ensure_groundness : bool, limited_types : (typ * int) list, prolog_system : prolog_system} 
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

51 

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

52 
val options = Unsynchronized.ref {ensure_groundness = false, limited_types = [], 
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

53 
prolog_system = SWI_PROLOG}; 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

54 

38073  55 
(* general string functions *) 
56 

57 
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode; 

58 
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; 

59 

60 
(* internal program representation *) 

61 

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

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

63 

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

64 
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

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

66 

38735  67 
fun dest_Var (Var v) = v 
68 

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

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

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

72 
 add_vars _ = I 

73 

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

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

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

77 
 map_vars f t = t 

78 

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

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

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

81 

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

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

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

84 

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

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

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

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

88 
 is_arith_term _ = false 
38073  89 

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

90 
fun string_of_prol_term (Var s) = "Var " ^ s 
38075  91 
 string_of_prol_term (Cons s) = "Cons " ^ s 
92 
 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

93 
 string_of_prol_term (Number n) = "Number " ^ string_of_int n 
38075  94 

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

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

96 
 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

97 
 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

98 
 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

99 
 Ground of string * typ; 
38735  100 

38073  101 
fun dest_Rel (Rel (c, ts)) = (c, ts) 
38735  102 

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

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

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

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

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

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

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

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

111 

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

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

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

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

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

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

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

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

120 

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

121 
type clause = ((string * prol_term list) * prem); 
38073  122 

123 
type logic_program = clause list; 

124 

125 
(* translation from introduction rules to internal representation *) 

126 

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

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

128 

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

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

130 

38073  131 
(* assuming no clashing *) 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

133 
AList.make (first_lower o Long_Name.base_name) consts 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

134 

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

135 
fun declare_consts consts constant_table = 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

136 
fold (fn c => AList.update (op =) (c, first_lower (Long_Name.base_name c))) consts constant_table 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

137 

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

138 
fun translate_const constant_table c = 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

140 
SOME c' => c' 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

141 
 NONE => error ("No such constant: " ^ c) 
38073  142 

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

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

144 
 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

145 
if eq (value', value) then SOME key 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

147 

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

148 
fun restore_const constant_table c = 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

150 
SOME c' => c' 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

151 
 NONE => error ("No constant corresponding to " ^ c) 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

152 

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

153 
(** 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

154 

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

155 
fun translate_arith_const @{const_name "Groups.plus_class.plus"} = SOME Plus 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

156 
 translate_arith_const @{const_name "Groups.minus_class.minus"} = SOME Minus 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

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

158 

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

159 
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

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

161 
val zero = translate_const constant_table @{const_name "Groups.zero_class.zero"} 
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

162 
val Suc = translate_const constant_table @{const_name "Suc"} 
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

163 
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

164 

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

165 
fun translate_term ctxt constant_table t = 
38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

166 
case try HOLogic.dest_number t of 
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

167 
SOME (@{typ "int"}, n) => Number n 
38734
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

168 
 SOME (@{typ "nat"}, n) => mk_nat_term constant_table n 
38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

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

170 
(case strip_comb t of 
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

171 
(Free (v, T), []) => Var v 
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

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

173 
 (Const (c, _), args) => 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

174 
(case translate_arith_const c of 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

175 
SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args) 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

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

177 
AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)) 
38112
cf08f4780938
adding numbers as basic term in prolog code generation
bulwahn
parents:
38082
diff
changeset

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

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

180 
fun translate_literal ctxt constant_table t = 
38073  181 
case strip_comb t of 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

182 
(Const (@{const_name "op ="}, _), [l, r]) => 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

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

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

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

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

187 
(if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r') 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

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

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

190 
Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args) 
38073  191 
 _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t) 
192 

193 
fun NegRel_of (Rel lit) = NotRel lit 

194 
 NegRel_of (Eq eq) = NotEq eq 

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

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

196 

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

197 
fun mk_groundness_prems t = map Ground (Term.add_frees t []) 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

198 

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

199 
fun translate_prem ensure_groundness ctxt constant_table t = 
38073  200 
case try HOLogic.dest_not t of 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

201 
SOME t => 
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

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

203 
Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)]) 
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

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

205 
NegRel_of (translate_literal ctxt constant_table t) 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

206 
 NONE => translate_literal ctxt constant_table t 
38114
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

207 

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

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

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

210 
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct 
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

211 
 _ => Conv.all_conv ct 
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

212 

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

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

214 
case Thm.term_of ct of 
38558  215 
Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct 
38114
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

216 
 _ => raise Fail "Trueprop_conv" 
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

217 

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

218 
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

219 
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

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

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

222 
(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

223 

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

224 
fun translate_intros ensure_groundness ctxt gr const constant_table = 
38073  225 
let 
38114
0f06e3cc04a6
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
bulwahn
parents:
38113
diff
changeset

226 
val intros = map (preprocess_intro (ProofContext.theory_of ctxt)) (Graph.get_node gr const) 
38073  227 
val (intros', ctxt') = Variable.import_terms true (map prop_of intros) ctxt 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

228 
val constant_table' = declare_consts (fold Term.add_const_names intros' []) constant_table 
38734
e5508a74b11f
changing hotel trace definition; adding simple handling of numerals on natural numbers
bulwahn
parents:
38733
diff
changeset

229 
> declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] 
38073  230 
fun translate_intro intro = 
231 
let 

232 
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

233 
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

234 
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

235 
val clause = (dest_Rel (translate_literal ctxt' constant_table' head), prems') 
38073  236 
in clause end 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

237 
in (map translate_intro intros', constant_table') end 
38073  238 

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

239 
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

240 
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

241 

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

242 
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

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

244 
fun extend' key (G, visited) = 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

245 
case try (Graph.get_node G) key of 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

246 
SOME v => 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

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

248 
val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v)) 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

249 
val (G', visited') = fold extend' 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

250 
(subtract (op =) (key :: visited) new_edges) (G, key :: visited) 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

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

252 
(fold (Graph.add_edge o (pair key)) new_edges G', visited') 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

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

254 
 NONE => (G, visited) 
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

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

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

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

258 

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

259 
fun generate ensure_groundness ctxt const = 
38073  260 
let 
38731
2c8a595af43e
invocation of values for prolog execution does not require invocation of code_pred anymore
bulwahn
parents:
38729
diff
changeset

261 
fun strong_conn_of gr keys = 
38073  262 
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr) 
38732
3371dbc806ae
moving preprocessing to values in prolog generation
bulwahn
parents:
38731
diff
changeset

263 
val gr = Predicate_Compile_Core.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

264 
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

265 
val scc = strong_conn_of gr' [const] 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

266 
val constant_table = mk_constant_table (flat scc) 
38073  267 
in 
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

268 
apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table) 
38073  269 
end 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

270 

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

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

272 
for sizelimited predicates for enumerating the values of a datatype upto a specific size *) 
38073  273 

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

274 
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

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

276 
 add_ground_typ _ = I 
38073  277 

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

278 
fun mk_relname (Type (Tcon, Targs)) = 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

279 
first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

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

281 

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

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

283 

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

284 
(* This is copied from "pat_completeness.ML" *) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

285 
fun inst_constrs_of thy (T as Type (name, _)) = 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

286 
map (fn (Cn,CT) => 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

287 
Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

288 
(the (Datatype.get_constrs thy name)) 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

289 
 inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

290 

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

291 
fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T 
38728
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

292 

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

293 
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

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

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

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

297 
val (limited, size) = case AList.lookup (op =) limited_types T of 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

298 
SOME s => (true, s) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

299 
 NONE => (false, 0) 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

300 
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

301 
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

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

303 
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

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

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

306 
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

307 
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

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

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

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

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

312 
else [] 
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

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

314 
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

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

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

317 
((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

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

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

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

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

322 
val constrs = inst_constrs_of (ProofContext.theory_of ctxt) T 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

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

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

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

326 
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

327 
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

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

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

330 
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

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

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

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

334 
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

335 

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

336 
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

337 
 replace_ground (Ground (x, T)) = 
182b180e9804
improving ensure_groundness in prolog generation; added further example
bulwahn
parents:
38727
diff
changeset

338 
Rel (mk_relname T, [Var x]) 
38727
c7f5f0b7dc7f
adding very basic transformation to ensure groundness before negations
bulwahn
parents:
38558
diff
changeset

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

340 

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

341 
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

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

343 
val ground_typs = fold (add_ground_typ o snd) p [] 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

344 
val (grs, (_, constant_table')) = 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

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

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

349 

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

350 

38735  351 
(* rename variables to prologfriendly names *) 
352 

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

354 

355 
fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming) 

356 

357 
fun dest_Char (Symbol.Char c) = c 

358 

359 
fun is_prolog_conform v = 

360 
forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v) 

361 

362 
fun mk_conform avoid v = 

363 
let 

364 
val v' = space_implode "" (map (dest_Char o Symbol.decode) 

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

366 
(Symbol.explode v))) 

367 
val v' = if v' = "" then "var" else v' 

368 
in Name.variant avoid (first_upper v') end 

369 

370 
fun mk_renaming v renaming = 

371 
(v, mk_conform (map snd renaming) v) :: renaming 

372 

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

374 
let 

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

376 
val renaming = fold mk_renaming vars [] 

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

378 

379 
val rename_vars_program = map rename_vars_clause 

380 

38073  381 
(* code printer *) 
382 

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

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

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

385 

38735  386 
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

387 
 write_term (Cons c) = c 
38113
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

388 
 write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
81f08bbb3be7
adding basic arithmetic support for prolog code generation
bulwahn
parents:
38112
diff
changeset

389 
 write_term (ArithOp (oper, [a1, a2])) = 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

390 
 write_term (Number n) = string_of_int n 
38073  391 

392 
fun write_rel (pred, args) = 

393 
pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 

394 

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

396 
 write_prem (Rel p) = write_rel p 

397 
 write_prem (NotRel p) = "not(" ^ write_rel p ^ ")" 

398 
 write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r 

399 
 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

400 
 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

401 
 write_prem (NotArithEq (l, r)) = write_term l ^ " =\\= " ^ write_term r 
38073  402 

403 
fun write_clause (head, prem) = 

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

405 

406 
fun write_program p = 

407 
cat_lines (map write_clause p) 

408 

38790  409 
(* query templates *) 
38078  410 

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

411 
(** 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

412 

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

413 
fun swi_prolog_query_first rel vnames = 
38073  414 
"eval : once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^ 
38082  415 
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ 
416 
"\\n', [" ^ space_implode ", " vnames ^ "]).\n" 

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

417 

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

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

419 
"eval : findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^ 
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

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

421 
"writelist([]).\n" ^ 
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

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

423 
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^ 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

424 
"\\n', [" ^ space_implode ", " vnames ^ "]), writelist(T).\n" 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

425 

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

426 
val swi_prolog_prelude = 
38073  427 
"#!/usr/bin/swipl q t main f\n\n" ^ 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

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

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

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

431 
": style_check(atom).\n\n" ^ 
38073  432 
"main : catch(eval, E, (print_message(error, E), fail)), halt.\n" ^ 
433 
"main : halt(1).\n" 

38075  434 

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

435 
(** 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

436 

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

437 
fun yap_query_first rel 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

438 
"eval : once(" ^ rel ^ "(" ^ 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

439 
"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

440 
"\\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

441 

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

442 
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

443 
"#!/usr/bin/yap L\n\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

444 
": 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

445 

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

446 
(* 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

447 

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

448 
fun query system nsols = 
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

449 
case system of 
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

450 
SWI_PROLOG => 
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

451 
(case nsols of NONE => swi_prolog_query_first  SOME n => swi_prolog_query_firstn 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

452 
 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

453 
case nsols of NONE => yap_query_first  SOME 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

454 
error "No support for querying multiple solutions in the prolog system 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

455 

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

456 
fun prelude system = 
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

457 
case system of SWI_PROLOG => swi_prolog_prelude  YAP => 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

458 

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

459 
fun invoke system file_name = 
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

460 
let 
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

461 
val cmd = 
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

462 
case system of SWI_PROLOG => "/usr/local/bin/swipl f "  YAP => "/usr/local/bin/yap L " 
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

463 
in bash_output (cmd ^ file_name) end 
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

464 

38075  465 
(* parsing prolog solution *) 
38790  466 

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

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

468 
Scan.many1 Symbol.is_ascii_digit 
38075  469 

470 
val scan_atom = 

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

471 
Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) 
38075  472 

473 
val scan_var = 

38078  474 
Scan.many1 
475 
(fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) 

38075  476 

38076  477 
val scan_ident = 
478 
Scan.repeat (Scan.one 

479 
(fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)) 

480 

38075  481 
fun dest_Char (Symbol.Char s) = s 
482 

483 
val string_of = concat o map (dest_Char o Symbol.decode) 

484 

38076  485 
val is_atom_ident = forall Symbol.is_ascii_lower 
486 

487 
val is_var_ident = 

488 
forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) 

38078  489 

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

490 
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

491 

38078  492 
fun scan_terms xs = (((scan_term  $$ ",") ::: scan_terms) 
493 
 (scan_term >> single)) xs 

494 
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

495 
((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

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

498 
>> (fn (f, ts) => AppF (string_of f, ts))) 
38078  499 
 (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

500 

38075  501 
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

502 
(Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term) 
38075  503 
o explode 
504 

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

505 
fun parse_solutions sol = 
38075  506 
let 
38077
46ff55ace18c
querying for multiple solutions in values command for prolog execution
bulwahn
parents:
38076
diff
changeset

507 
fun dest_eq s = case space_explode "=" s of 
38075  508 
(l :: r :: []) => parse_term (unprefix " " r) 
38078  509 
 _ => 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

510 
fun parse_solution s = map dest_eq (space_explode ";" s) 
38075  511 
in 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

512 
map parse_solution (fst (split_last (space_explode "\n" sol))) 
38075  513 
end 
38073  514 

515 
(* calling external interpreter and getting results *) 

516 

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

517 
fun run system p query_rel vnames nsols = 
38073  518 
let 
519 
val cmd = Path.named_root 

38735  520 
val p' = rename_vars_program p 
521 
val _ = tracing "Renaming variable names..." 

522 
val renaming = fold mk_renaming vnames [] 

523 
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames 

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

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

525 
val _ = tracing ("Generated prolog program:\n" ^ prog) 
38073  526 
val prolog_file = File.tmp_path (Path.basic "prolog_file") 
527 
val _ = File.write prolog_file prog 

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

528 
val (solution, _) = invoke system (File.shell_path prolog_file) 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

529 
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

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

532 
tss 
38073  533 
end 
534 

38790  535 
(* restoring types in terms *) 
38075  536 

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

537 
fun restore_term ctxt constant_table (Var s, T) = Free (s, T) 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

538 
 restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

539 
 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

540 
 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

541 
 restore_term ctxt constant_table (AppF (f, args), T) = 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

543 
val thy = ProofContext.theory_of ctxt 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

544 
val c = restore_const constant_table f 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

545 
val cT = Sign.the_const_type thy c 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

546 
val (argsT, resT) = strip_type cT 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

547 
val subst = Sign.typ_match thy (resT, T) Vartab.empty 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

548 
val argsT' = map (Envir.subst_type subst) argsT 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

550 
list_comb (Const (c, Envir.subst_type subst cT), 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

551 
map (restore_term ctxt constant_table) (args ~~ argsT')) 
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

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

553 

38790  554 
(* values command *) 
555 

556 
val preprocess_options = Predicate_Compile_Aux.Options { 

557 
expected_modes = NONE, 

558 
proposed_modes = NONE, 

559 
proposed_names = [], 

560 
show_steps = false, 

561 
show_intermediate_results = false, 

562 
show_proof_trace = false, 

563 
show_modes = false, 

564 
show_mode_inference = false, 

565 
show_compilation = false, 

566 
show_caught_failures = false, 

567 
skip_proof = true, 

568 
no_topmost_reordering = false, 

569 
function_flattening = true, 

570 
specialise = false, 

571 
fail_safe_function_flattening = false, 

572 
no_higher_order_predicate = [], 

573 
inductify = false, 

574 
detect_switches = true, 

575 
compilation = Predicate_Compile_Aux.Pred 

576 
} 

577 

38075  578 
fun values ctxt soln t_compr = 
579 
let 

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

580 
val options = !options 
38075  581 
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t 
582 
 _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); 

583 
val (body, Ts, fp) = HOLogic.strip_psplits split; 

584 
val output_names = Name.variant_list (Term.add_free_names body []) 

585 
(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

586 
val output_frees = rev (map2 (curry Free) output_names Ts) 
38075  587 
val body = subst_bounds (output_frees, body) 
588 
val (pred as Const (name, T), all_args) = 

589 
case strip_comb body of 

590 
(Const (name, T), all_args) => (Const (name, T), all_args) 

591 
 (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) 

592 
val vnames = 

593 
case try (map (fst o dest_Free)) all_args of 

594 
SOME vs => vs 

595 
 NONE => error ("Not only free variables in " ^ commas (map (Syntax.string_of_term ctxt) all_args)) 

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

596 
val _ = tracing "Preprocessing specification..." 
3371dbc806ae
moving preprocessing to values in prolog generation
bulwahn
parents:
38731
diff
changeset

597 
val T = Sign.the_const_type (ProofContext.theory_of ctxt) name 
3371dbc806ae
moving preprocessing to values in prolog generation
bulwahn
parents:
38731
diff
changeset

598 
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

599 
val thy' = 
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

600 
Theory.copy (ProofContext.theory_of ctxt) 
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

601 
> Predicate_Compile.preprocess preprocess_options t 
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

602 
val ctxt' = ProofContext.init_global thy' 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

603 
val _ = tracing "Generating prolog program..." 
38797
abe92b33ac9f
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
wenzelm
diff
changeset

604 
val (p, constant_table) = generate (#ensure_groundness options) ctxt' name 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

605 
> (if #ensure_groundness options then 
38797
abe92b33ac9f
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
wenzelm
diff
changeset

606 
add_ground_predicates ctxt' (#limited_types options) 
38789
d171840881fd
added generation of predicates for sizelimited enumeration of values
bulwahn
parents:
38735
diff
changeset

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

608 
val _ = tracing "Running prolog program..." 
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

609 
val tss = run (#prolog_system options) 
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

610 
p (translate_const constant_table name) (map first_upper vnames) soln 
38079
7fb011dd51de
improving translation to prolog; restoring terms from prolog output; adding tracing support
bulwahn
parents:
38078
diff
changeset

611 
val _ = tracing "Restoring terms..." 
38115
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

612 
val empty = Const("Orderings.bot_class.bot", fastype_of t_compr) 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

613 
fun mk_insert x S = 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

614 
Const (@{const_name "Set.insert"}, fastype_of x > fastype_of S > fastype_of S) $ x $ S 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

615 
fun mk_set_compr in_insert [] xs = 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

616 
rev ((Free ("...", fastype_of t_compr)) :: 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

617 
(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

618 
 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

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

620 
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

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

622 
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

623 
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

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

625 
let 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

626 
val uu as (uuN, uuT) = 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

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

628 
HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t)) 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

629 
frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"}))) 
987edb27f449
adding parsing of numbers; improving output of solution without free variables in prolog code generation
bulwahn
parents:
38114
diff
changeset

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

631 
mk_set_compr [] ts 
9c9d14827380
improving output of set comprehensions; adding style_check flags
bulwahn
parents:
38728
diff
changeset

632 
(set_compr :: (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

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

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

636 
foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr [] 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

637 
(map (fn ts => HOLogic.mk_tuple (map (restore_term ctxt' constant_table) (ts ~~ Ts))) tss) []) 
38075  638 
end 
639 

640 
fun values_cmd print_modes soln raw_t state = 

641 
let 

642 
val ctxt = Toplevel.context_of state 

643 
val t = Syntax.read_term ctxt raw_t 

644 
val t' = values ctxt soln t 

645 
val ty' = Term.type_of t' 

646 
val ctxt' = Variable.auto_fixes t' ctxt 

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

647 
val _ = tracing "Printing terms..." 
38075  648 
val p = Print_Mode.with_modes print_modes (fn () => 
649 
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, 

650 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); 

651 
in Pretty.writeln p end; 

652 

653 

654 
(* renewing the values command for Prolog queries *) 

655 

656 
val opt_print_modes = 

657 
Scan.optional (Parse.$$$ "("  Parse.!!! (Scan.repeat1 Parse.xname  Parse.$$$ ")")) []; 

658 

659 
val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag 

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

660 
(opt_print_modes  Scan.optional (Parse.nat >> SOME) NONE  Parse.term 
38075  661 
>> (fn ((print_modes, soln), t) => Toplevel.keep 
38504
76965c356d2a
removed Code_Prolog: modifies global environment setup nonconservatively
haftmann
parents:
38115
diff
changeset

662 
(values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*) 
38075  663 

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

664 
(* 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

665 

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

666 
(* FIXME: large copy of Predicate_Compile_Quickcheck  refactor out commons *) 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

667 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38735
diff
changeset

668 
fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B 
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

669 
 strip_imp_prems _ = []; 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

670 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38735
diff
changeset

671 
fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ A $ B) = strip_imp_concl B 
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

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

673 

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

674 
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

675 

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

676 
fun quickcheck ctxt report t size = 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

677 
let 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

678 
val thy = Theory.copy (ProofContext.theory_of ctxt) 
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

679 
val (vs, t') = strip_abs t 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

680 
val vs' = Variable.variant_frees ctxt [] vs 
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

681 
val Ts = map snd vs' 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

682 
val t'' = subst_bounds (map Free (rev vs'), t') 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

683 
val (prems, concl) = strip_horn t'' 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

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

685 
val full_constname = Sign.full_bname thy constname 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

686 
val constT = Ts > @{typ bool} 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

687 
val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

688 
val const = Const (full_constname, constT) 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

689 
val t = Logic.list_implies 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

690 
(map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

691 
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

692 
val tac = fn _ => Skip_Proof.cheat_tac thy1 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

693 
val intro = Goal.prove (ProofContext.init_global thy1) (map fst vs') [] t tac 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

694 
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

695 
val thy3 = Predicate_Compile.preprocess preprocess_options const thy2 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

696 
val ctxt' = ProofContext.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

697 
val _ = tracing "Generating prolog program..." 
38797
abe92b33ac9f
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
wenzelm
diff
changeset

698 
val (p, constant_table) = generate true ctxt' full_constname 
abe92b33ac9f
merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
wenzelm
diff
changeset

699 
> add_ground_predicates ctxt' (#limited_types (!options)) 
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

700 
val _ = tracing "Running prolog program..." 
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

701 
val [ts] = run (#prolog_system (!options)) 
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

702 
p (translate_const constant_table full_constname) (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

703 
val _ = tracing "Restoring terms..." 
38755
a37d39fe32f8
standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;
wenzelm
parents:
38735
diff
changeset

704 
val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts)) 
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

705 
val empty_report = ([], false) 
4b8fd91ea59a
added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system
bulwahn
parents:
38732
diff
changeset

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

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

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

709 

38073  710 
end; 