5.68. Why interface

Interface to Why program.
Start ocaml section to src/flx_why.mli[1 /1 ]
     1: # 6 "./lpsrc/flx_why.ipk"
     2: open Flx_ast
     3: open Flx_types
     4: open Flx_typing
     5: open Flx_mtypes2
     6: 
     7: val emit_whycode:
     8:   string ->
     9:   sym_state_t ->
    10:   fully_bound_symbol_table_t ->
    11:   int -> (* root for lookup of and/or/not etc *)
    12:   unit
    13: 
End ocaml section to src/flx_why.mli[1]
Start ocaml section to src/flx_why.ml[1 /1 ]
     1: # 20 "./lpsrc/flx_why.ipk"
     2: open Flx_util
     3: open Flx_ast
     4: open Flx_types
     5: open Flx_mtypes1
     6: open Flx_mtypes2
     7: open Flx_print
     8: open Flx_typing
     9: open Flx_mbind
    10: open Flx_srcref
    11: open List
    12: open Flx_unify
    13: open Flx_treg
    14: open Flx_exceptions
    15: open Flx_maps
    16: open Flx_lookup
    17: 
    18: let sr  = "[flx_why]dummy",0,0,0,0
    19: 
    20: (* Hackery to find logic functions in the library *)
    21: let find_function syms env name =
    22:   let entries =
    23:     try Some (lookup_name_in_env syms env sr name)
    24:     with _ -> None
    25:   in
    26:   let entries = match entries with
    27:     | Some (`FunctionEntry ls) -> ls
    28:     | Some (`NonFunctionEntry _ ) ->
    29:       print_endline ("[flx_why] Expected '" ^ name ^ "' to be function");
    30:       []
    31:     |  None ->
    32:       print_endline ("[flx_why] Can't find logic function '" ^ name ^ "' ");
    33:       []
    34:   in
    35:   let entries =
    36:     filter (fun {base_sym=i} ->
    37:       match
    38:         try Some (Hashtbl.find syms.dfns i)
    39:         with Not_found -> None
    40:       with
    41:       | Some {symdef=`SYMDEF_fun (_,args,res,ct,_,_) } ->
    42:         begin match name,args,res with
    43:         | "lnot",[`AST_name (_,"bool",[])],`AST_name (_,"bool",[]) -> true
    44:         | _,[`AST_name (_,"bool",[]); `AST_name (_,"bool",[])],`AST_name (_,"bool",[]) -> true
    45:         | _ -> false
    46:         end
    47:       | _ -> false
    48:     )
    49:     entries
    50:   in
    51:   match entries with
    52:   | [{base_sym=i}] -> i
    53:   | [] -> print_endline ("WARNING: flx_why cannot find '" ^ name ^ "'"); 0
    54:   | _ -> print_endline ("WARNING: flx_why found too many '" ^ name ^ "'"); 0
    55: 
    56: let find_logics syms root =
    57:   let env = build_env syms (Some root) in
    58:   let ff x = find_function syms env x in
    59:   [
    60:     ff "land", "and";
    61:     ff "lor", "or";
    62:     ff "implies", "->";
    63:     ff "eq", "<->";
    64:     ff "lnot", "not"
    65:   ]
    66: 
    67: let mn s = Flx_name.cid_of_flxid s
    68: 
    69: let getname syms bbdfns i =
    70:   try match Hashtbl.find syms.dfns i with {id=id} -> mn id
    71:   with Not_found ->
    72:   try match Hashtbl.find bbdfns i with id,_,_,_ -> mn id
    73:   with Not_found -> "index_" ^ si i
    74: 
    75: let flx_bool = `BTYP_unitsum 2
    76: 
    77: let isbool2 t =
    78:   reduce_type t = `BTYP_array (flx_bool, flx_bool)
    79: 
    80: let rec why_expr syms bbdfns (e: tbexpr_t) =
    81:   let ee e = why_expr syms bbdfns e in
    82:   match e with
    83:   | `BEXPR_apply ((`BEXPR_closure (i,ts),_),b),_ ->
    84:     let id = getname syms bbdfns i in
    85:     id ^ "_" ^ si i ^ "(" ^
    86:     (
    87:       match b with
    88:       | `BEXPR_tuple [],_ -> "void"
    89:       | `BEXPR_tuple ls,_ -> catmap ", " ee ls
    90:       | x -> ee x
    91:     ) ^
    92:     ")"
    93: 
    94: 
    95:   | `BEXPR_apply (a,b),_ ->
    96:      "apply(" ^ ee a ^ "," ^ ee b ^")"
    97: 
    98:   (* this probably isn't right, ignoring ts *)
    99:   | `BEXPR_closure (i,ts),_ ->
   100:     let id = getname syms bbdfns i in
   101:     id ^ "_" ^ si i
   102: 
   103:   (* this probably isn't right, ignoring ts *)
   104:   | `BEXPR_name (i,ts),_ ->
   105:     let id = getname syms bbdfns i in
   106:     id ^ "_" ^ si i
   107: 
   108:   | `BEXPR_tuple ls,_ ->
   109:     "(" ^ catmap ", " ee ls ^ ")"
   110: 
   111:   | `BEXPR_literal x,_ -> begin match x with
   112:     | `AST_int (s,j) -> let j = Big_int.int_of_big_int j in si j
   113:     | _ -> "UNKLIT"
   114:     end
   115:   | _ -> "UNKEXPR"
   116: 
   117: 
   118: let rec why_prop syms bbdfns logics (e: tbexpr_t) =
   119:   let ee e = why_expr syms bbdfns e in
   120:   let ep e = why_prop syms bbdfns logics e in
   121:   match e with
   122:   | `BEXPR_apply ((`BEXPR_closure (i,ts),_),b),_ ->
   123:     let op = try assoc i logics with Not_found -> "" in
   124:     begin match op with
   125:     | "and"
   126:     | "or"
   127:     | "->" ->
   128:       begin match b with
   129:       | `BEXPR_tuple [x;y],t when isbool2 t ->
   130:         ep x ^ " " ^ op ^ " " ^ ep y
   131: 
   132:       | _ -> failwith ("[flx_why] Wrong number or type of args to '" ^ op ^ "'")
   133:       end
   134: 
   135:     | "<->" ->
   136:       begin match b with
   137:       | `BEXPR_tuple [x;y],t when isbool2 t ->
   138:         ep x ^ " " ^ op ^ " " ^ ep y
   139: 
   140:       | _ -> "true=" ^ ee e
   141:       end
   142: 
   143: 
   144:     | "not" -> op ^ " " ^ ep b
   145: 
   146:     | "" -> "true=" ^ ee e
   147:     | _ -> assert false
   148:     end
   149:   | _ -> "true=" ^ ee e
   150: 
   151: 
   152: let cal_bvs bvs =
   153:   let tps = match bvs with
   154:     | [] -> ""
   155:     | [s,_] -> "'" ^ s ^ " "
   156:     | ss -> "('" ^ catmap ", '" fst ss ^ ") "
   157:   in tps
   158: 
   159: let emit_type syms bbdfns f index name sr bvs =
   160:   let srt = Flx_srcref.short_string_of_src sr in
   161:   output_string f ("(* type " ^ name ^ ", at "^srt^" *)\n");
   162: 
   163:   (* NOTE BUG: needs namespace qualifier mangled in! *)
   164:   if name = "int" then
   165:     output_string f ("(* type int" ^ " -- USE why's builtin *)\n\n")
   166:   else
   167:     let tps = cal_bvs bvs in
   168:     output_string f ("type " ^ tps ^ name ^ "\n\n")
   169: 
   170: let rec cal_type syms bbdfns t =
   171:   let ct t = cal_type syms bbdfns t in
   172:   match t with
   173:   | `BTYP_lvalue t -> ct t ^ " lvalue "
   174:   | `BTYP_tuple [] -> "unit"
   175:   | `BTYP_void -> "unit" (* cheat *)
   176:   | `BTYP_unitsum 2 -> "bool"
   177:   | `BTYP_function (a,b) ->
   178:     "(" ^ ct a ^ ", " ^ ct b ^ ") fn"
   179: 
   180:   | `BTYP_inst (index,ts) ->
   181:     let id,sr,parent,entry = Hashtbl.find bbdfns index in
   182:     (* HACK! *)
   183:     let ts = match ts with
   184:       | [] -> ""
   185:       | [t] -> cal_type syms bbdfns t ^ " "
   186:       | ts -> "(" ^ catmap ", " ct ts ^ ")"
   187:     in
   188:     ts ^ id
   189:   | `BTYP_var (index,_) ->
   190:     begin try
   191:       let id,sr,parent,entry = Hashtbl.find bbdfns index
   192:       in "'" ^ id
   193:     with Not_found -> "'T" ^ si index
   194:     end
   195: 
   196:   | _ -> "dunno"
   197: 
   198: let emit_axiom syms bbdfns logics f (k:axiom_kind_t) (name,sr,parent,kind,bvs,bps,e) =
   199:   if k <> kind then () else
   200:   let srt = Flx_srcref.short_string_of_src sr in
   201:   let tkind,ykind =
   202:     match kind with
   203:     | `Axiom -> "axiom","axiom"
   204:     | `Lemma -> "lemma","goal"
   205:   in
   206:   output_string f ("(* "^tkind^" " ^ name ^ ", at "^srt^" *)\n\n");
   207:   output_string f (ykind ^ " " ^ name ^ ":\n");
   208:   iter (fun {pkind=pkind; pid=pid; pindex=pindex; ptyp=ptyp} ->
   209:     output_string f
   210:     ("  forall " ^ pid ^ "_" ^ si pindex^ ": " ^ cal_type syms bbdfns ptyp ^ ".\n")
   211:   )
   212:   (fst bps)
   213:   ;
   214:   begin match e with
   215:   | `BPredicate e ->
   216:     output_string f ("    " ^ why_prop syms bbdfns logics e)
   217: 
   218:   | `BEquation (l,r) ->
   219:     output_string f ("  " ^
   220:       why_expr syms bbdfns l ^ " = " ^
   221:       why_expr syms bbdfns r
   222:     )
   223: 
   224:   end;
   225:   output_string f "\n\n"
   226: 
   227: let emit_reduction syms bbdfns logics f (name,bvs,bps,el,er) =
   228:   output_string f ("(* reduction " ^ name ^ " *)\n\n");
   229:   output_string f ("axiom " ^ name ^ ":\n");
   230:   iter (fun {pkind=pkind; pid=pid; pindex=pindex; ptyp=ptyp} ->
   231:     output_string f
   232:     ("  forall " ^ pid ^ "_" ^ si pindex^ ": " ^ cal_type syms bbdfns ptyp ^ ".\n")
   233:   )
   234:   bps
   235:   ;
   236:   output_string f ("    " ^ why_expr syms bbdfns el);
   237:   output_string f ("\n  = " ^ why_expr syms bbdfns er);
   238:   output_string f "\n\n"
   239: 
   240: 
   241: let emit_function syms (bbdfns:fully_bound_symbol_table_t) f index id sr bvs ps ret =
   242:   let srt = Flx_srcref.short_string_of_src sr in
   243:   output_string f ("(* function " ^ id ^ ", at "^srt^" *)\n");
   244:   let name = mn id ^ "_" ^ si index in
   245:   let dom = match ps with
   246:     | [] -> "unit"
   247:     | _ -> catmap ", " (cal_type syms bbdfns) ps
   248:   in
   249:   let cod = cal_type syms bbdfns ret in
   250:   output_string f ("logic " ^ name ^ ": " ^ dom ^ " -> " ^ cod ^ "\n\n")
   251: 
   252: let calps ps =
   253:   let ps = fst ps in (* elide constraint *)
   254:   let ps =
   255:     map
   256:     (* again a bit of a hack! *)
   257:     (fun {pkind=pk; pid=name; pindex=pidx; ptyp=t} -> t)
   258:     ps
   259:   in ps
   260: 
   261: let unitt = `BTYP_tuple []
   262: 
   263: let emit_whycode filename syms bbdfns root =
   264:   let logics = find_logics syms root in
   265:   let f = open_out filename in
   266:   output_string f "(****** HACKS *******)\n";
   267:   output_string f "type 'a lvalue  (* Felix lvalues *) \n";
   268:   output_string f "type dunno      (* translation error *)\n";
   269:   output_string f "type ('a,'b) fn (* functions *)\n";
   270:   output_string f "logic apply: ('a,'b) fn, 'a -> 'b (* application *)\n";
   271:   output_string f "\n";
   272: 
   273:   output_string f "(****** ABSTRACT TYPES *******)\n";
   274:   Hashtbl.iter
   275:   (fun index (id,parent,sr,entry) -> match entry with
   276:   | `BBDCL_abs (bvs,qual,ct,breqs) ->
   277:     emit_type syms bbdfns f index id sr bvs
   278:   | _ -> ()
   279:   )
   280:   bbdfns
   281:   ;
   282: 
   283:   output_string f "(****** UNIONS *******)\n";
   284:   Hashtbl.iter
   285:   (fun index (id,parent,sr,entry) -> match entry with
   286:   | `BBDCL_union (bvs,variants) ->
   287:     emit_type syms bbdfns f index id sr bvs
   288:   | _ -> ()
   289:   )
   290:   bbdfns
   291:   ;
   292: 
   293:   output_string f "(****** STRUCTS *******)\n";
   294:   Hashtbl.iter
   295:   (fun index (id,parent,sr,entry) -> match entry with
   296:   | `BBDCL_cstruct (bvs,variants)
   297:   | `BBDCL_struct (bvs,variants) ->
   298:     emit_type syms bbdfns f index id sr bvs
   299:   | _ -> ()
   300:   )
   301:   bbdfns
   302:   ;
   303: 
   304:   output_string f "(****** CLASSES *******)\n";
   305:   Hashtbl.iter
   306:   (fun index (id,parent,sr,entry) -> match entry with
   307:   | `BBDCL_class (_,bvs)
   308:   | `BBDCL_cclass (bvs,_) ->
   309:     emit_type syms bbdfns f index id sr bvs
   310:   | _ -> ()
   311:   )
   312:   bbdfns
   313:   ;
   314: 
   315: 
   316:   output_string f "(******* FUNCTIONS ******)\n";
   317:   Hashtbl.iter
   318:   (fun index (id,parent,sr,entry) -> match entry with
   319:   | `BBDCL_procedure (_,bvs,ps,_) ->
   320:     let ps = calps ps in
   321:     emit_function syms bbdfns f index id sr bvs ps unitt
   322: 
   323:   | `BBDCL_function (_,bvs,ps,ret,_) ->
   324:     let ps = calps ps in
   325:     emit_function syms bbdfns f index id sr bvs ps ret
   326: 
   327:   | `BBDCL_fun (_,bvs,ps,ret,_,_,_) ->
   328:     emit_function syms bbdfns f index id sr bvs ps ret
   329: 
   330:   | `BBDCL_proc (_,bvs,ps,_,_) ->
   331:     emit_function syms bbdfns f index id sr bvs ps unitt
   332: 
   333:   | _ -> ()
   334:   )
   335:   bbdfns
   336:   ;
   337: 
   338:   output_string f "(******* AXIOMS ******)\n";
   339:   iter
   340:   (emit_axiom syms bbdfns logics f `Axiom)
   341:   syms.axioms
   342:   ;
   343: 
   344:   output_string f "(******* REDUCTIONS ******)\n";
   345:   iter
   346:   (emit_reduction syms bbdfns logics f)
   347:   syms.reductions
   348:   ;
   349: 
   350:   output_string f "(******* LEMMAS (goals) ******)\n";
   351:   iter
   352:   (emit_axiom syms bbdfns logics f `Lemma)
   353:   syms.axioms
   354:   ;
   355:   close_out f
   356:   ;
   357: 
   358: 
End ocaml section to src/flx_why.ml[1]