diff options
-rw-r--r-- | contrib/extraction/Extraction.v | 9 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 30 | ||||
-rw-r--r-- | contrib/extraction/extraction.ml | 11 | ||||
-rw-r--r-- | contrib/extraction/extraction.mli | 3 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 6 |
5 files changed, 46 insertions, 13 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 7a0ecd887..a5ec0a693 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -10,8 +10,11 @@ Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo". Grammar vernac vernac : ast := extr_constr [ "Extraction" constrarg($c) "." ] -> - [(Extraction $c)] + [ (Extraction $c) ] | extr_list [ "Extraction" "-r" ne_qualidarg_list($l) "." ] -> - [(ExtractionRec ($LIST $l))] + [ (ExtractionRec ($LIST $l)) ] | extr_list [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] -> - [(ExtractionFile $f ($LIST $l))]. + [ (ExtractionFile $f ($LIST $l)) ] +| extr_module [ "Extraction" "Module" identarg($m) "." ] -> + [ (ExtractionModule $m) ]. + diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index fa0ed7270..ac9fe6563 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -1,9 +1,10 @@ open Pp open Term +open Lib +open Extraction open Miniml open Mlutil -open Extraction (*s Topological sort of global CIC references. We introduce graphs of global references; a graph is a map @@ -140,7 +141,7 @@ let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d)) open Vernacinterp let _ = - vinterp_add "Extraction" + overwriting_vinterp_add "Extraction" (function | [VARG_CONSTR ast] -> (fun () -> @@ -181,3 +182,28 @@ let _ = | VARG_STRING f :: vl -> (fun () -> Ocaml.extract_to_file f (decl_of_vargl vl)) | _ -> assert false) + +(*s Extraction of a module. *) + +let extract_module m = + let seg = Library.module_segment (Some m) in + let get_reference = function + | sp, Leaf o -> + (match Libobject.object_tag o with + | "CONSTANT" -> ConstRef sp + | "INDUCTIVE" -> IndRef (sp,0) + | _ -> failwith "caught") + | _ -> failwith "caught" + in + let rl = Util.map_succeed get_reference seg in + List.map extract_declaration rl + +let _ = + vinterp_add "ExtractionModule" + (function + | [VARG_IDENTIFIER m] -> + (fun () -> + let m = Names.string_of_id m in + let f = (String.uncapitalize m) ^ ".ml" in + Ocaml.extract_to_file f (extract_module m)) + | _ -> assert false) diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 1ff031f41..661cfef3d 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -218,7 +218,8 @@ let rec push_many_rels_ctx keep_prop env ctx = function (env, ctx) let fix_environment env ctx fl tl = - push_many_rels_ctx true env ctx (List.combine fl (Array.to_list tl)) + let tl' = Array.mapi lift tl in + push_many_rels_ctx true env ctx (List.combine fl (Array.to_list tl')) (* Decomposition of a type beginning with at least n products when reduced *) @@ -499,9 +500,10 @@ and extract_term_with_type env ctx c t = let (_,e) = extract_branch_aux 0 br.(0) in Rmlterm e) | IsFix ((_,i),(ti,fi,ci)) -> + let n = Array.length ti in let (env', ctx') = fix_environment env ctx fi ti in - let extract_fix_body c t = - match extract_constr_with_type env' ctx' c t with + let extract_fix_body c t = + match extract_constr_with_type env' ctx' c (lift n t) with | Eprop -> MLprop | Emltype _ -> MLarity | Emlterm a -> a @@ -570,9 +572,8 @@ and signature_of_application env f t a = else let f' = mkApp (f, Array.sub a 0 nbp) in let a' = Array.sub a nbp (nargs-nbp) in - let t' = Typing.type_of env Evd.empty t in + let t' = Typing.type_of env Evd.empty f' in s @ signature_of_application env f' t' a' - (*s Extraction of a constr. *) diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index c218f9c31..8ad3f7556 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -32,8 +32,7 @@ type extraction_result = (*s Extraction functions. *) -val extract_constr : - env -> extraction_context -> constr -> extraction_result +val extract_constr : env -> extraction_context -> constr -> extraction_result (*s ML declaration corresponding to a Coq reference. *) diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 86217971f..144891849 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -15,6 +15,7 @@ open Util open Names open Term open Miniml +open Mlutil (*s Some utility functions. *) @@ -364,6 +365,9 @@ end module Pp = Make(OcamlParams) +let pp_ast a = Pp.pp_ast (betared_ast (uncurrify_ast a)) +let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d)) + let ocaml_preamble () = [< 'sTR "type prop = Prop"; 'fNL; 'fNL; 'sTR "type arity = Arity"; 'fNL; 'fNL >] @@ -374,7 +378,7 @@ let extract_to_file f decls = pP_with ft (hV 0 (ocaml_preamble ())); begin try - List.iter (fun d -> mSGNL_with ft (Pp.pp_decl d)) decls + List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls with e -> pp_flush_with ft (); close_out cout; raise e end; |