diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/correctness/pextract.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/correctness/pextract.ml')
-rw-r--r-- | contrib/correctness/pextract.ml | 473 |
1 files changed, 473 insertions, 0 deletions
diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml new file mode 100644 index 00000000..2a35d471 --- /dev/null +++ b/contrib/correctness/pextract.ml @@ -0,0 +1,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,v 1.5.6.1 2004/07/16 19:30:01 herbelin Exp $ *) + +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) |