1 (******************************************************************************)
2 (* FILE : counterexample.ml *)
3 (* DESCRIPTION : Simple counterexample checker *)
4 (* Based on ideas and suggestions from S. Wilson *)
6 (* READS FILES : <none> *)
7 (* WRITES FILES : <none> *)
9 (* AUTHOR : P. Papapanagiotou (University of Edinburgh) *)
10 (* DATE : July 2009 *)
11 (******************************************************************************)
13 (*----------------------------------------------------------------------------*)
14 (* Reference of how many examples will be tried on each check. *)
15 (* Set to 0 to turn off counterexample checker. *)
16 (*----------------------------------------------------------------------------*)
18 let counter_check_num = ref 5;;
20 let counter_checks t =
21 counter_check_num := t;;
24 (*----------------------------------------------------------------------------*)
25 (* Reference to count how many counterexamples were found during a proof. *)
26 (*----------------------------------------------------------------------------*)
28 let counterexamples = ref 0;;
30 let inc_counterexamples () = counterexamples := !counterexamples + 1 ; ();;
33 (*----------------------------------------------------------------------------*)
35 (*----------------------------------------------------------------------------*)
36 (* Hacky function to instantiate types. *)
37 (* I'm surprised there is no such function in HOL Light (or perhaps I just *)
38 (* haven't found it yet?). *)
39 (*----------------------------------------------------------------------------*)
40 (* Creates a variable of the given type. Instantiates the term using "inst" *)
41 (* then returns the type of the resulting term. *)
42 (*----------------------------------------------------------------------------*)
44 let inst_type : (hol_type * hol_type) list -> hol_type -> hol_type =
46 let tm = mk_var ("x",ty) in
47 let itm = inst ins tm in
51 (*----------------------------------------------------------------------------*)
52 (* shell_type_match *)
53 (*----------------------------------------------------------------------------*)
54 (* Does a deep search to check if a type can be properly grounded to a *)
55 (* combination of types defined in the shell. *)
56 (* Returns the type instantiation pairs to make it happen. *)
57 (* Variable types are instantiated by `:num`. *)
58 (*----------------------------------------------------------------------------*)
59 (* If the type is an instance of a type constructor (is_type) then it is *)
60 (* split. The name of the constructor is looked up in the system shells list. *)
61 (* The arguments are checked recursively. *)
62 (* If it's not an instance of a type constructor, we try to replace it by *)
64 (*----------------------------------------------------------------------------*)
66 let rec shell_type_match : hol_type -> (hol_type * hol_type) list =
69 let tys,tyargs = dest_type ty in
70 let info = try sys_shell_info tys
71 with Failure _ -> failwith ("No shell defined for type '" ^
72 (string_of_type ty) ^ "'") in
73 itlist union (map shell_type_match tyargs) []
75 try type_match ty `:num` []
76 with Failure _ -> failwith ("Unknown type '" ^
77 (string_of_type ty) ^ "' that doesn't match 'num'!");;
80 (*----------------------------------------------------------------------------*)
81 (* HL_rewrite_ground_term : term -> term *)
83 (* Uses HOL Light's REWRITE_CONV to rewrite a ground term. *)
84 (* The function and accessor definitions are used as rewrite rules. *)
85 (* This reduces valid expressions to `T`. *)
86 (*----------------------------------------------------------------------------*)
88 let HL_rewrite_ground_term tm =
89 (* ((proof_print_newline) o (proof_print_term) o (proof_print_string "Checking:")) tm ;*)
90 if (frees tm = []) then
91 (* let rules = (union ((flat o defs) ()) (all_accessor_thms ())) *)
92 (* let rules = (union (rewrite_rules ()) (all_accessor_thms ())) *)
93 let numred = try (rhs o concl o NUM_REDUCE_CONV) tm with Failure _ -> tm in
94 if (is_T numred) then numred else
95 let rew = REWRITE_CONV (union (rewrite_rules ()) (all_accessor_thms ()))
96 in (rhs o concl o rew) tm
97 else failwith ("rewrite_ground_term: free vars in term: " ^ (string_of_term tm));;
101 let HL_rewrite_ground_term' tm =
102 if (frees tm = []) then
103 (* let rules = (union ((flat o defs) ()) (all_accessor_thms ())) *)
104 let rules = (union ((flat o defs) ()) (all_accessor_thms ())) in
105 let arith_rules = [PRE;ADD;MULT;EXP;EVEN;ODD;LE;LT;GE;GT;SUB] in
106 (* Need to apply preprocessing similar to add_def in environment.ml *)
107 let rew = REWRITE_CONV (ARITH :: (subtract rules arith_rules))
108 in (rhs o concl o rew) tm
109 else failwith ("rewrite_ground_term: free vars in term: " ^ (string_of_term tm));;
111 (*----------------------------------------------------------------------------*)
112 (* random_example : int -> hol_type -> term *)
113 (*----------------------------------------------------------------------------*)
114 (* Creates a random example of a given type. *)
115 (* The first argument is a maximum depth so as to control the size of the *)
117 (*----------------------------------------------------------------------------*)
118 (* Uses "shell_type_match" in order to ground the type to a combination of *)
119 (* types defined as shells. Therefore, all variable types are instantiated to *)
121 (* Instantiates the arg_types of the shell for each constructor, then uses *)
122 (* mk_cons_type to create proper types for the constructors. Having those and *)
123 (* by using mk_mconst creates the constructors as terms. *)
124 (* random_example is called recursively for every constructor argument, while *)
125 (* decreasing the maxdepth to ensure termination. *)
126 (* If maxdepth is reached, we just pick randomly one of the base *)
128 (*----------------------------------------------------------------------------*)
129 (* NOTE: The current version can still afford a few optimisations. *)
130 (* eg. The preprocessing so as to ground the given type should only happen *)
132 (* NOTE: We could optimise this function further by accommodating the *)
133 (* constructors as terms (rather than or in addition to strings) within the *)
135 (*----------------------------------------------------------------------------*)
137 let random_example : int -> hol_type -> term =
138 let rec random_example': int->int->hol_type->term =
139 fun origdepth maxdepth ty ->
140 let tyi = shell_type_match ty in
141 let ty' = inst_type tyi ty in
142 let tystr,typarams = dest_type ty' in
143 let sinfo = sys_shell_info tystr in
144 let ocons = shell_constructors sinfo in
145 let sh_arg_types = shell_arg_types sinfo in
147 let arg_type_pairs = zip sh_arg_types typarams in
148 let arg_types_matches = try
149 itlist (fun (x,y) l -> type_match x y l) arg_type_pairs tyi
150 with Failure _ -> failwith "Shell argument types cannot be matched." in
152 let mk_cons_type = fun arglist ->
153 List.fold_left (fun ty i -> mk_type ("fun",[i;ty])) ty' (rev arglist) in
154 let inst_cons = map (fun x,y,_ -> x,map (inst_type arg_types_matches) y) ocons in
155 let mk_cons = fun x,y ->
156 try let n = num_of_string x in (mk_numeral n),y
157 with Failure _ -> mk_mconst(x,(mk_cons_type y)),y in
158 let cons = map mk_cons inst_cons in
160 let terminal_filter = fun (_,l) -> (l=[]) in
161 let tcons,ntcons = partition terminal_filter cons in
163 if (maxdepth > 1) then
164 let prob = 200/((maxdepth-1)*3) in
165 (* let newdepth = origdepth / (length cons) in*)
166 let newdepth = maxdepth - 1 in
167 let selcons = if ((Random.int 100) <= prob) then tcons else ntcons in
168 let cconstm,cconsargs = List.nth selcons (Random.int (length selcons)) in
169 let args = (map (random_example' origdepth newdepth) cconsargs) in
170 List.fold_left (fun x y -> mk_comb (x,y)) cconstm args
173 in fun maxdepth ty -> random_example' maxdepth maxdepth ty;;
175 (* print_string "*" ; print_term cconstm ; print_string "*" ; print_type (type_of cconstm); print_newline (); *)
176 (* map (fun x -> print_term x ; print_string ":" ; print_type (type_of x); print_newline()) args ; *)
177 (* print_newline (); *)
180 let random_grounding maxdepth tm =
181 let vars = frees tm in
182 let types = map type_of vars in
183 let examples = map (random_example maxdepth) types in
184 let pairs = zip vars examples in
185 let insts = map (fun v,e -> term_match [] v e) pairs in
186 itlist instantiate insts tm;;
189 let counter_check_once maxdepth tm =
190 let tm' = random_grounding maxdepth tm in
191 let tm'' = HL_rewrite_ground_term tm' in
192 if (is_T(tm'')) then true else let junk =
193 warn (!proof_printing) ("Found counterexample for " ^ string_of_term(tm) ^ " : " ^ string_of_term(tm')) in
194 inc_counterexamples() ; false;;
196 let rec counter_check_n maxdepth n tm =
198 else if (counter_check_once maxdepth tm) then counter_check_n maxdepth (n-1) tm
201 let counter_check maxdepth tm =
202 counter_check_n maxdepth !counter_check_num tm;;