Lines Matching defs:target
168 {target : hol_type, induction : thm, recursion : thm, left : term, right : term, predicate : term, bottom : term, bottom_thm : thm};
993 (* 'target' function deals with decoding and detecting whereas the *)
1173 "\nis not a valid source or target function",
1180 "\nis not a fully expanded source or target function,\n" ^
1538 val target = #target scheme
1540 val x = mk_var("x",target)
1542 raise (mkDebug ("Predicate for translation scheme " ^ type_to_string target ^
1544 fun mkP y p = mk_comb(mk_var("P" ^ (int_to_string p),target --> ``:bool``),beta_conv (mk_comb(y,x)))
1545 fun mkP_var n = mk_comb(mk_var("P" ^ (int_to_string n),target --> ``:bool``),x)
1570 GENL (map (fn (n,_) => mk_var("P" ^ (int_to_string n),target --> ``:bool``)) call_graph)
1700 let val target_type = #target scheme
1959 fun get_translations target =
1960 Binarymap.find (!codingBase,target) handle NotFound => (raise (translation_scheme_not_found target))
1963 fun get_translation_scheme target = snd (get_translations target)
1964 fun exists_translation_precise target t =
1965 case (Binarymap.peek(!((fst o fst) (get_translations target)),cannon_type t))
1968 fun exists_translation target t = exists_translation_precise target (vbase_type t)
1969 fun add_translation target t =
1970 if exists_translation target t then
1972 ("The translation " ^ type_to_string target ^ " --> " ^ type_to_string t ^
1974 else let val ((fbase,tbase),_) = get_translations target
1980 fun add_translation_precise target t =
1981 if exists_translation_precise target t then
1983 ("The translation " ^ type_to_string target ^ " --> " ^ type_to_string t ^
1985 else let val ((fbase,tbase),_) = get_translations target
1991 fun get_translation_precise target t =
1992 case (Binarymap.peek(!((fst o fst) (get_translations target)), cannon_type t))
1993 of NONE => raise (translation_not_found target t)
1995 fun get_translation target t = get_translation_precise target (vbase_type t)
1996 fun get_theorems_precise target t =
1997 case (Binarymap.peek(!((snd o fst) (get_translations target)),cannon_type t))
1998 of NONE => raise (translation_not_found target t)
2000 fun get_theorems target t = get_theorems_precise target (vbase_type t)
2001 fun get_translation_types target =
2002 map fst (Binarymap.listItems (! (fst (fst (get_translations target)))));
2032 fun exists_coding_function_precise target t name =
2033 if (exists_translation_precise target t)
2035 (case (Binarymap.peek(!(get_translation_precise target t),name))
2040 fun exists_coding_function target t name =
2042 (C (exists_coding_function_precise target) name)) t
2054 fun get_coding_function_precise target t name =
2055 case (Binarymap.peek(!(get_translation_precise target t),name))
2059 type_to_string target ^ " --> " ^ type_to_string t))
2062 fun get_coding_function target t name =
2063 inst_function (get_coding_function_precise target
2065 (C (exists_coding_function_precise target) name) t) name) t
2069 type_to_string target ^ " --> " ^ type_to_string t))
2071 fun get_coding_function_def target t name =
2072 #definition (get_coding_function target t name)
2073 fun get_coding_function_const target t name =
2074 #const (get_coding_function target t name)
2075 fun get_coding_function_induction target t name =
2076 case (#induction (get_coding_function target t name))
2079 " --> " ^ type_to_string target ^
2082 fun get_coding_function_precise_def target t name =
2083 #definition (get_coding_function_precise target t name)
2084 fun get_coding_function_precise_const target t name =
2085 #const (get_coding_function_precise target t name)
2086 fun get_coding_function_precise_induction target t name =
2087 case (#induction (get_coding_function_precise target t name))
2090 " --> " ^ type_to_string target ^
2094 fun add_coding_function_precise target t name {const,definition,induction} =
2097 val base = get_translation_precise target t handle e => wrapException "add_coding_function_precise" e
2106 fun add_coding_function target t name function = add_coding_function_precise target (base_type t handle _ => t) name function
2111 fun exists_coding_theorem_precise target t name =
2112 if exists_translation_precise target t then
2113 case (Binarymap.peek(!(get_theorems_precise target t),name))
2117 fun exists_coding_theorem target t name =
2118 exists_coding_theorem_precise target t name orelse
2119 exists_coding_theorem_precise target (base_type t handle _ => t) name
2121 fun add_coding_theorem_precise target t name thm =
2124 val _ = if exists_translation_precise target t then () else add_translation_precise target t
2125 val base = get_theorems_precise target t handle e => wrapException "add_coding_theorem_precise" e
2130 fun add_coding_theorem target t name thm = add_coding_theorem_precise target (base_type t handle _ => t) name thm
2132 fun get_coding_theorem_precise target t name =
2133 case (Binarymap.peek(!(get_theorems_precise target t),name))
2135 ("The theorem " ^ name ^ " does not exists for the translation " ^ type_to_string target ^ " --> " ^
2139 fun get_coding_theorem target t name =
2140 get_coding_theorem_precise target
2141 (most_precise_type (C (exists_coding_theorem_precise target) name) t)
2254 fun remove_coding_theorem_precise target t name =
2255 let val base = get_theorems_precise target t handle e => wrapException "remove_coding_theorem_precise" e
2282 fun split_size_thm target size_thm =
2298 val _ = if type_of xvar = target then () else raise (size_err
2300 " and not " ^ type_to_string target))
2304 fun make_recursion (specced,ml,left,right,p_term,xvar) target size_thm =
2305 let val f = mk_var("f",target --> beta) handle e => wrap1 e
2306 val f0 = mk_var("f0",target --> beta --> beta --> beta) handle e => wrap1 e
2309 mk_comb(mk_var("c0",target --> beta),xvar))) handle e => wrap1 e
2310 val measure = mk_comb(mk_const("measure",(target --> num) --> target --> target --> bool),ml)
2312 val decode_var = mk_var("decode",target --> beta) handle e => wrap1 e
2314 type_of measure --> type_of template --> target --> beta),
2335 fun make_induction (specced,ml,left,right,p_term,xvar) target size_thm =
2336 let val pred = mk_var("P",target --> bool) handle e => wrap2 e
2340 val measure = mk_comb(mk_const("measure",(target --> num) --> target --> target --> bool),ml)
2361 fun add_translation_scheme target size_thm dead_thm =
2362 let val (specced,ml,left,right,p_term,xvar) = split_size_thm target size_thm
2366 Binarymap.insert (!codingBase,target,
2369 {target = target,
2370 induction = make_induction (specced,ml,left,right,p_term,xvar) target size_thm,
2371 recursion = make_recursion (specced,ml,left,right,p_term,xvar) target size_thm,
2425 fun add_coding_function_generator target (name:string) (predicate:hol_type -> bool) (generator:hol_type -> function) =
2426 let val _ = case (Binarymap.peek (!coding_function_generators,target))
2427 of NONE => coding_function_generators := Binarymap.insert(!coding_function_generators,target,ref (mkDict String.compare))
2429 val generators = Binarymap.find (!coding_function_generators,target)
2454 fun err name target t = mkStandardExn "get_coding_function_generator"
2456 " in the translation: " ^ type_to_string target ^
2458 fun get_coding_function_generator target name t =
2459 case (Binarymap.peek(!coding_function_generators,target))
2460 of NONE => raise (err name target t)
2462 of NONE => raise (err name target t)
2463 | SOME x => (snd (first_e (err name target t) (fn (x,y) => x t) (!x)))
2464 fun gcf target name t =
2465 let val function = if exists_coding_function_precise target t name
2466 then get_coding_function_precise target t name
2469 (type_to_string target) ^ " --> " ^ type_to_string t ^ "\n") ;
2470 (get_coding_function_generator target name t) t)
2472 if exists_coding_function_precise target t name
2474 else add_coding_function_precise target t name function
2477 fun generate_coding_function target name t =
2478 check_loop ("gcf" ^ name ^ type_to_string (cannon_type target)) t (gcf target name)
2481 " for type " ^ type_to_string target ^
2527 fun setup target name =
2528 let val _ = case (Binarymap.peek (!coding_theorem_generators,target))
2529 of NONE => coding_theorem_generators := Binarymap.insert(!coding_theorem_generators,target,ref (mkDict String.compare))
2531 val generators = Binarymap.find (!coding_theorem_generators,target)
2539 fun set_coding_theorem_conclusion target name mk_conc =
2540 let val (conc,list) = setup target name
2544 fun exists_coding_theorem_conclusion target name = isSome(!(fst(setup target name)))
2545 fun get_coding_theorem_conclusion target name = valOf(!(fst(setup target name)))
2546 fun add_coding_theorem_generator target (name:string) (predicate:hol_type -> bool) (generator:hol_type -> thm) =
2547 let val (conc,list) = setup target name
2589 fun err name target t = mkStandardExn "get_coding_theorem_generator"
2591 " in the translation: " ^ type_to_string target ^
2593 fun get_coding_theorem_generator target name t =
2594 case (Binarymap.peek(!coding_theorem_generators,target))
2595 of NONE => raise (err name target t)
2597 of NONE => raise (err name target t)
2598 | SOME x => (snd (first_e (err name target t)
2600 fun gct target name t =
2604 exists_coding_theorem_precise target t name
2605 then () else (gct target name (base_type t) ; ())
2606 val theorem = if exists_coding_theorem_precise target t name
2607 then get_coding_theorem_precise target t name
2608 else (get_coding_theorem_generator target name t) t
2609 val mtheorem = if exists_coding_theorem_conclusion target name
2610 then MATCH_CONC theorem (get_coding_theorem_conclusion target name t)
2616 term_to_string (get_coding_theorem_conclusion target name t)))
2618 val _ = if exists_coding_theorem_precise target t name
2620 else add_coding_theorem_precise target t name mtheorem
2631 fun generate_coding_theorem target name t =
2632 check_loop ("gct" ^ name ^ type_to_string (cannon_type target)) t (gct target name)
2635 " for type " ^ type_to_string target ^
2688 (* make_term : Makes a function term of type :target -> 'a *)
2710 (* 'target' uses 'prove_induction_recursion_thms', and as such also *)
2711 (* returns a mapping and theorem of induction over the target type. *)
2851 "\nis not a correct target function, see help for details"))
2888 val eq_thm1 = mk_eq_thm "target" mk_term get_def get_func (wrap_conv false "target" conv) t
3106 (* Dead value theorems (only used in making target functions) *)
3422 fun mk_coding_functions name mk_term get_func conv create_conv target t =
3423 let val get_def = C (get_coding_function_def target) name
3428 val dead_thm = #bottom_thm (get_translation_scheme target)
3429 val dead_value = #bottom (get_translation_scheme target)
3430 val result = complete_function name mk_term (C (get_coding_function_induction target) name)
3433 store_funcs name (fn t => fn (term,thm) => add_coding_function target t name
3438 fun mk_target_functions name mk_term get_func conv create_conv target t =
3439 let val get_def = C (get_coding_function_def target) name
3440 val get_ind = C (get_coding_function_induction target) name
3443 val dead_thm = #bottom_thm (get_translation_scheme target)
3444 val dead_value = #bottom (get_translation_scheme target)
3446 (get_translation_scheme target) t handle e => wrap e
3450 store_funcs name (fn t => fn (term,thm) => add_coding_function target t name
3462 fun add_compound_coding_function_generator name mk_term get_func conv create_conv target =
3463 add_coding_function_generator target name (can TypeBase.constructors_of)
3467 val _ = map (generate_coding_function target name o base_type) required
3469 mk_coding_functions name mk_term get_func conv create_conv target t
3471 get_coding_function_precise target t name));
3472 fun add_compound_target_function_generator name mk_term get_func conv create_conv target =
3473 add_coding_function_generator target name (can TypeBase.constructors_of)
3477 val _ = map (generate_coding_function target name o base_type) required
3479 mk_target_functions name mk_term get_func conv create_conv target t
3481 get_coding_function_precise target t name));
3553 fun check_concs targ target [] = ()
3554 | check_concs targ target ((_,(_,(t,thm)))::rest) =
3557 if (not targ andalso (var = t)) orelse (targ andalso (var = target))
3558 then check_concs targ target rest
3561 type_to_string (if targ then target else t) ^ ".P a\""))
3631 fun prove_inductive_coding_theorem fname name mk_conc target t conv tactic =
3633 type_to_string target ^ " --> " ^ type_to_string t ^ "\n")
3634 val (induction,mapping) = get_coding_function_induction target t fname
3641 (CONV_RULE conv o C (get_coding_theorem target) name)
3656 app (fn (t,thm) => add_coding_theorem_precise target t name thm) thms
3659 fun inductive_coding_goal fname mk_conc target t (conv:term -> thm) =
3660 let val (induction,mapping) = get_coding_function_induction target t fname
3700 fun add_inductive_coding_theorem_generator fname name target conv tactic =
3701 add_coding_theorem_generator target name (can TypeBase.constructors_of)
3704 (fn t => if exists_coding_theorem_conclusion target name
3705 then get_coding_theorem_conclusion target name t
3708 target t conv tactic ;
3709 get_coding_theorem_precise target t name));
3721 fun add_tactic_coding_theorem_generator name test (tactic:hol_type -> tactic) target =
3722 add_coding_theorem_generator target name test
3723 (fn t => case (tactic t ([],get_coding_theorem_conclusion target name t))
3735 fun add_rule_coding_theorem_generator name test rule target =
3736 add_coding_theorem_generator target name test