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: