blob: a8de91466646eb6033a765917e8918a932a3cb67 [file] [log] [blame] [edit]
(*
* 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