diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-25 16:54:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-25 16:54:51 +0000 |
commit | 984890d972aaa0586b509058dc4fcea5f2c3ca2d (patch) | |
tree | 2cc33bf08d984ceec6f3324c2d94cdae5bf94943 /plugins | |
parent | 2fd746b3ca082ee403146a75ef2706f75bf13f9e (diff) |
Extraction: allow extraction of records with anonymous fields (fix #2555)
For Ocaml, we now use the extraction-reserved substring "__" :
The name foo__i will be pick for i-th field of record foo if it is anonymous.
For Haskell, still no printing of records as native records,
hence nothing to do.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/extraction.ml | 25 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 2 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 90 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 1 |
6 files changed, 63 insertions, 61 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 54fdbcaea..b9c42c30d 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -443,17 +443,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let mp,d,_ = repr_mind kn in let rec select_fields l typs = match l,typs with | [],[] -> [] - | (Name id)::l, typ::typs -> - if isDummy (expand env typ) then select_fields l typs - else - let knp = make_con mp d (label_of_id id) in - if List.for_all ((=) Keep) (type2signature env typ) - then - projs := Cset.add knp !projs; - (ConstRef knp) :: (select_fields l typs) + | _::l, typ::typs when isDummy (expand env typ) -> + select_fields l typs | Anonymous::l, typ::typs -> - if isDummy (expand env typ) then select_fields l typs - else error_record r + None :: (select_fields l typs) + | Name id::l, typ::typs -> + let knp = make_con mp d (label_of_id id) in + (* Is it safe to use [id] for projections [foo.id] ? *) + if List.for_all ((=) Keep) (type2signature env typ) + then projs := Cset.add knp !projs; + Some (ConstRef knp) :: (select_fields l typs) | _ -> assert false in let field_glob = select_fields field_names typ @@ -464,10 +463,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let n = nb_default_params env (Inductive.type_of_inductive env (mib,mip0)) in - List.iter - (Option.iter - (fun kn -> if Cset.mem kn !projs then add_projection n kn)) - (lookup_projections ip) + let check_proj kn = if Cset.mem kn !projs then add_projection n kn in + List.iter (Option.iter check_proj) (lookup_projections ip) with Not_found -> () end; Record field_glob diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 87ddcc7b4..edff48c85 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -55,7 +55,7 @@ type inductive_kind = | Singleton | Coinductive | Standard - | Record of global_reference list + | Record of global_reference option list (* None for anonymous field *) (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 3dd51ae81..a548c7866 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -67,7 +67,7 @@ let struct_iter do_decl do_spec s = type do_ref = global_reference -> unit let record_iter_references do_term = function - | Record l -> List.iter do_term l + | Record l -> List.iter (Option.iter do_term) l | _ -> () let type_iter_references do_type t = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index f34bcf1e9..9885c64b1 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -111,9 +111,18 @@ let get_infix r = let s = find_custom r in String.sub s 1 (String.length s - 2) -exception NoRecord +let get_ind = function + | IndRef _ as r -> r + | ConstructRef (ind,_) -> IndRef ind + | _ -> assert false -let find_projections = function Record l -> l | _ -> raise NoRecord +let pp_one_field r i = function + | Some r -> pp_global Term r + | None -> pp_global Type (get_ind r) ++ str "__" ++ int i + +let pp_field r fields i = pp_one_field r i (List.nth fields i) + +let pp_fields r fields = list_map_i (pp_one_field r) 0 fields (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) @@ -201,9 +210,9 @@ let rec pp_expr par env args = | MLcons (_,r,[]) -> assert (args=[]); pp_global Cons r - | MLcons ({c_kind = Record projs}, r, args') -> + | MLcons ({c_kind = Record fields}, r, args') -> assert (args=[]); - pp_record_pat (projs, List.map (pp_expr true env []) args') + pp_record_pat (pp_fields r fields, List.map (pp_expr true env []) args') | MLcons (_,r,[arg1;arg2]) when is_infix r -> assert (args=[]); pp_par par @@ -233,25 +242,25 @@ let rec pp_expr par env args = (pp_expr false env [] t) in (try - let projs = find_projections info.m_kind in - let (_, ids, c) = pv.(0) in + (* First, can this match be printed as a mere record projection ? *) + let fields = + match info.m_kind with Record f -> f | _ -> raise Impossible + in + let (r, ids, c) = pv.(0) in let n = List.length ids in + let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in + let proj_hd i = + pp_expr true env [] t ++ str "." ++ pp_field r fields i + in match c with - | MLrel i when i <= n -> - apply (pp_par par' (pp_expr true env [] t ++ str "." ++ - pp_global Term (List.nth projs (n-i)))) - | MLapp (MLrel i, a) when i <= n -> - if List.exists (ast_occurs_itvl 1 n) a - then raise NoRecord - else - 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))) - par ((List.map (pp_expr true env' []) a) @ args)) - | _ -> raise NoRecord - with NoRecord -> + | MLrel i when i <= n -> apply (pp_par par' (proj_hd (n-i))) + | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) -> + let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in + (pp_apply (proj_hd (n-i)) + par ((List.map (pp_expr true env' []) a) @ args)) + | _ -> raise Impossible + with Impossible -> + (* Second, can this match be printed as a let-in ? *) if Array.length pv = 1 then let s1,s2 = pp_one_pat env info pv.(0) in apply @@ -262,6 +271,7 @@ let rec pp_expr par env args = ++ spc () ++ str "in") ++ spc () ++ hov 0 s2))) else + (* Otherwise, standard match *) apply (pp_par par' (try pp_ifthenelse par' env expr pv @@ -282,11 +292,11 @@ let rec pp_expr par env args = pp_par par (str "failwith \"AXIOM TO BE REALIZED\"") -and pp_record_pat (projs, args) = +and pp_record_pat (fields, args) = str "{ " ++ prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a) - (List.combine projs args) ++ + (fun (f,a) -> f ++ str " =" ++ spc () ++ a) + (List.combine fields args) ++ str " }" and pp_ifthenelse par env expr pv = match pv with @@ -303,18 +313,18 @@ and pp_ifthenelse par env expr pv = match pv with and pp_one_pat env info (r,ids,t) = 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 info.m_kind in - pp_record_pat (projs, List.rev_map pr_id ids), expr - with NoRecord -> - (match List.rev ids with - | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2 - | [] -> pp_global Cons r - | ids -> + let patt = match info.m_kind with + | Record fields -> + pp_record_pat (pp_fields r fields, List.rev_map pr_id ids) + | _ -> match List.rev ids with + | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2 + | [] -> pp_global Cons r + | ids -> (* hack Extract Inductive prod *) (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ()) - ++ pp_boxed_tuple pr_id ids), - expr + ++ pp_boxed_tuple pr_id ids + in + patt, expr and pp_pat env info pv = let factor_br, factor_set = try match info.m_same with @@ -447,10 +457,11 @@ let pp_singleton kn packet = pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) -let pp_record kn projs ip_equiv packet = - let name = pp_global Type (IndRef (kn,0)) in - let projnames = List.map (pp_global Term) projs in - let l = List.combine projnames packet.ip_types.(0) in +let pp_record kn fields ip_equiv packet = + let ind = IndRef (kn,0) in + let name = pp_global Type ind in + let fieldnames = pp_fields ind fields in + let l = List.combine fieldnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in str "type " ++ pp_parameters pl ++ name ++ pp_equiv pl name ip_equiv ++ str " = { "++ @@ -511,8 +522,7 @@ let pp_mind kn i = match i.ind_kind with | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i - | Record projs -> - pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0) + | Record fields -> pp_record kn fields (i.ind_equiv,0) i.ind_packets.(0) | Standard -> pp_ind false kn i let pp_decl = function diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index c58672ca0..502d06235 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -362,10 +362,6 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let error_record r = - err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++ - fnl () ++ str "To help extraction, please use an explicit name.") - let msg_non_implicit r n id = let name = match id with | Anonymous -> "" diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7860dd6a5..cdd792222 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -34,7 +34,6 @@ val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a val error_MPfile_as_mod : module_path -> bool -> 'a -val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit |