| (* |
| * Copyright 2018, Data61 |
| * Commonwealth Scientific and Industrial Research Organisation (CSIRO) |
| * ABN 41 687 119 230. |
| * |
| * This software may be distributed and modified according to the terms of |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. |
| * See "LICENSE_BSD2.txt" for details. |
| * |
| * @TAG(DATA61_BSD) |
| *) |
| |
| theory Heap_Relation_Generation |
| imports Read_Table |
| begin |
| |
| ML\<open> (* local_setup_heap_rel *) |
| local |
| |
| fun mk_heap_rel ctxt (uvals:uval list) = |
| |
| (* mk_heap_rel makes the equation that defines heap relation for a given type. |
| * For example, "heap_rel \<sigma> h \<equiv> (\<forall>(p :: t2_C ptr). heap_rel_ptr \<sigma> h p)". *) |
| |
| let |
| fun mk_pointed_ty ty_nm_C = Syntax.read_typ ctxt ty_nm_C; |
| fun mk_pointer_ty ty_nm_C = Type ("CTypesBase.ptr", [mk_pointed_ty ty_nm_C]); |
| fun mk_a_conjct ty_nm_C = |
| Const ("HOL.All", dummyT) $ |
| Abs ("p", mk_pointer_ty ty_nm_C, |
| (Syntax.read_term ctxt "heap_rel_ptr" $ |
| Free ("\<sigma>", dummyT) $ Free ("h", dummyT) $ Bound 0)); |
| fun mk_conjcts [] = [] |
| | mk_conjcts (ty_nm_C::ty_nm_Cs) = mk_a_conjct ty_nm_C :: mk_conjcts ty_nm_Cs; |
| (* We have heap_rels for URecords only.*) |
| val ty_nm_Cs = uvals |> get_urecords |> map get_ty_nm_C; |
| (* FIXME later: hey, Yutaka. rhs is a bit stupid.*) |
| val rhs= if mk_conjcts ty_nm_Cs = [] then @{term "True"} else mk_conjcts ty_nm_Cs |> mk_HOL_conjs ; |
| val heap_rel = Free ("heap_rel", dummyT); |
| val lhs = strip_atype @{term "\<lambda> heap_rel . heap_rel \<sigma> h"} $ heap_rel |> strip_atype; |
| in |
| mk_eq_tm lhs rhs ctxt |
| end : term; |
| |
| in |
| |
| fun local_setup_heap_rel file_nm lthy = |
| (* local_setup_heap_rels defines and register a number of heap_rels |
| * when called inside local_setup quotation.*) |
| let |
| val thy = Proof_Context.theory_of lthy; |
| val uvals = read_table file_nm thy |
| |> map (unify_usum_tys o unify_sigils) |
| |> rm_redundancy |
| |> get_uvals_for_which_ac_mk_heap_getters file_nm thy; |
| val heap_rel = mk_heap_rel lthy uvals; |
| val lthy' = Specification.definition NONE [] [] ((Binding.name ("heap_rel_def"), []), heap_rel) lthy |> snd; |
| in lthy' end; |
| |
| end; |
| \<close> |
| end |