diff options
| -rw-r--r-- | plugins/extraction/extract_env.ml | 13 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.mli | 6 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 9 | ||||
| -rw-r--r-- | plugins/extraction/extraction.mli | 6 | ||||
| -rw-r--r-- | plugins/extraction/miniml.mli | 2 | ||||
| -rw-r--r-- | plugins/extraction/modutil.mli | 1 |
6 files changed, 37 insertions, 0 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 791294902..a10d9904d 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -644,3 +644,16 @@ let extraction_library is_rec m = in List.iter print struc; reset () + +let structure_for_compute c = + init false false; + let env = Global.env () in + let ast, mlt = Extraction.extract_constr env c in + let ast = Mlutil.normalize ast in + let refs = ref Refset.empty in + let add_ref r = refs := Refset.add r !refs in + let () = ast_iter_references add_ref add_ref add_ref ast in + let refs = Refset.elements !refs in + let struc = optimize_struct (refs,[]) (mono_environment refs []) in + let flatstruc = List.map snd (List.flatten (List.map snd struc)) in + flatstruc, ast, mlt diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 6c648b981..b68baf871 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -26,3 +26,9 @@ val mono_environment : val print_one_decl : Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds + +(* Used by Extraction Compute *) + +val structure_for_compute : + Term.constr -> + Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0be0a882b..a0e61c3b3 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1055,6 +1055,15 @@ let extract_with_type env c = Some (vl, t) | _ -> None +let extract_constr env c = + reset_meta_count (); + let typ = type_of env c in + match flag_of_type env typ with + | (_,TypeScheme) -> MLdummy, Tdummy Ktype + | (Logic,_) -> MLdummy, Tdummy Kother + | (Info,Default) -> + let mlt = extract_type env [] 1 typ [] in + extract_term env Mlenv.empty mlt c [], mlt let extract_inductive env kn = let ind = extract_ind env kn in diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 8d3cf76fd..940e264c4 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -18,6 +18,8 @@ val extract_constant : env -> constant -> constant_body -> ml_decl val extract_constant_spec : env -> constant -> constant_body -> ml_spec +(** For extracting "module ... with ..." declaration *) + val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option val extract_fixpoint : @@ -25,6 +27,10 @@ val extract_fixpoint : val extract_inductive : env -> mutual_inductive -> ml_ind +(** For extraction compute *) + +val extract_constr : env -> constr -> ml_ast * ml_type + (*s Is a [ml_decl] or a [ml_spec] logical ? *) val logical_decl : ml_decl -> bool diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 5aaef254e..a749f2407 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -183,6 +183,8 @@ type ml_structure = (module_path * ml_module_structure) list type ml_signature = (module_path * ml_module_sig) list +type ml_flat_structure = ml_structure_elem list + type unsafe_needs = { mldummy : bool; tdummy : bool; diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 42c8b11f3..88ead482b 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -17,6 +17,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool type do_ref = global_reference -> unit +val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit |