diff options
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 38 |
1 files changed, 25 insertions, 13 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index d467f508..c242e4ab 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) +(*i $Id: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i*) (*i*) open Pp @@ -110,22 +110,17 @@ let rec type_occurs alpha t = let rec mgu = function | Tmeta m, Tmeta m' when m.id = m'.id -> () - | Tmeta m, t when m.contents=None -> - if type_occurs m.id t then raise Impossible - else m.contents <- Some t - | t, Tmeta m when m.contents=None -> - if type_occurs m.id t then raise Impossible - else m.contents <- Some t - | Tmeta {contents=Some u}, t -> mgu (u, t) - | t, Tmeta {contents=Some u} -> mgu (t, u) + | Tmeta m, t | t, Tmeta m -> + (match m.contents with + | Some u -> mgu (u, t) + | None when type_occurs m.id t -> raise Impossible + | None -> m.contents <- Some t) | Tarr(a, b), Tarr(a', b') -> mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when r = r' -> List.iter mgu (List.combine l l') - | Tvar i, Tvar j when i = j -> () - | Tvar' i, Tvar' j when i = j -> () | Tdummy _, Tdummy _ -> () - | Tunknown, Tunknown -> () + | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *) | _ -> raise Impossible let needs_magic p = try mgu p; false with Impossible -> true @@ -828,6 +823,23 @@ let is_atomic = function let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false +(** Program creates a let-in named "program_branch_NN" for each branch of match. + Unfolding them leads to more natural code (and more dummy removal) *) + +let is_program_branch = function + | Id id -> + let s = string_of_id id in + let br = "program_branch_" in + let n = String.length br in + (try + ignore (int_of_string (String.sub s n (String.length s - n))); + String.sub s 0 n = br + with _ -> false) + | Tmp _ | Dummy -> false + +let expand_linear_let o id e = + o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e + (*S The main simplification function. *) (* Some beta-iota reductions + simplifications. *) @@ -844,7 +856,7 @@ let rec simpl o = function if (is_atomic c) || (is_atomic e) || (let n = nb_occur_match e in - (n = 0 || (n=1 && (is_tmp id || is_imm_apply e || o.opt_lin_let)))) + (n = 0 || (n=1 && expand_linear_let o id e))) then simpl o (ast_subst c e) else |