diff options
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 67 |
1 files changed, 45 insertions, 22 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f8c846725e..9f5c1f1a17 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1,13 +1,14 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) -open API open Util open Names open Libnames @@ -58,7 +59,7 @@ let rec eq_ml_type t1 t2 = match t1, t2 with | Tarr (tl1, tr1), Tarr (tl2, tr2) -> eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2 | Tglob (gr1, t1), Tglob (gr2, t2) -> - eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2 + GlobRef.equal gr1 gr2 && List.equal eq_ml_type t1 t2 | Tvar i1, Tvar i2 -> Int.equal i1 i2 | Tvar' i1, Tvar' i2 -> Int.equal i1 i2 | Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2 @@ -119,9 +120,8 @@ let rec mgu = function | None -> m.contents <- Some t) | Tarr(a, b), Tarr(a', b') -> mgu (a, a'); mgu (b, b') - | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> + | Tglob (r,l), Tglob (r',l') when GlobRef.equal r r' -> List.iter mgu (List.combine l l') - | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> () | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () | Tvar' i, Tvar' j when Int.equal i j -> () @@ -129,11 +129,15 @@ let rec mgu = function | Taxiom, Taxiom -> () | _ -> raise Impossible -let needs_magic p = try mgu p; false with Impossible -> true +let skip_typing () = lang () == Scheme || is_extrcompute () -let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a +let needs_magic p = + if skip_typing () then false + else try mgu p; false with Impossible -> true -let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a +let put_magic_if b a = if b then MLmagic a else a + +let put_magic p a = if needs_magic p then MLmagic a else a let generalizable a = lang () != Ocaml || @@ -266,7 +270,7 @@ let rec var2var' = function | Tglob (r,l) -> Tglob (r, List.map var2var' l) | a -> a -type abbrev_map = global_reference -> ml_type option +type abbrev_map = GlobRef.t -> ml_type option (*s Delta-reduction of type constants everywhere in a ML type [t]. [env] is a function of type [ml_type_env]. *) @@ -377,9 +381,9 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with eq_ml_ident na1 na2 && eq_ml_ast t1 t2 | MLletin (na1, c1, t1), MLletin (na2, c2, t2) -> eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2 -| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2 +| MLglob gr1, MLglob gr2 -> GlobRef.equal gr1 gr2 | MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) -> - eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2 + eq_ml_type t1 t2 && GlobRef.equal gr1 gr2 && List.equal eq_ml_ast c1 c2 | MLtuple t1, MLtuple t2 -> List.equal eq_ml_ast t1 t2 | MLcase (t1, c1, p1), MLcase (t2, c2, p2) -> @@ -394,13 +398,13 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with and eq_ml_pattern p1 p2 = match p1, p2 with | Pcons (gr1, p1), Pcons (gr2, p2) -> - eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2 + GlobRef.equal gr1 gr2 && List.equal eq_ml_pattern p1 p2 | Ptuple p1, Ptuple p2 -> List.equal eq_ml_pattern p1 p2 | Prel i1, Prel i2 -> Int.equal i1 i2 | Pwild, Pwild -> true -| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2 +| Pusual gr1, Pusual gr2 -> GlobRef.equal gr1 gr2 | _ -> false and eq_ml_branch (id1, p1, t1) (id2, p2, t2) = @@ -537,24 +541,24 @@ let dump_unused_vars a = | MLcase (t,e,br) -> let e' = ren env e in - let br' = Array.smartmap (ren_branch env) br in + let br' = Array.Smart.map (ren_branch env) br in if e' == e && br' == br then a else MLcase (t,e',br') | MLfix (i,ids,v) -> let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in - let v' = Array.smartmap (ren env') v in + let v' = Array.Smart.map (ren env') v in if v' == v then a else MLfix (i,ids,v') | MLapp (b,l) -> - let b' = ren env b and l' = List.smartmap (ren env) l in + let b' = ren env b and l' = List.Smart.map (ren env) l in if b' == b && l' == l then a else MLapp (b',l') | MLcons(t,r,l) -> - let l' = List.smartmap (ren env) l in + let l' = List.Smart.map (ren env) l in if l' == l then a else MLcons (t,r,l') | MLtuple l -> - let l' = List.smartmap (ren env) l in + let l' = List.Smart.map (ren env) l in if l' == l then a else MLtuple l' | MLmagic b -> @@ -771,6 +775,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. *) @@ -966,7 +984,7 @@ let rec iota_red i lift br ((typ,r,a) as cons) = if i >= Array.length br then raise Impossible; let (ids,p,c) = br.(i) in match p with - | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons + | Pusual r' | Pcons (r',_) when not (GlobRef.equal r' r) -> iota_red (i+1) lift br cons | Pusual r' -> let c = named_lams (List.rev ids) c in let c = ast_lift lift c @@ -1053,7 +1071,12 @@ let rec simpl o = function | MLmagic(MLcase(typ,e,br)) -> let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in 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 *) |