Lines Matching refs:function
18 (* Debug : Input to a lower function was of the wrong form *)
36 (* Create the different levels of exception given a function and message *)
66 (* Prints a function trace *)
158 (* function : *)
159 (* Represents a polytypic function, also holds its induction principle *)
170 type function = {const : term, definition : thm, induction : (thm * (term * (term * hol_type)) list) option}
172 type functions = (hol_type,(string,function) dict ref) dict;
186 (* Level 3 : Output most intermediate results and function calls *)
259 (* Builds the graph of elements reachable from ''a under the function *)
371 (* Pushes all function applications over a conditional *)
718 " are not used in the function"))
722 " are used in the function but not specified in the axiom"))
882 (* b) the function must be defined for all constructors of all *)
895 (* Returns true if the term is a function term and every recusive call: *)
899 (* has the function (f0 in this case) defined in the conjunction *)
971 (* rewrite occurs for a variable in the constructor of the function *)
982 (* the pair is of the form pair f0 f1 (L/R x) then a new function is *)
992 (* Checks to see if a pair term in a function requires splitting, the *)
993 (* 'target' function deals with decoding and detecting whereas the *)
994 (* 'source' function deals with encoding *)
1038 ("Term is not a conjunction of function (not constant) definitions",
1044 val _ = assert' [("Constants specified in higher order function: " ^ thm_to_string hfun_def,
1163 raise (debug_exn ("Unable to split function, neither conv applies to term:\n " ^
1165 "\n remaining function defs: " ^
1173 "\nis not a valid source or target function",
1180 "\nis not a fully expanded source or target function,\n" ^
1181 "perhaps higher functions are missing from the function definitions given?",
1228 (* Given a list of function clauses returns a list of mapping functions *)
1233 (* specified earlier proves a mutually recursive function of the form: *)
1240 (* Given a mutually recursive theorem of the form output by the function *)
1265 ("Second argument is not a list of function clauses",all (is_eq o snd o strip_forall)),
1266 ("Second argument is not a list of function (not constant) definitions",
1441 (debug_exn "Recursion theorem has a different number of clauses than the function clauses supplied")
1456 [("x is free in the function body, should be either R x or L x, in function clause:\n" ^
1496 [("Recursion theorem has a different number of clauses than the function clauses supplied",
1647 (* Given a function definition term with some clauses that are simply: *)
1759 (* Finds all terms in the clause such that there is a function call: *)
1895 (* (string,function) dict ref *)
1902 (* add_coding_function : hol_type -> hol_type -> string -> function -> unit *)
1908 (* Tests for the existence of a coding function, adds a new coding *)
1909 (* function and returns a function's definition, constant and principle *)
1920 (* add_source_function : hol_type -> string -> function -> unit *)
1925 (* Tests for the existence of a source function, adds a new source *)
1926 (* function and returns a function's definition, constant and principle *)
1976 ref (mkDict String.compare : (string,function) dict)) ;
1987 ref (mkDict String.compare : (string,function) dict)) ;
2006 (* This function performs a breadth-first search, finding the most precise *)
2026 "No sub-type exists such that the function given holds")
2057 ("The function " ^ name ^
2060 | SOME function => inst_function function t;
2067 ("The function " ^ name ^
2078 ("The function " ^ name ^ "(" ^ type_to_string t ^
2089 ("The function " ^ name ^ "(" ^ type_to_string t ^
2095 let val _ = type_trace 1 ("Adding coding function, " ^ name ^ ", for type: "
2106 fun add_coding_function target t name function = add_coding_function_precise target (base_type t handle _ => t) name function
2161 ("The function " ^ name ^ " has not been defined for the type " ^ type_to_string t))
2162 | SOME function => inst_function function t
2173 ("The function " ^ name ^ " has not been defined for any sub-type of " ^
2183 ("The function " ^ name ^ "(" ^ type_to_string t ^
2193 ("The function " ^ name ^ "(" ^ type_to_string t ^
2199 val _ = type_trace 1 ("Adding source function, " ^ name ^ ", for type: " ^
2381 (* Loop checking for function generators *)
2383 (* Simply provides a function 'check_loop' that when giving an identifying *)
2384 (* string for a function can detect whether the function is looping. *)
2423 (hol_type -> function)) list ref) dict ref) dict ref
2425 fun add_coding_function_generator target (name:string) (predicate:hol_type -> bool) (generator:hol_type -> function) =
2442 (hol_type -> function)) list ref) dict ref
2444 fun add_source_function_generator name (predicate:hol_type -> bool) (generator : hol_type -> function) =
2455 ("No coding function generator exists for functions named " ^ name ^
2465 let val function = if exists_coding_function_precise target t name
2468 "Generating function " ^ name ^ " for translation " ^
2474 else add_coding_function_precise target t name function
2480 ("Experienced a loop whilst generating the coding function " ^ name ^
2487 ("No source function generator exists for functions named " ^ name ^
2494 let val function = if exists_source_function_precise t name
2497 "Generating function " ^ name ^ " for type " ^ type_to_string t ^ "\n") ;
2502 else add_source_function_precise t name function
2508 ("Experienced a loop whilst generating the source function " ^ name ^
2688 (* make_term : Makes a function term of type :target -> 'a *)
2689 (* get_def : Returns the definition of a previously defined function *)
2697 (* Each function returns a fully instantiated definition, however *)
2709 (* uses 'prove_rec_fn_exists' to form the mutual recursive function and *)
2727 (* Given a mapping from predicates to function constants and types, *)
2734 (* Given a list mapping function terms to types and a theorem *)
2739 (* Given a pair function, the list of proved split terms and a the *)
2807 ("Sub-function returned by expanded_function_def not used in main function"))
2828 ("Could not find a match for the function:\n" ^ thm_to_string main ^
2840 let val name = ("conv (supplied function)")
2848 "\nis not a correct source function, see help for details"))
2851 "\nis not a correct target function, see help for details"))
2864 val _ = type_trace 3 ("Target function: \n" ^ term_to_string term ^ "\n")
2938 (* A function *not* in funcs is supplied with one in funcs *)
2972 ("Proof term is not an implication from a function definition to a conjunction of function equalities",
3005 fun prove_split_term mapping induction function (dead_thm,dead_value) term =
3011 ("Proof term is not an implication from a function definition to a conjunction of function equalities",
3069 val clauses = (CONJUNCTS o SPEC_ALL) function
3072 "The function given does not exactly match the induction theorem"
3082 "The term given does not match the induction theorem and function")
3143 "\nusing the function set: " ^ xlist_to_string thm_to_string functions ^
3146 val function = expanded_function_def conv create_conv get_def t
3150 val th = prove_split_term mapping induction function (dead_thm,dead_value) ((fst o dest_imp_only o concl) sh')
3153 "\nusing the expanded function definition: " ^ (thm_to_string function) ^
3175 "is not an implication from a function definition to a conjunction of function equalities"),
3296 ("Could not find type for function: " ^ term_to_string func))
3310 let fun mkExn s = raise (mkStandardExn "get_ind (supplied function)" s)
3385 ("Can't create function for type " ^ type_to_string t ^ " as this is dependent upon type " ^
3387 " for which no function is returned by get_def"))) handle Empty => ()
3506 (* Given the name of the function the induction is based around, the name *)
3507 (* of the theorem being proved, a function to generate conclusions, the *)
3519 (* Simply prove functions given a function to generate conclusions, a *)