diff options
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/common.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 1 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 18 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 6 |
4 files changed, 23 insertions, 4 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9772ebd64..9aec190d0 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) = let idg = safe_basename_of_global r in match l with | [""] -> (* this happens only at toplevel of the monolithic case *) - let globs = Id.Set.elements (get_global_ids ()) in + let globs = get_global_ids () in let id = next_ident_away (kindcase_id k idg) globs in Id.to_string id | _ -> modular_rename k idg diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 7644b49ce..a227478d0 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -141,6 +141,7 @@ let make_typvar n vl = if not (String.contains s '\'') && Unicode.is_basic_ascii s then id else id_of_name Anonymous in + let vl = Id.Set.of_list vl in next_ident_away id' vl let rec type_sign_vl env c = diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a4c2bcd88..b16b430a8 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -769,6 +769,20 @@ let eta_red e = else e | _ -> e +(* Performs an eta-reduction when the core is atomic, + or otherwise returns None *) + +let atomic_eta_red e = + let ids,t = collect_lams e in + let n = List.length ids in + match t with + | MLapp (f,a) when test_eta_args_lift 0 n a -> + (match f with + | MLrel k when k>n -> Some (MLrel (k-n)) + | MLglob _ | MLexn _ | MLdummy _ -> Some f + | _ -> None) + | _ -> None + (*s Computes all head linear beta-reductions possible in [(t a)]. Non-linear head beta-redex become let-in. *) @@ -1053,6 +1067,10 @@ let rec simpl o = function simpl o (MLcase(typ,e,br')) | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e + | MLlam _ as e -> + (match atomic_eta_red e with + | Some e' -> e' + | None -> ast_map (simpl o) e) | a -> ast_map (simpl o) a (* invariant : list [a] of arguments is non-empty *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ca98f07e8..30e3b520f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -750,11 +750,11 @@ let extraction_implicit r l = let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist" -let modfile_ids = ref [] +let modfile_ids = ref Id.Set.empty let modfile_mps = ref MPmap.empty let reset_modfile () = - modfile_ids := Id.Set.elements !blacklist_table; + modfile_ids := !blacklist_table; modfile_mps := MPmap.empty let string_of_modfile mp = @@ -763,7 +763,7 @@ let string_of_modfile mp = let id = Id.of_string (raw_string_of_modfile mp) in let id' = next_ident_away id !modfile_ids in let s' = Id.to_string id' in - modfile_ids := id' :: !modfile_ids; + modfile_ids := Id.Set.add id' !modfile_ids; modfile_mps := MPmap.add mp s' !modfile_mps; s' |