From b5d11e695f935bfc28f833baaa481d604009db33 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 3 Nov 2001 14:29:15 +0000 Subject: Creation de Recursive Extarction Module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2152 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/Extraction.v | 7 ++ contrib/extraction/common.ml | 4 +- contrib/extraction/common.mli | 2 + contrib/extraction/extract_env.ml | 138 +++++++++++++++++++++++++------------- contrib/extraction/haskell.ml | 2 +- contrib/extraction/miniml.mli | 2 +- 6 files changed, 104 insertions(+), 51 deletions(-) (limited to 'contrib/extraction') diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index b8c7eeb9a..7153d652a 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -29,6 +29,13 @@ Grammar vernac vernac : ast := | haskell_extr_module [ "Haskell" "Extraction" "Module" identarg($m) "." ] -> [ (ExtractionModule "haskell" $m) ] +| rec_extr_module + [ "Recursive" "Extraction" "Module" identarg($m) "." ] + -> [ (RecursiveExtractionModule "ocaml" $m) ] +| rec_haskell_extr_module + [ "Haskell" "Recursive" "Extraction" "Module" identarg($m) "." ] + -> [ (RecursiveExtractionModule "haskell" $m) ] + (* Custum inlining directives *) | inline_constant diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 5fe9264c5..fd7c3da03 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -22,12 +22,12 @@ open Nametab let current_module = ref None let module_of_r r = - string_of_id (snd (split_dirpath (dirpath (sp_of_r r)))) + snd (split_dirpath (dirpath (sp_of_r r))) let module_option r = let m = module_of_r r in if Some m = !current_module then "" - else (String.capitalize m) ^ "." + else (String.capitalize (string_of_id m)) ^ "." let check_ml r d = if to_inline r then diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 00136ef93..823388f4b 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -14,6 +14,8 @@ open Names module ToplevelPp : Mlpp +val module_of_r : global_reference -> identifier + val extract_to_file : string -> extraction_params -> ml_decl list -> unit diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 007fcf1d8..da5d0d9c1 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -20,6 +20,21 @@ open Mlutil open Vernacinterp open Common +(*s [extract_module m] returns all the global reference declared in a module *) + +let extract_module m = + let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in + let seg = Library.module_segment (Some m) in + let get_reference = function + | sp, Leaf o -> + (match Libobject.object_tag o with + | "CONSTANT" | "PARAMETER" -> ConstRef sp + | "INDUCTIVE" -> IndRef (sp,0) + | _ -> failwith "caught") + | _ -> failwith "caught" + in + Util.map_succeed get_reference seg + (*s Recursive computation of the global references to extract. We use a set of functions visiting the extracted objects in a depth-first way ([visit_type], [visit_ast] and [visit_decl]). @@ -33,73 +48,90 @@ open Common type extracted_env = { mutable visited : Refset.t; - mutable to_extract : global_reference list + mutable to_extract : global_reference list; + mutable modules : identifier list } -let empty () = { visited = ml_extractions (); to_extract = [] } +let empty () = + { visited = ml_extractions (); to_extract = []; modules = []} -let rec visit_reference eenv r = +let rec visit_reference m eenv r = let r' = match r with | ConstructRef ((sp,_),_) -> IndRef (sp,0) | IndRef (sp,i) -> if i = 0 then r else IndRef (sp,0) | _ -> r in if not (Refset.mem r' eenv.visited) then begin - (* we put [r'] in [visited] first to avoid loops in inductive defs *) + (* we put [r'] in [visited] first to avoid loops in inductive defs + and in module extraction *) eenv.visited <- Refset.add r' eenv.visited; - visit_decl eenv (extract_declaration r); + if m then begin + let m_name = module_of_r r' in + if not (List.mem m_name eenv.modules) then begin + eenv.modules <- m_name :: eenv.modules; + List.iter (visit_reference m eenv) (extract_module m_name) + end + end; + visit_decl m eenv (extract_declaration r); eenv.to_extract <- r' :: eenv.to_extract end - -and visit_type eenv t = + +and visit_type m eenv t = let rec visit = function - | Tglob r -> visit_reference eenv r + | Tglob r -> visit_reference m eenv r | Tapp l -> List.iter visit l | Tarr (t1,t2) -> visit t1; visit t2 | Tvar _ | Tprop | Tarity -> () in visit t - -and visit_ast eenv a = + +and visit_ast m eenv a = let rec visit = function - | MLglob r -> visit_reference eenv r + | MLglob r -> visit_reference m eenv r | MLapp (a,l) -> visit a; List.iter visit l | MLlam (_,a) -> visit a | MLletin (_,a,b) -> visit a; visit b - | MLcons (r,l) -> visit_reference eenv r; List.iter visit l + | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l | MLcase (a,br) -> - visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br + visit a; Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br | MLfix (_,_,l) -> Array.iter visit l - | MLcast (a,t) -> visit a; visit_type eenv t + | MLcast (a,t) -> visit a; visit_type m eenv t | MLmagic a -> visit a | MLrel _ | MLprop | MLarity | MLexn _ -> () in visit a -and visit_inductive eenv inds = - let visit_constructor (_,tl) = List.iter (visit_type eenv) tl in +and visit_inductive m eenv inds = + let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in let visit_ind (_,_,cl) = List.iter visit_constructor cl in List.iter visit_ind inds -and visit_decl eenv = function +and visit_decl m eenv = function | Dtype (inds,_) -> - visit_inductive eenv inds + visit_inductive m eenv inds | Dabbrev (_,_,t) -> - visit_type eenv t + visit_type m eenv t | Dglob (_,a) -> - visit_ast eenv a + visit_ast m eenv a | Dcustom _ -> () - + (*s Recursive extracted environment for a list of reference: we just iterate [visit_reference] on the list, starting with an empty extracted environment, and we return the reversed list of - references in the field [to_extract]. *) + references in the field [to_extract], and the visited_modules in + case of recursive module extraction *) let extract_env rl = let eenv = empty () in - List.iter (visit_reference eenv) rl; + List.iter (visit_reference false eenv) rl; List.rev eenv.to_extract +let modules_extract_env m = + let eenv = empty () in + eenv.modules <- [m]; + List.iter (visit_reference true eenv) (extract_module m); + eenv.modules, List.rev eenv.to_extract + (*s Extraction in the Coq toplevel. We display the extracted term in Ocaml syntax and we use the Coq printers for globals. The vernacular command is \verb!Extraction! [term]. Whenever [term] is @@ -107,8 +139,7 @@ let extract_env rl = let refs_set_of_list l = List.fold_right Refset.add l Refset.empty -let decl_of_refs refs = - List.map extract_declaration (extract_env refs) +let decl_of_refs refs = List.map extract_declaration (extract_env refs) let local_optimize refs = let prm = @@ -182,25 +213,12 @@ let _ = module [M]. We just keep constants and inductives, and we remove those having an ML extraction. *) -let extract_module m = - let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in - let seg = Library.module_segment (Some m) in - let get_reference = function - | sp, Leaf o -> - (match Libobject.object_tag o with - | "CONSTANT" | "PARAMETER" -> ConstRef sp - | "INDUCTIVE" -> IndRef (sp,0) - | _ -> failwith "caught") - | _ -> failwith "caught" - in - Util.map_succeed get_reference seg - -let decl_mem rl = function - | Dglob (r,_) -> List.mem r rl - | Dabbrev (r,_,_) -> List.mem r rl - | Dtype ((_,r,_)::_, _) -> List.mem r rl +let decl_in_m m = function + | Dglob (r,_) -> m = module_of_r r + | Dabbrev (r,_,_) -> m = module_of_r r + | Dtype ((_,r,_)::_, _) -> m = module_of_r r | Dtype ([],_) -> false - | Dcustom (r,s) -> List.mem r rl + | Dcustom (r,_) -> m = module_of_r r let file_suffix = function | "ocaml" -> ".ml" @@ -212,15 +230,41 @@ let _ = (function | [VARG_STRING lang; VARG_IDENTIFIER m] -> (fun () -> - let ms = Names.string_of_id m in - let f = (String.uncapitalize ms) ^ (file_suffix lang) in + let f = (String.uncapitalize (string_of_id m)) + ^ (file_suffix lang) in let prm = {lang=lang; toplevel=false; - mod_name= Some ms; + mod_name= Some m; to_appear= []} in let rl = extract_module m in let decls = optimize prm (decl_of_refs rl) in let decls = add_ml_decls prm decls in - let decls = List.filter (decl_mem rl) decls in + let decls = List.filter (decl_in_m m) decls in extract_to_file f prm decls) | _ -> assert false) + + +let _ = + vinterp_add "RecursiveExtractionModule" + (function + | [VARG_STRING lang; VARG_IDENTIFIER m] -> + (fun () -> + let modules,refs = modules_extract_env m in + let dummy_prm = {lang=lang; + toplevel=false; + mod_name= Some m; + to_appear= []} in + let decls = optimize dummy_prm (decl_of_refs refs) in + let decls = add_ml_decls dummy_prm decls in + List.iter + (fun m -> + let f = (String.uncapitalize (string_of_id m)) + ^ (file_suffix lang) in + let prm = {lang=lang; + toplevel=false; + mod_name= Some m; + to_appear= []} in + let decls = List.filter (decl_in_m m) decls in + extract_to_file f prm decls) + modules) + | _ -> assert false) diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index f3d64fcee..cb1ac038d 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -32,7 +32,7 @@ let keywords = let preamble prm = let m = match prm.mod_name with | None -> "Main" - | Some m -> String.capitalize m + | Some m -> String.capitalize (string_of_id m) in [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL; 'sTR "type Prop = ()"; 'fNL; diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 35cd8a592..125bf7865 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -62,7 +62,7 @@ type ml_decl = type extraction_params = { lang : string; toplevel : bool; - mod_name : string option; + mod_name : identifier option; to_appear : global_reference list } module type Mlpp_param = sig -- cgit v1.2.3