From d52c5090bd9969aa1c6370c7ac103b1150149db5 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 5 Jun 2018 09:39:38 +0200 Subject: [PATCH] First correct attribute calculation. --- examples/scholarly/Article.thy | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/examples/scholarly/Article.thy b/examples/scholarly/Article.thy index d01fbc2..588205e 100644 --- a/examples/scholarly/Article.thy +++ b/examples/scholarly/Article.thy @@ -50,17 +50,21 @@ Thm.concl_of; ML{* val X = (@{term scholarly_paper.example.comment}) -val Y = Type.legacy_freeze @{docitem_value \bgrnd\} +val Y = Type.legacy_freeze @{docitem_value \bgrnd\}; +Syntax.string_of_term *} ML{* fun calculate_attr_access ctxt f term = - let val term = Type.legacy_freeze term; - val ty = type_of term + (* term assumed to be ground type, (f term) not necessarily *) + let val _ = writeln("XXX"^(Syntax.string_of_term ctxt term)) + val [subterm'] = Type_Infer_Context.infer_types ctxt [f term] + val ty = type_of (subterm') + val _ = writeln("YYY"^(Syntax.string_of_term ctxt subterm')) val term' = (Const(@{const_name "HOL.eq"}, ty --> ty --> HOLogic.boolT) - $ (Type.legacy_freeze(f term)) + $ subterm' $ Free("_XXXXXXX", ty)) - val term'' = (HOLogic.mk_Trueprop(term')) - val thm = simplify @{context} (Thm.assume(Thm.cterm_of ctxt term'')); + val _ = writeln("ZZZ"^(Syntax.string_of_term ctxt term')) + val thm = simplify ctxt (Thm.assume(Thm.cterm_of ctxt (HOLogic.mk_Trueprop term'))); val Const(@{const_name "HOL.eq"},_) $ lhs $ _ = HOLogic.dest_Trueprop (Thm.concl_of thm) in lhs end @@ -69,6 +73,9 @@ val H = fn X => @{term scholarly_paper.example.comment} $ X *} +ML{*val t = calculate_attr_access @{context} H @{docitem_value \bgrnd\}; *} + + term "scholarly_paper.author.affiliation_update" term "scholarly_paper.abstract.keywordlist_update" term "scholarly_paper.introduction.comment_update"