(******************************************************************************) (* FILE : counterexample.ml *) (* DESCRIPTION : Simple counterexample checker *) (* Based on ideas and suggestions from S. Wilson *) (* *) (* READS FILES : *) (* WRITES FILES : *) (* *) (* AUTHOR : P. Papapanagiotou (University of Edinburgh) *) (* DATE : July 2009 *) (******************************************************************************) (*----------------------------------------------------------------------------*) (* Reference of how many examples will be tried on each check. *) (* Set to 0 to turn off counterexample checker. *) (*----------------------------------------------------------------------------*) let counter_check_num = ref 5;; let counter_checks t = counter_check_num := t;; (*----------------------------------------------------------------------------*) (* Reference to count how many counterexamples were found during a proof. *) (*----------------------------------------------------------------------------*) let counterexamples = ref 0;; let inc_counterexamples () = counterexamples := !counterexamples + 1 ; ();; (*----------------------------------------------------------------------------*) (* inst_type *) (*----------------------------------------------------------------------------*) (* Hacky function to instantiate types. *) (* I'm surprised there is no such function in HOL Light (or perhaps I just *) (* haven't found it yet?). *) (*----------------------------------------------------------------------------*) (* Creates a variable of the given type. Instantiates the term using "inst" *) (* then returns the type of the resulting term. *) (*----------------------------------------------------------------------------*) let inst_type : (hol_type * hol_type) list -> hol_type -> hol_type = fun ins ty -> let tm = mk_var ("x",ty) in let itm = inst ins tm in type_of itm;; (*----------------------------------------------------------------------------*) (* shell_type_match *) (*----------------------------------------------------------------------------*) (* Does a deep search to check if a type can be properly grounded to a *) (* combination of types defined in the shell. *) (* Returns the type instantiation pairs to make it happen. *) (* Variable types are instantiated by `:num`. *) (*----------------------------------------------------------------------------*) (* If the type is an instance of a type constructor (is_type) then it is *) (* split. The name of the constructor is looked up in the system shells list. *) (* The arguments are checked recursively. *) (* If it's not an instance of a type constructor, we try to replace it by *) (* `:num`. *) (*----------------------------------------------------------------------------*) let rec shell_type_match : hol_type -> (hol_type * hol_type) list = fun ty -> if (is_type ty) then let tys,tyargs = dest_type ty in let info = try sys_shell_info tys with Failure _ -> failwith ("No shell defined for type '" ^ (string_of_type ty) ^ "'") in itlist union (map shell_type_match tyargs) [] else try type_match ty `:num` [] with Failure _ -> failwith ("Unknown type '" ^ (string_of_type ty) ^ "' that doesn't match 'num'!");; (*----------------------------------------------------------------------------*) (* HL_rewrite_ground_term : term -> term *) (* *) (* Uses HOL Light's REWRITE_CONV to rewrite a ground term. *) (* The function and accessor definitions are used as rewrite rules. *) (* This reduces valid expressions to `T`. *) (*----------------------------------------------------------------------------*) let HL_rewrite_ground_term tm = (* ((proof_print_newline) o (proof_print_term) o (proof_print_string "Checking:")) tm ;*) if (frees tm = []) then (* let rules = (union ((flat o defs) ()) (all_accessor_thms ())) *) (* let rules = (union (rewrite_rules ()) (all_accessor_thms ())) *) let numred = try (rhs o concl o NUM_REDUCE_CONV) tm with Failure _ -> tm in if (is_T numred) then numred else let rew = REWRITE_CONV (union (rewrite_rules ()) (all_accessor_thms ())) in (rhs o concl o rew) tm else failwith ("rewrite_ground_term: free vars in term: " ^ (string_of_term tm));; let HL_rewrite_ground_term' tm = if (frees tm = []) then (* let rules = (union ((flat o defs) ()) (all_accessor_thms ())) *) let rules = (union ((flat o defs) ()) (all_accessor_thms ())) in let arith_rules = [PRE;ADD;MULT;EXP;EVEN;ODD;LE;LT;GE;GT;SUB] in (* Need to apply preprocessing similar to add_def in environment.ml *) let rew = REWRITE_CONV (ARITH :: (subtract rules arith_rules)) in (rhs o concl o rew) tm else failwith ("rewrite_ground_term: free vars in term: " ^ (string_of_term tm));; (*----------------------------------------------------------------------------*) (* random_example : int -> hol_type -> term *) (*----------------------------------------------------------------------------*) (* Creates a random example of a given type. *) (* The first argument is a maximum depth so as to control the size of the *) (* example. *) (*----------------------------------------------------------------------------*) (* Uses "shell_type_match" in order to ground the type to a combination of *) (* types defined as shells. Therefore, all variable types are instantiated to *) (* `:num`. *) (* Instantiates the arg_types of the shell for each constructor, then uses *) (* mk_cons_type to create proper types for the constructors. Having those and *) (* by using mk_mconst creates the constructors as terms. *) (* random_example is called recursively for every constructor argument, while *) (* decreasing the maxdepth to ensure termination. *) (* If maxdepth is reached, we just pick randomly one of the base *) (* constructors. *) (*----------------------------------------------------------------------------*) (* NOTE: The current version can still afford a few optimisations. *) (* eg. The preprocessing so as to ground the given type should only happen *) (* once. *) (* NOTE: We could optimise this function further by accommodating the *) (* constructors as terms (rather than or in addition to strings) within the *) (* shell. *) (*----------------------------------------------------------------------------*) let random_example : int -> hol_type -> term = let rec random_example': int->int->hol_type->term = fun origdepth maxdepth ty -> let tyi = shell_type_match ty in let ty' = inst_type tyi ty in let tystr,typarams = dest_type ty' in let sinfo = sys_shell_info tystr in let ocons = shell_constructors sinfo in let sh_arg_types = shell_arg_types sinfo in let arg_type_pairs = zip sh_arg_types typarams in let arg_types_matches = try itlist (fun (x,y) l -> type_match x y l) arg_type_pairs tyi with Failure _ -> failwith "Shell argument types cannot be matched." in let mk_cons_type = fun arglist -> List.fold_left (fun ty i -> mk_type ("fun",[i;ty])) ty' (rev arglist) in let inst_cons = map (fun x,y,_ -> x,map (inst_type arg_types_matches) y) ocons in let mk_cons = fun x,y -> try let n = num_of_string x in (mk_numeral n),y with Failure _ -> mk_mconst(x,(mk_cons_type y)),y in let cons = map mk_cons inst_cons in let terminal_filter = fun (_,l) -> (l=[]) in let tcons,ntcons = partition terminal_filter cons in if (maxdepth > 1) then let prob = 200/((maxdepth-1)*3) in (* let newdepth = origdepth / (length cons) in*) let newdepth = maxdepth - 1 in let selcons = if ((Random.int 100) <= prob) then tcons else ntcons in let cconstm,cconsargs = List.nth selcons (Random.int (length selcons)) in let args = (map (random_example' origdepth newdepth) cconsargs) in List.fold_left (fun x y -> mk_comb (x,y)) cconstm args else (fst o hd) tcons in fun maxdepth ty -> random_example' maxdepth maxdepth ty;; (* print_string "*" ; print_term cconstm ; print_string "*" ; print_type (type_of cconstm); print_newline (); *) (* map (fun x -> print_term x ; print_string ":" ; print_type (type_of x); print_newline()) args ; *) (* print_newline (); *) let random_grounding maxdepth tm = let vars = frees tm in let types = map type_of vars in let examples = map (random_example maxdepth) types in let pairs = zip vars examples in let insts = map (fun v,e -> term_match [] v e) pairs in itlist instantiate insts tm;; let counter_check_once maxdepth tm = let tm' = random_grounding maxdepth tm in let tm'' = HL_rewrite_ground_term tm' in if (is_T(tm'')) then true else let junk = warn (!proof_printing) ("Found counterexample for " ^ string_of_term(tm) ^ " : " ^ string_of_term(tm')) in inc_counterexamples() ; false;; let rec counter_check_n maxdepth n tm = if (n<=0) then true else if (counter_check_once maxdepth tm) then counter_check_n maxdepth (n-1) tm else false;; let counter_check maxdepth tm = counter_check_n maxdepth !counter_check_num tm;;