1 files changed, 0 insertions, 473 deletions

diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
deleted file mode 100644
index 407567ad..00000000
--- a/contrib/correctness/pextract.ml
+++ /dev/null
@@ -1,473 +0,0 @@
-(************************************************************************)
-(*  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)