supression vieux fichiers extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1529 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 495 deletions

diff --git a/contrib/extraction/mlimport.ml b/contrib/extraction/mlimport.ml
deleted file mode 100644
index 6fd5d8657..000000000
--- a/contrib/extraction/mlimport.ml
+++ /dev/null
@@ -1,495 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-open Pp
-open Names
-open Term
-open Libobject
-open Declare
-open Summary
-
-(* TODO : move this function to another file, like more_util. *)
-
-let list0n = 
-  let rec gen acc = function
-      -1 -> acc
-    | n  -> gen (n::acc) (n-1)
-  in 
-  gen []
-
-(* get a fresh name if necessary *)
-let rec next_global_ident id =
-  if not (is_global id) then id else next_global_ident (lift_ident id)
-
-(*s Importing ML objects, and linking axioms to terms. *)
-
-(* A table to keep the ML imports. *)
-
-let ml_import_tab = ref (Gmap.empty : (global_reference, identifier) Gmap.t)
-
-let ml_inductives = ref ([] : section_path list)
-
-let add_ml_inductive_import sp =
-  if not (List.mem sp !ml_inductives) then
-    ml_inductives := sp :: !ml_inductives
-
-let add_ml_import imp id =
-  ml_import_tab := Gmap.add imp id !ml_import_tab;
-  match imp with
-    | IndRef (sp,_) -> add_ml_inductive_import sp
-    | _ -> ()
-
-let find_ml_import imp = Gmap.find imp !ml_import_tab
-
-let is_ml_import op =
-  try let _ = find_ml_import op in true with Not_found -> false
-
-let sp_is_ml_import sp =
-     (is_ml_import (ConstRef sp))
-  or (is_ml_import (IndRef (sp,0)))
-  or (is_ml_import (ConstructRef ((sp,0),1)))
-
-let sp_prod = path_of_string "#Datatypes#prod.fw"
-
-let sp_is_ml_import_or_prod sp =
-  (sp = sp_prod) or (sp_is_ml_import sp)
-
-let inMLImport,outMLImport =
-  declare_object ("MLIMPORT",
-     { load_function = (fun _ -> ());
-       open_function = (fun (_,(imp,id)) -> add_ml_import imp id);
-       cache_function = (fun (_,(imp,id)) -> add_ml_import imp id);
-       export_function = (fun x -> Some x) })
-
-(* A table to keep the extractions to ML objects *)
-
-let ml_extract_tab = ref (Gmap.empty : (global_reference, identifier) Gmap.t)
-
-let add_ml_extract op id =
-  ml_extract_tab := Gmap.add op id !ml_extract_tab;
-  match op with 
-    | IndRef (sp,_) -> add_ml_inductive_import sp
-    | _ -> ()
-
-let find_ml_extract gr = Gmap.find gr !ml_extract_tab
-
-let is_ml_extract op = 
-  try let _ = find_ml_extract op in true with Not_found -> false
-
-let sp_is_ml_extract sp =
-     (is_ml_extract (ConstRef sp))
-  or (is_ml_extract (IndRef (sp,0)))
-  or (is_ml_extract (ConstructRef ((sp,0),1)))
-
-let inMLExtract,outMLExtract =
-  declare_object ("MLEXTRACT",
-     { load_function = (fun _ -> ());
-       open_function = (fun (_,(op,id)) -> add_ml_extract op id);
-       cache_function = (fun (_,(op,id)) -> add_ml_extract op id);
-       export_function = (fun x -> Some x) })
-
-let is_import_or_extract sp = sp_is_ml_import sp or sp_is_ml_extract sp
-
-(* Those two tables are rolled-back *)
-
-let freeze () =
-  (!ml_import_tab, !ml_inductives, !ml_extract_tab)
-
-let unfreeze (ft,stk,et) =
-  ml_import_tab := ft;
-  ml_inductives := stk;
-  ml_extract_tab := et
-
-let _ = declare_summary "MLIMPORT-TABLE"
-  { freeze_function   = freeze ;
-    unfreeze_function = unfreeze ;
-    init_function     = (fun () -> ml_import_tab := Gmap.empty;
-      	       	       	       	   ml_inductives := [];
-				   ml_extract_tab := Gmap.empty);
-    survive_section = false }
-
-(**************************************************************************)
-(*                      ML Import file__name : type.                      *)
-(**************************************************************************)
-
-(***** constants__make_parameter_body *****)
-let make_fw_parameter_body (hyps,jt) =
-  match level_of_type jt with
-    (Prop Pos) | (Type _) ->
-      {cONSTKIND = FW;
-       cONSTHYPS=hyps;
-       cONSTBODY=None;
-       cONSTEVAL = None;
-       cONSTOPAQUE = true;
-       cONSTTYPE= jt;
-       cONSTIMPARGS = NO_IMPL }
-  | _ -> errorlabstrm "make_fw_parameter_body" 
-         [< Printer.fprtype jt ; 'sTR " is not an informative term." >]
-
-
-(***** constants__infexecute_parameter *****)
-let fw_infexecute_parameter fhyps name t =
-  let sp = Lib.make_path OBJ name in
-  let (u,j) = fexecute_type_with_univ empty_evd fhyps sp t in
-  let ids = auto_save_variables() in
-  let fhyps' = thin_to_level fhyps (body_of_type j) in
-    (u,[FW,make_fw_parameter_body (fhyps',j)])
-
-
-(***** declare__machine_parameter *****)
-let fw_machine_parameter fhyps (name,cty) =
-  let (u',cmap) = fw_infexecute_parameter fhyps name cty in
-    add_named_object (name,OBJ) (inConstant(cmap,NeverDischarge,u'))
-
-
-(***** command__parameter_def_var *****)
-let fw_parameter id com =
-  let tcci = fconstr_of_com empty_evd (initial_fsign()) com in
-  let tfw = fwify tcci in
-  let _,fhyps = initial_assumptions() in
-  fw_machine_parameter fhyps (id,tfw)
-
-
-let ml_import id' id com =
-  fw_parameter id com ;
-  let sp = Lib.make_path FW id in
-  add_anonymous_object (inMLImport (Const sp, id')) ;
-  mSGNL [< 'sTR(string_of_id id) ; 'sTR" imported." >]
-
-
-let id_of_varg = function
-    VARG_IDENTIFIER id -> id
-  | VARG_STRING s -> (try id_of_string s with _ -> id_of_string (" "^s))
-  | _ -> invalid_arg "id_of_varg"
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("ML_IMPORT", function
-   [id'; VARG_IDENTIFIER id; VARG_COMMAND com] -> 
-     (fun () -> ml_import (id_of_varg id') id com)
- | _ -> anomaly "ML_IMPORT called with bad arguments.")
-
-
-
-(**************************************************************************)
-(*                         Link ident := Fw-term.                         *)
-(**************************************************************************)
-
-let not_an_axiom id =
-  errorlabstrm "ml_import__fw_link"
-  [< 'sTR(string_of_id id) ; 'sTR" is not an FW axiom." >]
-
-
-let not_have_type env cb' cb =
-  let c = match cb'.cONSTBODY with
-      Some {contents=COOKED x} -> x
-    | _ -> anomaly "ml_import__not_have_type: should be a constant" in
-    errorlabstrm "Ml_import.not_convertible"
-  [< pENV [< 'sTR"In environment " >] env ; 'fNL ;
-     'sTR"The term: " ; pFTERMINENV(env,c) ; 'sPC ; 
-     'sTR"does not have type" ; 'sPC ; pFTYPEINENV(env,cb.cONSTTYPE) ;
-     'sTR"." ; 'fNL ;
-     'sTR"Actually, it has type" ; 'sPC ; pFTYPEINENV(env,cb'.cONSTTYPE) >]
-
-
-let fw_infexecute_constant fhyps id c =
-  let sp = Lib.make_path OBJ id in
-  let (u,j) = fexecute_with_univ empty_evd fhyps sp c in
-  let ids = auto_save_variables() in
-  let fhyps' = thin_to_level fhyps j._KIND in
-    (u,[FW, make_constant_body FW false (fhyps',j)])
-
-
-let fw_link id com =
-
-  (*** First we check that id corresponds to an informative axiom. ***)
-  let sp = fwsp_of_id id in
-  let osp = objsp_of sp in
-  let (cmap,s,u) = match Lib.leaf_object_tag osp with
-                     "CONSTANT" -> outConstant (Lib.map_leaf osp)
-		   | _ -> not_an_axiom id in
-  let cb = try Listmap.map cmap FW
-           with Not_found -> not_an_axiom id in
-  if cb.cONSTBODY <> None then not_an_axiom id ;
-
-  (*** Then we execute the term com. ***)
-  let (hyps,fhyps) = initial_assumptions() in
-  let tcci = fconstr_of_com empty_evd hyps com in
-  let tfw = fwify tcci in
-  let (u',cmap') = fw_infexecute_constant fhyps id tfw in
-  let cb' = Listmap.map cmap' FW in
-
-  (*** We check that the type of com is convertible with cb.CONSTTYPE ***)
-  if (not (conv empty_evd 
-	     (body_of_type cb.cONSTTYPE) 
-	     (body_of_type cb'.cONSTTYPE))) then
-    not_have_type (gLOB fhyps) cb' cb ;
-
-  (*** At last, we transform the original axiom into a constant. ***)
-(**lib__remap (osp,lib__LEAF (inConstant(listmap__remap cmap FW cb',s,u))); **)
-  cb.cONSTBODY <- cb'.cONSTBODY ;
-  cb.cONSTOPAQUE <- false ;
-
-  let c = match cb'.cONSTBODY with
-      Some {contents=COOKED x} -> x
-    | _ -> anomaly "ml_import__fw_link: should be a constant" in
-  mSGNL (hOV 0 [< 'sTR"Constant " ; print_id id ; 'sTR" linked to" ; 'sPC ;
-		  pFTERM c >])
-
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("LINK", function
-   [VARG_IDENTIFIER id; VARG_COMMAND com] -> (fun () -> fw_link id com)
- | _ -> anomaly "ML_IMPORT called with bad arguments.")
-
-
-
-(**************************************************************************)
-(*       ML Inductive name [ c1 ... cn ] == <Inductive Definition>.       *)
-(**************************************************************************)
-(*                     ML Inductive name1 [ c1,1 ... c1,n1 ]              *)
-(*                                  ...                                   *)
-(*                    	       	    namek [ ck,1 ... ck,nk ]              *)
-(*                     == <Mutual Inductive Definition>.                  *)
-(**************************************************************************)
-
-(***** declare__machine_minductive *****)
-let fw_machine_minductive fhyps nparams mispecvec finite = 
-  if Array.length mispecvec = 0 then anomaly "fw_machine_minductive" 
-  else 
-   let mindidvec = 
-     Array.map (fun  (indid,_,_,_,_) -> indid) mispecvec
-   and arlcvec = 
-     Array.map (fun  (_,_,indarity,indconstructors,_) ->
-      	       	       	 (indarity,indconstructors)) mispecvec
-   and namesvec = 
-     Array.map (fun  (indid,indstamp,_,_,consnames) -> 
-      	       	       	 (indstamp,indid,consnames)) mispecvec in
-
-  let sp = Lib.make_path OBJ mindidvec.(0) in
-  let (u',mimap) = with_universes 
-      (execute_minductive fhyps nparams namesvec finite)
-                               (sp,initial_universes,arlcvec) in
-
-  (***  declare_minductive (mindidvec,mimap,u')  ***)
-  add_named_object (mindidvec.(0),OBJ) (inMutualInductive (mimap,u'))
-  (***  do_vect declare_eliminations mindidvec  ***)
-
-
-(***** trad__fconstruct *****)
-let fw_fconstruct sigma fsign com =
-  let c = fconstr_of_com sigma fsign com in
-  Mach.fexecute_type sigma fsign c
-
-
-(***** command__build_mutual *****)
-let fw_build_mutual lparams lnamearconstrs finite =
-
-  let lrecnames = List.map (fun (x,_,_)->x)  lnamearconstrs
-  and nparams = List.length lparams
-  and sign0 = initial_fsign() in
-
-  let (ind_sign,arityl) = List.fold_left 
-    (fun (sign,arl) (recname,arityc,_) -> 
-      let arity = fw_fconstruct empty_evd sign0 (mkProdCit lparams arityc) in
-      (add_sign (recname,arity) sign, (arity::arl)))
-      (sign0,[]) lnamearconstrs in
-
-  let mispecvec = Array.of_list 
-    (List.map2 (fun ar (name,_,lname_constr) -> 
-    let consconstrl = List.map 
-     (fun (_,constr) -> 
-      	let c = fconstr_of_com empty_evd ind_sign 
-		  (mkProdCit lparams constr)
-      	in fwify c) lname_constr in
-    (name,Anonymous,ar,
-        put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl),
-              Array.of_list (List.map fst lname_constr)))
-    (List.rev arityl) lnamearconstrs) in
-
-  let _,fhyps = initial_assumptions() in
-  fw_machine_minductive fhyps nparams mispecvec finite
-
-
-let not_same_number_types () =
-  errorlabstrm "ml_import__ml_import_inductive"
-  [< 'sTR"Not the same number of types." >]
-
-let not_same_number_constructors (id,id') =
-  errorlabstrm "ml_import__ml_import_inductive"
-    (hOV 0
-       [< 'sTR"The ML type" ; 'sPC ; print_id id ;
-          'sTR" and the FW type" ; 'sPC ; print_id id' ; 'sPC ;
-          'sTR"do not have the same number" ;
-      	  'sPC ; 'sTR"of constructors." >])
-
-let ml_import_inductive names lparams lnamearconstrs finite =
-
-  let assoc_list =
-    if (List.length names) <> (List.length lnamearconstrs) then
-      not_same_number_types ()
-    else
-      List.fold_right2 (fun (id,l) (id',_,l') acc ->
-      	  if (List.length l)<>(List.length l') then
-	    not_same_number_constructors (id,id')
-	  else
-	    ( (id,id'), List.combine l (List.map fst l') )::acc ) 
-            names lnamearconstrs [] in
-
-  fw_build_mutual lparams lnamearconstrs finite;
-
-  List.iter
-      (fun i ->
-      	  let (mlid,id), l = List.nth assoc_list i in
-      	  let sp = Lib.make_path FW id in
-	  add_anonymous_object (inMLImport (MutInd (sp,i), mlid)) ;
-	  List.iter (fun j ->
-      	      let (mlid,id) = List.nth l (j-1) in
-      	      add_anonymous_object
-      	       	       	   (inMLImport (MutConstruct ((sp,i),j), mlid)) )
-	  (List.tl (list0n (List.length l))) )
-      (list0n ((List.length assoc_list) - 1)) ;
-
-  pPNL [< 'sTR"ML inductive type(s) " ;
-      	  prlist_with_sep (fun () -> [< 'sTR"," ; 'sPC >])
-	                  (fun (id,_) -> [< 'sTR(string_of_id id) >]) names ;
-         'sTR" imported." >]
-  
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("ML_ONEINDUCTIVE",
-    function [VARG_VARGLIST nl;
-         VARG_IDENTIFIER s;
-         VARG_COMMAND c;
-         VARG_BINDERLIST binders;
-         VARG_BINDERLIST constructors] ->
-        if List.length nl <> 1 then not_same_number_types () ;
-	(match nl with
-	     [VARG_VARGLIST (v::l)] ->
-	       let cnames = List.map id_of_varg l in
-               let la = join_binders binders in
-               let li = List.map (fun (l,c) -> (List.hd l,c)) constructors in
-        	 (function () -> ml_import_inductive [id_of_varg v,cnames] 
-		      la [(s,c,li)] true)
-	   | _ -> assert false)
-      | _ -> anomaly "ML_ONEINDUCTIVE called with bad arguments.")
-
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("ML_MUTUALINDUCTIVE",
-    function [VARG_VARGLIST l;
-      	 VARG_BINDERLIST binders;
-      	 VARG_VARGLIST indl] ->
-	let names = 
-	  List.map (function (VARG_VARGLIST (v::ll)) ->
-      	       	      id_of_varg v, List.map id_of_varg ll
-		      | _ -> assert false) l in
-        let la = join_binders binders in
-        let lnamearconstructs = 
-          List.map (function (VARG_VARGLIST [VARG_IDENTIFIER arid;
-      	       	       	       	   VARG_COMMAND arc;
-      	       	       	       	   VARG_BINDERLIST lconstr])
-                	-> (arid,arc,
-			    List.map (fun (l,c) -> (List.hd l,c)) lconstr)
-		      | _ -> assert false)
-      	      indl in
-        (function () -> ml_import_inductive names la lnamearconstructs true)
-      | _ -> anomaly "ML_MUTUALINDUCTIVE called with bad arguments.")
-
-
-
-(**************************************************************************)
-(*                       Extract Constant id => id                        *)
-(*        Extract Inductive (id [id ... id])+ => (id [id ... id])+        *)
-(**************************************************************************)
-
-let extract_constant id id' =
-  try
-    let sp = Nametab.sp_of_id FW id in
-      (match global_operator sp id with
-	   Const _,_ -> add_anonymous_object (inMLExtract (Const sp,id'))
-	 | _ -> raise Not_found)
-  with Not_found ->
-    errorlabstrm "Ml_import.extract_constant"
-      [< pID id; 'sPC; 'sTR"is not an FW constant" >]
-
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("EXTRACT_CONSTANT",
-  function 
-      [VARG_IDENTIFIER id; id'] -> 
-	fun () -> extract_constant id (id_of_varg id')
-    | _ -> assert false)
-
-
-let extract_inductive id (id2,l2) =
-  try
-    let sp = Nametab.sp_of_id FW id in
-      (match global_operator sp id with
-	  MutInd (sp,i),_ -> 
-	    add_anonymous_object (inMLExtract (MutInd (sp,i),id2));
-	    (* TODO: verifier le nombre de constructeurs *)
-	    List.iter
-	      (fun (id,j) -> 
-		 add_anonymous_object 
-		   (inMLExtract (MutConstruct ((sp,i),j),id)))
-	      (List.combine l2 (List.tl (list0n (List.length l2))))
-	| _ -> raise Not_found)
-  with Not_found ->
-    errorlabstrm "Ml_import.extract_inductive"
-      [< pID id; 'sPC; 'sTR"is not an FW inductive type" >]
-
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("EXTRACT_INDUCTIVE",
-  function 
-      [VARG_IDENTIFIER id1; VARG_VARGLIST (id2::l2)] ->
-	fun () -> extract_inductive id1 (id_of_varg id2,List.map id_of_varg l2)
-    | _ -> assert false)
-
-
-(**************************************************************************)
-(*                            Fw Print ident.                             *)
-(*                     To see FW constants or axioms.                     *)
-(**************************************************************************)
-
-let fprint_recipe = function
-    Some{contents=COOKED c} -> pFTERM c
-  | Some{contents=RECIPE _} -> [< 'sTR"<recipe>" >]
-  | None -> [< 'sTR"<uncookable>" >]
-
-
-let fprint_name id =
-  try let sp = Nametab.sp_of_id FW id in
-      let obj = Lib.map_leaf (objsp_of sp) in
-      (match object_tag obj with
-       	 "CONSTANT" ->
-      	     let (cmap,_,_) = outConstant obj in
-	     let {cONSTBODY=val_0;cONSTTYPE=typ} = Listmap.map cmap FW in
-	     hOV 0 (match val_0 with
-	        None -> [< 'sTR"*** [ "; 'sTR(string_of_id id);  'sTR " : ";
-                           'cUT ; fprtype typ ; 'sTR" ]"; 'fNL >] 
-	      | _    -> [< 'sTR(string_of_id id); 'sTR" = " ; 
-                           fprint_recipe val_0 ;
-	                   'fNL ; 'sTR "     : "; fprtype typ ; 'fNL >] )
-
-       | "MUTUALINDUCTIVE" ->
-       	     let (cmap,_) = outMutualInductive obj in
-	     [< print_mutual FW (Listmap.map cmap FW) ; 'fNL >]
-  
-       | _ -> invalid_arg "fprint_name" )
-  with Not_found | Invalid_argument _ -> errorlabstrm "ml_import__fprint_name"
-                    [< 'sTR(string_of_id id) ; 'sTR" is not an FW constant." >]
-
-
-(*** TODO: remove overwriting ***)
-let _ = overwriting_vinterp_add("FWPRINT",
-    function [VARG_IDENTIFIER id] -> (function () -> mSG(fprint_name id))
-      | _ -> anomaly "FWPRINT called with bad arguments.")
-