From 063fbe9077e6b75f327dd105774c3b3b77bda5c9 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 5 Mar 2014 20:18:58 +0100 Subject: Extraction : some more support functions for a future "Extraction Compute" --- plugins/extraction/extract_env.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'plugins/extraction/extract_env.ml') 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 -- cgit v1.2.3