1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11(* interface to Norbert Schirmer's Hoare Package code *) 12structure HPfninfo = 13struct 14 15 type t = {fname : string, 16 inparams : (string * typ * int Absyn.ctype option) list, 17 outparams : (string * typ * int Absyn.ctype) list, 18 body : Absyn.ext_decl HoarePackage.bodykind option, 19 spec : (string * Element.context) list, 20 mod_annotated_protop : bool, 21 recursivep : bool} 22 23end 24 25signature HPINTER = 26sig 27 28 type csenv = ProgramAnalysis.csenv 29 type fninfo = HPfninfo.t 30 val globalsN : string 31 val asm_to_string : (term -> string) -> ('typ,term,'fact) Element.ctxt -> string 32 val mk_fninfo : theory -> csenv -> (string -> bool) -> 33 Absyn.ext_decl list -> fninfo list 34 val make_function_definitions : 35 string -> (* name of locale where definitions will live *) 36 csenv -> (* result of ProgramAnalysis over declarations *) 37 typ list -> (* type arguments to state type operator *) 38 thm list -> (* theorems defining names of functions *) 39 fninfo list -> (* result of mk_fninfo above *) 40 (Absyn.ext_decl list -> Proof.context -> (string * term * term) list) -> 41 (* compilation/translation function *) 42 string -> (* name of globals locale *) 43 (typ,'a,'b) Element.ctxt list -> 44 (* globals living in the globals locale *) 45 theory -> 46 (string * theory) 47 48 49end 50 51structure HPInter : HPINTER = 52struct 53 54type fninfo = HPfninfo.t 55type csenv = ProgramAnalysis.csenv 56 57(* make function information - perform a preliminary analysis on the 58 abstract syntax to extract function names, parameters and specifications *) 59fun mk_fninfo thy csenv includeP decllist : fninfo list = let 60 open Absyn NameGeneration 61 (* don't fold top-level declarations into the table again: the program 62 analysis that built the csenv in the first place will have already 63 grabbed this *) 64 fun toInclude (FnDefn((_, fname), _, _, _)) = includeP (node fname) 65 | toInclude _ = false 66 val table = List.foldl 67 (fn (d, tab) => if toInclude d then 68 ProgramAnalysis.update_hpfninfo0 d tab 69 else tab) 70 (ProgramAnalysis.get_hpfninfo csenv) 71 decllist 72 fun parse_spec fname fspec = 73 case fspec of 74 fnspec spec => let 75 val toklist = Token.explode (Thy_Header.get_keywords thy) Position.none (node spec) 76 (* it might be nice to remember where the spec came 77 from so we could put in a reasonable pos'n above *) 78 val filtered = List.filter Token.is_proper toklist 79 val eof = Token.stopper 80 val nameproplist = valOf (Scan.read eof 81 HoarePackage.proc_specs 82 filtered) 83 handle Option => 84 raise Fail ("Failed to scan spec for "^fname) 85 fun nprop2Assume (name, prop) = 86 ((Binding.name name, []), [(prop, [])]) 87 in 88 [("", Element.Assumes (map nprop2Assume nameproplist))] 89 end 90 | fn_modifies slist => let 91 val mgoal = Modifies_Proofs.gen_modify_goalstring csenv fname slist 92 in 93 [("", Element.Assumes [((Binding.name (fname ^ "_modifies"), []), 94 [(mgoal, [])])])] 95 end 96 | didnt_translate => [] 97 | gcc_attribs _ => [] 98 | relspec _ => [] (* fixme *) 99 fun parse_specs fname fspecs = 100 List.concat (map (parse_spec fname) fspecs) 101 fun mk_ret rettype = 102 if rettype = Void then [] 103 else [(MString.dest (return_var_name rettype), 104 CalculateState.ctype_to_typ (thy, rettype), 105 rettype)] 106 fun to_param vi = let 107 open CalculateState ProgramAnalysis 108 val cty = get_vi_type vi 109 val typ = ctype_to_typ (thy,cty) 110 in 111 (MString.dest (get_mname vi), typ, SOME cty) 112 end 113 fun foldthis (_, d) acc = 114 case d of 115 FnDefn((_ (* retty *),fname_w), _ (* inparams *), prepost, _ (* body *)) => let 116 open HoarePackage CalculateState ProgramAnalysis 117 val fname = node fname_w 118 val rettype = valOf (get_rettype fname csenv) 119 in 120 {fname = fname, 121 inparams = map to_param (valOf (get_params fname csenv)) 122 handle Option => 123 raise Fail ("mk_fninfo: No function information for "^ 124 fname), 125 outparams = mk_ret rettype, 126 recursivep = is_recursivefn csenv fname, 127 body = SOME (BodyTerm d), spec = parse_specs fname prepost, 128 mod_annotated_protop = false} 129 :: 130 acc 131 end 132 | Decl d0 => let 133 in 134 case node d0 of 135 ExtFnDecl { name, specs, params = _, rettype = _ } => let 136 open CalculateState ProgramAnalysis 137 val fname = node name 138 val params = map to_param (valOf (get_params fname csenv)) 139 handle Option => 140 raise Fail ("mk_fninfo: No function information for "^ 141 fname) 142 val rettype = valOf (get_rettype fname csenv) 143 val _ = Feedback.informStr (0, "Added external decl for " ^ 144 fname ^ " with " ^ Int.toString (length params) ^ 145 " args.") 146 val spec = parse_specs fname specs 147 val mod_annotated_protop = isSome (get_modifies csenv fname) 148 val body = NONE 149 in 150 {fname = fname, 151 inparams = params, recursivep = false, 152 outparams = mk_ret rettype, body = body, 153 spec = spec, mod_annotated_protop = mod_annotated_protop} 154 :: 155 acc 156 end 157 | _ => acc 158 end 159in 160 Symtab.fold foldthis table [] 161end 162 163fun extract_element_asms e = 164 case e of 165 Element.Assumes asms => 166 map (fn (nm, [(t,_)]) => (nm, t) 167 | _ => raise Fail "extract_element_term: malformed Assumes") asms 168 | _ => raise Fail "extract_element_term: malformed element" 169 170fun mkSpecFunction thy gloc cse styargs (f : fninfo) = let 171 open TermsTypes 172 val {fname,...} = f 173 val state_ty = hd styargs 174 val ctxt = thy2ctxt thy 175 val mods = fname |> ProgramAnalysis.get_modifies cse 176 |> valOf |> Binaryset.listItems 177 val s = Free("s", state_ty) 178 val t = Free("t", state_ty) 179 val relbody = Modifies_Proofs.gen_modify_body thy state_ty s t mods 180 val collect_t = mk_collect_t (mk_prod_ty (state_ty, state_ty)) 181 fun typedterm t = 182 Syntax.string_of_term ctxt t ^ " :: " ^ 183 Syntax.string_of_typ ctxt (type_of t) 184 fun appi f l = let 185 fun recurse i l = case l of [] => () | h::t => (f i h; recurse (i + 1) t) 186 in 187 recurse 0 l 188 end 189 190 fun parse_spec thy (_, e) = let 191 val lnm_strs = extract_element_asms e 192 fun innermap thy (((speclocalename_b,_), tstr)) = let 193 val speclocalename = Binding.name_of speclocalename_b 194 (* jump into an lthy corresponding to globloc to parse the tstr; this lthy 195 is dropped and not used again *) 196 val lthy = Named_Target.init gloc thy 197 val tm = Syntax.read_term lthy tstr 198 val (vs, body) = strip_forall tm 199 val PQopt = 200 case body of 201 Const(@{const_name "hoarep"}, _) $ _ (* gamma *) $ _ $_ $ P $ _ $ Q $ _ => 202 if String.isSuffix "modifies" speclocalename then NONE 203 else SOME (P,Q) 204 | _ => 205 let 206 val (f, args) = strip_comb tm 207 val cstr = case f of Const(s, _) => "const: "^s 208 | Free(s, _) => "free: "^s 209 | _ => "huh?" 210 in 211 raise Fail ("parse_spec: bad specification " ^ speclocalename ^ " : " ^ 212 Syntax.string_of_term ctxt t ^ "\n(" ^ 213 cstr ^ " applied to " ^ 214 Int.toString (length args) ^ " arguments)") 215 end 216 in 217 case PQopt of 218 NONE => NONE 219 | SOME (P0, Q0) => 220 let 221 val _ = appi (fn n => fn v => 222 Feedback.informStr(0, "var#"^Int.toString n^" "^typedterm v)) vs 223 val elty0 = dest_set_type (type_of P0) 224 val sigma = valOf (TermsTypes.match_type_frees{pattern = elty0, m = state_ty}) 225 handle Option => raise Fail "Couldn't match state types" 226 val ptype = Syntax.string_of_typ ctxt 227 fun foldthis (ty1, ty2) acc = (ptype ty1 ^ " |-> " ^ ptype ty2) :: acc 228 val sigma_elts0 = TypTable.fold foldthis sigma [] 229 val sigma_elts = String.concatWith ", " sigma_elts0 230 val _ = Feedback.informStr(0, "Sigma = " ^ sigma_elts) 231 val P1 = subst_frees sigma P0 232 val Q1 = subst_frees sigma Q0 233 val vs = map (subst_frees sigma) vs 234 val s = variant vs s 235 val t = variant vs t 236 val P2 = List.foldr (fn (v, t) => unbeta{bv=v,body=t}) P1 vs 237 val Q2 = List.foldr (fn (v, t) => unbeta{bv=v,body=t}) Q1 vs 238 val _ = Feedback.informStr(0, "P2 : " ^ typedterm P2) 239 val _ = Feedback.informStr(0, "Q2 : " ^ typedterm Q2) 240 val P = list_mk_comb(P2, vs) 241 val Q = list_mk_comb(Q2, vs) 242 243 val _ = Feedback.informStr(0, "P : " ^ typedterm P) 244 val _ = Feedback.informStr(0, "Q : " ^ typedterm Q) 245 val _ = Feedback.informStr(0, "s : " ^ typedterm s) 246 val _ = Feedback.informStr(0, "t : " ^ typedterm t) 247 val body_imp = list_mk_forall(vs, mk_imp(mk_IN(s,P), mk_IN(t,Q))) 248 val Pexists = list_mk_exists(vs, mk_IN(s,P)) 249 val res = collect_t $ list_mk_pabs([s,t], mk_conj(body_imp, Pexists)) 250 val _ = Feedback.informStr(0, "Type of PQ combo: " ^ ptype (type_of res)) 251 in 252 SOME res 253 end 254 end 255 in 256 List.mapPartial (innermap thy) lnm_strs 257 end 258 259 val mod_spec = collect_t $ list_mk_pabs([s,t], relbody) 260 val _ = Feedback.informStr(0, "modstr : " ^ typedterm mod_spec) 261 val otherspecs = List.concat (map (parse_spec thy) (#spec f)) 262 val fbody = 263 if null otherspecs then 264 mk_Spec(styargs, mod_spec) 265 else 266 let 267 val _ = appi (fn n => fn t => Feedback.informStr(0, 268 "spec#" ^ Int.toString n ^ ": " ^ typedterm t)) otherspecs 269 val spec_t = List.foldl mk_inter mod_spec otherspecs 270 in 271 Const(@{const_name "guarded_spec_body"}, 272 @{typ "strictc_errortype"} --> type_of spec_t --> 273 mk_com_ty styargs) $ @{const "ImpossibleSpec"} $ spec_t 274 end 275in 276 (fname, fbody, fbody) 277end 278 279 280(* compile bodies - turn a list of AST values into a term list *) 281fun compile_fninfos globloc cse styargs compfn lthy (fninfo : fninfo list) = let 282 open HoarePackage 283 fun partition (acc as (asts,specs)) fns = 284 case fns of 285 [] => (List.rev asts, specs) 286 | {body = SOME (BodyTerm x),...} :: t => partition (x::asts,specs) t 287 | (i as {mod_annotated_protop = true, ...}) :: t => 288 partition (asts,i::specs) t 289 | _ :: t => partition acc t 290 val (asts,toSpec) = partition ([],[]) fninfo 291in 292 compfn asts lthy @ 293 map (mkSpecFunction (Proof_Context.theory_of lthy) globloc cse styargs) toSpec 294end 295 296fun rhs_extras rhs = 297 Term.fold_aterms 298 (fn v as Free _ => insert (op aconv) v | _ => I) 299 rhs 300 []; 301 302fun extract_fixes elems = let 303 open Element 304 fun fix2term (n,tyopt,_) = 305 case tyopt of 306 NONE => NONE 307 | SOME ty => SOME (Free(Binding.name_of n,ty)) 308 fun recurse elems = 309 case elems of 310 [] => [] 311 | Fixes fs::rest => List.mapPartial fix2term fs @ recurse rest 312 | _ :: rest => recurse rest 313in 314 recurse elems 315end 316 317fun create_bodyloc_elems globs thy (name, body_t, body_stripped_t) = 318let 319 val rhs_vars0 = rhs_extras body_t 320 321 (* Library.subtract has arguments in wrong order - sheesh! *) 322 val rhs_vars = subtract (op aconv) globs rhs_vars0 323 324 fun mk_rhs(nm, vars, t) = let 325 val t0 = TermsTypes.list_mk_abs (vars, t) 326 in 327 (nm, Term.map_types (Sign.certify_typ thy) t0) 328 end 329 330 val eqt_stripped = mk_rhs(name ^ "_body", [], body_stripped_t) 331 val eqt = mk_rhs(name ^ (if null rhs_vars then "_body" else "_invs_body"), 332 rhs_vars, body_t) 333 fun eqn_to_definfo (nm, t) = let 334 val b = Binding.name nm 335 in 336 ((b, NoSyn), ((Thm.def_binding b, []), t)) 337 end 338 val elems = 339 if null rhs_vars then [eqn_to_definfo eqt] 340 else [eqn_to_definfo eqt_stripped, eqn_to_definfo eqt] 341 type lthy_def_info = (binding * mixfix) * (Attrib.binding * term) 342in 343 (elems : lthy_def_info list, 344 (name, if null rhs_vars then body_t else body_stripped_t)) 345end 346 347val globalsN = "_global_addresses" 348fun add_syntax (name,recp,inpars,outpars) thy = let 349 open HoarePackage 350 val name = suffix HoarePackage.proc_deco name 351 val pars = map (fn par => (In,varname par)) inpars@ 352 map (fn par => (Out,varname par)) outpars 353 354 val thy_decl = 355 thy |> Context.theory_map (add_params Morphism.identity name pars) 356 |> Context.theory_map 357 (add_state_kind Morphism.identity name HoarePackage.Record) 358 |> (if recp then 359 Context.theory_map (add_recursive Morphism.identity name) 360 else (fn x => x)) 361in 362 thy_decl 363end 364 365fun asm_to_string tmw e = 366 case e of 367 Element.Assumes asms => let 368 fun asm_element pfx ((nm, _ (*attrs*)), ttmlist) = 369 pfx ^ Binding.name_of nm ^ ": " ^ 370 commas (map (tmw o #1) ttmlist) ^ "\n" 371 in 372 "Assumes:" ^ (if length asms = 1 then 373 " " ^ String.concat (map (asm_element "") asms) 374 else 375 "\n" ^ String.concat (map (asm_element " ") asms)) 376 end 377 | Element.Fixes stysynlist => 378 "Fixes: " ^ commas (map (Binding.name_of o #1) stysynlist) ^ "\n" 379 | _ => "??\n" 380; 381 382(* The following is modelled on the code in HoarePackage.procedures_definition 383*) 384fun make_function_definitions localename 385 (cse : ProgramAnalysis.csenv) 386 (styargs : typ list) 387 (nmdefs : thm list) 388 (fninfo : fninfo list) 389 compfn 390 globloc 391 globals_elems 392 thy = 393let 394 open HoarePackage 395 val localename_b = Binding.name localename 396 val thy = thy |> Context.theory_map (HoarePackage.set_default_state_kind 397 HoarePackage.Record) 398 val name_pars = 399 map (fn {fname,inparams,outparams,recursivep,...} => 400 (fname, recursivep, map #1 inparams, map #1 outparams)) 401 fninfo 402 val name_specs = map (fn {fname,spec,...} => (fname,spec)) fninfo 403 val thy = List.foldr (uncurry add_syntax) thy name_pars 404 val lthy = Named_Target.init globloc thy 405 val name_body = compile_fninfos globloc cse styargs compfn lthy fninfo 406 val _ = Feedback.informStr (0, "Translated all functions") 407 val globs = extract_fixes globals_elems 408 409 val body_elems = map (create_bodyloc_elems globs thy) name_body 410 411 fun add_body_defs ((elems, _ (* name-body *)), lthy) = let 412 fun foldthis (e, lthy) = let 413 val _ = Feedback.informStr (0, "Adding body_def for " ^ Binding.name_of (#1 (#1 e))) 414 in 415 Local_Theory.reset (#2 (Local_Theory.define e lthy)) 416 end 417 in 418 List.foldl foldthis lthy elems 419 end 420 val lthy = List.foldl add_body_defs lthy body_elems 421 val thy = Local_Theory.exit_global lthy 422 423 (* set up _impl by defining \<Gamma> *) 424 val thy = 425 if List.exists (isSome o #body) fninfo then let 426 val lthy = Named_Target.init globloc thy 427 fun get_body fni = let 428 val nm = #fname fni 429 in 430 case (#body fni, #mod_annotated_protop fni) of 431 (NONE, false) => NONE 432 | _ => let 433 val realnm = 434 Consts.intern (Proof_Context.consts_of lthy) (nm ^ "_body") 435 in 436 SOME (Syntax.check_term lthy (Const(realnm, dummyT))) 437 end 438 end 439 (* name for thm, (proc constant, body constant) *) 440 val (_, lthy) = StaticFun.define_tree_and_thms_with_defs 441 @{binding \<Gamma>} (map (suffix HoarePackage.implementationN o #fname) fninfo) 442 nmdefs (map get_body fninfo) @{term "id :: int => int"} lthy 443 in 444 Local_Theory.exit_global lthy 445 end 446 else thy 447 448 val globloc_expr = ([(globloc, (("", false), (Expression.Named [], [])))], []) 449 450 (* three levels of folding - woohoo *) 451 fun add_spec_locales ((name,specs), (localemap, thy)) = let 452 (* add any spec locales *) 453 fun foldthis ((_, e), (localemap, thy)) = let 454 val lnm_strs = extract_element_asms e 455 fun innerfold (((speclocalename_b,_), tstr), (localemap, thy)) = let 456 val speclocalename = Binding.name_of speclocalename_b 457 (* jump into an lthy corresponding to globloc to parse the tstr; this lthy 458 is dropped and not used again *) 459 val lthy = Named_Target.init globloc thy 460 val t = Syntax.read_term lthy tstr 461 val _ = Feedback.informStr (0, "Adding spec locale "^speclocalename^ 462 (if speclocalename = "" then "" else " ")^ 463 "for function "^name ^ " (" ^ tstr ^ ")") 464 val e' = Element.Assumes [((speclocalename_b,[]), 465 [(TermsTypes.mk_prop t, [])])] 466 val speclocalename_b = Binding.map_name 467 (fn s => if s = "" then 468 suffix HoarePackage.specL name 469 else s) 470 speclocalename_b 471 val (locname, ctxt') = 472 Expression.add_locale 473 speclocalename_b 474 speclocalename_b 475 globloc_expr 476 [e'] 477 thy 478 (* localename is the name we wanted, locname is the name Isabelle 479 gives back to us. This will be properly qualified yadda yadda *) 480 in 481 (Symtab.update (speclocalename, locname) localemap, 482 Local_Theory.exit_global ctxt') 483 end 484 in 485 List.foldl innerfold (localemap,thy) lnm_strs 486 end 487 val (speclocnames,thy) = List.foldl foldthis (localemap, thy) specs 488 in 489 (speclocnames, thy) 490 end 491 val (_ (* specloc_names *), thy) = 492 List.foldl add_spec_locales (Symtab.empty, thy) name_specs 493 494 val (globloc, ctxt) = 495 Expression.add_locale localename_b localename_b globloc_expr [] thy 496 497in 498 (globloc, Local_Theory.exit_global ctxt) 499end 500 501 502end (* struct *) 503