(* $Header: /users/lal/black/hol/Disser/RCS/partialTactics.sml,v 1.33 1997/07/09 17:33:22 black Exp $ *) (* *created "Thu Oct 26 16:02:50 1995" *by "Paul E. Black" *) (* *modified "Wed Jul 9 11:32:54 1997" *by "Paul E. Black" *) (*----------------------------------------------------------------------- C inference rules for partial correctness rules after Mike Gordon and Peter Homeier implementation after William Harrison and Michael Norrish -----------------------------------------------------------------------*) new_parent "partialInf"; use "wellfrmTactics.sml"; (* for conversions and tactics *) use "semeqTactics.sml"; val IS_VALUE = definition "partialInf" "IS_VALUE"; add_theorems_to_sml "partialInf"; val PL2CEL_DEF = definition "c_ast" "PL2CEL_DEF"; (*---------------------------------------------------------------- C axiom introduction schemas ----------------------------------------------------------------*) (* create the axiom for the truth value of an expression (no side effects) *) fun mk_VALUE cexpr = let val holexpr = cexpr2hol cexpr in SPECL [cexpr, holexpr] (REWRITE_RULE [] IS_VALUE) end; (*--------------------------------------------------------------------------- Prove what the result of substituting variables by expressions in a predicate is. ---------------------------------------------------------------------------*) (* alpha conversion, that is, return wff with each element of lhsList which is free replaced by the corresponding element of exprList *) fun alpha_convert wff lhsList exprList = subst (combineSubst(lhsList, exprList)) wff; (* some test cases test_result (alpha_convert (--`a + b`--) [(--`a:num`--),(--`b:num`--)] [(--`b:num`--),(--`a:num`--)]) (--`b + a`--); test_result (alpha_convert (--`x >= a + b /\ x < c`--) [(--`x:num`--),(--`a:num`--)] [(--`y - 1`--),(--`x:num`--)]) (--`(y - 1) >= (x + b) /\ (y - 1) < c`--); test_result (alpha_convert (--`\t.t * (a+1)`--) [(--`a+1`--)] [(--`m:num`--)]) (--`\t.t * m`--); test_result (alpha_convert (--`\t.t+1`--) [(--`t:num`--)] [(--`k + 3`--)]) (--`\t.t+1`--); *) (* extract the "core" variable from the term. This is needed since array variables are returned as functions. Inputs should be like (--`a:num`--) (--`CA (CA_FN (ar:num CArray)) arSz`--) *) fun extCoreVar trm = if is_var trm then trm else (hd o #2 o strip_comb o hd o #2 o strip_comb) trm; (* convert a C AST variable to a HOL variable *) fun cvar2hol cvar = extCoreVar (cexpr2hol cvar); (* test map cvar2hol (lsthol2sml (--`[Var "b" 0 Char; Var "a" 0 (Array Int (CCint 32)); Var "c" 0 Void]`--)); *) local (* for substituteCVars *) (* return lst1 with elements castToBool if the corresponding element of lst2 is a :bool *) fun conformToBool [] _ = [] | conformToBool (hd1::rest1) (hd2::rest2) = if type_of hd2 = (==`:bool`==) then (castToBool hd1 :: (conformToBool rest1 rest2)) else (hd1 :: (conformToBool rest1 rest2)); in (* utility for SUBSE_CONV and SUBS_CONV *) fun substituteCVars pred vrl exl = (* return lst1 with elements changed to conform to the corresponding element of lst2. This is a KLUDGE. *) let fun conformToType [] _ = [] | conformToType (hd1::rest1) (hd2::rest2) = if type_of hd2 = (==`:string`==) andalso type_of hd1 <> (==`:string`==) then let val retyped=mk_var{Name=(#Name o dest_var o extCoreVar)hd1, Ty = (==`:string`==)} in (retyped :: (conformToType rest1 rest2)) end else (hd1 :: (conformToType rest1 rest2)) val els = map cexpr2hol (lsthol2sml exl) val vls = map cvar2hol (lsthol2sml vrl) in alpha_convert pred (conformToBool vls els) (conformToType els vls) end; end; fun SUBSE_CONV (trm:term) = let val [pred,vrl,exl] = strip_op (--`SUBSE`--) trm in mk_thm([], (--`^trm = ^(substituteCVars pred vrl exl)`--)) end; fun prove_SUBSE pred vrl exl = GSYM (SUBSE_CONV (--`SUBSE ^pred ^vrl ^exl`--)); fun SUBS_CONV (trm:term) = let val [pred,newvl,oldvl] = strip_op (--`SUBS`--) trm in mk_thm([], (--`^trm = ^(substituteCVars pred oldvl newvl)`--)) end; (* test cases val sc1 = (--`SUBS (a > b) [Var "a" 0 Int; Var "b" 0 Int] [Var "b" 0 Int; Var "a" 0 Int]`--); test_result (concl (SUBS_CONV sc1)) (--`^sc1 = b > a`--); val sc2 = (--`SUBS (x >= a + b /\ x < c) [Var "y" 0 Int; Var "x" 0 Int] [Var "x" 0 Int; Var "a" 0 Int]`--); test_result (concl (SUBS_CONV sc2)) (--`^sc2 = y >= (x + b) /\ y < c`--); val sc3 = (--`SUBS (q=(\t.t+1)) [Var "t" 0 Int] [Var "k" 3 Int]`--); test_result (concl (SUBS_CONV sc3)) (--`^sc3 = (q=(\t.t+1))`--); *) local (* for SUBSAE_CONV *) (* substitute a new array fn for occurrences of the array in pred *) fun substituteArray pred ary ind ex = let val e = cexpr2hol ex val j = cexpr2hol ind val arFull = cexpr2hol ary val arVar = (#Rand o dest_comb o el 1 o #2 o strip_comb) arFull in alpha_convert pred [arVar] [(--`CA_PUT ^arFull ^j ^e`--)] end; in fun SUBSAE_CONV (trm:term) = let val [pred,ar,ind,ex] = strip_op (--`SUBSAE`--) trm in mk_thm([], (--`^trm = ^(substituteArray pred ar ind ex)`--)) end; end; (* test cases val sa1 = (--`SUBSAE (CA_IDX ar n = 0) (Var "ar" 0 (Array Int (CCid "arSz"))) (Lval (Vref (Var "j" 0 Int))) (Lval (Vref (Var "b" 0 Int)))`--); test_result (concl (SUBSAE_CONV sa1)) (--`^sa1 = (CA_IDX (CA_PUT (CA (CA_FN ar) arSz) j (b:num)) n = 0)`--); *) fun prove_SUBSAE pred ar ind ex = GSYM ( SUBSAE_CONV (--`SUBSAE ^pred ^ar ^ind ^ex`--) ); (* example prove_SUBSAE (--`CA_IDX ar n = 0`--) (--`Var "ar" 0 (Array Int (CCid "arSz"))`--) (--`Lval (Vref (Var "j" 0 Int))`--) (--`Lval (Vref (Var "b" 0 Int))`--); *) (*---------------------------------------------------------------- tactics corresponding to inference rules ----------------------------------------------------------------*) (*----------------- Tactics for handling sequences --------------------------*) (* break a partial correctness assertion into components *) fun strip_partial partial = let val [pre,code,post] = strip_op (--`Partial`--) partial in (pre, code, post) end; (* prove partial correctness by proving a semantically equivalent statement *) fun SEM_EQ_TAC equivsl (asl, goal) = (MATCH_MP_TAC Sem_equiv_rule THEN EXISTS_TAC equivsl THEN CONJ_TAC) (asl, goal); (* separate the proof for the first statement in a sequence *) fun SEQUENCE_TAC intermediate (asl, goal) = (MATCH_MP_TAC Sequence_rule THEN EXISTS_TAC intermediate THEN CONJ_TAC) (asl, goal); (* remove the final statement in a Seq *) fun dest_final_seq code = let val [codeFirst,codeRest] = strip_op (--`Seq`--) code val (codeRestOp,_) = strip_comb codeRest in if codeRestOp = (--`Seq`--) then let val (reworked,final) = dest_final_seq codeRest in ((--`Seq ^codeFirst ^reworked`--), final) end else (codeFirst, codeRest) end; (* test cases test_result (fst (dest_final_seq (--`Seq a b`--))) (--`a:CStmt`--); test_result (snd (dest_final_seq (--`Seq a b`--))) (--`b:CStmt`--); test_result (fst (dest_final_seq (--`Seq a (Seq b c)`--))) (--`Seq a b`--); test_result (snd (dest_final_seq (--`Seq a (Seq b c)`--))) (--`c:CStmt`--); *) (* turn Partial p (Seq a (Seq b (Seq ... (Seq w x)...))) q into Partial p (Seq (Seq ... (Seq a b) ... w) x) q *) fun LEFT_NORM_SEQ thm = let val t = ref thm val transform = MATCH_MP Sequence_assoc2 in ((while can transform (!t) do t := transform (!t)); !t) end; (* turn Partial p (Seq (Seq ... (Seq a b) ... w) x) q into Partial p (Seq a (Seq b (Seq ... (Seq w x)...))) q *) fun RIGHT_NORM_SEQ thm = let val t = ref thm val transform = MATCH_MP Sequence_assoc1 in ((while can transform (!t) do t := transform (!t)); !t) end; (* separate the proof for the last statement in a sequence *) (* SKIMP: this is VERY inefficient; it could be a bottleneck in proofs *) fun TL_SEQUENCE_TAC intermediate (asl, goal) = let val (pre,code,post) = strip_partial goal val (codeButLast,codeLast) = dest_final_seq code val subgoal1 = (--`Partial ^pre ^codeButLast ^intermediate`--) and subgoal2 = (--`Partial ^intermediate ^codeLast ^post`--) in ([(asl,subgoal1),(asl,subgoal2)], fn [th1,th2] => RIGHT_NORM_SEQ (MATCH_MP Sequence_rule (CONJ (LEFT_NORM_SEQ th1) th2))) end; (*------------------- pre- and post- conditions ----------------------------*) fun PRE_STRENGTHEN_TAC weaker (asl, goal) = (MATCH_MP_TAC Pre_strengthen_rule THEN EXISTS_TAC weaker THEN PURE_ONCE_REWRITE_TAC [CONJ_SYM] THEN CONJ_TAC) (asl, goal); fun POST_WEAKEN_TAC post (asl, goal) = (MATCH_MP_TAC Post_weaken_rule THEN EXISTS_TAC post THEN PURE_ONCE_REWRITE_TAC [CONJ_SYM] THEN CONJ_TAC) (asl, goal); (*------------------------ Tactic to prove Skip ------------------------*) fun SKIP_TAC (asl, goal) = let val (pre,code,post) = strip_partial goal in (POST_WEAKEN_TAC pre THENL [ (ARITH_TAC ORELSE TAUT_TAC ORELSE REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] ORELSE ALL_TAC), REWRITE_TAC [SKIP_AX] ]) (asl, goal) end; (*--------- Tactic to prove Simple expressions without side effects ---------*) local (* for find_variants *) (* return true if first list is a prefix of second list *) fun is_prefix [] _ = true | is_prefix _ [] = false | is_prefix (h1::t1) (h2::t2) = h1 = h2 andalso is_prefix t1 t2; in (* return any variants of nam which are free in expr *) fun find_variants nam expr = let val exnam = explode nam in filter (fn x => is_prefix exnam ((explode o #Name o dest_var) x)) (free_vars expr) end; end; fun GENERAL_EXPR_TAC cresultStr (asl, goal) = let val (pre,code,post) = strip_partial goal val [expr] = strip_op (--`Simple`--) code val exprNseThm = prove_NoSE expr val exprTyp = ctype_of expr val cresultVar = (--`Var ^(mk_str cresultStr) 0 ^exprTyp`--) val preThm = prove_SUBSE post (--`[^cresultVar]`--) (--`[^expr]`--) val newpre = lresult preThm val partlThm = MATCH_MP Simple_nse_rule (CONJ preThm exprNseThm) in if newpre = pre then (ACCEPT_TAC partlThm) (asl, goal) else (* strengthen the precondition *) (PRE_STRENGTHEN_TAC newpre THENL [ ARITH_TAC ORELSE TAUT_TAC ORELSE REWRITE_TAC [] THEN TAUT_TAC ORELSE ALL_TAC, ACCEPT_TAC partlThm ]) (asl, goal) end; fun EXPR_TAC (asl, goal) = let val (_,_,post) = strip_partial goal val cresults = find_variants C_RESULT post val cresultNm = case length cresults of 0 => (* no C_Result, use a dummy *) C_RESULT | 1 => (* exactly one C_Result *) (#Name o dest_var o hd) cresults | _ => (* more than one C_Result *) raise Fail "multiple C_Result's in post: use GENERAL_EXPR_TAC" in (GENERAL_EXPR_TAC cresultNm) (asl, goal) end; (*---------------------------------------------------------------------------- Tactics for assignments and sequences ----------------------------------------------------------------------------*) (* not needed with the LAL extensions load_library{lib = find_library "arith", theory = "-"}; load_library{lib = find_library "taut", theory = "-"}; *) (* I use this all the time *) val ARITH_TAC = CONV_TAC ARITH_CONV; (* break apart an assignment statement into the left hand side and the expr: (--`Simple (Assign (Vref (Var "var" 0 Int))) expr)`--) -> ((--`Vref (Var "var" 0 Int)`--), expr) *) fun strip_assign_stm ccode = let val [assignl] = strip_op (--`Simple`--) ccode (* lhs is something like (--`Vref(Var "x" 0 Int)`--) and expr is something like (--`Const(CCint 3)Int`--) *) val [lhs,expr] = strip_op (--`Assign`--) assignl in (lhs, expr) end; local (* for Assign_CONV *) (* prove theorem for {pre} (Simple (Assign (Vref x) expr)) {post} Compute pre from post. *) fun Assign_Vref_CONV lhs expr post = let val vari = hd (strip_op (--`Vref`--) lhs) (* create the precondition *) val preThm = prove_SUBSE post (--`[^vari]`--) (--`[^expr]`--) val nseThm = prove_NoSE expr in MATCH_MP Assign_vref_rule (CONJ preThm nseThm) end; (* prove theorem for {pre} (Simple (Assign (Aryref a i) expr)) {post} Compute pre from post. *) fun Assign_Aryref_CONV lhs expr post = let val [avar,ind] = strip_op (--`Aryref`--) lhs (* create the precondition *) val preThm = prove_SUBSAE post avar ind expr val nseIthm = prove_NoSE ind val nseEthm = prove_NoSE expr in MATCH_MP Assign_aryref_rule (LIST_CONJ [preThm, nseIthm, nseEthm]) end; in (* prove theorem for {pre} (Simple lhs expr)) {post} Compute pre from post. *) fun Assign_CONV code post = let val (lhs,expr) = strip_assign_stm code in if (#1 o strip_comb) lhs = (--`Vref`--) then (Assign_Vref_CONV lhs expr post) else (Assign_Aryref_CONV lhs expr post) end; end; (* prove assignments statements work *) (* SKIMP - need not do PRE_STRENGTHEN_TAC sometimes - pass other proof tactics (in those rare cases that neither ARITH_TAC nor TAUT_TAC work)? *) fun ASSIGN_TAC (asl, goal) = let val (pre,code,post) = strip_partial goal val assignThm = Assign_CONV code post val (weaker,_,_) = (strip_partial o snd o dest_thm) assignThm in (PRE_STRENGTHEN_TAC weaker THENL [ ARITH_TAC ORELSE TAUT_TAC ORELSE REWRITE_TAC [] THEN TAUT_TAC ORELSE ALL_TAC, ACCEPT_TAC assignThm ]) (asl, goal) end; (* prove the final assignment in a list of statements *) fun SEQ_ASSIGN_TAC (asl, goal) = let val (pre,code,post) = strip_partial goal val (codeOp,codeRest) = strip_comb code in if not (codeOp = (--`Seq`--)) then (* if this is a lone assignment, just do it *) ASSIGN_TAC (asl, goal) else let val (firstStmts,lastStmt) = dest_final_seq code val assignThm = Assign_CONV lastStmt post val (intermediate,_,_) = (strip_partial o snd o dest_thm) assignThm in (TL_SEQUENCE_TAC intermediate THENL [ ALL_TAC, ACCEPT_TAC assignThm ]) (asl, goal) end end (* so REPEAT SEQ_ASSIGN_TAC stops gracefully if an implication remains *) handle HOL_ERR _ => NO_TAC (asl, goal); (* return true if var is found in trm *) fun find_var var trm = if is_comb trm then find_var var (rator trm) orelse find_var var (rand trm) else if is_abs trm then find_var var (bvar trm) orelse find_var var (body trm) else if is_var trm then let val varname = #Name (dest_var trm) in var = varname end else (* is_const is the only remaining case, and vars are never constants *) false; (* test cases *) (* fun btest_result a b = test_result (case a of true => (--`T`--) | false => (--`F`--)) (case b of true => (--`T`--) | false => (--`F`--)); btest_result (find_var "P" (--`P:num`--)) true; btest_result (find_var "P" (--`1`--)) false; btest_result (find_var "P" (--`a \/ P`--)) true; btest_result (find_var "P" (--`a \/ p`--)) false; btest_result (find_var "P" (--`!z. z > P`--)) true; btest_result (find_var "P" (--`!z. z > 0`--)) false; *) (* append a new term to a conjunction, eg, append (--`a /\ b`--) (--`c`--) gives (--`a /\ b /\ c`--) *) fun append_conj a b = if is_comb a then let val (rator,rands) = strip_comb a in if rator = (--`$/\`--) then list_mk_comb(rator,[el 1 rands, append_conj (el 2 rands) b]) else (--`^a /\ ^b`--) end else (--`^a /\ ^b`--); (* test cases *) (* test_result (append_conj (--`a:bool`--) (--`b:bool`--)) (--`a /\ b`--); test_result (append_conj (--`T`--) (--`b:bool`--)) (--`T /\ b`--); test_result (append_conj (--`e /\ f`--) (--`b:bool`--)) (--`e /\ f /\ b`--); test_result (append_conj (--`p \/ q`--) (--`b:bool`--)) (--`(p \/ q) /\ b`--); test_result (append_conj (--`~r`--) (--`b:bool`--)) (--`(~r) /\ b`--); test_result (append_conj (--`(g==>h)/\(j==>k)`--) (--`b:bool`--)) (--`(g==>h)/\(j==>k)/\b`--); *) (* try to prove the first assignment in a list of statements *) fun FWD_SEQ_ASSIGN_TAC (asl, goal) = let val (pre,code,post) = strip_partial goal val (codeOp,codeRest) = strip_comb code in if codeOp = (--`Simple`--) then (* if this is a lone assignment, just do it *) ASSIGN_TAC (asl, goal) else if codeOp = (--`Seq`--) then let val firstStmt = hd codeRest val (lhs,expr) = strip_assign_stm firstStmt val vari = hd (strip_op (--`Vref`--) lhs) val varstr = dest_cvar vari in if find_var varstr pre then raise Fail "FWD_SEQ_ASSIGN_TAC: cannot handle lhs in precondition (yet)" else let val eqexpr = cexpr2hol (--`Binary (Lval(Vref ^vari)) Eq ^(expr)`--) val newPost = append_conj pre eqexpr in (SEQUENCE_TAC newPost THENL [ ASSIGN_TAC, REWRITE_TAC [] (* in case we can simplify something *) ]) (asl, goal) end end else (* this is something else; fail so REPEAT FWD_ASSIGN_TAC stops *) NO_TAC (asl, goal) end; (*--------------------------------------------------------------------------- Tactics for side effects ---------------------------------------------------------------------------*) (* create axiom for unary operators with side effects (++ and --). mk_LUNARY (--`Simple (LUnary op lval)`--) post yields |- Partial pre (Simple (LUnary op lval)) (post /\ C_Result=somevalue) The predicate pre is computed from post. *) fun mk_LUNARY code post c_resultName = if mem c_resultName (map (fn x=>(#Name o dest_var)x) (free_vars post))then (print_term post; print "\n"; raise HOL_ERR {origin_structure = "partialTactics", origin_function = "mk_LUNARY", message = c_resultName ^ "must not appear in post"}) else let val [lu] = strip_op (--`Simple`--) code val [opr,lv] = strip_op (--`LUnary`--) lu val [varref] = strip_op (--`Vref`--) lv val [_,_,vtype] = strip_op (--`Var`--) varref val lvNoSEthm = prove_NoSE (--`Lval ^lv`--) val holvar = cexpr2hol varref val typedCResult = mk_var{Name=c_resultName, Ty=ctype2hol vtype} val (veffect,reffect) = if opr = (--`PreInc`--) then ((--`^holvar + 1`--), (--`^typedCResult = ^holvar`--)) else if opr = (--`PreDec`--) then ((--`^holvar - 1`--), (--`^typedCResult = ^holvar`--)) else if opr = (--`PostInc`--) then ((--`^holvar + 1`--), (--`^typedCResult = ^holvar - 1`--)) else if opr = (--`PostDec`--) then ((--`^holvar - 1`--), (--`^typedCResult = ^holvar + 1`--)) else raise HOL_ERR {origin_structure = "partialTactics", origin_function = "LUNARY_TAC", message = "Unknown operator"} (* create the precondition and the postcondition with C_Result *) val pre = alpha_convert post [holvar] [veffect] val newpost = append_conj post reffect in SPECL [pre, opr, newpost] (MATCH_MP Side_effect_rule lvNoSEthm) end; (* prove simple side-effect statements *) fun GENERAL_LUNARY_TAC newvarName post (asl, goal) = let val (_,code,_) = strip_partial goal val lunaryAx = mk_LUNARY code post newvarName val (newpre,_,newpost) = (strip_partial o snd o dest_thm) lunaryAx in (PRE_STRENGTHEN_TAC newpre THENL [ ARITH_TAC ORELSE TAUT_TAC ORELSE REWRITE_TAC [] THEN TAUT_TAC ORELSE ALL_TAC, POST_WEAKEN_TAC newpost THENL [ ARITH_TAC ORELSE REWRITE_TAC [] ORELSE ALL_TAC, ACCEPT_TAC lunaryAx ] ]) (asl, goal) end; fun LUNARY_TAC (asl, goal) = let val (_,_,post) = strip_partial goal in GENERAL_LUNARY_TAC (new_C_Result()) post (asl, goal) end; (* simplify a goal by separating an expression which has pre-evaluation side effects *) fun GENERAL_PRE_SIDE_EFFECT_TAC expr newvarName (asl, goal) = let val (pre,goalstm,post) = strip_partial goal in if (--`Simple ^expr`--) = goalstm then (print_term expr;print "\n"; print_term goal;print "\n"; raise HOL_ERR {origin_structure = "partialTactics", origin_function = "GENERAL_PRE_SIDE_EFFECT_TAC", message = "redundant PRE_SIDE_EFFECT_TAC: code is already `Simple expr`"}) else let val repeq = sep_preeval_expr expr goalstm (SOME newvarName) val semeqThm = MATCH_MP Preeval_seq_equiv repeq val newstm = (hd o strip_op (--`SEM_EQ`--) o concl) semeqThm val newgoal = (--`Partial ^pre ^newstm ^post`--) in ([(asl,newgoal)], fn [th1] => MATCH_MP Sem_equiv_rule (CONJ th1 semeqThm)) end end; fun PRE_SIDE_EFFECT_TAC interm expr = GENERAL_PRE_SIDE_EFFECT_TAC expr (new_C_Result()) THEN SEQUENCE_TAC interm; (* simplify a goal by separating an expression which has post-evaluation side effects *) fun GENERAL_POST_SIDE_EFFECT_TAC expr (asl, goal) = let val (pre,goalstm,post) = strip_partial goal in if (--`Simple ^expr`--) = goalstm then (print_term expr;print "\n"; print_term goal;print "\n"; raise HOL_ERR {origin_structure = "partialTactics", origin_function = "GENERAL_POST_SIDE_EFFECT_TAC", message = "redundant POST_SIDE_EFFECT_TAC: code is already `Simple expr`"}) else let val repeq = sep_posteval_expr expr goalstm val semeqThm = MATCH_MP Posteval_seq_equiv repeq val newstm = (hd o strip_op (--`SEM_EQ`--) o concl) semeqThm val newgoal = (--`Partial ^pre ^newstm ^post`--) in ([(asl,newgoal)], fn [th1] => MATCH_MP Sem_equiv_rule (CONJ th1 semeqThm)) end end; fun POST_SIDE_EFFECT_TAC interm expr = GENERAL_POST_SIDE_EFFECT_TAC expr THEN SEQUENCE_TAC interm; (*----------------------------------------------------------------------- Tactic for If statements -----------------------------------------------------------------------*) fun GENERAL_IFTHENELSE_TAC test (asl, goal) = let val (pre,code,post) = strip_partial goal val [expr,body1,body2] = strip_op (--`IfElse`--) code val tstax = (--`IS_VALUE ^expr ^test`--) and body1ax = (--`Partial (^pre /\ ^test) ^body1 ^post`--) and body2ax = (--`Partial (^pre /\ ~ ^test) ^body2 ^post`--) in ([(asl,tstax),(asl,body1ax),(asl,body2ax)], fn [th1,th2,th3] => MATCH_MP IfThenElse_rule (LIST_CONJ [th2, th3, th1])) end; (* auxilliary function. Given an IS_VALUE axiom created by mk_VALUE from a C expression, return the equivalent HOL expression. *) fun get_hol_expr valAx = (el 2 o snd o strip_comb o snd o dest_thm) valAx; fun IFTHENELSE_TAC (asl, goal) = let val (_,code,_) = strip_partial goal val [expr,_,_] = strip_op (--`IfElse`--) code val tstthm = mk_VALUE expr val test = get_hol_expr tstthm in (GENERAL_IFTHENELSE_TAC test THENL [ ACCEPT_TAC tstthm, ALL_TAC, ALL_TAC]) (asl, goal) end; fun GENERAL_IFTHEN_TAC test (asl, goal) = let val (pre,code,post) = strip_partial goal val [expr,body] = strip_op (--`If`--) code val tstax = (--`IS_VALUE ^expr ^test`--) and bodyax = (--`Partial (^pre /\ ^test) ^body ^post`--) and skipax = (--`^pre /\ ~ ^test ==> ^post`--) in ([(asl,tstax),(asl,skipax),(asl,bodyax)], fn [th1,th2,th3] => MATCH_MP IfThen_rule (LIST_CONJ [th1, th3, th2])) end; fun IFTHEN_TAC (asl, goal) = let val (_,code,_) = strip_partial goal val [expr,_] = strip_op (--`If`--) code val tstthm = mk_VALUE expr val test = get_hol_expr tstthm in (GENERAL_IFTHEN_TAC test THENL [ ACCEPT_TAC tstthm, TAUT_TAC ORELSE ALL_TAC, ALL_TAC]) (asl, goal) end; (*----------------------------------------------------------------------- Tactic for while loops -----------------------------------------------------------------------*) local (* for GENERAL_WHILE_TAC *) (* sometimes we just need a simple, dummy expression *) val const0expr = (--`Const (CCint 0) Int`--); (* writing an ML variable is easier than writing the term *) val EmptyStmt = (--`EmptyStmt`--); local (* for extract_expr *) (* how much should we extract from the expression? *) datatype howFaithful = Value | Minimal; datatype howMuchSE = PreSE | PostSE | NoSE; type exflags = {sideefs : howMuchSE, extent : howFaithful}; (* this marks a branch which should never be taken or code is not finished *) val SKIMPstmt = (--`SKIMP:CStmt`--); (* If the term is an Lvalue, return the equivalent Cexpr. If it is already a Cexpr, return it unchanged. *) fun makeCexpr trm = if type_of trm = (==`:Lvalue`==) then (--`Lval ^trm`--) else trm; (* test cases test_result (makeCexpr (--`Vref (Var "ouch" 0 Int)`--)) (--`Lval (Vref (Var "ouch" 0 Int))`--); test_result (makeCexpr const0expr) const0expr; *) (* Return an certain extract of cexpr. It may include or exclude preeval side effects and posteval side effects. It may return a minimal expression or an expression with the same value as the original (assuming preeval side effects have taken place). A temporary variable may be returned instead of a function call. *) fun extract_expr_lv xf lval = let val {sideefs,extent} = xf val (opr,rands) = strip_comb lval in if opr = (--`Vref`--) then if extent = Value then lval else EmptyStmt else if opr = (--`Aryref`--) then let val extrand = extract_expr xf (el 2 rands) in if extent = Minimal then extrand else (* Value *) (--`Aryref ^(el 1 rands) ^extrand`--) end else if opr = (--`Deref`--) then let val extrand = extract_expr xf (el 1 rands) in if extent = Minimal then extrand else (* Value *) (--`Deref ^extrand`--) end else if opr = (--`Field`--) orelse opr = (--`Arrow`--) then let val extrand = extract_expr_lv xf (el 1 rands) in if extent = Minimal then extrand else (* Value *) (--`^opr ^extrand ^(el 2 rands)`--) end else raise Fail "unknown Lval operation" end and extract_expr (xf:exflags) cexpr = let val {sideefs,extent} = xf val (opr,rands) = strip_comb cexpr in if opr = (--`Const`--) then if extent = Minimal then EmptyStmt else cexpr else if opr = (--`Lval`--) then let val extlv = extract_expr_lv xf (el 1 rands) in makeCexpr extlv end else if opr = (--`Assign`--) then if sideefs = NoSE then (--`Lval ^(extract_expr_lv xf (el 1 rands))`--) else if sideefs = PreSE then let val newxf = {sideefs=sideefs,extent=Value} val extlhs = extract_expr_lv newxf (el 1 rands) val extrhs = extract_expr newxf (el 2 rands) in (--`Assign ^extlhs ^extrhs`--) end else (* PostSE *) let val extlhs = extract_expr_lv xf (el 1 rands) val extrhs = extract_expr xf (el 2 rands) in if extent = Minimal then if extlhs = EmptyStmt then extrhs else if extrhs = EmptyStmt then extlhs else (* don't repeat the assignment, just do the expressions *) (--`Comma ^(makeCexpr extlhs) ^(makeCexpr extrhs)`--) else (* Value *) makeCexpr extlhs end else if opr = (--`Binary`--) then if sideefs = NoSE then if extent = Value then (--`Binary ^(extract_expr xf (el 1 rands)) ^(el 2 rands) ^(extract_expr xf (el 3 rands))`--) else SKIMPstmt else (* PreSE or PostSE *) let val extlop = extract_expr xf (el 1 rands) val extrop = extract_expr xf (el 3 rands) in (* Note: if we ask for Value above, we'll never get EmptyStmt *) if extlop = EmptyStmt then extrop else if extrop = EmptyStmt then extlop else (--`Binary ^extlop ^(el 2 rands) ^extrop`--) end else if opr = (--`LUnary`--) then let val luop = el 1 rands val lurand = el 2 rands in if sideefs = NoSE then let val extrand = extract_expr_lv xf lurand in if luop = (--`AdrOf`--) then (--`LUnary ^luop ^extrand`--) else makeCexpr extrand end else if sideefs = PreSE then if luop = (--`PreInc`--) orelse luop = (--`PreDec`--) then let val newxf = {sideefs=sideefs,extent=Value} val extrand = extract_expr_lv newxf lurand in (--`LUnary ^luop ^extrand`--) end else let val extrand = extract_expr_lv xf lurand in if luop = (--`AdrOf`--) andalso extent = Value then (--`LUnary ^luop ^extrand)`--) else makeCexpr extrand end else (* must be sideefs = PostSE *) if luop = (--`PostInc`--) orelse luop = (--`PostDec`--) then let val newxf = {sideefs=sideefs,extent=Value} val extrand = extract_expr_lv newxf lurand in (--`LUnary ^luop ^extrand`--) end else let val extrand = extract_expr_lv xf lurand in if luop = (--`AdrOf`--) andalso extent = Value then (--`LUnary ^luop ^extrand)`--) else makeCexpr extrand end end else if opr = (--`Unary`--) then let val extrand = extract_expr xf (el 2 rands) in if extent = Value then (--`Unary ^(el 1 rands) ^extrand`--) else extrand end else if opr = (--`Call`--) then if sideefs = NoSE then let val newname = new_C_Result() val cresultType = el 3 (strip_op (--`Var`--) (el 1 rands)) in (--`Lval (Vref (Var ^(mk_str newname) 0 ^cresultType))`--) end else if sideefs = PreSE then let val cvar = el 1 rands val plst = el 2 rands val newxf = {sideefs=sideefs,extent=Value} val extpl = foldrpl (fn plhd=> (fn rest=> (--`PL ^(extract_expr newxf plhd) ^rest`--))) plst (--`PLnull`--) in (--`Call ^cvar ^extpl`--) end else (* must be PostSE *) let val cvar = el 1 rands val plst = el 2 rands in if extent = Minimal then let fun filtEmpty plhd rest = let val extpl = extract_expr xf plhd in if extpl = EmptyStmt then rest else if rest = EmptyStmt then extpl else (--`Comma ^extpl ^rest`--) end in foldrpl filtEmpty plst EmptyStmt end else (* extent is Value *) let fun extractpls plhd rest = (--`PL ^(extract_expr xf plhd) ^rest`--) val extpl = foldrpl extractpls plst (--`PLnull`--) in (--`Call ^cvar ^extpl`--) end end else raise Fail "unknown CExpr operation" end; (* test cases test_result (extract_expr {sideefs=NoSE,extent=Value} (--`Binary (Lval(Vref(Var "k" 0 Int))) NEq (Const(CCint 0)Int)`--)) (--`Binary (Lval(Vref(Var "k" 0 Int))) NEq (Const(CCint 0)Int)`--); test_result (extract_expr {sideefs=NoSE,extent=Value} (--`Binary (Assign (Vref(Var "t" 0 Int))(Const(CCint 1)Int)) Mul (LUnary PreInc (Vref(Var "s" 0 Int)))`--)) (--`Binary (Lval(Vref(Var "t" 0 Int))) Mul (Lval(Vref(Var "s" 0 Int)))`--); test_result (extract_expr {sideefs=NoSE,extent=Value} (--`Assign (Aryref (Var "t" 0 Char) (LUnary PreInc (Vref(Var "s" 0 Int)))) (Const (CCstr "trouble") (Ptr Char))`--)) (--`Lval (Aryref (Var "t" 0 Char) (Lval(Vref(Var "s" 0 Int))))`--); test_result (extract_expr {sideefs=NoSE,extent=Value} (--`Unary Not (Call (Var "logfile" 0 Char) PLnull)`--)) (--`Unary Not (Lval (Vref (Var "C_Resultnn" 0 Char)))`--); test_result (extract_expr {sideefs=PreSE,extent=Minimal} (--`Binary (Lval(Vref(Var "k" 0 Int))) NEq (Const(CCint 0)Int)`--)) EmptyStmt; test_result (extract_expr {sideefs=PreSE,extent=Minimal} (--`Binary (Assign (Vref(Var "t" 0 Int))(Const(CCint 1)Int)) Mul (LUnary PreInc (Vref(Var "s" 0 Int)))`--)) (--`Binary (Assign (Vref(Var "t" 0 Int))(Const(CCint 1)Int)) Mul (LUnary PreInc (Vref(Var "s" 0 Int)))`--); test_result (extract_expr {sideefs=PreSE,extent=Minimal} (--`Assign (Aryref (Var "t" 0 Char) (LUnary PostInc (Vref(Var "s" 0 Int)))) (Const (CCstr "trouble") (Ptr Char))`--)) (--`Assign (Aryref (Var "t" 0 Char) (Lval(Vref(Var "s" 0 Int)))) (Const (CCstr "trouble") (Ptr Char))`--); test_result (extract_expr {sideefs=PreSE,extent=Minimal} (--`Unary Not (Call (Var "logfile" 0 Char) (PL (LUnary PostDec (Vref(Var "s" 0 Int))) PLnull))`--)) (--`Call (Var "logfile" 0 Char) (PL (Lval(Vref(Var "s" 0 Int))) PLnull)`--); test_result (extract_expr {sideefs=PostSE,extent=Minimal} (--`Binary (Lval(Vref(Var "k" 0 Int))) NEq (Const(CCint 0)Int)`--)) EmptyStmt; test_result (extract_expr {sideefs=PostSE,extent=Minimal} (--`Binary (Assign (Vref(Var "t" 0 Int))(Const(CCint 1)Int)) Mul (LUnary PostInc (Vref(Var "s" 0 Int)))`--)) (--`LUnary PostInc (Vref(Var "s" 0 Int))`--); test_result (extract_expr {sideefs=PostSE,extent=Minimal} (--`Assign (Aryref (Var "t" 0 Char) (LUnary PostInc (Vref(Var "s" 0 Int)))) (LUnary PostDec (Vref(Var "u" 0 Int)))`--)) (--`Comma (LUnary PostInc (Vref(Var "s" 0 Int))) (LUnary PostDec (Vref(Var "u" 0 Int)))`--); test_result (extract_expr {sideefs=PostSE,extent=Minimal} (--`Unary Not (Call (Var "logfile" 0 Char) (PL (LUnary PostDec (Vref(Var "s" 0 Int)))PLnull))`--)) (--`LUnary PostDec (Vref(Var "s" 0 Int))`--); test_result (extract_expr {sideefs=PostSE,extent=Value} (--`Assign (Vref (Var "n" 0 Int)) (Call (Var "read" 0 Int) (PL (Lval (Vref (Var "i" 0 Int))) PLnull))`--)) (--`Lval (Vref (Var "n" 0 Int))`--); *) in fun extract_prese cexpr = extract_expr {sideefs=PreSE,extent=Minimal} cexpr and extract_nose cexpr = extract_expr {sideefs=NoSE,extent=Value} cexpr and extract_nopre cexpr = extract_expr {sideefs=PostSE,extent=Value} cexpr and extract_postse cexpr = extract_expr {sideefs=PostSE,extent=Minimal} cexpr; end; (* local extract_cexpr *) fun makeSimple trm = if type_of trm = (==`:CExpr`==) then (--`Simple ^trm`--) else trm; (* from pre or post SE statement extract the side effect expression (or use a dummy), and build the empty-or-simple theorem *) fun emptyOrSimp stm = if stm = EmptyStmt then let val seExpr = const0expr (* dummy expr *) in (true, DISJ1 (REFL stm) (--`^stm = (Simple ^seExpr)`--), seExpr) end else let val seExpr = el 1 (strip_op (--`Simple`--) stm) in (false, DISJ2 (--`^stm = EmptyStmt`--) (REFL (--`Simple ^seExpr`--)), seExpr) end; (* some lemmas to break SEM_EQ goals into subgoals *) val Lemma_Empty_Empty = prove( (--`!s.SEM_EQ (Seq EmptyStmt (Seq s EmptyStmt)) s`--), REPEAT STRIP_TAC THEN MATCH_MP_TAC SEM_EQ_TRANS THEN EXISTS_TAC (--`Seq s EmptyStmt`--) THEN CONJ_TAC THEN REWRITE_TAC [Empty_null_left, Empty_null_right]); val Lemma_Empty_Post = prove( (--`! testEx postSeEx orig. PostEval (Simple testEx) postSeEx (Simple orig) ==> SEM_EQ (Seq EmptyStmt (Seq (Simple testEx) (Simple postSeEx))) (Simple orig)`--), REPEAT STRIP_TAC THEN MATCH_MP_TAC SEM_EQ_TRANS THEN EXISTS_TAC (--`Seq (Simple testEx) (Simple postSeEx)`--) THEN CONJ_TAC THENL [ REWRITE_TAC [Empty_null_left], MATCH_MP_TAC Posteval_seq_equiv THEN ASM_REWRITE_TAC [] ] ); val Lemma_Pre_Empty = prove( (--`! lv preSeEx testEx orig. PreEval lv preSeEx (Simple testEx) (Simple orig) ==> SEM_EQ (Seq (Simple preSeEx) (Seq (Simple testEx) EmptyStmt)) (Simple orig)`--), REPEAT STRIP_TAC THEN MATCH_MP_TAC SEM_EQ_TRANS THEN EXISTS_TAC (--`Seq (Simple preSeEx) (Simple testEx)`--) THEN CONJ_TAC THENL [ MATCH_MP_TAC Seq_semantic_comp THEN CONJ_TAC THEN REWRITE_TAC [SEM_EQ_REFL,Empty_null_right], MATCH_MP_TAC Preeval_seq_equiv THEN EXISTS_TAC (--`lv:Lvalue`--) THEN ASM_REWRITE_TAC [] ] ); val Lemma_Pre_Post = prove( (--`! preSeEx testEx postSeEx lv testNoPre orig. PreEval lv preSeEx (Simple testNoPre) (Simple orig) /\ PostEval (Simple testEx) postSeEx (Simple testNoPre) ==> SEM_EQ (Seq (Simple preSeEx) (Seq (Simple testEx) (Simple postSeEx))) (Simple orig)`--), REPEAT STRIP_TAC THEN MATCH_MP_TAC SEM_EQ_TRANS THEN EXISTS_TAC (--`Seq (Simple preSeEx) (Simple testNoPre)`--) THEN CONJ_TAC THENL [ MATCH_MP_TAC Seq_semantic_comp THEN CONJ_TAC THENL [ REWRITE_TAC [SEM_EQ_REFL], MATCH_MP_TAC Posteval_seq_equiv THEN ASM_REWRITE_TAC [] ], MATCH_MP_TAC Preeval_seq_equiv THEN EXISTS_TAC (--`lv:Lvalue`--) THEN ASM_REWRITE_TAC [] ] ); val Lemma_impl = prove((--`! n . n ==> n`--), REWRITE_TAC []); in fun GENERAL_WHILE_TAC testStateOpt bodyCondOpt (asl, goal) = let val (invariant,code,post) = strip_partial goal val [expr,body] = strip_op (--`CWhile`--) code (* pick out preeval side effects and prove some "matching" theorems *) val preStm = makeSimple (extract_prese expr) val testNoPre = extract_nopre expr val (preIsEmpty,preStmThm,preSeEx) = emptyOrSimp preStm val noSEpreThm = prove_NoPostSE preSeEx val (testCond,prePrtlThm,prePrtlGoal) = if preIsEmpty then (invariant, SPEC invariant SKIP_AX, (--`0`--) (* not needed *)) else if testStateOpt = NONE then (print "preeval side effects: ";print_term preSeEx; print "\n"; raise HOL_ERR {origin_structure = "partialTactics", origin_function = "GENERAL_WHILE_TAC", message = "test has preeval side effects, so a test state condition is required"}) else (strip_SOME testStateOpt, TRUTH (* not needed *), (--`Partial ^invariant ^preStm ^(strip_SOME testStateOpt)`--)) (* pick out posteval side effects and prove some "matching" theorems *) val postStm = makeSimple (extract_postse testNoPre) val (postIsEmpty,postStmThm,postSeEx) = emptyOrSimp postStm val noSEpostThm = prove_NoPreSE postSeEx (* pick out the actual loop test condition (no side effects) *) val testExpr = extract_nose testNoPre val isvalThm = mk_VALUE testExpr val test = get_hol_expr isvalThm (* develop conditions, theorems, or goals depending on circumstances *) val (postCond,postPrtlThm,postPrtlGoal) = let val tcondNottest = (--`^testCond /\ ~ ^test`--) in if postIsEmpty then (tcondNottest, SPEC tcondNottest SKIP_AX, (--`0`--) (* not needed *)) else (post, TRUTH (* not needed *), (--`Partial ^tcondNottest ^postStm ^post`--)) end val (bodyCond,postBodyThm,postBodyGoal) = let val tcondAndtest = (--`^testCond /\ ^test`--) in if postIsEmpty then (tcondAndtest, SPEC tcondAndtest SKIP_AX, (--`0`--) (* not needed *)) else if bodyCondOpt = NONE then (print "posteval side effects: ";print_term postSeEx;print"\n"; raise HOL_ERR {origin_structure = "partialTactics", origin_function = "GENERAL_WHILE_TAC", message = "test has posteval side effects, so a body state condition is required"}) else (strip_SOME bodyCondOpt, TRUTH (* not needed *), (--`Partial ^tcondAndtest ^postStm ^(strip_SOME bodyCondOpt)`--)) end (* create more goals and theorems *) val bodyGoal = (--`Partial ^bodyCond ^body ^invariant`--) val (mustWeaken,postImplThm,postImplGoal) = if postCond <> post then (true, TRUTH, (* not used *) (--`^postCond ==> ^post`--)) else (false, SPEC post Lemma_impl, const0expr (* not used *)); in if preIsEmpty andalso postIsEmpty then let val semeqThm = SPEC (--`Simple ^expr`--) Lemma_Empty_Empty in if mustWeaken then ([(asl,postImplGoal),(asl,bodyGoal)], fn [postImplThm,bodyThm] => MATCH_MP While_rule (LIST_CONJ [prePrtlThm, postBodyThm, bodyThm, postPrtlThm, semeqThm, noSEpreThm, noSEpostThm, preStmThm, postStmThm, isvalThm, postImplThm]) ) else ([(asl,bodyGoal)], fn [bodyThm] => MATCH_MP While_rule (LIST_CONJ [prePrtlThm, postBodyThm, bodyThm, postPrtlThm, semeqThm, noSEpreThm, noSEpostThm, preStmThm, postStmThm, isvalThm, postImplThm]) ) end else if preIsEmpty andalso not postIsEmpty then let val postImpSemeqThm = SPECL [testExpr,postSeEx,expr] Lemma_Empty_Post val postEvThm = prove_PostEval ((#ant o dest_imp o concl) postImpSemeqThm) val semeqThm = MATCH_MP postImpSemeqThm postEvThm in ([(asl,postPrtlGoal),(asl,postBodyGoal),(asl,bodyGoal)], fn [postPrtlThm,postBodyThm,bodyThm] => MATCH_MP While_rule (LIST_CONJ [prePrtlThm, postBodyThm, bodyThm, postPrtlThm, semeqThm, noSEpreThm, noSEpostThm, preStmThm, postStmThm, isvalThm, postImplThm]) ) end else if not preIsEmpty andalso postIsEmpty then (* SKIMP - we should get some real lvalue here some day *) let val newlval = (--`Deref ^const0expr`--) val preImpSemeqThm = SPECL [newlval,preSeEx,testExpr,expr] Lemma_Pre_Empty val preEvThm = prove_PreEval ((#ant o dest_imp o concl) preImpSemeqThm) val semeqThm = MATCH_MP preImpSemeqThm preEvThm in if mustWeaken then ([(asl,postImplGoal),(asl,prePrtlGoal),(asl,bodyGoal)], fn [postImplThm,prePrtlThm,bodyThm] => MATCH_MP While_rule (LIST_CONJ [prePrtlThm, postBodyThm, bodyThm, postPrtlThm, semeqThm, noSEpreThm, noSEpostThm, preStmThm, postStmThm, isvalThm, postImplThm]) ) else ([(asl,prePrtlGoal),(asl,bodyGoal)], fn [prePrtlThm,bodyThm] => MATCH_MP While_rule (LIST_CONJ [prePrtlThm, postBodyThm, bodyThm, postPrtlThm, semeqThm, noSEpreThm, noSEpostThm, preStmThm, postStmThm, isvalThm, postImplThm]) ) end else (* both pre and post side effects *) let val newlval = (--`Deref ^const0expr`--) val prePostImpSemeqThm = SPECL [preSeEx,testExpr,postSeEx,newlval, testNoPre,expr] Lemma_Pre_Post val {conj1=preGoal,conj2=postGoal} = (dest_conj o #ant o dest_imp o concl) prePostImpSemeqThm; val preEvThm = prove_PreEval preGoal val postEvThm = prove_PostEval postGoal val semeqThm = MATCH_MP prePostImpSemeqThm (CONJ preEvThm postEvThm) in ([(asl,prePrtlGoal),(asl,postPrtlGoal),(asl,postBodyGoal),(asl,bodyGoal)], fn [prePrtlThm,postPrtlThm,postBodyThm,bodyThm] => MATCH_MP While_rule (LIST_CONJ [prePrtlThm, postBodyThm, bodyThm, postPrtlThm, semeqThm, noSEpreThm, noSEpostThm, preStmThm, postStmThm, isvalThm, postImplThm]) ) end end; end; (* local for GENERAL_WHILE_TAC *) (* this is only useful if there are no side effects in the test *) fun WHILE_TAC (asl, goal) = GENERAL_WHILE_TAC NONE NONE (asl, goal); (*----------------------------------------------------------------------- Tactic for Blocks with local variables -----------------------------------------------------------------------*) fun BLOCK_TAC (asl, goal) = MATCH_MP_TAC Block_rule (asl, goal); (*----------------------------------------------------------------------- Tactics for functions calls -----------------------------------------------------------------------*) (* prove a theorem of the result of some constructors by applying conversions which rewrite each one. For example, prove_convs [APPEND_CONV,ADD_CONV] (--`APPEND [1+2;3+4] [7;2+3]`--) returns |- [3; 7; 7; 5] = APPEND [1 + 2; 3 + 4] [7; 2 + 3] *) fun prove_convs convs tm = GSYM (DEPTH_CONV(FIRST_CONV convs) tm); (*------ Define a specialization of varargs in the formals ----------------*) local val nilCvar = (--`[]:Cvar list`--) fun specialize formals actuals = if formals = nilCvar then if actuals = (--`PLnull`--) then nilCvar else raise HOL_ERR {origin_structure = "partialTactics", origin_function = "specVarargs_CONV", message = "too many actuals"} else if formals = (--`varargs:Cvar list`--) then (* convert actuals from here on *) let fun retype chd = let val newvarName=(mk_str o #Name o dest_var o genvar)(==`:string`==) in (--`Var ^newvarName 0 ^(ctype_of chd)`--) end in foldrpl (fn chd=>(fn rest=>(--`CONS ^(retype chd) ^rest`--))) actuals nilCvar end else (* formals is a list *) if actuals = (--`PLnull`--) then raise HOL_ERR {origin_structure = "partialTactics", origin_function = "specVarargs_CONV", message = "too many formals"} else let val [fhd,ftl] = strip_op (--`CONS:Cvar->Cvar list->Cvar list`--)formals val [_,atl] = strip_op (--`PL`--) actuals in (--`CONS ^fhd ^(specialize ftl atl)`--) end in fun specVarargs_CONV (trm:term) = let val [formals,actuals] = strip_op (--`specialize_varargs`--) trm in mk_thm([], (--`^trm = ^(specialize formals actuals)`--)) end end; (* test ... val vspecs1 = (--`specialize_varargs [] PLnull`--); test_result (concl (specVarargs_CONV vspecs1)) (--`^vspecs1 = []`--); val vspecs2 = (--`specialize_varargs [Var "f1" 0 Int] PLnull`--); "too many formals"; specVarargs_CONV vspecs2 handle e=>Raise e; val vspecs3 = (--`specialize_varargs [Var "f1" 0 Int] (PL (Const(CCint 1)Int) PLnull)`--); test_result (concl (specVarargs_CONV vspecs3)) (--`^vspecs3 = [Var "f1" 0 Int]`--); val vspecs4 = (--`specialize_varargs (varargs) PLnull`--); test_result (concl (specVarargs_CONV vspecs4)) (--`^vspecs4 = []`--); val vspecs5 = (--`specialize_varargs (varargs) (PL (Const(CCint 1)Int) PLnull)`--); "fails because genvar won't match"; test_result (concl (specVarargs_CONV vspecs5)) (--`^vspecs5 = [Var "%%genvar%%something" 0 Int]`--); val vspecs6 = (--`specialize_varargs (CONS (Var "f1" 0 Int) varargs) (PL (Const(CCint 1)Int) (PL (Const (CCstr "hello, dolly") (Ptr Char)) (PL (Binary (Const(CCint 1)Int) Add (Lval(Vref(Var "j" 0 Int)))) PLnull)))`--); "fails because genvar won't match"; test_result (concl (specVarargs_CONV vspecs6)) (--`^vspecs6 = [Var "f1" 0 Int;Var "%%genvar%%something" 0 (Ptr Char); Var "%%genvar%%something" 0 Int]`--); *) fun prove_specVarargs nm pred = GSYM (specVarargs_CONV (--`specialize_varargs ^nm ^pred`--)); local fun univquant [] pred = pred | univquant (vh::vt) pred = (--`! ^(cvar2hol vh) . ^(univquant vt pred)`--); in fun UNIVQUANT_CONV uqTm = let val [vl,pred] = strip_op (--`UNIVQUANT`--) uqTm in mk_thm([], (--`^uqTm = ^(univquant (lsthol2sml vl) pred)`--)) end end; (* test val uq1 = (--`UNIVQUANT [Var "b" 0 Char; Var "a" 0 (Array Int (CCint 32)); Var "c" 0 Void] (z>a/\b)`--); val _ = "we must specify this term, where b is a bool and a is a CArray,"; val _ = "separately from uq1 since the parser insists that variables in the"; val _ = "same term are the same type"; val uq1r = (--`!(c :void). z > a /\ b`--); test_result (concl (UNIVQUANT_CONV uq1)) (--`^uq1 = ! (b:ascii) (a:num CArray). ^uq1r`--); *) local (* for PL2CEL_CONV *) (* reduce a PL2CEL equality theorem *) fun reduce_PL2CEL predThm = let (* rewrite one step of PL2CEL. The resulting theorem is something like |- PL2CEL a = CONS (hd a) (PL2CEL (tl a)) or it hasn't changed *) val spredThm = PURE_ONCE_REWRITE_RULE [GEN_REWRITE_CONV (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites [PL2CEL_DEF] (concl predThm)] predThm in if spredThm = predThm then (* progress halted *) (print_thm predThm; print "\n"; raise HOL_ERR {origin_structure = "partialTactics", origin_function = "reduce_PL2CEL", message = "cannot reduce term"}) else if hasOpr "PL2CEL" ((#rhs o dest_eq o concl) spredThm) then reduce_PL2CEL spredThm else spredThm end; in fun PL2CEL_CONV pl2celTm = (* fail quickly when term doesn't start with PL2CEL *) if (#Name o dest_const o fst o strip_comb) pl2celTm <> "PL2CEL" orelse pl2celTm = (--`PL2CEL`--) then raise HOL_ERR {origin_structure = "partialTactics", origin_function = "PL2CEL", message = "term is not PL2CEL ..."} else reduce_PL2CEL (REFL pl2celTm); end; (* tests val p2c1 = (--`PL2CEL PLnull`--); test_result (concl (PL2CEL_CONV p2c1)) (--`^p2c1 = []`--); val p2c2 = (--`PL2CEL (PL (Lval (Vref (Var "b" 1 Char))) PLnull)`--); test_result (concl (PL2CEL_CONV p2c2)) (--`^p2c2 = [Lval (Vref (Var "b" 1 Char))]`--); val p2c3 = (--`PL2CEL (PL (Const (CCint 20) Int) (PL (Binary (Const (CCint 60) Int) Mul (Const (CCint 5) Int)) (PL (Call (Var "localtime" 0 (Ptr (Struct "tm"))) (PL (LUnary AdrOf (Vref (Var "t" 0 Int))) PLnull)) PLnull)))`--); test_result (concl (PL2CEL_CONV p2c3)) (--`^p2c3 = [Const (CCint 20) Int; Binary (Const (CCint 60) Int) Mul (Const (CCint 5) Int); Call (Var "localtime" 0 (Ptr (Struct "tm"))) (PL (LUnary AdrOf (Vref (Var "t" 0 Int))) PLnull)]`--); val p2c4 = (--`PL2CEL (PL (Lval (Vref (Var "b" 1 Char))) varargs)`--); "should fail since PL2CEL varargs can't be decided by this"; PL2CEL_CONV p2c4 handle e=>Raise e; "should fail quietly since term is a bare PL2CEL"; PL2CEL_CONV (--`PL2CEL`--) handle e=>Raise e; "should fail since term doesn't begin with PL2CEL"; PL2CEL_CONV (--`T`--) handle e=>Raise e; *) (* make sure the reduction is successful, ie, that the argument is a list *) fun reduced value = let val opnm = (#Name o dest_const o #1 o strip_comb) value in if opnm <> "CONS" andalso opnm <> "NIL" then (print "value not reduced:\n"; print_term value; print "\n"; raise Fail "value not reduced") else value end; (* prove a Simple Call from a WF_fnp Func theorem (does precondition strengthening, too) *) fun GENERAL_CALL_TAC wffnpthm newcr (asl, goal) = let val (goalpre,simpcall,qpost) = strip_partial goal val [namevar,plist] = strip_op (--`Call`--) (hd (strip_op (--`Simple`--) simpcall)) val [pre,func,post] = strip_op (--`WF_fnp`--) (concl wffnpthm) val [tnamevar,vvals,globls,_] = strip_op (--`Func`--) func in if namevar <> tnamevar then raise HOL_ERR {origin_structure = "partialTactics", origin_function = "GENERAL_CALL_TAC", message = "Call var and WF_fnp Func var differ"} else let val wfcthm = prove_WF_c simpcall val vargspecEqthm = prove_specVarargs vvals plist val vals = lresult vargspecEqthm val vals'Eqthm = prove_convs [APPEND_CONV,variants_CONV,FV_a_CONV] (--`variants ^vals (APPEND (FV_a ^qpost) ^globls)`--) val vals' = reduced (lresult vals'Eqthm) val yEqthm = prove_append vals globls val y = reduced (lresult yEqthm) val xEqthm = prove_append vals' globls val x = reduced (lresult xEqthm) val x0Eqthm = prove_logicals x val x0 = lresult x0Eqthm val y0Eqthm = prove_logicals y val y0 = lresult y0Eqthm val x0'Eqthm = prove_convs [variants_CONV,FV_a_CONV] (--`variants ^x0 (FV_a ^qpost)`--) val x0' = lresult x0'Eqthm (* get the C_Result's (if any) in the WF_fnp postconditions *) val cresults = find_variants C_RESULT post val cresultType = case length cresults of 0 => (* no C_Result, use a dummy *) (--`Void`--) | 1 => (* exactly one C_Result *) (holtype2c o type_of o hd) cresults | _ => (* more than one C_Result *) raise HOL_ERR {origin_structure = "partialTactics", origin_function = "GENERAL_CALL_TAC", message = "WF_fnp post has multiple C_Result's"} val genrC_Result = (--`[Var ^(mk_str C_RESULT) 0 ^cresultType]`--) val newC_Result = (--`[Var ^(mk_str newcr) 0 ^cresultType]`--) val specpostEqthm = prove_convs [APPEND_CONV,SUBS_CONV] (--`SUBS ^post (APPEND ^vals' ^x0') (APPEND ^vals ^y0)`--) val specpost = lresult specpostEqthm val postimpqEqthm = prove_convs [SUBS_CONV] (--`SUBS (^specpost ==> ^qpost) ^newC_Result ^genrC_Result`--) val postimpq = lresult postimpqEqthm val univpostEqthm = prove_convs [UNIVQUANT_CONV,SUBS_CONV] (--`SUBS (UNIVQUANT ^x ^postimpq) ^x ^x0'`--) val univpost = lresult univpostEqthm val specpreEqthm = prove_convs [SUBS_CONV] (--`SUBS ^pre ^vals' ^vals`--) val specpre = lresult specpreEqthm val newpreEqthm = prove_convs [SUBSE_CONV,PL2CEL_CONV] (--`SUBSE (^specpre /\ ^univpost) ^vals' (PL2CEL ^plist)`--) val newpre = lresult newpreEqthm val impsubgoal = (--`^goalpre ==> ^newpre`--) in ([(asl,impsubgoal)], fn [th1] => MATCH_MP Pre_strengthen_rule (CONJ (MATCH_MP Call_rule (LIST_CONJ [wffnpthm, wfcthm, vargspecEqthm, vals'Eqthm, yEqthm, xEqthm, x0Eqthm, y0Eqthm, x0'Eqthm, specpostEqthm, postimpqEqthm, univpostEqthm, specpreEqthm, newpreEqthm])) th1)) end end; fun CALL_TAC wffnpthm = GENERAL_CALL_TAC wffnpthm (new_C_Result()); local (* for SEP_CALL_TAC *) (* find the leftmost, deepest call to the function, eg, for (Call k (PL 7)) + (Call k (PL 6)) it returns (Call k (PL 7)) and for 3 + (Call k (PL 1 (Call k (PL 2 3)))) * 6 it returns (Call k (PL 2 3)) *) fun find_first_call fname trm = if is_comb trm then let val {Rator=rator,Rand=rand} = dest_comb trm in if rator = (--`Call ^fname`--) then let val deep = find_first_call fname rand in if deep = NONE then (* this is a call and there is no deeper one *) SOME trm else (* return the deeper call *) deep end else let val ratorres = find_first_call fname rator in if ratorres <> NONE then ratorres else find_first_call fname rand end end else (* this is a constant or var. (Can't have binders in C AST's) *) NONE; (* tests val kvar = (--`Var "k" 0 Int`--); fun ffc kv trm = let val result = find_first_call kv trm in case result of SOME t => t | NONE => (--`"no call found"`--) end; test_result (ffc kvar (--`Binary (Call ^kvar (PL (Const (CCstr "7") (Ptr Char)) PLnull)) Add (Call ^kvar (PL (Const (CCstr "6") (Ptr Char))PLnull))`--)) (--`Call ^kvar (PL (Const (CCstr "7") (Ptr Char)) PLnull)`--); test_result (ffc kvar (--`Binary (Binary (Const(CCint 3)Int) Add (Call ^kvar (PL (Const (CCstr "1") (Ptr Char)) (PL (Call ^kvar (PL (Const (CCstr "2") (Ptr Char)) PLnull)) PLnull)))) Mul (Const(CCint 6)Int)`--)) (--`Call ^kvar (PL (Const (CCstr "2") (Ptr Char)) PLnull)`--); *) (* specialize a predicate for a particular C_Result name *) fun specPred pred newCRstr newCtype = let val holexpType = ctype2hol newCtype val genericCResult = mk_var{Name=C_RESULT, Ty=holexpType} val newCResult = mk_var{Name=newCRstr, Ty=holexpType} in alpha_convert pred [genericCResult] [newCResult] end; in (* (set up to) prove an embedded function call. The steps are: Find the first call to the function, separate out the function call as a side effect, and finish the subgoal with GENERAL_CALL_TAC Subgoals may be left from the pre- and post- condition matching. *) fun SEP_CALL_TAC interm wffnpthm (asl, goal) = let val newResultName = new_C_Result() val fname = (hd o strip_op (--`Func`--) o el 2 o strip_op (--`WF_fnp`--) o concl) wffnpthm val SOME expr = find_first_call fname (#2 (strip_partial goal)) in (GENERAL_PRE_SIDE_EFFECT_TAC expr newResultName THEN SEQUENCE_TAC (specPred interm newResultName (ctype_of expr)) THENL [ GENERAL_CALL_TAC wffnpthm newResultName, ALL_TAC (* leave the simplified expression alone *) ]) (asl, goal) end; end; (* end of $Source: /users/lal/black/hol/Disser/RCS/partialTactics.sml,v $ *)