summaryrefslogtreecommitdiff
path: root/contrib/correctness/pextract.ml
blob: 407567ad795dcfd2f9256d38ea088cc820a9256a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)

(* $Id: pextract.ml 5920 2004-07-16 20:01:26Z herbelin $ *)

open Pp_control
open Pp
open Util
open System
open Names
open Term
open Himsg
open Reduction

open Putil
open Ptype
open Past
open Penv
open Putil

let extraction env c =
  let ren = initial_renaming env in
  let sign = Pcicenv.now_sign_of ren env in
  let fsign = Mach.fsign_of_sign (Evd.mt_evd()) sign in
  match Mach.infexecute (Evd.mt_evd()) (sign,fsign) c with
    | (_,Inf j) -> j._VAL
    | (_,Logic) -> failwith "Prog_extract.pp: should be informative"

(* les tableaux jouent un role particulier, puisqu'ils seront extraits
 * vers des tableaux ML *)

let sp_access = coq_constant ["correctness"; "Arrays"] "access"
let access = ConstRef sp_access

let has_array = ref false

let pp_conversions () =
  (str"\
let rec int_of_pos = function
    XH -> 1
  | XI p -> 2 * (int_of_pos p) + 1
  | XO p -> 2 * (int_of_pos p)
 ++ ++

let int_of_z = function
    ZERO -> 0
  | POS p -> int_of_pos p
  | NEG p -> -(int_of_pos p)
 ++ ++
") (* '"' *)

(* collect all section-path in a CIC constant *)

let spset_of_cci env c =
  let spl = Fw_env.collect (extraction env c) in
  let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in
  has_array := !has_array or (SpSet.mem sp_access sps) ++
  SpSet.remove sp_access sps


(* collect all Coq constants and all pgms appearing in a given program *)

let add_id env ((sp,ids) as s) id =
  if is_local env id then
    s
  else if is_global id then
    (sp,IdSet.add id ids)
  else
    try (SpSet.add (Nametab.sp_of_id FW id) sp,ids) with Not_found -> s

let collect env =
  let rec collect_desc env s = function
    | Var x -> add_id env s x
    | Acc x -> add_id env s x
    | Aff (x,e1) -> add_id env (collect_rec env s e1) x
    | TabAcc (_,x,e1) ->
	has_array := true ++
	add_id env (collect_rec env s e1) x
    | TabAff (_,x,e1,e2) ->
	has_array := true ++
	add_id env (collect_rec env (collect_rec env s e1) e2) x
    | Seq bl ->
	List.fold_left (fun s st -> match st with
			    Statement p -> collect_rec env s p
			  | _ -> s) s bl
    | If (e1,e2,e3) ->
    	collect_rec env (collect_rec env (collect_rec env s e1) e2) e3
    | While (b,_,_,bl) ->
	let s = List.fold_left (fun s st -> match st with
				    Statement p -> collect_rec env s p
				  | _ -> s) s bl in
	  collect_rec env s b
    | Lam (bl,e) ->
	collect_rec (traverse_binders env bl) s e
    | App (e1,l) ->
	let s = List.fold_left (fun s a -> match a with
				    Term t -> collect_rec env s t
				  | Type _ | Refarg _ -> s) s l in
	  collect_rec env s e1
    | SApp (_,l) ->
	List.fold_left (fun s a -> collect_rec env s a) s l
    | LetRef (x,e1,e2) ->
	let (_,v),_,_,_ = e1.info.kappa in
	  collect_rec (add (x,Ref v) env) (collect_rec env s e1) e2
    | LetIn (x,e1,e2) ->
	let (_,v),_,_,_ = e1.info.kappa in
	  collect_rec (add (x,v) env) (collect_rec env s e1) e2
    | LetRec (f,bl,_,_,e) ->
	let env' = traverse_binders env bl in
	let env'' = add (f,make_arrow bl e.info.kappa) env' in
	  collect_rec env'' s e
    | Debug (_,e1) -> collect_rec env s e1
    | PPoint (_,d) -> collect_desc env s d
    | Expression c ->
	let (sp,ids) = s in
	let sp' = spset_of_cci env c in
	SpSet.fold 
	  (fun s (es,ei) ->
	     let id = basename s in
	     if is_global id then (*SpSet.add s*)es,IdSet.add id ei
	     else SpSet.add s es,ei)
	  sp' (sp,ids)

  and collect_rec env s p = collect_desc env s p.desc

  in
  collect_rec env (SpSet.empty,IdSet.empty)


(* On a besoin de faire du renommage, tout comme pour l'extraction des
 * termes Coq. En ce qui concerne les globaux, on utilise la table de
 * Fwtoml. Pour les objects locaux, on introduit la structure de
 * renommage rename_struct
 *)

module Ocaml_ren = Ocaml.OCaml_renaming

let rename_global id =
  let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in
  Fwtoml.add_global_renaming (id,id') ++
  id'

type rename_struct = { rn_map : identifier IdMap.t;
		       rn_avoid : identifier list }

let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] }

let rename_local rn id =
  let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in
  { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid },
  id'

let get_local_name rn id = IdMap.find id rn.rn_map

let get_name env rn id =
  if is_local env id then
    get_local_name rn id
  else
    Fwtoml.get_global_name id

let rec rename_binders rn = function
  | [] -> rn
  | (id,_) :: bl -> let rn',_ = rename_local rn id in rename_binders rn' bl

(* on a bespoin d'un pretty-printer de constr particulier, qui reconnaisse
 * les acces a des references et dans des tableaux, et qui de plus n'imprime
 * pas de GENTERM lorsque des identificateurs ne sont pas visibles.
 * Il est simplifie dans la mesure ou l'on a ici que des constantes et
 * des applications.
 *)

let putpar par s =
  if par then (str"(" ++ s ++ str")") else s

let is_ref env id =
  try
    (match type_in_env env id with Ref _ -> true | _ -> false)
  with
    Not_found -> false

let rec pp_constr env rn = function
  | VAR id ->
      if is_ref env id then 
	(str"!" ++ pID (get_name env rn id)) 
      else
	pID (get_name env rn id)
  | DOPN((Const _|MutInd _|MutConstruct _) as oper, _) ->
      pID (Fwtoml.name_of_oper oper)
  | DOPN(AppL,v) ->
      if Array.length v = 0 then
	  (mt ())
      else begin
	match v.(0) with
	    DOPN(Const sp,_) when sp = sp_access ->
	      (pp_constr env rn v.(3) ++ 
		 str".(int_of_z " ++ pp_constr env rn v.(4) ++ str")")
	  | _ ->
	      hov 2 (putpar true (prvect_with_sep (fun () -> (spc ()))
				    (pp_constr env rn) v))
      end
  | DOP2(Cast,c,_) -> pp_constr env rn c
  | _ -> failwith "Prog_extract.pp_constr: unexpected constr"


(* pretty-print of imperative programs *)

let collect_lambda = 
  let rec collect acc p = match p.desc with
    | Lam(bl,t) -> collect (bl@acc) t
    | x         -> acc,p
  in 
  collect []

let pr_binding rn = 
  prlist_with_sep (fun () -> (mt ()))
    (function 
       | (id,(Untyped | BindType _)) -> 
	   (str" " ++ pID (get_local_name rn id))
       | (id,BindSet) -> (mt ()))

let pp_prog id =
  let rec pp_d env rn par = function
    | Var x -> pID (get_name env rn x)
    | Acc x -> (str"!" ++ pID (get_name env rn x))
    | Aff (x,e1) -> (pID (get_name env rn x) ++ 
		       str" := " ++ hov 0 (pp env rn false e1))
    | TabAcc (_,x,e1) ->
	(pID (get_name env rn x) ++ 
	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")")
    | TabAff (_,x,e1,e2) ->
	(pID (get_name env rn x) ++
	   str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")" ++
	   str" <-" ++ spc () ++ hov 2 (pp env rn false e2))
    | Seq bl ->
	(str"begin" ++ fnl () ++
	   str"  " ++ hov 0 (pp_block env rn bl) ++ fnl () ++
	   str"end")
    | If (e1,e2,e3) ->
	putpar par (str"if " ++ (pp env rn false e1) ++
		      str" then" ++ fnl () ++
		      str"  " ++ hov 0 (pp env rn false e2) ++ fnl () ++
		      str"else" ++ fnl () ++
		      str"  " ++ hov 0 (pp env rn false e3))
	(* optimisations : then begin .... end else begin ... end *)
    | While (b,inv,_,bl) ->
	(str"while " ++ (pp env rn false b) ++ str" do" ++ fnl () ++		    
	   str"  " ++
	   hov 0 ((match inv with
			 None -> (mt ()) 
		       | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ 
				      str" *)" ++ fnl ())) ++
		    pp_block env rn bl) ++ fnl () ++
	   str"done")
    | Lam (bl,e) ->
	let env' = traverse_binders env bl in
	let rn' = rename_binders rn bl in
	  putpar par 
	    (hov 2 (str"fun" ++ pr_binding rn' bl ++ str" ->" ++
		      spc () ++ pp env' rn' false e))
    | SApp ((Var id)::_,  [e1; e2])
	when id = connective_and or id = connective_or ->
	  let conn = if id = connective_and then "&" else "or" in
	  putpar par 
	    (hov 0 (pp env rn true e1 ++ spc () ++ str conn ++ spc () ++
		      pp env rn true e2))
    | SApp ((Var id)::_, [e]) when id = connective_not ->
	putpar par 
	  (hov 0 (str"not" ++ spc () ++ pp env rn true e))
    | SApp _ ->
	invalid_arg "Prog_extract.pp_prog (SApp)"
    | App(e1,[]) ->
	hov 0 (pp env rn false e1)
    | App (e1,l) ->
	putpar true
	  (hov 2 (pp env rn true e1 ++
		    prlist (function 
				Term p -> (spc () ++ pp env rn true p)
			      | Refarg x -> (spc () ++ pID (get_name env rn x))
			      | Type _ -> (mt ())) 
		      l))
    | LetRef (x,e1,e2) ->
	let (_,v),_,_,_ = e1.info.kappa in
	let env' = add (x,Ref v) env in
	let rn',x' = rename_local rn x in
	putpar par 
	  (hov 0 (str"let " ++ pID x' ++ str" = ref " ++ pp env rn false e1 ++
		    str" in" ++ fnl () ++ pp env' rn' false e2))
    | LetIn (x,e1,e2) ->
	let (_,v),_,_,_ = e1.info.kappa in
	let env' = add (x,v) env in
	let rn',x' = rename_local rn x in
	putpar par 
	  (hov 0 (str"let " ++ pID x' ++ str" = " ++ pp env rn false e1 ++
		    str" in" ++ fnl () ++ pp env' rn' false e2))
    | LetRec (f,bl,_,_,e) ->
	let env' = traverse_binders env bl in
	let rn' = rename_binders rn bl in
	let env'' = add (f,make_arrow bl e.info.kappa) env' in
	let rn'',f' = rename_local rn' f in
	putpar par 
	  (hov 0 (str"let rec " ++ pID f' ++ pr_binding rn' bl ++ str" =" ++ fnl () ++
		    str"  " ++ hov 0 (pp env'' rn'' false e) ++ fnl () ++
		    str"in " ++ pID f'))
    | Debug (_,e1) -> pp env rn par e1
    | PPoint (_,d) -> pp_d env rn par d
    | Expression c -> 
	pp_constr env rn (extraction env c)

  and pp_block env rn bl =
    let bl =
      map_succeed (function Statement p -> p | _ -> failwith "caught") bl
    in
      prlist_with_sep (fun () -> (str";" ++ fnl ()))
      	(fun p -> hov 0 (pp env rn false p)) bl

  and pp env rn par p = 
    (pp_d env rn par p.desc)

  and pp_mut v c = match v with
    | Ref _ ->
	(str"ref " ++ pp_constr empty rn_empty (extraction empty c))
    | Array (n,_) ->
	(str"Array.create " ++ cut () ++
	   putpar true 
	     (str"int_of_z " ++
		pp_constr empty rn_empty (extraction empty n)) ++
	   str" " ++ pp_constr empty rn_empty (extraction empty c))
    | _ -> invalid_arg "pp_mut"
  in
  let v = lookup_global id in
  let id' = rename_global id in
    if is_mutable v then
      try
	let c = find_init id in
	hov 0 (str"let " ++ pID id' ++ str" = " ++ pp_mut v c)
      with Not_found -> 
	errorlabstrm "Prog_extract.pp_prog"
	  (str"The variable " ++ pID id ++
	     str" must be initialized first !")
    else
      match find_pgm id with
	| None -> 
	    errorlabstrm "Prog_extract.pp_prog"
	      (str"The program " ++ pID id ++
		 str" must be realized first !")
      	| Some p ->
	    let bl,p = collect_lambda p in
	    let rn = rename_binders rn_empty bl in
	    let env = traverse_binders empty bl in
	    hov 0  (str"let " ++ pID id' ++ pr_binding rn bl ++ str" =" ++ fnl () ++ 
		      str"  " ++ hov 2 (pp env rn false p))

(* extraction des programmes impératifs/fonctionnels vers ocaml *)

(* Il faut parfois importer des modules non ouverts, sinon
 * Ocaml.OCaml_pp_file.pp echoue en disant "machin is not a defined
 * informative object". Cela dit, ce n'est pas tres satisfaisant, vu que
 * la constante existe quand meme: il vaudrait mieux contourner l'echec
 * de ml_import.fwsp_of_id
 *)

let import sp = match repr_path sp with
  | [m],_,_ ->
      begin
	try Library.import_export_module m true
        with _ -> ()
      end
  | _ -> ()

let pp_ocaml file prm =
  has_array := false ++
  (* on separe objects Coq et programmes *)
  let cic,pgms =
    List.fold_left
      (fun (sp,ids) id ->
	 if is_global id then (sp,IdSet.add id ids) else (IdSet.add id sp,ids))
      (IdSet.empty,IdSet.empty) prm.needed
  in
  (* on met les programmes dans l'ordre et pour chacun on recherche les
   * objects Coq necessaires, que l'on rajoute a l'ensemble cic *)
  let cic,_,pgms =
    let o_pgms = fold_all (fun (id,_) l -> id::l) empty [] in
    List.fold_left
      (fun (cic,pgms,pl) id -> 
	 if IdSet.mem id pgms then
	   let spl,pgms' =
	     try
	       (match find_pgm id with
		  | Some p -> collect empty p
		  | None ->
		      (try 
			 let c = find_init id in
			 spset_of_cci empty c,IdSet.empty
		       with Not_found -> 
			 SpSet.empty,IdSet.empty))
	     with Not_found -> SpSet.empty,IdSet.empty
	   in
	   let cic' = 
	     SpSet.fold 
	       (fun sp cic -> import sp ++ IdSet.add (basename sp) cic)
	       spl cic
	   in
	   (cic',IdSet.union pgms pgms',id::pl)
	 else
	   (cic,pgms,pl)) 
      (cic,pgms,[]) o_pgms
  in
  let cic = IdSet.elements cic in
  (* on pretty-print *)
  let prm' = { needed = cic ++ expand = prm.expand ++ 
	       expansion = prm.expansion ++ exact = prm.exact } 
  in
  let strm = (Ocaml.OCaml_pp_file.pp_recursive prm' ++
		fnl () ++ fnl () ++
		if !has_array then pp_conversions() else (mt ()) ++
		prlist (fun p -> (pp_prog p ++ fnl () ++ str";;" ++ fnl () ++ fnl ()))
		  pgms
)
  in
  (* puis on ecrit dans le fichier *)
  let chan = open_trapping_failure open_out file ".ml" in
  let ft = with_output_to chan in
  begin
    try  pP_with ft strm ++ pp_flush_with ft ()
    with e -> pp_flush_with ft () ++ close_out chan ++ raise e
  end ++
  close_out chan
    

(* Initializations of mutable objects *)

let initialize id com =
  let loc = Ast.loc com in
  let c = constr_of_com (Evd.mt_evd()) (initial_sign()) com in
  let ty = 
    Reductionops.nf_betaiota (type_of (Evd.mt_evd()) (initial_sign()) c) in
  try
    let v = lookup_global id in
    let ety = match v with 
      | Ref (TypePure c) -> c | Array (_,TypePure c) -> c
      | _ -> raise Not_found 
    in
    if conv (Evd.mt_evd()) ty ety then
      initialize id c
    else
      errorlabstrm "Prog_extract.initialize"
	(str"Not the expected type for the mutable " ++ pID id)
  with Not_found -> 
    errorlabstrm "Prog_extract.initialize"
      (pr_id id ++ str" is not a mutable")

(* grammaire *)

open Vernacinterp

let _ = vinterp_add "IMPERATIVEEXTRACTION"
	  (function 
	     | VARG_STRING file :: rem ->
		 let prm = parse_param rem in (fun () -> pp_ocaml file prm)
	     | _ -> assert false)
	  
let _ = vinterp_add "INITIALIZE"
	  (function 
	     | [VARG_IDENTIFIER id; VARG_COMMAND com] ->
		 (fun () -> initialize id com)
	     | _ -> assert false)