diff options
author | 2001-04-04 08:32:46 +0000 | |
---|---|---|
committer | 2001-04-04 08:32:46 +0000 | |
commit | 3af1bf4e2de34d3647b9c5395740b431a8ff6e7e (patch) | |
tree | f3a5be87ec9a4a35284811c48373179fe808923a /contrib/extraction | |
parent | a68a0a97a940002d87682b3b304bc9828c0481e5 (diff) |
supression vieux fichiers extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1529 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/extraction.ml | 1 | ||||
-rw-r--r-- | contrib/extraction/genpp.ml | 147 | ||||
-rw-r--r-- | contrib/extraction/genpp.mli | 66 | ||||
-rw-r--r-- | contrib/extraction/mlimport.ml | 495 | ||||
-rw-r--r-- | contrib/extraction/mlimport.mli | 97 |
5 files changed, 0 insertions, 806 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 1e8b8248f..1921b2a6b 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -19,7 +19,6 @@ open Inductive open Instantiate open Miniml open Mlutil -open Mlimport open Closure (*s Extraction results. *) diff --git a/contrib/extraction/genpp.ml b/contrib/extraction/genpp.ml deleted file mode 100644 index 55d80d846..000000000 --- a/contrib/extraction/genpp.ml +++ /dev/null @@ -1,147 +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_control -open Pp -open System -open Util -open Names -open Vernacinterp -open Mlimport -open Miniml -open Genpp - -(*s Utility functions. *) - -let open_par = function true -> [< 'sTR"(" >] | false -> [< >] -let close_par = function true -> [< 'sTR")" >] | false -> [< >] - -(* uncurry_list : ('a -> std_pcmds) -> 'a list -> std_ppcmds - * formats a list [x1;...;xn] in its uncurried form (x1,...,xn). *) - -let uncurry_list f = function - [] -> [< >] - | [x] -> [< (f x) >] - | xl -> [< 'sTR"(" ; - prlist_with_sep (fun () -> [< 'sTR", " >]) (fun x -> (f x)) xl ; - 'sTR")" - >] - -let uncurry_list2 f = function - [] -> [< >] - | [x] -> [< (f x) >] - | xl -> [< 'sTR"(" ; - hOV 0 [< prlist_with_sep - (fun () -> [< 'sTR"," ; 'sPC >]) - (fun x -> (f x)) xl ; - 'sTR")" >] - >] - -type extraction_params = { - needed : identifier list; - expand : identifier list; - expansion : bool; - exact : bool - } - -let list_ids = - List.map (function (VARG_IDENTIFIER id) -> id | _ -> assert false) - -let rec parse_rem op = function - VARG_STRING "noopt" :: r -> - parse_rem - { needed = op.needed; expand = op.expand; - expansion = false; exact = op.exact } r - | VARG_STRING "exact" :: r -> - parse_rem - { needed = op.needed; expand = op.expand; - expansion = op.expansion; exact = true } r - | VARG_STRING "expand" :: VARG_VARGLIST l :: r -> - parse_rem { needed = op.needed; expand = op.expand @ list_ids l; - expansion = op.expansion; exact = op.exact } r - | [] -> op - | _ -> assert false - -let parse_param = function - VARG_VARGLIST l :: r -> - parse_rem { needed = list_ids l; expand = []; - expansion = true; exact = false } r - | _ -> assert false - -module type ExtractionParams = sig - val opt : extraction_params -> ml_decl list -> ml_decl list - val suffixe : string - val cofix : bool - val pp_of_env : ml_decl list -> std_ppcmds - module Renaming : Extraction.Renaming -end - -module Make = functor (M : ExtractionParams) -> struct - - module Translation = Extraction.Make(M.Renaming) - - let change_names = - map_succeed - (fun id -> try Extraction.get_global_name id - with Anomaly _ -> failwith "caught") - - let exact prm env = - let keep = function - | Dtype il -> - List.exists (fun (_,id,_) -> List.mem id prm.needed) il - | Dabbrev (id,_,_) -> List.mem id prm.needed - | Dglob (id,_) -> List.mem id prm.needed - in - map_succeed - (fun d -> if not (keep d) then failwith "caught" else d) env - - let pp cicenv prm = - let mlenv = Translation.extract M.cofix cicenv in - let needed' = change_names prm.needed in - let expand' = change_names prm.expand in - let prm' = - { needed = needed' ; expand = expand' ; - expansion = prm.expansion ; exact = prm.exact } - in - let env = M.opt prm' mlenv in - let env = if prm'.exact then exact prm' env else env in - M.pp_of_env env - - let pp_recursive prm = - let gl = List.map (Nametab.sp_of_id CCI) prm.needed in - let cicenv = Close_env.close gl in - pp cicenv prm - - let write file strm = - let chan = open_trapping_failure open_out file M.suffixe in - let ft = with_output_to chan in - (try pP_with ft strm ; pp_flush_with ft () - with e -> pp_flush_with ft () ; close_out chan; raise e); - close_out chan - - let write_extraction_file file prm = - (* TODO: comment tester qu'il n'y a pas de section ouverte et - pemettre pour autant la compilation (donc une section - particuliere qui est le module) if Lib.cwd() <> [] then - errorlabstrm "Genpp.Pp_to_file.write_extraction_file" [< 'sTR - "There are still open sections !" >]; *) - let strm = pp_recursive prm in - write file strm - - let write_extraction_module m = - let cicenv = Close_env.module_env m in - let idl = List.map (Environ.id_of_global (Global.env())) cicenv in - let prm = - { needed = idl; expand = []; expansion = false; exact = true } in - let strm = pp cicenv prm in - let file = string_of_id m in - write file strm - -end diff --git a/contrib/extraction/genpp.mli b/contrib/extraction/genpp.mli deleted file mode 100644 index 376b069d0..000000000 --- a/contrib/extraction/genpp.mli +++ /dev/null @@ -1,66 +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*) - -(*s This module defines the generic part of the code production, as a - functor [Make] taking extraction parameters as argument (of type - [ExtractionParams]), including a renaming functor (of type - [Extraction.Renaming]) and returning a module to output the - code. *) - -open Pp -open Names -open Miniml -open Vernacinterp - -(*s Some utility functions, used in instance modules ([Caml], [Ocaml] and - [Haskell]). *) - -val open_par : bool -> std_ppcmds -val close_par : bool -> std_ppcmds - -val uncurry_list : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val uncurry_list2 : ('a -> std_ppcmds) -> 'a list -> std_ppcmds - -(*s Extraction parameters parsed on the command line. *) - -type extraction_params = { - needed : identifier list; (*r constants to keep *) - expand : identifier list; (*r constants to expand *) - expansion : bool; (*r do we expand *) - exact : bool (*r without recursivity *) -} - -val parse_param : vernac_arg list -> extraction_params - -(*s The whole bunch of extraction parameters has the following signature. *) - -module type ExtractionParams = - sig - (* optimisation function *) - val opt : extraction_params -> ml_decl list -> ml_decl list - (* file suffix *) - val suffixe : string - (* co-inductive types are (not) allowed *) - val cofix : bool - (* pretty-print function *) - val pp_of_env : ml_decl list -> std_ppcmds - (* the renaming functions *) - module Renaming : Extraction.Renaming - end - -(*s The functor itself. *) - -module Make : functor (M : ExtractionParams) -> - sig - module Translation : Extraction.Translation - val pp_recursive : extraction_params -> std_ppcmds - val write_extraction_file : string -> extraction_params -> unit - val write_extraction_module : identifier -> unit - end 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.") - diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli deleted file mode 100644 index 4fdb2e9ea..000000000 --- a/contrib/extraction/mlimport.mli +++ /dev/null @@ -1,97 +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 Names -open Term - -val add_ml_import : global_reference -> identifier -> unit -val is_ml_import : global_reference -> bool -val find_ml_import : global_reference -> identifier - -val add_ml_extract : global_reference -> identifier -> unit -val find_ml_extract : global_reference -> identifier -val is_ml_extract : global_reference -> bool - -(* -val list0n : int -> int list -val next_global_ident : Names.identifier -> Names.identifier -val ml_import_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t -val mL_INDUCTIVES : Names.section_path list ref -val add_ml_inductive_import : Names.section_path -> unit -val sp_is_ml_import : Names.section_path -> bool -val sp_prod : Names.section_path -val sp_is_ml_import_or_prod : Names.section_path -> bool -val inMLImport : Term.sorts Term.oper * Names.identifier -> Libobject.obj -val outMLImport : Libobject.obj -> Term.sorts Term.oper * Names.identifier -val ml_extract_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t -val sp_is_ml_extract : Names.section_path -> bool -val inMLExtract : Term.sorts Term.oper * Names.identifier -> Libobject.obj -val outMLExtract : Libobject.obj -> Term.sorts Term.oper * Names.identifier -val is_import_or_extract : Names.section_path -> bool -val freeze : - unit -> - (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t * - Names.section_path list * - (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t -val unfreeze : - (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t * - Names.section_path list * - (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t -> unit -val whd_fwify : 'a Term.oper Generic.term -> 'a Term.oper Generic.term -val fwify : Reduction.reduction_function -val fwsp_of_id : Names.identifier -> Names.section_path -val make_fw_parameter_body : - Term.type_judgement Names.signature * Term.type_judgement -> - Constrtypes.constant_body -val fw_infexecute_parameter : - Term.context -> - Names.identifier -> - Term.constr -> - Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list -val fw_machine_parameter : - Term.context -> Names.identifier * Term.constr -> unit -val fw_parameter : Names.identifier -> CoqAst.t -> unit -val ml_import : Names.identifier -> Names.identifier -> CoqAst.t -> unit -val id_of_varg : Vernacinterp.vernac_arg -> Names.identifier -val not_an_axiom : Names.identifier -> 'a -val not_have_type : - Term.environment -> - Constrtypes.constant_body -> Constrtypes.constant_body -> 'a -val fw_infexecute_constant : - Term.context -> - Names.identifier -> - Term.constr -> - Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list -val fw_link : Names.identifier -> CoqAst.t -> unit -val fw_machine_minductive : - Term.context -> - int -> - (Names.identifier * Names.name * Term.type_judgement * Term.constr * - Names.identifier array) - array -> bool -> unit -val fw_fconstruct : - 'a Evd.evar_map -> Term.context -> CoqAst.t -> Term.type_judgement -val fw_build_mutual : - (Names.identifier * CoqAst.t) list -> - (Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list -> - bool -> unit -val not_same_number_types : unit -> 'a -val not_same_number_constructors : Names.identifier * Names.identifier -> 'a -val ml_import_inductive : - (Names.identifier * Names.identifier list) list -> - (Names.identifier * CoqAst.t) list -> - (Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list -> - bool -> unit -val extract_constant : Names.identifier -> Names.identifier -> unit -val extract_inductive : - Names.identifier -> Names.identifier * Names.identifier list -> unit -val fprint_recipe : Constrtypes.recipe ref option -> Pp.std_ppcmds -val fprint_name : Names.identifier -> Pp.std_ppcmds -*) |