wenzelm@42153: (* Title: HOL/Hoare/hoare_syntax.ML wenzelm@42153: Author: Leonor Prensa Nieto & Tobias Nipkow wenzelm@42153: wenzelm@42153: Syntax translations for Hoare logic. wenzelm@42153: *) wenzelm@42153: wenzelm@42153: signature HOARE_SYNTAX = wenzelm@42153: sig wenzelm@42153: val hoare_vars_tr: term list -> term wenzelm@42153: val spec_tr': string -> term list -> term wenzelm@42153: end; wenzelm@42153: wenzelm@42153: structure Hoare_Syntax: HOARE_SYNTAX = wenzelm@42153: struct wenzelm@42153: wenzelm@42153: (** parse translation **) wenzelm@42153: wenzelm@42153: local wenzelm@42153: wenzelm@42153: fun idt_name (Free (x, _)) = SOME x wenzelm@51693: | idt_name (Const (@{syntax_const "_constrain"}, _) $ t $ _) = idt_name t wenzelm@42153: | idt_name _ = NONE; wenzelm@42153: wenzelm@42153: fun eq_idt tu = wenzelm@59058: (case apply2 idt_name tu of wenzelm@42153: (SOME x, SOME y) => x = y wenzelm@42153: | _ => false); wenzelm@42153: wenzelm@42284: fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body] wenzelm@42153: | mk_abstuple (x :: xs) body = haftmann@61424: Syntax.const @{const_syntax case_prod} $ Syntax_Trans.abs_tr [x, mk_abstuple xs body]; wenzelm@42153: wenzelm@42153: fun mk_fbody x e [y] = if eq_idt (x, y) then e else y wenzelm@42153: | mk_fbody x e (y :: xs) = wenzelm@42153: Syntax.const @{const_syntax Pair} $ wenzelm@42153: (if eq_idt (x, y) then e else y) $ mk_fbody x e xs; wenzelm@42153: wenzelm@42153: fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs); wenzelm@42153: wenzelm@42153: wenzelm@42153: (* bexp_tr & assn_tr *) wenzelm@42153: (*all meta-variables for bexp except for TRUE are translated as if they wenzelm@42153: were boolean expressions*) wenzelm@42153: wenzelm@55659: fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE" (* FIXME !? *) wenzelm@42153: | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; wenzelm@42153: wenzelm@42153: fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; wenzelm@42153: wenzelm@42153: wenzelm@42153: (* com_tr *) wenzelm@42153: wenzelm@42153: fun com_tr (Const (@{syntax_const "_assign"}, _) $ x $ e) xs = wenzelm@42153: Syntax.const @{const_syntax Basic} $ mk_fexp x e xs wenzelm@55659: | com_tr (Const (@{const_syntax Basic},_) $ f) _ = Syntax.const @{const_syntax Basic} $ f wenzelm@42153: | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = wenzelm@42153: Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs wenzelm@42153: | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = wenzelm@42153: Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs wenzelm@42153: | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = wenzelm@42153: Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs wenzelm@42153: | com_tr t _ = t; wenzelm@42153: wenzelm@42153: fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = idt :: vars_tr vars wenzelm@42153: | vars_tr t = [t]; wenzelm@42153: wenzelm@42153: in wenzelm@42153: wenzelm@42153: fun hoare_vars_tr [vars, pre, prg, post] = wenzelm@42153: let val xs = vars_tr vars wenzelm@42153: in Syntax.const @{const_syntax Valid} $ wenzelm@42153: assn_tr pre xs $ com_tr prg xs $ assn_tr post xs wenzelm@42153: end wenzelm@42153: | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); wenzelm@42153: wenzelm@42153: end; wenzelm@42153: wenzelm@42153: wenzelm@42153: wenzelm@42153: (** print translation **) wenzelm@42153: wenzelm@42153: local wenzelm@42153: wenzelm@42153: fun dest_abstuple haftmann@61424: (Const (@{const_syntax case_prod}, _) $ Abs (v, _, body)) = wenzelm@42153: subst_bound (Syntax.free v, dest_abstuple body) wenzelm@42153: | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body) wenzelm@42153: | dest_abstuple tm = tm; wenzelm@42153: haftmann@61424: fun abs2list (Const (@{const_syntax case_prod}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t wenzelm@55659: | abs2list (Abs (x, T, _)) = [Free (x, T)] wenzelm@42153: | abs2list _ = []; wenzelm@42153: haftmann@61424: fun mk_ts (Const (@{const_syntax case_prod}, _) $ Abs (_, _, t)) = mk_ts t wenzelm@55659: | mk_ts (Abs (_, _, t)) = mk_ts t wenzelm@42153: | mk_ts (Const (@{const_syntax Pair}, _) $ a $ b) = a :: mk_ts b wenzelm@42153: | mk_ts t = [t]; wenzelm@42153: haftmann@61424: fun mk_vts (Const (@{const_syntax case_prod},_) $ Abs (x, _, t)) = wenzelm@42153: (Syntax.free x :: abs2list t, mk_ts t) wenzelm@42153: | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t]) wenzelm@55659: | mk_vts _ = raise Match; wenzelm@42153: wenzelm@55659: fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *) wenzelm@42153: | find_ch ((v, t) :: vts) i xs = wenzelm@42153: if t = Bound i then find_ch vts (i - 1) xs wenzelm@42153: else (true, (v, subst_bounds (xs, t))); wenzelm@42153: haftmann@61424: fun is_f (Const (@{const_syntax case_prod}, _) $ Abs _) = true wenzelm@55659: | is_f (Abs _) = true wenzelm@55659: | is_f _ = false; wenzelm@42153: wenzelm@42153: wenzelm@42153: (* assn_tr' & bexp_tr'*) wenzelm@42153: wenzelm@42153: fun assn_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T wenzelm@42153: | assn_tr' (Const (@{const_syntax inter}, _) $ wenzelm@42153: (Const (@{const_syntax Collect}, _) $ T1) $ (Const (@{const_syntax Collect}, _) $ T2)) = wenzelm@42153: Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 wenzelm@42153: | assn_tr' t = t; wenzelm@42153: wenzelm@42153: fun bexp_tr' (Const (@{const_syntax Collect}, _) $ T) = dest_abstuple T wenzelm@42153: | bexp_tr' t = t; wenzelm@42153: wenzelm@42153: wenzelm@42153: (* com_tr' *) wenzelm@42153: wenzelm@42153: fun mk_assign f = wenzelm@42153: let wenzelm@42153: val (vs, ts) = mk_vts f; wenzelm@42153: val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs); wenzelm@42153: in wenzelm@42153: if ch wenzelm@42153: then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which wenzelm@42153: else Syntax.const @{const_syntax annskip} wenzelm@42153: end; wenzelm@42153: wenzelm@42153: fun com_tr' (Const (@{const_syntax Basic}, _) $ f) = wenzelm@42153: if is_f f then mk_assign f wenzelm@42153: else Syntax.const @{const_syntax Basic} $ f wenzelm@42153: | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = wenzelm@42153: Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 wenzelm@42153: | com_tr' (Const (@{const_syntax Cond}, _) $ b $ c1 $ c2) = wenzelm@42153: Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 wenzelm@42153: | com_tr' (Const (@{const_syntax While}, _) $ b $ I $ c) = wenzelm@42153: Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c wenzelm@42153: | com_tr' t = t; wenzelm@42153: wenzelm@42153: in wenzelm@42153: wenzelm@55659: fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q; wenzelm@42153: wenzelm@42153: end; wenzelm@42153: wenzelm@42153: end; wenzelm@42153: