Lines Matching defs:target
116 (* a) (encode : t -> target) x where encode is a valid encoder *)
117 (* b) (f : t -> target) x where target is a known translation *)
129 val target = type_of term
130 val enc = get_encode_function target t
134 (is_vartype target orelse can get_translation_scheme target))
140 val target = type_of term
141 val enc = get_encode_function target t
153 (is_vartype target orelse can get_translation_scheme target))
209 val target = type_of (lhs final)
274 val target = type_of term
275 fun mk_varv s = variant (free_vars term) (Term.mk_var(s,target))
557 let val (t,target) = dest_encdec term handle e => wrapException "match_encdec" e
559 FULL_ENCODE_DECODE_THM target t handle e => wrapException "match_encdec" e
570 val target = type_of var
572 val _ = if exists_translation target t then () else raise err
573 val _ = with_exn (match_term encode) (gen_encode_function target t) err
574 val _ = with_exn (match_term (rator decoded_term)) (gen_decode_function target t) err
575 val _ = with_exn (match_term (rator detect)) (gen_detect_function target t) err
577 (t,target)
582 let val (t,target) = dest_decenc term handle e => wrapException "match_decenc" e
584 FULL_DECODE_ENCODE_THM target t handle e => wrapException "match_decenc" e
594 val target = type_of encoded_term
596 val _ = if exists_translation target t then () else raise err
597 val _ = with_exn (match_term (rator encoded_term)) (gen_encode_function target t) err
598 val _ = with_exn (match_term detect) (gen_detect_function target t) err
600 (t,target)
605 let val (t,target) = dest_encdet term handle e => wrapException "match_encdet" e
607 FULL_ENCODE_DETECT_THM target t handle e => wrapException "match_encdet" e
850 val target = (type_of o lhs) final
852 val encoders = mapfilter (gen_encode_function target o type_of o rand o
933 (* append_detector target (L,e) A takes an encoding term representing *)
941 fun append_detector target ([],e) A =
944 (FULL_ENCODE_DETECT_THM target (type_of (rand (lhs e))))))::A
947 | append_detector target _ A = A;
1075 val target = type_of (rhs final)
1098 in (n,conved):: (enc (append_detector target (L,e) A) rest)
1264 let val target = type_of (lhs (concl thm))
1266 val thm' = AP_TERM (get_decode_function target t) thm
1267 val encdec = FULL_ENCODE_DECODE_THM target t
2156 fun set_destructors target destructors =
2170 val _ = remove_coding_theorem_precise target t "destructors" handle e => ()
2171 val _ = remove_coding_theorem_precise target t "initial" handle e => ()
2172 val _ = add_coding_theorem_precise target t "destructors"
2174 val _ = add_coding_theorem_precise target t "initial" (LIST_CONJ initials)
2178 fun nested_constructor_theorem target term =
2182 val initial = get_coding_theorem target t "initial"
2191 fun nested_constructor_rewrite target term =
2198 val initial = get_coding_theorem target t "initial"
2222 fun mk_destructor_rewrites target destructors =
2224 val encs = map (get_encode_function target) types
2228 genvar target))) lhss encs;
2243 fun mk_predicates target t =
2244 let val encoders = CONJUNCTS (get_coding_function_def target t "encode")
2245 val decode_pair = gen_decode_function target
2246 (pairLib.mk_prod(numLib.num,target));
2247 val map_thm = FULL_ENCODE_DECODE_MAP_THM target
2267 fun mk_predicate_resolve target t =
2268 let val encoders = CONJUNCTS (get_coding_function_def target t "encode")
2269 val p1 = pairLib.mk_prod(numLib.num,target);
2271 val decode_pair = gen_decode_function target p1
2272 val encode_pair = gen_encode_function target p1
2278 (FULL_ENCODE_DECODE_MAP_THM target p2))) THENC
2281 (FULL_ENCODE_MAP_ENCODE_THM target p2) THENC
2303 fun mk_predicate_rewrites target t =
2304 let val predicates = mk_predicates target t
2323 (mk_destructor_rewrites target predicates,
2324 map (AP_TERM (get_encode_function target bool))
2358 fun mk_case_propagation_theorem target t =
2360 val destructor_thm = set_type t (get_coding_theorem target t "destructors")
2404 val enc = mk_var("encode",mk_vartype "'out" --> mk_vartype "'target")
2471 fun check_term target M =
2472 (is_var M andalso type_of M = target) orelse
2474 all (curry op= target)
2477 both ((all (curry op= target o type_of) o pairSyntax.strip_pair ##
2478 check_term target) (pairSyntax.dest_pabs M))) orelse
2479 (is_comb M andalso check_term target (rator M) andalso
2480 check_term target (rand M));
2482 fun target_function_conv target term =
2483 if same_const (rator term) (mk_const("I",target --> target)) andalso
2484 check_term target (rand term)
2492 fun dummy_encoder_conv target term =
2493 if same_const (rator term) (mk_const("I",target --> target)) andalso
2494 type_of (rand term) = target andalso is_encoded_term (rand term)
2515 fun check_case_thm target t =
2521 filter (can (C match_type target) o type_of) all_lhss)
2525 fun encode_names target t =
2527 (get_coding_function_def target t "encode"))
2541 fun add_decodeencode_rewrites target t =
2543 (FULL_DECODE_ENCODE_THM target t)))))
2549 fun add_encode_rewrites target t =
2550 let val filtered = filter (not o exists_rewrite o fst) (encode_names target t)
2555 fun add_case_rewrites target t =
2557 if exists_coding_theorem target t "destructors"
2561 else let val (p,d) = mk_destructors target t
2562 val _ = set_destructors target d
2563 in (p,mk_destructor_rewrites target d)
2566 if check_case_thm target t then NONE else
2571 else SOME (mk_case_propagation_theorem target t
2577 else mk_predicate_rewrites target t
2580 val predicate_resolve = total (mk_predicate_resolve target) t;
2600 fun add_standard_coding_rewrites target t =
2608 val _ = encode_type target t
2609 val _ = add_encode_rewrites target t
2612 val _ = add_decodeencode_rewrites target t
2614 val _ = add_case_rewrites target t
2631 val target = type_of term
2633 val decoder = get_decode_function target var_type
2636 then conditionize_rewrite (add_decodeencode_rewrites target var_type)
2704 val target = type_of right
2714 mk_comb(gen_decode_function target (type_of a),b))
2721 mk_comb(gen_encode_function target (type_of d),
2729 rule o generate_coding_theorem target "encode_detect_all" o type_of) decoded_args
2732 rule o generate_coding_theorem target "encode_decode_map" o type_of) decoded_args
2741 total (rule o FULL_ENCODE_MAP_ENCODE_THM target o type_of o
2836 (* mk_analogue_definition target name *)
2854 fun MK_DEFINITION tvs target limits function =
2855 let val tfunction = INST_TYPE (map (fn x => x |-> target) tvs) function
2861 val new_args = map (C (curry mk_var) target o fst o dest_var) normal_args
2863 mk_comb(gen_decode_function target (type_of arg),new_arg))
2869 mk_comb(gen_detect_function target (type_of arg),new_arg))
2876 val bottom = #bottom (get_translation_scheme target)
2879 (body,new_args,detected_args,specced_limits,target,result_type,bottom)
2882 fun mk_analogue_definition_term target name limits function =
2888 target,result_type,bottom) =
2889 MK_DEFINITION [] target limits function
2895 (fn x => is_vartype x orelse x = target) bottom result_type)
2897 val right = mk_comb(gen_encode_function target result_type,conditional)
2899 val new_fconst = mk_var(name,foldl op--> target (map type_of new_args))
2916 fun mk_analogue_definition target name tautologies limits function =
2922 ,target,result_type,bottom) =
2923 MK_DEFINITION [] target limits function
2930 (fn x => is_vartype x orelse x = target) bottom result_type)
2932 val right = mk_comb(gen_encode_function target result_type,conditional)
2934 val new_fconst = mk_var(name,foldl op--> target (map type_of new_args))
2942 target name map_thm tautologies limits extras function =
2952 val map_thm1 = INST_TYPE (map (fn x => x |-> target) tvs) map_thm
2962 val type_vars = map #redex (filter (curry op= target o #residue)
2965 ,target,result_type,bottom) =
2966 MK_DEFINITION type_vars target limits function
2973 (fn x => is_vartype x orelse x = target) bottom result_type)
2975 val right = mk_comb(gen_encode_function target result_type,conditional)
2977 val new_fconst = mk_var(name,foldl op--> target (map type_of new_args))
3026 fun limit_to_theorems target term =
3027 (mapfilter (nested_constructor_theorem target) o strip_conj o dest_neg o
3184 fun calculate_extra_theorems target list =
3191 val _ = map (encode_type target o base_type)
3203 val nested_theorems = map (limit_to_theorems target) clause_limits
3214 target name_map limits extras definition =
3229 mk_analogue_definition target name (map SPEC_ALL extras)
3236 val extra_theorems = calculate_extra_theorems target list
3260 fun convert_definition target name_map limits extras definition =
3262 target name_map
3265 target name_map limits map_thms extras definition =
3274 mad target name_map limits extras definition
3342 fun mk_encoder target x = mk_comb(get_encode_function target (type_of x),x);
3343 fun ap_decoder target x =
3344 AP_TERM (get_decode_function target (type_of (rand (lhs (concl x))))) x;
3345 fun left_encdec target x =
3346 CONV_RULE (LAND_CONV (REWR_CONV (FULL_ENCODE_DECODE_THM target
3349 fun mk_pres target arg =
3350 let val p = mk_eq(mk_encoder target arg,genvar target)
3352 ((left_encdec target o ap_decoder target o ASSUME) p,SOME p)
3357 val target = type_of term
3358 val (rwrs,pres) = unzip (map (mk_pres target) args)
3391 fun get_all_detect_types target t =
3393 (C (exists_coding_function_precise target) "detect") t
3403 fun is_recursive_detect_type target t =
3405 (C (exists_coding_function_precise target) "detect") t
3418 fun mk_fullname target t =
3419 if is_vartype t orelse t = target then "ANY"
3420 else String.concat (op:: ((I ## map (mk_fullname target)) (dest_type t)))
3427 fun generate_recognizer_terms namef target full_types =
3428 let val _ = map (encode_type target) (filter (not o is_vartype)
3430 val KT = mk_comb(mk_const("K",bool --> target --> bool),
3433 val detectors = map (get_detect_function target) full_types
3437 val var = mk_var("x",target);
3438 val bool_enc = get_encode_function target bool
3441 mk_eq(mk_comb(mk_var(namef t,target --> target),var),
3445 fun flatten_recognizers namef target t =
3448 val full_types = get_all_detect_types target t
3449 val funcs = generate_recognizer_terms namef target full_types
3461 map (C (get_coding_function_def target) "detect") full_types
3465 mapfilter (generate_coding_theorem target "general_detect" o base_type)
3478 let val target = last (fst (strip_fun (type_of term)))
3480 (get_detect_function target target,target) ::
3481 (mapfilter (fn t => (get_coding_function_const target t "detect",t))
3482 (get_translation_types target))
3497 fun recognizer_rewrite target t =
3498 let val detector = SPEC_ALL (get_coding_function_def target t "detect")
3500 val prior = mk_eq(imk_comb(mk_const("I",alpha --> alpha),var),genvar target)
3504 val thm'' = AP_TERM (get_encode_function target bool) thm'
3505 val rrwr = ASSUME (mk_eq(rhs (concl thm''),genvar target))
3513 let val target = type_of term
3515 val detector = get_detect_function target t
3516 val encoder = get_encode_function target bool
3517 val var = mk_var("x",target);
3520 if is_recursive_detect_type target t
3521 then (flatten_recognizers (mk_fullname target) target t ;
3523 else recognizer_rewrite target t
3561 fun get_wf_relation target =
3562 let val scheme = get_translation_scheme target
3568 val x = mk_var("x",target)
3569 val y = mk_var("y",target)
3601 fun make_abstract_funcs target abstract_terms funcs input_terms =
3603 (mk_var("ABS" ^ implode (base26 i),target)))
3614 foldl (op-->) target (map type_of (args @ new_args))),
3625 fun create_abstract_recognizers namef f target t =
3628 val full_types = get_all_detect_types target t
3630 (generate_recognizer_terms namef target full_types)
3634 generate_coding_theorem target "general_detect" o base_type)
3644 map (C (get_coding_function_def target) "detect") full_types
3650 make_abstract_funcs target (mk_set (flatten terminals))
3828 (* R : target # 'a + target # 'a + .... -> ... -> bool or *)
3829 (* R : target + target + ... -> ... -> bool *)
3837 val target = hd (pairSyntax.strip_prod (hd txs));
3838 val WF_R = MATCH_MP relationTheory.WF_TC (get_wf_relation target)
3879 (* target type induction scheme. *)
3895 (* find_conditional_thm target t : hol_type -> thm *)
3901 fun find_conditional_thm target =
3902 let val scheme = get_translation_scheme target
3903 val i = mk_const("I",target --> target);
3904 val vars = map (C (curry mk_var) target) ["a","b"]
3905 val pred = beta_conv (mk_comb(#predicate scheme,mk_var("p",target)))
4040 fun flatten_abstract_recognizers fname f target t =
4041 let val conditional = find_conditional_thm target
4042 val (props,thms,terms) = create_abstract_recognizers fname f target t
4070 fun generalize_abstract_recognizer_term target t =
4071 let val var = mk_var("x",target)
4072 val detector = get_detect_function target t
4073 val boolenc = get_encode_function target bool
4074 val booldec = get_decode_function target bool
4082 val basetype = (mk_type o (I ## map (K target)) o dest_type) t
4083 val right = mk_comb(get_detect_function target basetype,var);
4088 fun ENCODE_BOOL_UNTIL_CONV target terms term =
4089 let val bool_encdec = FULL_ENCODE_DECODE_THM target bool
4096 fun GENERALIZE_ABSTRACT_RECOGNIZER_TAC target t thm (a,g) =
4101 ONCE_REWRITE_TAC [get_coding_function_def target t "detect"] THEN
4103 CONV_TAC (RAND_CONV (ENCODE_BOOL_UNTIL_CONV target [right]))) (a,g)
4106 fun generalize_abstract_recognizer target t pre_rewrites thm =
4107 prove(generalize_abstract_recognizer_term target t,
4108 GENERALIZE_ABSTRACT_RECOGNIZER_TAC target t thm THEN
4126 val target = type_of term
4127 fun mk_encoder x = imk_comb(get_encode_function target (type_of x),x)
4139 f target name limits extras function =
4141 (mk_analogue_definition_term target name
4148 val extra_theorems = calculate_extra_theorems target [(function,limits)];
4170 (fn t => PURE_REWRITE_RULE [FULL_ENCODE_DECODE_THM target t]
4171 (AP_TERM (get_decode_function target t) x))
4178 make_abstract_funcs target terminals [snd (strip_forall term)]
4190 f target name limits extras thm pre_rewrites tactic1 tactic2 =
4194 f target name limits' extras function
4202 (can (match_term (get_decode_function target (type_of term)))
4208 get_encode_function target (type_of dv),
4219 val encdets = map (FULL_ENCODE_DETECT_THM target o type_of) nvars;
4220 val encdecs = map (FULL_ENCODE_DECODE_THM target o type_of) nvars;
4237 fun convert_abstracted_nonrec_definition f target name limits extras thm =
4238 convert_abstracted_definition f target name limits extras thm []
4244 REWRITE_TAC (map (FULL_ENCODE_DETECT_THM target) types) THEN
4245 REWRITE_TAC (map (FULL_ENCODE_DECODE_THM target) types) THEN