From 07c737eccfd766300be275f949ab7b9f74e67937 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 21 Feb 2003 03:22:42 +0000 Subject: bugs/améliorations trouvés via FTA MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3688 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/common.ml | 13 ------- contrib/extraction/extraction.ml | 80 ++++++++++++++++++++++++++-------------- contrib/extraction/mlutil.ml | 16 ++++---- contrib/extraction/mlutil.mli | 1 + contrib/extraction/ocaml.ml | 65 ++++++++++++++++++++++---------- contrib/extraction/table.ml | 11 +++--- contrib/extraction/table.mli | 3 +- 7 files changed, 114 insertions(+), 75 deletions(-) diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 0b5b10e21..a02dff295 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -20,19 +20,6 @@ open Miniml open Mlutil open Ocaml -(* Add _all_ direct subobjects of a module, not only those exported. - Build on the Modops.add_signature model. *) - -let add_structure mp msb env = - let add_one env (l,elem) = - let kn = make_kn mp empty_dirpath l in - match elem with - | SEBconst cb -> Environ.add_constant kn cb env - | SEBmind mib -> Environ.add_mind kn mib env - | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env - | SEBmodtype mtb -> Environ.add_modtype kn mtb env - in List.fold_left add_one env msb - (* Add _all_ direct subobjects of a module, not only those exported. Build on the Modops.add_signature model. *) diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 294f962dc..401e4f98f 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -98,6 +98,14 @@ let rec type_sign_vl env c = else true::s, (next_ident_away (id_of_name n) vl) :: vl | _ -> [],[] +let rec nb_default_params env c = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + let n = nb_default_params (push_rel_assum (n,t) env) d in + if is_default env t then n+1 else n + | _ -> 0 + + (*S Management of type variable contexts. *) (* A De Bruijn variable context (db) is a context for translating Coq [Rel] @@ -332,11 +340,12 @@ and extract_ind env kn = (* kn is supposed to be in long form *) with Not_found -> raise (I Standard); in let s = List.map (type_neq (mlt_env env) Tdummy) typ in + let n = nb_default_params env mip0.mind_nf_arity in let check (_,o) = match o with | None -> raise (I Standard) | Some kn -> ConstRef kn in - add_record kn (List.map check (List.filter fst (List.combine s projs))); + add_record kn n (List.map check (List.filter fst (List.combine s projs))); raise (I Record) with (I info) -> info in @@ -509,31 +518,44 @@ and extract_cst_app env mle mlt kn args = let schema = nb, type_expand env t in (* Then the expected type of this constant. *) let metas = List.map new_meta args in - let type_head = type_recomp (metas,mlt) in - (* The head gets a magic if stored and expected types differ. *) - let head = - let h = MLglob (ConstRef kn) in - put_magic (type_recomp (metas,mlt), instantiation schema) h in + (* We compare stored and expected types in two steps. *) + (* First, can [kn] be applied to all args ? *) + let a = new_meta () in + let magic1 = needs_magic (type_recomp (metas, a), instantiation schema) in + (* Second, is the resulting type compatible with the expected type [mlt] ? *) + let magic2 = needs_magic (a, mlt) in + (* The internal head receives a magic if [magic1] *) + let head = put_magic_if magic1 (MLglob (ConstRef kn)) in (* Now, the extraction of the arguments. *) let s = type_to_sign env (snd schema) in let ls = List.length s in let la = List.length args in let mla = make_mlargs env mle s args metas in + let mla = + if not magic1 then + try + let l,l' = list_chop (projection_arity (ConstRef kn)) mla in + if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' + else mla + with _ -> mla + else mla + in (* Different situations depending of the number of arguments: *) - if ls = 0 then head + if ls = 0 then put_magic_if magic2 head else if List.mem true s then - if la >= ls then MLapp (head, mla) + if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, mla)) else (* Not enough arguments. We complete via eta-expansion. *) let ls' = ls-la in let s' = list_lastn ls' s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in - anonym_or_dummy_lams (MLapp (head, mla)) s' + put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s') else (* In the special case of always false signature, one dummy lam is left. *) (* So a [MLdummy] is left accordingly. *) - if la >= ls then MLapp (head, MLdummy :: mla) - else dummy_lams head (ls-la-1) + if la >= ls + then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla)) + else put_magic_if magic2 (dummy_lams head (ls-la-1)) (*s Extraction of an inductive constructor applied to arguments. *) @@ -564,26 +586,29 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let args' = list_lastn la' args in (* Now, we build the expected type of the constructor *) let metas = List.map new_meta args' in - let type_head = type_recomp (metas, mlt) in (* If stored and expected types differ, then magic! *) - let magic = needs_magic (type_cons, type_head) in + let a = new_meta () in + let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in + let magic2 = needs_magic (a, mlt) in let head mla = if mi.ind_info = Singleton then - put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *) - else put_magic_if magic (MLcons (ConstructRef cp, mla)) + put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *) + else put_magic_if magic1 (MLcons (ConstructRef cp, mla)) in (* Different situations depending of the number of arguments: *) if la < params_nb then let head' = head (eta_args_sign ls s) in - dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la) + put_magic_if magic2 + (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)) else let mla = make_mlargs env mle s args' metas in - if la = ls + params_nb then head mla + if la = ls + params_nb + then put_magic_if (magic2 && not magic1) (head mla) else (* [ params_nb <= la <= ls + params_nb ] *) let ls' = params_nb + ls - la in let s' = list_lastn ls' s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in - anonym_or_dummy_lams (head mla) s' + put_magic_if magic2 (anonym_or_dummy_lams (head mla) s') (*S Extraction of a case. *) @@ -658,9 +683,9 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) -let rec decomp_lams_eta env c t = - let rels = fst (splay_prod env none t) in - let n = List.length rels in +let rec decomp_lams_eta_n n env c t = + let rels = fst (decomp_n_prod env none n t) in + let rels = List.map (fun (id,_,c) -> (id,c)) rels in let m = nb_lam c in if m >= n then decompose_lam_n n c else @@ -674,13 +699,6 @@ let rec decomp_lams_eta env c t = (*s From a constant to a ML declaration. *) let extract_std_constant env kn body typ = - (* Decomposing the top level lambdas of [body]. *) - let rels,c = decomp_lams_eta env body typ in - (* The lambdas names. *) - let ids = List.map (fun (n,_) -> id_of_name n) rels in - (* The according Coq environment. *) - let env = push_rels_assum rels env in - (* The ML part: *) reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) let t = snd (record_constant_type env kn (Some typ)) in @@ -690,6 +708,12 @@ let extract_std_constant env kn body typ = let s = List.map ((<>) Tdummy) l in (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in + (* Decomposing the top level lambdas of [body]. *) + let rels,c = decomp_lams_eta_n (List.length s) env body typ in + (* The lambdas names. *) + let ids = List.map (fun (n,_) -> id_of_name n) rels in + (* The according Coq environment. *) + let env = push_rels_assum rels env in (* The real extraction: *) let e = extract_term env mle t' c [] in (* Expunging term and type from dummy lambdas. *) diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 3355fc2aa..ba0659b32 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -401,7 +401,7 @@ let ast_occurs k t = (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)] in [t] with [k<=i<=k'] *) -let occurs_itvl k k' t = +let ast_occurs_itvl k k' t = try ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false with Found -> true @@ -561,7 +561,7 @@ let eta_red e = else let a1,a2 = list_chop m a in let f = if m = 0 then f else MLapp (f,a1) in - if test_eta_args_lift 0 n a2 && not (occurs_itvl 1 n f) + if test_eta_args_lift 0 n a2 && not (ast_occurs_itvl 1 n f) then ast_lift (-n) f else e | _ -> e @@ -601,12 +601,12 @@ let check_constant_case br = if br = [||] then raise Impossible; let (r,l,t) = br.(0) in let n = List.length l in - if occurs_itvl 1 n t then raise Impossible; + if ast_occurs_itvl 1 n t then raise Impossible; let cst = ast_lift (-n) t in for i = 1 to Array.length br - 1 do let (r,l,t) = br.(i) in let n = List.length l in - if (occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) + if (ast_occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) then raise Impossible done; cst @@ -683,7 +683,7 @@ let rec simpl o = function simpl o (ast_subst c e) | MLfix(i,ids,c) as t when o -> let n = Array.length ids in - if occurs_itvl 1 n c.(i) then + if ast_occurs_itvl 1 n c.(i) then MLfix (i, ids, Array.map (simpl o) c) else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *) | a -> ast_map (simpl o) a @@ -917,7 +917,7 @@ let optimize_fix a = let m = List.length args in (match a' with | MLfix(_,_,_) when - (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') + (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a') -> a' | MLfix(_,[|f|],[|c|]) -> (try general_optimize_fix f ids n args m c @@ -1061,8 +1061,8 @@ let inline r t = not (to_keep r) (* The user DOES want to keep it *) && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) - || (auto_inline () && lang () <> Haskell - && (is_recursor r || manual_inline r || inline_test t))) + || (auto_inline () && lang () <> Haskell && not (is_projection r) + && (is_recursor r || manual_inline r || inline_test t))) (*S Optimization. *) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index b8f817eab..13f37b32b 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -96,6 +96,7 @@ val eta_args_sign : int -> bool list -> ml_ast list val ast_iter : (ml_ast -> unit) -> ml_ast -> unit val ast_occurs : int -> ml_ast -> bool +val ast_occurs_itvl : int -> int -> ml_ast -> bool val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 311c346d5..d65a46710 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -222,11 +222,12 @@ let rec pp_expr par env args = (hov 2 (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ spc () ++ str "in") ++ spc () ++ hov 0 pp_a2)) - | MLglob r when is_projection r && args <> [] -> - let record = List.hd args in - pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) | MLglob r -> - apply (pp_global r) + (try + let _,args = list_chop (projection_arity r) args in + let record = List.hd args in + pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) + with _ -> apply (pp_global r)) | MLcons (r,[]) -> assert (args=[]); if Refset.mem (long_r r) !cons_cofix then @@ -250,22 +251,43 @@ let rec pp_expr par env args = (pp_expr false env [] t) in let record = - try ignore (find_projections (kn_of_r r)); true with Not_found -> false + try Some (find_projections (kn_of_r r)) with Not_found -> None in - if Array.length pv = 1 && not record then - let s1,s2 = pp_one_pat env pv.(0) in - apply - (hv 0 - (pp_par par' - (hv 0 - (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) - ++ spc () ++ str "in") ++ - spc () ++ hov 0 s2))) - else - apply - (pp_par par' - (v 0 (str "match " ++ expr ++ str " with" ++ - fnl () ++ str " | " ++ pp_pat env pv))) + (try + match record with + | None -> raise Not_found + | Some projs -> + let (_, ids, c) = pv.(0) in + let n = List.length ids in + match c with + | MLrel i when i <= n -> + apply (pp_par par' (pp_expr true env [] t ++ str "." ++ + pp_global (List.nth projs (n-i)))) + | MLapp (MLrel i, a) when i <= n -> + if List.exists (ast_occurs_itvl 1 n) a + then raise Not_found + else + let ids,env' = push_vars (List.rev ids) env in + (pp_apply + (pp_expr true env [] t ++ str "." ++ + pp_global (List.nth projs (n-i))) + par ((List.map (pp_expr true env' []) a) @ args)) + | _ -> raise Not_found + with Not_found -> + if Array.length pv = 1 && record = None then + let s1,s2 = pp_one_pat env pv.(0) in + apply + (hv 0 + (pp_par par' + (hv 0 + (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) + ++ spc () ++ str "in") ++ + spc () ++ hov 0 s2))) + else + apply + (pp_par par' + (v 0 (str "match " ++ expr ++ str " with" ++ + fnl () ++ str " | " ++ pp_pat env pv)))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -476,7 +498,10 @@ let pp_decl mp = (str "let " ++ if is_custom r then e ++ str " = " ++ str (find_custom r) - else if is_projection r then e ++ str " x = x." ++ e + else if is_projection r then + let s = prvecti (fun _ -> str) + (Array.make (projection_arity r) " _") in + e ++ s ++ str " x = x." ++ e else pp_function (empty_env ()) e a) | Dfix (rv,defs,typs) -> pp_Dfix true 0 (rv,defs,typs) diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 1f13d9ce1..9f0b2cf73 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -154,15 +154,16 @@ let is_recursor = function let records = ref (KNmap.empty : global_reference list KNmap.t) let init_records () = records := KNmap.empty -let projs = ref Refset.empty -let init_projs () = projs := Refset.empty +let projs = ref (Refmap.empty : int Refmap.t) +let init_projs () = projs := Refmap.empty -let add_record kn l = +let add_record kn n l = records := KNmap.add (long_kn kn) l !records; - projs := List.fold_right (fun r -> Refset.add (long_r r)) l !projs + projs := List.fold_right (fun r -> Refmap.add (long_r r) n) l !projs let find_projections kn = KNmap.find (long_kn kn) !records -let is_projection r = Refset.mem (long_r r) !projs +let is_projection r = Refmap.mem (long_r r) !projs +let projection_arity r = Refmap.find (long_r r) !projs (*s Tables synchronization. *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 413fa8ed3..e4169a9bf 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -62,9 +62,10 @@ val lookup_ind : kernel_name -> ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool -val add_record : kernel_name -> global_reference list -> unit +val add_record : kernel_name -> int -> global_reference list -> unit val find_projections : kernel_name -> global_reference list val is_projection : global_reference -> bool +val projection_arity : global_reference -> int val add_aliases : module_path -> module_path -> unit val long_mp : module_path -> module_path -- cgit v1.2.3