diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/extraction.ml | 13 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 8 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 11 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 60 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 12 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 12 |
8 files changed, 83 insertions, 49 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 693c92ece..835337952 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -536,8 +536,9 @@ let rec extract_term env mle mlt c args = in extract_term env mle mlt d' [] | [] -> let env' = push_rel_assum (Name id, t) env in - let id, a = try check_default env t; id, new_meta() - with NotDefault d -> dummy_name, Tdummy d + let id, a = + try check_default env t; Id id, new_meta() + with NotDefault d -> Dummy, Tdummy d in let b = new_meta () in (* If [mlt] cannot be unified with an arrow type, then magic! *) @@ -554,7 +555,7 @@ let rec extract_term env mle mlt c args = let c1' = extract_term env mle a c1 [] in (* The type of [c1'] is generalized and stored in [mle]. *) let mle' = Mlenv.push_gen mle a in - MLletin (id, c1', extract_term env' mle' mlt c2 args') + MLletin (Id id, c1', extract_term env' mle' mlt c2 args') with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) @@ -777,7 +778,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = assert (br_size = 1); let (_,ids,e') = extract_branch 0 in assert (List.length ids = 1); - MLletin (List.hd ids,a,e') + MLletin (tmp_id (List.hd ids),a,e') end else (* Standard case: we apply [extract_branch]. *) @@ -842,7 +843,7 @@ let extract_std_constant env kn body typ = (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in (* The lambdas names. *) - let ids = List.map (fun (n,_) -> id_of_name n) rels in + let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in (* The according Coq environment. *) let env = push_rels_assum rels env in (* The real extraction: *) @@ -877,7 +878,7 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> if not (is_custom r) then add_info_axiom r; let n = type_scheme_nb_args env typ in - let ids = iterate (fun l -> anonymous::l) n [] in + let ids = iterate (fun l -> anonymous_name::l) n [] in Dtype (r, ids, Taxiom) | (Info,Default) -> if not (is_custom r) then add_info_axiom r; diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 6973bb454..579f42df5 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -121,11 +121,11 @@ let rec pp_expr par env args = pp_expr par env (stl @ args) f | MLlam _ as a -> let fl,a' = collect_lams a in - let fl,env' = push_vars fl env in + let fl,env' = push_vars (List.map id_of_mlid fl) env in let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in apply (pp_par par' st) | MLletin (id,a1,a2) -> - let i,env' = push_vars [id] env in + let i,env' = push_vars [id_of_mlid id] env in let pp_id = pr_id (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in @@ -166,7 +166,7 @@ let rec pp_expr par env args = and pp_pat env factors pv = let pp_one_pat (name,ids,t) = - let ids,env' = push_vars (List.rev ids) env in + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let par = expr_needs_par t in hov 2 (pp_global Cons name ++ (match ids with @@ -204,7 +204,7 @@ and pp_fix par env i (ids,bl) args = and pp_function env f t = let bl,t' = collect_lams t in - let bl,env' = push_vars bl env in + let bl,env' = push_vars (List.map id_of_mlid bl) env in (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ hov 2 (pp_expr false env' [] t')) diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 91c60d205..00df1a98d 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -92,15 +92,20 @@ type ml_ind = { (*s ML terms. *) +type ml_ident = + | Dummy + | Id of identifier + | Tmp of identifier + type ml_ast = | MLrel of int | MLapp of ml_ast * ml_ast list - | MLlam of identifier * ml_ast - | MLletin of identifier * ml_ast * ml_ast + | MLlam of ml_ident * ml_ast + | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference | MLcons of inductive_info * global_reference * ml_ast list | MLcase of (inductive_info*case_info) * ml_ast * - (global_reference * identifier list * ml_ast) array + (global_reference * ml_ident list * ml_ast) array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2aee7b8a9..2cd1ee708 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -25,14 +25,27 @@ exception Impossible (*S Names operations. *) -let anonymous = id_of_string "x" +let anonymous_name = id_of_string "x" let dummy_name = id_of_string "_" +let anonymous = Id anonymous_name + let id_of_name = function - | Anonymous -> anonymous - | Name id when id = dummy_name -> anonymous + | Anonymous -> anonymous_name + | Name id when id = dummy_name -> anonymous_name | Name id -> id +let id_of_mlid = function + | Dummy -> dummy_name + | Id id -> id + | Tmp id -> id + +let tmp_id = function + | Id id -> Tmp id + | a -> a + +let is_tmp = function Tmp _ -> true | _ -> false + (*S Operations upon ML types (with meta). *) let meta_count = ref 0 @@ -298,7 +311,9 @@ let isKill = function Kill _ -> true | _ -> false let isDummy = function Tdummy _ -> true | _ -> false -let sign_of_id i = if i = dummy_name then Kill Kother else Keep +let sign_of_id = function + | Dummy -> Kill Kother + | _ -> Keep (*s Removing [Tdummy] from the top level of a ML type. *) @@ -536,14 +551,14 @@ let rec anonym_lams a = function let rec dummy_lams a = function | 0 -> a - | n -> dummy_lams (MLlam (dummy_name,a)) (pred n) + | n -> dummy_lams (MLlam (Dummy,a)) (pred n) (*s mixed according to a signature. *) let rec anonym_or_dummy_lams a = function | [] -> a | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s) - | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s) + | Kill _ :: s -> MLlam(Dummy, anonym_or_dummy_lams a s) (*S Operations concerning eta. *) @@ -603,12 +618,19 @@ let rec linear_beta_red a t = match a,t with MLletin (id, a0, linear_beta_red a t)) | _ -> MLapp (t, a) +let rec tmp_head_lams = function + | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t) + | e -> e + (*s Applies a substitution [s] of constants by their body, plus - linear beta reductions at modified positions. *) + linear beta reductions at modified positions. + Moreover, we mark some lambdas as suitable for later linear + reduction (this helps the inlining of recursors). +*) let rec ast_glob_subst s t = match t with | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> - let a = List.map (ast_glob_subst s) a in + let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in (try linear_beta_red a (Refmap.find refe s) with Not_found -> MLapp (f, a)) | MLglob ((ConstRef kn) as refe) -> @@ -692,7 +714,7 @@ let rec merge_ids ids ids' = match ids,ids' with | [],l -> l | l,[] -> l | i::ids, i'::ids' -> - (if i = dummy_name then i' else i) :: (merge_ids ids ids') + (if i = Dummy then i' else i) :: (merge_ids ids ids') let is_exn = function MLexn _ -> true | _ -> false @@ -765,11 +787,13 @@ let rec simpl o = function | MLcase (i,e,br) -> let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in simpl_case o i br (simpl o e) + | MLletin(Dummy,_,e) -> simpl o (ast_pop e) | MLletin(id,c,e) -> - let e = (simpl o e) in + let e = simpl o e in if - (id = dummy_name) || (is_atomic c) || (is_atomic e) || - (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) + (is_atomic c) || (is_atomic e) || + (let n = nb_occur_match e in + (n = 0 || (n=1 && (is_tmp id || o.opt_lin_let)))) then simpl o (ast_subst c e) else @@ -783,12 +807,12 @@ let rec simpl o = function and simpl_app o a = function | MLapp (f',a') -> simpl_app o (a'@a) f' - | MLlam (id,t) when id = dummy_name -> + | MLlam (Dummy,t) -> simpl o (MLapp (ast_pop t, List.tl a)) | MLlam (id,t) -> (* Beta redex *) (match nb_occur_match t with | 0 -> simpl o (MLapp (ast_pop t, List.tl a)) - | 1 when o.opt_lin_beta -> + | 1 when (is_tmp id || o.opt_lin_beta) -> simpl o (MLapp (ast_subst (List.hd a) t, List.tl a)) | _ -> let a' = List.map (ast_lift 1) (List.tl a) in @@ -896,7 +920,7 @@ let eta_expansion_sign s (ids,c) = let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels in ids, MLapp (ast_lift (i-1) c, a) | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l - | Kill _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l + | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l in abs ids [] 1 s (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] @@ -920,7 +944,7 @@ let term_expunge s (ids,c) = else let ids,c = kill_some_lams (List.rev s) (ids,c) in if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then - MLlam (dummy_name, ast_lift 1 c) + MLlam (Dummy, ast_lift 1 c) else named_lams ids c (*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and @@ -1083,10 +1107,6 @@ let rec non_stricts add cand = function pop 1 (non_stricts add cand t) | MLrel n -> List.filter ((<>) n) cand - | MLapp (MLrel n, _) -> - List.filter ((<>) n) cand - (* In [(x y)] we say that only x is strict. Cf [sig_rec]. We may *) - (* gain something if x is replaced by a function like a projection *) | MLapp (t,l)-> let cand = non_stricts false cand t in List.fold_left (non_stricts false) cand l diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 9c5feac82..7fd8006a5 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -69,22 +69,24 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val isDummy : ml_type -> bool val isKill : sign -> bool -val case_expunge : signature -> ml_ast -> identifier list * ml_ast -val term_expunge : signature -> identifier list * ml_ast -> ml_ast +val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast +val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast (*s Special identifiers. [dummy_name] is to be used for dead code and will be printed as [_] in concrete (Caml) code. *) -val anonymous : identifier +val anonymous_name : identifier val dummy_name : identifier val id_of_name : name -> identifier +val id_of_mlid : ml_ident -> identifier +val tmp_id : ml_ident -> ml_ident (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns the list [idn;...;id1] and the term [t]. *) -val collect_lams : ml_ast -> identifier list * ml_ast -val collect_n_lams : int -> ml_ast -> identifier list * ml_ast +val collect_lams : ml_ast -> ml_ident list * ml_ast +val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast val nb_lams : ml_ast -> int val dummy_lams : ml_ast -> int -> ml_ast diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 107b5368f..1c19bf06b 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -176,11 +176,12 @@ let rec pp_expr par env args = pp_expr par env (stl @ args) f | MLlam _ as a -> let fl,a' = collect_lams a in + let fl = List.map id_of_mlid fl in let fl,env' = push_vars fl env in let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in apply (pp_par par' st) | MLletin (id,a1,a2) -> - let i,env' = push_vars [id] env in + let i,env' = push_vars [id_of_mlid id] env in let pp_id = pr_id (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in @@ -238,7 +239,8 @@ let rec pp_expr par env args = if List.exists (ast_occurs_itvl 1 n) a then raise NoRecord else - let ids,env' = push_vars (List.rev ids) env in + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env + in (pp_apply (pp_expr true env [] t ++ str "." ++ pp_global Term (List.nth projs (n-i))) @@ -294,7 +296,7 @@ and pp_ifthenelse par env expr pv = match pv with | _ -> raise Not_found and pp_one_pat env i (r,ids,t) = - let ids,env' = push_vars (List.rev ids) env in + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let expr = pp_expr (expr_needs_par t) env' [] t in try let projs = find_projections i in @@ -324,7 +326,7 @@ and pp_pat env (info,factors) pv = and pp_function env t = let bl,t' = collect_lams t in - let bl,env' = push_vars bl env in + let bl,env' = push_vars (List.map id_of_mlid bl) env in match t' with | MLcase(i,MLrel 1,pv) when fst i=Standard -> if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 50339d473..9cc34634a 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -72,10 +72,10 @@ let rec pp_expr env args = pp_expr env (stl @ args) f | MLlam _ as a -> let fl,a' = collect_lams a in - let fl,env' = push_vars fl env in + let fl,env' = push_vars (List.map id_of_mlid fl) env in apply (pp_abst (pp_expr env' [] a') (List.rev fl)) | MLletin (id,a1,a2) -> - let i,env' = push_vars [id] env in + let i,env' = push_vars [id_of_mlid id] env in apply (hv 0 (hov 2 @@ -123,7 +123,7 @@ and pp_cons_args env = function and pp_one_pat env (r,ids,t) = - let ids,env' = push_vars (List.rev ids) env in + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let args = if ids = [] then mt () else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index df9f02dfd..866f499b5 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -400,10 +400,14 @@ let flag_of_int n = opt_lin_let = kth_digit n 9; opt_lin_beta = kth_digit n 10 } -(* For the moment, we allow by default everything except the type-unsafe - optimization [opt_case_idg]. *) - -let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024 +(* For the moment, we allow by default everything except : + - the type-unsafe optimization [opt_case_idg] + - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta] + (may lead to complexity blow-up, subsumed by finer reductions + when inlining recursors). +*) + +let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*) let int_flag_ref = ref int_flag_init let opt_flag_ref = ref (flag_of_int int_flag_init) |