From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- plugins/extraction/ExtrOcamlBasic.v | 4 +- plugins/extraction/ExtrOcamlBigIntConv.v | 2 +- plugins/extraction/ExtrOcamlIntConv.v | 2 +- plugins/extraction/ExtrOcamlNatBigInt.v | 6 +- plugins/extraction/ExtrOcamlNatInt.v | 8 +- plugins/extraction/ExtrOcamlString.v | 2 +- plugins/extraction/ExtrOcamlZBigInt.v | 70 +++---- plugins/extraction/ExtrOcamlZInt.v | 66 ++++--- plugins/extraction/big.ml | 2 +- plugins/extraction/common.ml | 37 +++- plugins/extraction/common.mli | 15 +- plugins/extraction/extract_env.ml | 128 +++++++----- plugins/extraction/extract_env.mli | 10 +- plugins/extraction/extraction.ml | 178 ++++++++++------- plugins/extraction/extraction.mli | 4 +- plugins/extraction/g_extraction.ml4 | 8 +- plugins/extraction/haskell.ml | 158 +++++++-------- plugins/extraction/haskell.mli | 4 +- plugins/extraction/miniml.mli | 50 +++-- plugins/extraction/mlutil.ml | 287 +++++++++++++++------------ plugins/extraction/mlutil.mli | 11 +- plugins/extraction/modutil.ml | 91 ++++++--- plugins/extraction/modutil.mli | 7 +- plugins/extraction/ocaml.ml | 327 +++++++++++++++---------------- plugins/extraction/ocaml.mli | 4 +- plugins/extraction/scheme.ml | 29 +-- plugins/extraction/scheme.mli | 4 +- plugins/extraction/table.ml | 219 +++++++++++++-------- plugins/extraction/table.mli | 38 +++- 29 files changed, 1003 insertions(+), 768 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index eab2f67c..c9556972 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool [ true false ]. Extract Inductive option => option [ Some None ]. Extract Inductive unit => unit [ "()" ]. diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index e38d41e3..69e72918 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "fun n -> Big.max Big.zero (Big.pred n)". Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)". Extract Constant max => "Big.max". Extract Constant min => "Big.min". -Extract Constant nat_beq => "Big.eq". +(*Extract Constant nat_beq => "Big.eq".*) Extract Constant EqNat.beq_nat => "Big.eq". Extract Constant EqNat.eq_nat_decide => "Big.eq". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index e577ebe1..a0cb26b5 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "fun n m -> max 0 (n-m)". Extract Constant mult => "( * )". Extract Inlined Constant max => max. Extract Inlined Constant min => min. -Extract Inlined Constant nat_beq => "(=)". +(*Extract Inlined Constant nat_beq => "(=)".*) Extract Inlined Constant EqNat.beq_nat => "(=)". Extract Inlined Constant EqNat.eq_nat_decide => "(=)". @@ -72,4 +72,4 @@ Definition test n m (H:m>0) := nat_compare n (q*m+r). Recursive Extraction test fact. -*) \ No newline at end of file +*) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index 48260e3d..f8f942c8 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* "Big.big_int" (** Efficient (but uncertified) versions for usual functions *) -Extract Constant Pplus => "Big.add". -Extract Constant Psucc => "Big.succ". -Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)". -Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)". -Extract Constant Pmult => "Big.mult". -Extract Constant Pmin => "Big.min". -Extract Constant Pmax => "Big.max". -Extract Constant Pcompare => +Extract Constant Pos.add => "Big.add". +Extract Constant Pos.succ => "Big.succ". +Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)". +Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)". +Extract Constant Pos.mul => "Big.mult". +Extract Constant Pos.min => "Big.min". +Extract Constant Pos.max => "Big.max". +Extract Constant Pos.compare => + "fun x y -> Big.compare_case Eq Lt Gt x y". +Extract Constant Pos.compare_cont => "fun x y c -> Big.compare_case c Lt Gt x y". -Extract Constant Nplus => "Big.add". -Extract Constant Nsucc => "Big.succ". -Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)". -Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)". -Extract Constant Nmult => "Big.mult". -Extract Constant Nmin => "Big.min". -Extract Constant Nmax => "Big.max". -Extract Constant Ndiv => +Extract Constant N.add => "Big.add". +Extract Constant N.succ => "Big.succ". +Extract Constant N.pred => "fun n -> Big.max Big.zero (Big.pred n)". +Extract Constant N.sub => "fun n m -> Big.max Big.zero (Big.sub n m)". +Extract Constant N.mul => "Big.mult". +Extract Constant N.min => "Big.min". +Extract Constant N.max => "Big.max". +Extract Constant N.div => "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b". -Extract Constant Nmod => +Extract Constant N.modulo => "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b". -Extract Constant Ncompare => "Big.compare_case Eq Lt Gt". - -Extract Constant Zplus => "Big.add". -Extract Constant Zsucc => "Big.succ". -Extract Constant Zpred => "Big.pred". -Extract Constant Zminus => "Big.sub". -Extract Constant Zmult => "Big.mult". -Extract Constant Zopp => "Big.opp". -Extract Constant Zabs => "Big.abs". -Extract Constant Zmin => "Big.min". -Extract Constant Zmax => "Big.max". -Extract Constant Zcompare => "Big.compare_case Eq Lt Gt". - -Extract Constant Z_of_N => "fun p -> p". -Extract Constant Zabs_N => "Big.abs". +Extract Constant N.compare => "Big.compare_case Eq Lt Gt". + +Extract Constant Z.add => "Big.add". +Extract Constant Z.succ => "Big.succ". +Extract Constant Z.pred => "Big.pred". +Extract Constant Z.sub => "Big.sub". +Extract Constant Z.mul => "Big.mult". +Extract Constant Z.opp => "Big.opp". +Extract Constant Z.abs => "Big.abs". +Extract Constant Z.min => "Big.min". +Extract Constant Z.max => "Big.max". +Extract Constant Z.compare => "Big.compare_case Eq Lt Gt". + +Extract Constant Z.of_N => "fun p -> p". +Extract Constant Z.abs_N => "Big.abs". (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index a7046626..55ba0ca1 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* int [ "0" "" ] (** Efficient (but uncertified) versions for usual functions *) -Extract Constant Pplus => "(+)". -Extract Constant Psucc => "succ". -Extract Constant Ppred => "fun n -> max 1 (n-1)". -Extract Constant Pminus => "fun n m -> max 1 (n-m)". -Extract Constant Pmult => "( * )". -Extract Constant Pmin => "min". -Extract Constant Pmax => "max". -Extract Constant Pcompare => +Extract Constant Pos.add => "(+)". +Extract Constant Pos.succ => "succ". +Extract Constant Pos.pred => "fun n -> max 1 (n-1)". +Extract Constant Pos.sub => "fun n m -> max 1 (n-m)". +Extract Constant Pos.mul => "( * )". +Extract Constant Pos.min => "min". +Extract Constant Pos.max => "max". +Extract Constant Pos.compare => + "fun x y -> if x=y then Eq else if x "fun x y c -> if x=y then c else if x "(+)". -Extract Constant Nsucc => "succ". -Extract Constant Npred => "fun n -> max 0 (n-1)". -Extract Constant Nminus => "fun n m -> max 0 (n-m)". -Extract Constant Nmult => "( * )". -Extract Constant Nmin => "min". -Extract Constant Nmax => "max". -Extract Constant Ndiv => "fun a b -> if b=0 then 0 else a/b". -Extract Constant Nmod => "fun a b -> if b=0 then a else a mod b". -Extract Constant Ncompare => +Extract Constant N.add => "(+)". +Extract Constant N.succ => "succ". +Extract Constant N.pred => "fun n -> max 0 (n-1)". +Extract Constant N.sub => "fun n m -> max 0 (n-m)". +Extract Constant N.mul => "( * )". +Extract Constant N.min => "min". +Extract Constant N.max => "max". +Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b". +Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b". +Extract Constant N.compare => "fun x y -> if x=y then Eq else if x "(+)". -Extract Constant Zsucc => "succ". -Extract Constant Zpred => "pred". -Extract Constant Zminus => "(-)". -Extract Constant Zmult => "( * )". -Extract Constant Zopp => "(~-)". -Extract Constant Zabs => "abs". -Extract Constant Zmin => "min". -Extract Constant Zmax => "max". -Extract Constant Zcompare => +Extract Constant Z.add => "(+)". +Extract Constant Z.succ => "succ". +Extract Constant Z.pred => "pred". +Extract Constant Z.sub => "(-)". +Extract Constant Z.mul => "( * )". +Extract Constant Z.opp => "(~-)". +Extract Constant Z.abs => "abs". +Extract Constant Z.min => "min". +Extract Constant Z.max => "max". +Extract Constant Z.compare => "fun x y -> if x=y then Eq else if x "fun p -> p". -Extract Constant Zabs_N => "abs". +Extract Constant Z.of_N => "fun p -> p". +Extract Constant Z.abs_N => "abs". (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index ae04ba6d..4c33691d 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* true | _ -> false let pp_par par st = if par then str "(" ++ st ++ str ")" else st +(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *) + let pp_apply st par args = match args with | [] -> st | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) +(** Same as [pp_apply], but with also protection of the head by parenthesis *) + +let pp_apply2 st par args = + let par' = args <> [] || par in + pp_apply (pp_par par' st) par args + let pr_binding = function | [] -> mt () | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l +let pp_tuple_light f = function + | [] -> mt () + | [x] -> f true x + | l -> + pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l) + +let pp_tuple f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l) + +let pp_boxed_tuple f = function + | [] -> mt () + | [x] -> f x + | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l)) + (** By default, in module Format, you can do horizontal placing of blocks even if they include newlines, as long as the number of chars in the - blocks are less that a line length. To avoid this awkward situation, + blocks is less that a line length. To avoid this awkward situation, we attach a big virtual size to [fnl] newlines. *) let fnl () = stras (1000000,"") ++ fnl () @@ -54,8 +76,6 @@ let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () -let sec_space_if = function true -> spc () | false -> mt () - let is_digit = function | '0'..'9' -> true | _ -> false @@ -352,12 +372,13 @@ let ref_renaming_fun (k,r) = let l = mp_renaming mp in let l = if lang () <> Ocaml && not (modular ()) then [""] else l in let s = + let idg = safe_basename_of_global r in if l = [""] (* this happens only at toplevel of the monolithic case *) then let globs = Idset.elements (get_global_ids ()) in - let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in + let id = next_ident_away (kindcase_id k idg) globs in string_of_id id - else modular_rename k (safe_basename_of_global r) + else modular_rename k idg in add_global_ids (id_of_string s); s::l diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 22bad6cd..02a496be 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* std_ppcmds val fnl2 : unit -> std_ppcmds val space_if : bool -> std_ppcmds -val sec_space_if : bool -> std_ppcmds val pp_par : bool -> std_ppcmds -> std_ppcmds + +(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *) val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds + +(** Same as [pp_apply], but with also protection of the head by parenthesis *) +val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds + +val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds +val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds + val pr_binding : identifier list -> std_ppcmds val rename_id : identifier -> Idset.t -> identifier diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 3fa674d3..73062328 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* failwith "caught" in - match current_toplevel () with - | _ -> SEBstruct (List.rev (map_succeed get_reference seg)) - + SEBstruct (List.rev (map_succeed get_reference seg)) + let environment_until dir_opt = let rec parse = function | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] | [] -> [] | d :: l -> - let mb = Global.lookup_module (MPfile d) in - (* If -dont-load-proof has been used, mod_expr is None, - we try with mod_type *) - let meb = Option.default mb.mod_type mb.mod_expr in - if dir_opt = Some d then [MPfile d, meb] - else (MPfile d, meb) :: (parse l) + match (Global.lookup_module (MPfile d)).mod_expr with + | Some meb -> + if dir_opt = Some d then [MPfile d, meb] + else (MPfile d, meb) :: (parse l) + | _ -> assert false in parse (Library.loaded_libraries ()) @@ -68,6 +64,9 @@ module type VISIT = sig (* Add the module_path and all its prefixes to the mp visit list *) val add_mp : module_path -> unit + (* Same, but we'll keep all fields of these modules *) + val add_mp_all : module_path -> unit + (* Add kernel_name / constant / reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) val add_ind : mutual_inductive -> unit @@ -81,6 +80,7 @@ module type VISIT = sig val needed_ind : mutual_inductive -> bool val needed_con : constant -> bool val needed_mp : module_path -> bool + val needed_mp_all : module_path -> bool end module Visit : VISIT = struct @@ -88,16 +88,26 @@ module Visit : VISIT = struct (for inductives and modules names) and a Cset_env for constants (and still the remaining MPset) *) type must_visit = - { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t } + { mutable ind : KNset.t; mutable con : KNset.t; + mutable mp : MPset.t; mutable mp_all : MPset.t } (* the imperative internal visit lists *) - let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty } + let v = { ind = KNset.empty ; con = KNset.empty ; + mp = MPset.empty; mp_all = MPset.empty } (* the accessor functions *) - let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty + let reset () = + v.ind <- KNset.empty; + v.con <- KNset.empty; + v.mp <- MPset.empty; + v.mp_all <- MPset.empty let needed_ind i = KNset.mem (user_mind i) v.ind let needed_con c = KNset.mem (user_con c) v.con - let needed_mp mp = MPset.mem mp v.mp + let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all + let needed_mp_all mp = MPset.mem mp v.mp_all let add_mp mp = check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_mp_all mp = + check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp; + v.mp_all <- MPset.add mp v.mp_all let add_ind i = let kn = user_mind i in v.ind <- KNset.add kn v.ind; add_mp (modpath kn) @@ -120,12 +130,17 @@ let check_arity env cb = let check_fix env cb i = match cb.const_body with - | None -> raise Impossible - | Some lbody -> - match kind_of_term (Declarations.force lbody) with + | Def lbody -> + (match kind_of_term (Declarations.force lbody) with | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd) | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd) - | _ -> raise Impossible + | _ -> raise Impossible) + | Undef _ | OpaqueDef _ -> raise Impossible + +let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = + na1 = na2 && + array_equal eq_constr ca1 ca2 && + array_equal eq_constr ta1 ta2 let factor_fix env l cb msb = let _,recd as check = check_fix env cb 0 in @@ -139,7 +154,8 @@ let factor_fix env l cb msb = (fun j -> function | (l,SFBconst cb') -> - if check <> check_fix env cb' (j+1) then raise Impossible; + let check' = check_fix env cb' (j+1) in + if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; labels, recd, msb'' @@ -157,7 +173,8 @@ let rec seb2mse = function let expand_seb env mp seb = let seb,_,_,_ = - Mod_typing.translate_struct_module_entry env mp true (seb2mse seb) + let inl = Some (Flags.get_inline_level()) in + Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb) in seb (** When possible, we use the nicer, shorter, algebraic type structures @@ -200,9 +217,8 @@ let rec extract_sfb_spec env mp = function if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let kn = make_kn mp empty_dirpath l in - let mind = mind_of_kn kn in - let s = Sind (kn, extract_inductive env mind) in + let mind = make_mind mp empty_dirpath l in + let s = Sind (mind, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end @@ -223,7 +239,7 @@ let rec extract_sfb_spec env mp = function *) and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with - | SEBident mp -> Visit.add_mp mp; MTident mp + | SEBident mp -> Visit.add_mp_all mp; MTident mp | SEBwith(seb',With_definition_body(idl,cb))-> let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in let mt = extract_seb_spec env mp1 (seb,seb') in @@ -231,7 +247,7 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with | None -> mt | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ))) | SEBwith(seb',With_module_body(idl,mp))-> - Visit.add_mp mp; + Visit.add_mp_all mp; MTwith(extract_seb_spec env mp1 (seb,seb'), ML_With_module(idl,mp)) | SEBfunctor (mbid, mtb, seb_alg') -> @@ -283,11 +299,10 @@ let rec extract_sfb env mp all = function else ms) | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in - let kn = make_kn mp empty_dirpath l in - let mind = mind_of_kn kn in + let mind = make_mind mp empty_dirpath l in let b = Visit.needed_ind mind in if all || b then - let d = Dind (kn, extract_inductive env mind) in + let d = Dind (mind, extract_inductive env mind) in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms @@ -312,7 +327,7 @@ and extract_seb env mp all = function extract_seb env mp all (expand_seb env mp seb) | SEBident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; - Visit.add_mp mp; MEident mp + Visit.add_mp_all mp; MEident mp | SEBapply (meb, meb',_) -> MEapply (extract_seb env mp true meb, extract_seb env mp true meb') @@ -346,11 +361,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = Visit.reset (); List.iter Visit.add_ref refs; - List.iter Visit.add_mp mpl; + List.iter Visit.add_mp_all mpl; let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l + (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m)) + l (**************************************) (*S Part II : Input/Output primitives *) @@ -488,13 +504,18 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init modular = +let init modular library = check_inside_section (); check_inside_module (); set_keywords (descr ()).keywords; set_modular modular; + set_library library; reset (); if modular && lang () = Scheme then error_scheme () +let warns () = + warning_opaques (access_opaque ()); + warning_axioms () + (* From a list of [reference], let's retrieve whether they correspond to modules or [global_reference]. Warn the user if both is possible. *) @@ -503,7 +524,8 @@ let rec locate_ref = function | r::l -> let q = snd (qualid_of_reference r) in let mpo = try Some (Nametab.locate_module q) with Not_found -> None - and ro = try Some (Nametab.locate q) with Not_found -> None in + and ro = try Some (Smartlocate.global_with_alias r) with _ -> None + in match mpo, ro with | None, None -> Nametab.error_global_not_found q | None, Some r -> let refs,mps = locate_ref l in r::refs,mps @@ -518,25 +540,41 @@ let rec locate_ref = function \verb!Extraction "file"! [qualid1] ... [qualidn]. *) let full_extr f (refs,mps) = - init false; + init false false; List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps; - let struc = optimize_struct refs (mono_environment refs mps) in - warning_axioms (); + let struc = optimize_struct (refs,mps) (mono_environment refs mps) in + warns (); print_structure_to_file (mono_filename f) false struc; reset () let full_extraction f lr = full_extr f (locate_ref lr) +(*s Separate extraction is similar to recursive extraction, with the output + decomposed in many files, one per Coq .v file *) + +let separate_extraction lr = + init true false; + let refs,mps = locate_ref lr in + let struc = optimize_struct (refs,mps) (mono_environment refs mps) in + warns (); + let print = function + | (MPfile dir as mp, sel) as e -> + print_structure_to_file (module_filename mp) false [e] + | _ -> assert false + in + List.iter print struc; + reset () + (*s Simple extraction in the Coq toplevel. The vernacular command is \verb!Extraction! [qualid]. *) let simple_extraction r = match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> - init false; - let struc = optimize_struct [r] (mono_environment [r] []) in + init false false; + let struc = optimize_struct ([r],[]) (mono_environment [r] []) in let d = get_decl_in_structure r struc in - warning_axioms (); + warns (); if is_custom r then msgnl (str "(** User defined extraction *)"); print_one_decl struc (modpath_of_r r) d; reset () @@ -547,12 +585,12 @@ let simple_extraction r = match locate_ref [r] with \verb!(Recursive) Extraction Library! [M]. *) let extraction_library is_rec m = - init true; + init true true; let dir_m = let q = qualid_of_ident m in try Nametab.full_name_module q with Not_found -> error_unknown_module q in - Visit.add_mp (MPfile dir_m); + Visit.add_mp_all (MPfile dir_m); let env = Global.env () in let l = List.rev (environment_until (Some dir_m)) in let select l (mp,meb) = @@ -561,8 +599,8 @@ let extraction_library is_rec m = else l in let struc = List.fold_left select [] l in - let struc = optimize_struct [] struc in - warning_axioms (); + let struc = optimize_struct ([],[]) struc in + warns (); let print = function | (MPfile dir as mp, sel) as e -> let dry = not is_rec && dir <> dir_m in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 145cd6b3..e587bf21 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val full_extraction : string option -> reference list -> unit +val separate_extraction : reference list -> unit val extraction_library : bool -> identifier -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : global_reference list -> module_path list -> Miniml.ml_structure + +(* Used by the Relation Extraction plugin *) + +val print_one_decl : + Miniml.ml_structure -> module_path -> Miniml.ml_decl -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 27f32a4a..219b3913 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* error_singleton_become_prop id -let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None - (*S Generation of flags and signatures. *) (* The type [flag] gives us information about any Coq term: @@ -197,6 +193,27 @@ let parse_ind_args si args relmax = | _ -> parse (i+1) (j+1) s) in parse 1 1 si +let oib_equal o1 o2 = + id_ord o1.mind_typename o2.mind_typename = 0 && + list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && + begin match o1.mind_arity, o2.mind_arity with + | Monomorphic {mind_user_arity=c1; mind_sort=s1}, + Monomorphic {mind_user_arity=c2; mind_sort=s2} -> + eq_constr c1 c2 && s1 = s2 + | ma1, ma2 -> ma1 = ma2 end && + o1.mind_consnames = o2.mind_consnames + +let mib_equal m1 m2 = + array_equal oib_equal m1.mind_packets m1.mind_packets && + m1.mind_record = m2.mind_record && + m1.mind_finite = m2.mind_finite && + m1.mind_ntypes = m2.mind_ntypes && + list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps && + m1.mind_nparams = m2.mind_nparams && + m1.mind_nparams_rec = m2.mind_nparams_rec && + list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && + m1.mind_constraints = m2.mind_constraints + (*S Extraction of a type. *) (* [extract_type env db c args] is used to produce an ML type from the @@ -215,7 +232,7 @@ let rec extract_type env db j c args = extract_type env db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> (match args with - | [] -> assert false (* otherwise the lambda would be reductible. *) + | [] -> assert false (* A lambda cannot be a type. *) | a :: args -> extract_type env db j (subst1 a d) args) | Prod (n,t,d) -> assert (args = []); @@ -255,12 +272,13 @@ let rec extract_type env db j c args = let cb = lookup_constant kn env in let typ = Typeops.type_of_constant_type env cb.const_type in (match flag_of_type env typ with + | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> let mlt = extract_type_app env db (r, type_sign env typ) args in (match cb.const_body with - | None -> mlt - | Some _ when is_custom r -> mlt - | Some lbody -> + | Undef _ | OpaqueDef _ -> mlt + | Def _ when is_custom r -> mlt + | Def lbody -> let newc = applist (Declarations.force lbody, args) in let mlt' = extract_type env db j newc [] in (* ML type abbreviations interact badly with Coq *) @@ -269,10 +287,11 @@ let rec extract_type env db j c args = (* The shortest is [mlt], which use abbreviations *) (* If possible, we take [mlt], otherwise [mlt']. *) if expand env mlt = expand env mlt' then mlt else mlt') - | _ -> (* only other case here: Info, Default, i.e. not an ML type *) + | (Info, Default) -> + (* Not an ML type, for example [(c:forall X, X->X) Type nat] *) (match cb.const_body with - | None -> Tunknown (* Brutal approximation ... *) - | Some lbody -> + | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) + | Def lbody -> (* We try to reduce. *) let newc = applist (Declarations.force lbody, args) in extract_type env db j newc [])) @@ -282,14 +301,6 @@ let rec extract_type env db j c args = | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false -(* [extract_maybe_type] calls [extract_type] when used on a Coq type, - and otherwise returns [Tdummy] or [Tunknown] *) - -and extract_maybe_type env db c = - let t = whd_betadeltaiota env none (type_of env c) in - if isSort t then extract_type env db 0 c [] - else if sort_of env t = InProp then Tdummy Kother else Tunknown - (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], and is completely applied: [List.length args = List.length s]. *) @@ -337,13 +348,18 @@ and extract_ind env kn = (* kn is supposed to be in long form *) We hence check that the mib has not changed from recording time to retrieving time. Ideally we should also check the env. *) let (mib0,ml_ind) = lookup_ind kn in - if not (mib = mib0) then raise Not_found; + if not (mib_equal mib mib0) then raise Not_found; ml_ind with Not_found -> - (* First, if this inductive is aliased via a Module, *) - (* we process the original inductive. *) - let equiv = - if (canonical_mind kn) = (user_mind kn) then + (* First, if this inductive is aliased via a Module, + we process the original inductive if possible. + When at toplevel of the monolithic case, we cannot do much + (cf Vector and bug #2570) *) + let equiv = + if lang () <> Ocaml || + (not (modular ()) && at_toplevel (mind_modpath kn)) || + kn_ord (canonical_mind kn) (user_mind kn) = 0 + then NoEquiv else begin @@ -370,8 +386,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_logical = (not b); ip_sign = s; ip_vars = v; - ip_types = t; - ip_optim_id_ok = None }) + ip_types = t }) mib.mind_packets in @@ -412,7 +427,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if Array.length p.ip_types <> 1 then raise (I Standard); let typ = p.ip_types.(0) in let l = List.filter (fun t -> not (isDummy (expand env t))) typ in - if List.length l = 1 && not (type_mem_kn kn (List.hd l)) + if not (keep_singleton ()) && + List.length l = 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if l = [] then raise (I Standard); if not mib.mind_record then raise (I Standard); @@ -464,6 +480,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ind_equiv = equiv } in add_ind kn mib i; + add_inductive_kind kn i.ind_kind; i (*s [extract_type_cons] extracts the type of an inductive @@ -496,8 +513,8 @@ and mlt_env env r = match r with let cb = Environ.lookup_constant kn env in let typ = Typeops.type_of_constant_type env cb.const_type in match cb.const_body with - | None -> None - | Some l_body -> + | Undef _ | OpaqueDef _ -> None + | Def l_body -> (match flag_of_type env typ with | Info,TypeScheme -> let body = Declarations.force l_body in @@ -560,6 +577,8 @@ let rec extract_term env mle mlt c args = | LetIn (n, c1, t1, c2) -> let id = id_of_name n in let env' = push_rel (Name id, Some c1, t1) env in + (* We directly push the args inside the [LetIn]. + TODO: the opt_let_app flag is supposed to prevent that *) let args' = List.map (lift 1) args in (try check_default env t1; @@ -727,8 +746,8 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = | Tglob (_,l) -> List.map type_simpl l | _ -> assert false in - let info = {c_kind = mi.ind_kind; c_typs = typeargs} in - put_magic_if magic1 (MLcons (info, ConstructRef cp, mla)) + let typ = Tglob(IndRef ip, typeargs) in + put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla)) in (* Different situations depending of the number of arguments: *) if la < params_nb then @@ -792,22 +811,22 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* We suppress dummy arguments according to signature. *) let ids,e = case_expunge s e in let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in - (r, List.rev ids, e') + (List.rev ids, Pusual r, e') in if mi.ind_kind = Singleton then begin (* Informative singleton case: *) (* [match c with C i -> t] becomes [let i = c' in t'] *) assert (br_size = 1); - let (_,ids,e') = extract_branch 0 in + let (ids,_,e') = extract_branch 0 in assert (List.length ids = 1); MLletin (tmp_id (List.hd ids),a,e') end else (* Standard case: we apply [extract_branch]. *) let typs = List.map type_simpl (Array.to_list metas) in - let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone } - in MLcase (info, a, Array.init br_size extract_branch) + let typ = Tglob (IndRef ip,typs) in + MLcase (typ, a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) @@ -869,7 +888,7 @@ let extract_std_constant env kn body typ = and m = nb_lam body in if n <= m then decompose_lam_n n body else - let s,s' = list_split_at m s in + let s,s' = list_chop m s in if List.for_all ((=) Keep) s' && (lang () = Haskell || sign_kind s <> UnsafeLogicalSig) then decompose_lam_n m body @@ -878,7 +897,7 @@ let extract_std_constant env kn body typ = (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) let rels, c = let n = List.length rels in - let s,s' = list_split_at n s in + let s,s' = list_chop n s in let k = sign_kind s in let empty_s = (k = EmptySig || k = SafeLogicalSig) in if lang () = Ocaml && empty_s && not (gentypvar_ok c) @@ -888,7 +907,7 @@ let extract_std_constant env kn body typ = in let n = List.length rels in let s = list_firstn n s in - let l,l' = list_split_at n l in + let l,l' = list_chop n l in let t' = type_recomp (l',t') in (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in @@ -925,34 +944,45 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in let typ = Typeops.type_of_constant_type env cb.const_type in - match cb.const_body with - | None -> (* A logical axiom is risky, an informative one is fatal. *) - (match flag_of_type env typ with - | (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_name::l) n [] in - Dtype (r, ids, Taxiom) - | (Info,Default) -> - if not (is_custom r) then add_info_axiom r; - let t = snd (record_constant_type env kn (Some typ)) in - Dterm (r, MLaxiom, type_expunge env t) - | (Logic,TypeScheme) -> - add_log_axiom r; Dtype (r, [], Tdummy Ktype) - | (Logic,Default) -> - add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother)) - | Some body -> - (match flag_of_type env typ with - | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother) - | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype) - | (Info, Default) -> - let e,t = extract_std_constant env kn (force body) typ in - Dterm (r,e,t) - | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db (force body) (List.length s) - in Dtype (r, vl, t)) + let warn_info () = if not (is_custom r) then add_info_axiom r in + let warn_log () = if not (constant_has_body cb) then add_log_axiom r + in + let mk_typ_ax () = + let n = type_scheme_nb_args env typ in + let ids = iterate (fun l -> anonymous_name::l) n [] in + Dtype (r, ids, Taxiom) + in + let mk_typ c = + let s,vl = type_sign_vl env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db c (List.length s) + in Dtype (r, vl, t) + in + let mk_ax () = + let t = snd (record_constant_type env kn (Some typ)) in + Dterm (r, MLaxiom, type_expunge env t) + in + let mk_def c = + let e,t = extract_std_constant env kn c typ in + Dterm (r,e,t) + in + match flag_of_type env typ with + | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) + | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother) + | (Info,TypeScheme) -> + (match cb.const_body with + | Undef _ -> warn_info (); mk_typ_ax () + | Def c -> mk_typ (force c) + | OpaqueDef c -> + add_opaque r; + if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ()) + | (Info,Default) -> + (match cb.const_body with + | Undef _ -> warn_info (); mk_ax () + | Def c -> mk_def (force c) + | OpaqueDef c -> + add_opaque r; + if access_opaque () then mk_def (force_opaque c) else mk_ax ()) let extract_constant_spec env kn cb = let r = ConstRef kn in @@ -963,8 +993,8 @@ let extract_constant_spec env kn cb = | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in (match cb.const_body with - | None -> Stype (r, vl, None) - | Some body -> + | Undef _ | OpaqueDef _ -> Stype (r, vl, None) + | Def body -> let db = db_from_sign s in let t = extract_type_scheme env db (force body) (List.length s) in Stype (r, vl, Some t)) @@ -977,9 +1007,13 @@ let extract_with_type env cb = match flag_of_type env typ with | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in - let body = Option.get cb.const_body in let db = db_from_sign s in - let t = extract_type_scheme env db (force body) (List.length s) in + let c = match cb.const_body with + | Def body -> force body + (* A "with Definition ..." is necessarily transparent *) + | Undef _ | OpaqueDef _ -> assert false + in + let t = extract_type_scheme env db c (List.length s) in Some (vl, t) | _ -> None @@ -995,7 +1029,7 @@ let extract_inductive env kn = let l' = filter (succ i) l in if isDummy (expand env t) || List.mem i implicits then l' else t::l' - in filter 1 l + in filter (1+ind.ind_nparams) l in let packets = Array.mapi (fun i p -> { p with ip_types = Array.mapi (f i) p.ip_types }) diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 8a2125fe..48f05acb 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ full_extraction (Some f) l ] END +VERNAC COMMAND EXTEND SeparateExtraction +(* Same, with content splitted in several files *) +| [ "Separate" "Extraction" ne_global_list(l) ] + -> [ separate_extraction l ] +END + (* Modular extraction (one Coq library = one ML module) *) VERNAC COMMAND EXTEND ExtractionLibrary | [ "Extraction" "Library" ident(m) ] diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index aeacef93..96731ed2 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* b -#ifdef __GLASGOW_HASKELL__ -import qualified GHC.Base -unsafeCoerce = GHC.Base.unsafeCoerce# -#else --- HUGS -import qualified IOExts -unsafeCoerce = IOExts.unsafeCoerce -#endif" ++ fnl2 ()) +\nunsafeCoerce :: a -> b\ +\n#ifdef __GLASGOW_HASKELL__\ +\nimport qualified GHC.Base\ +\nunsafeCoerce = GHC.Base.unsafeCoerce#\ +\n#else\ +\n-- HUGS\ +\nimport qualified IOExts\ +\nunsafeCoerce = IOExts.unsafeCoerce\ +\n#endif" ++ fnl2 ()) ++ (if not usf.mldummy then mt () else str "__ :: any" ++ fnl () ++ @@ -78,17 +76,17 @@ let pp_global k r = let kn_sig = let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in - make_kn specif empty_dirpath (mk_label "sig") + make_mind specif empty_dirpath (mk_label "sig") let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (r,l) -> - if r = IndRef (mind_of_kn kn_sig,0) then + | Tglob (IndRef(kn,0),l) + when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" -> pp_type true vl (List.hd l) - else + | Tglob (r,l) -> pp_par par (pp_global Type r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l) @@ -113,8 +111,8 @@ let expr_needs_par = function let rec pp_expr par env args = - let par' = args <> [] || par - and apply st = pp_apply st par args in + let apply st = pp_apply st par args + and apply2 st = pp_apply2 st par args in function | MLrel n -> let id = get_db_name n env in apply (pr_id id) @@ -125,7 +123,7 @@ let rec pp_expr par env args = let fl,a' = collect_lams a 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) + apply2 st | MLletin (id,a1,a2) -> let i,env' = push_vars [id_of_mlid id] env in let pp_id = pr_id (List.hd i) @@ -135,37 +133,42 @@ let rec pp_expr par env args = str "let {" ++ cut () ++ hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}") in - apply - (pp_par par' - (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2))) + apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2)) | MLglob r -> apply (pp_global Term r) - | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c - | MLcons (_,r,[]) -> - assert (args=[]); pp_global Cons r - | MLcons (_,r,[a]) -> - assert (args=[]); - pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) - | MLcons (_,r,args') -> - assert (args=[]); - pp_par par (pp_global Cons r ++ spc () ++ - prlist_with_sep spc (pp_expr true env []) args') + | MLcons (_,r,a) as c -> + assert (args=[]); + begin match a with + | _ when is_native_char c -> pp_native_char c + | [] -> pp_global Cons r + | [a] -> + pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) + | _ -> + pp_par par (pp_global Cons r ++ spc () ++ + prlist_with_sep spc (pp_expr true env []) a) + end + | MLtuple l -> + assert (args=[]); + pp_boxed_tuple (pp_expr true env []) l | MLcase (_,t, pv) when is_custom_match pv -> - let mkfun (_,ids,e) = + if not (is_regular_match pv) then + error "Cannot mix yet user-given match and general patterns."; + let mkfun (ids,_,e) = if ids <> [] then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 in - apply - (pp_par par' - (hov 2 - (str (find_custom_match pv) ++ fnl () ++ - prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv - ++ pp_expr true env [] t))) - | MLcase (info,t, pv) -> - apply (pp_par par' - (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++ - fnl () ++ pp_pat env info pv))) + let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in + let inner = + str (find_custom_match pv) ++ fnl () ++ + prvect pp_branch pv ++ + pp_expr true env [] t + in + apply2 (hov 2 inner) + | MLcase (typ,t,pv) -> + apply2 + (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++ + fnl () ++ 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 @@ -178,44 +181,31 @@ let rec pp_expr par env args = pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") -and pp_pat env info pv = - let pp_one_pat (name,ids,t) = - let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in - let par = expr_needs_par t in - hov 2 (str " " ++ pp_global Cons name ++ - (match ids with - | [] -> mt () - | _ -> (str " " ++ - prlist_with_sep spc pr_id (List.rev ids))) ++ - str " ->" ++ spc () ++ pp_expr par env' [] t) - in - let factor_br, factor_set = try match info.m_same with - | BranchFun ints -> - let i = Intset.choose ints in - branch_as_fun info.m_typs pv.(i), ints - | BranchCst ints -> - let i = Intset.choose ints in - ast_pop (branch_as_cst pv.(i)), ints - | BranchNone -> MLdummy, Intset.empty - with _ -> MLdummy, Intset.empty - in - let last = Array.length pv - 1 in +and pp_cons_pat par r ppl = + pp_par par + (pp_global Cons r ++ space_if (ppl<>[]) ++ prlist_with_sep spc identity ppl) + +and pp_gen_pat par ids env = function + | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l) + | Pusual r -> pp_cons_pat par r (List.map pr_id ids) + | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l + | Pwild -> str "_" + | Prel n -> pr_id (get_db_name n env) + +and pp_one_pat env (ids,p,t) = + let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in + hov 2 (str " " ++ + pp_gen_pat false (List.rev ids') env' p ++ + str " ->" ++ spc () ++ + pp_expr (expr_needs_par t) env' [] t) + +and pp_pat env pv = prvecti - (fun i x -> if Intset.mem i factor_set then mt () else - (pp_one_pat pv.(i) ++ - if i = last && Intset.is_empty factor_set then str "}" else - (str ";" ++ fnl ()))) pv - ++ - if Intset.is_empty factor_set then mt () else - let par = expr_needs_par factor_br in - match info.m_same with - | BranchFun _ -> - let ids, env' = push_vars [anonymous_name] env in - hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br ++ str "}") - | BranchCst _ -> - hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}") - | BranchNone -> mt () + (fun i x -> + pp_one_pat env pv.(i) ++ + if i = Array.length pv - 1 then str "}" else + (str ";" ++ fnl ())) + pv (*s names of the functions ([ids]) are already pushed in [env], and passed here just for convenience. *) @@ -293,12 +283,10 @@ let rec pp_ind first kn i ind = (*s Pretty-printing of a declaration. *) -let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") - let pp_decl = function | Dind (kn,i) when i.ind_kind = Singleton -> - pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () - | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i) + pp_singleton kn i.ind_packets.(0) ++ fnl () + | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i) | Dtype (r, l, t) -> if is_inline_custom r then mt () else diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli index eb774db7..0f8949e3 100644 --- a/plugins/extraction/haskell.mli +++ b/plugins/extraction/haskell.mli @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* c" or "x -> f x" + and cases to avoid type-unsafe optimisations. This will be + either the type of the applied constructor or the type + of the head of the match. *) -type constructor_info = { - c_kind : inductive_kind; - c_typs : ml_type list; -} - -type branch_same = - | BranchNone - | BranchFun of Intset.t - | BranchCst of Intset.t +(** Nota : the constructor [MLtuple] and the extension of [MLcase] + to general patterns have been proposed by P.N. Tollitte for + his Relation Extraction plugin. [MLtuple] is currently not + used by the main extraction, as well as deep patterns. *) -type match_info = { - m_kind : inductive_kind; - m_typs : ml_type list; - m_same : branch_same -} - -type ml_branch = global_reference * ml_ident list * ml_ast +type ml_branch = ml_ident list * ml_pattern * ml_ast and ml_ast = | MLrel of int @@ -128,24 +114,32 @@ and ml_ast = | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference - | MLcons of constructor_info * global_reference * ml_ast list - | MLcase of match_info * ml_ast * ml_branch array + | MLcons of ml_type * global_reference * ml_ast list + | MLtuple of ml_ast list + | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy | MLaxiom | MLmagic of ml_ast +and ml_pattern = + | Pcons of global_reference * ml_pattern list + | Ptuple of ml_pattern list + | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *) + | Pwild + | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **) + (*s ML declarations. *) type ml_decl = - | Dind of kernel_name * ml_ind + | Dind of mutual_inductive * ml_ind | Dtype of global_reference * identifier list * ml_type | Dterm of global_reference * ml_ast * ml_type | Dfix of global_reference array * ml_ast array * ml_type array type ml_spec = - | Sind of kernel_name * ml_ind + | Sind of mutual_inductive * ml_ind | Stype of global_reference * identifier list * ml_type option | Sval of global_reference * ml_type diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 3c7ee0f2..c244e046 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* t0 - | Tmeta {contents=None} -> t - | Tmeta {contents=Some u} -> subst u - | Tarr (a,b) -> Tarr (subst a, subst b) - | Tglob (r, l) -> Tglob (r, List.map subst l) - | a -> a - in subst t - (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *) let type_subst_list l t = @@ -378,54 +364,61 @@ let ast_iter_rel f = | MLlam (_,a) -> iter (n+1) a | MLletin (_,a,b) -> iter n a; iter (n+1) b | MLcase (_,a,v) -> - iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v + iter n a; Array.iter (fun (l,_,t) -> iter (n + (List.length l)) t) v | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v | MLapp (a,l) -> iter n a; List.iter (iter n) l - | MLcons (_,_,l) -> List.iter (iter n) l + | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () in iter 0 (*s Map over asts. *) -let ast_map_case f (c,ids,a) = (c,ids,f a) +let ast_map_branch f (c,ids,a) = (c,ids,f a) + +(* Warning: in [ast_map] we assume that [f] does not change the type + of [MLcons] and of [MLcase] heads *) let ast_map f = function | MLlam (i,a) -> MLlam (i, f a) | MLletin (i,a,b) -> MLletin (i, f a, f b) - | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v) + | MLcase (typ,a,v) -> MLcase (typ,f a, Array.map (ast_map_branch f) v) | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v) | MLapp (a,l) -> MLapp (f a, List.map f l) - | MLcons (i,c,l) -> MLcons (i,c, List.map f l) + | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) + | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a (*s Map over asts, with binding depth as parameter. *) -let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a) +let ast_map_lift_branch f n (ids,p,a) = (ids,p, f (n+(List.length ids)) a) + +(* Same warning as for [ast_map]... *) let ast_map_lift f n = function | MLlam (i,a) -> MLlam (i, f (n+1) a) | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b) - | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v) + | MLcase (typ,a,v) -> MLcase (typ,f n a,Array.map (ast_map_lift_branch f n) v) | MLfix (i,ids,v) -> let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v) | MLapp (a,l) -> MLapp (f n a, List.map (f n) l) - | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l) + | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) + | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a (*s Iter over asts. *) -let ast_iter_case f (c,ids,a) = f a +let ast_iter_branch f (c,ids,a) = f a let ast_iter f = function | MLlam (i,a) -> f a | MLletin (i,a,b) -> f a; f b - | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v + | MLcase (_,a,v) -> f a; Array.iter (ast_iter_branch f) v | MLfix (i,ids,v) -> Array.iter f v | MLapp (a,l) -> f a; List.iter f l - | MLcons (_,c,l) -> List.iter f l + | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () @@ -446,15 +439,6 @@ let ast_occurs_itvl k k' t = ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false with Found -> true -(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *) - -let nb_occur_k k t = - let cpt = ref 0 in - ast_iter_rel (fun i -> if i = k then incr cpt) t; - !cpt - -let nb_occur t = nb_occur_k 1 t - (* Number of occurences of [Rel 1] in [t], with special treatment of match: occurences in different branches aren't added, but we rather use max. *) @@ -464,13 +448,13 @@ let nb_occur_match = | MLcase(_,a,v) -> (nb k a) + Array.fold_left - (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v + (fun r (ids,_,a) -> max r (nb (k+(List.length ids)) a)) 0 v | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b) | MLfix (_,ids,v) -> let k = k+(Array.length ids) in Array.fold_left (fun r a -> r+(nb k a)) 0 v | MLlam (_,a) -> nb (k+1) a | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l - | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l + | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0 in nb 1 @@ -530,6 +514,39 @@ let gen_subst v d t = | a -> ast_map_lift subst n a in subst 0 t +(*S Operations concerning match patterns *) + +let is_basic_pattern = function + | Prel _ | Pwild -> true + | Pusual _ | Pcons _ | Ptuple _ -> false + +let has_deep_pattern br = + let deep = function + | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l) + | Pusual _ | Prel _ | Pwild -> false + in + array_exists (function (_,pat,_) -> deep pat) br + +let is_regular_match br = + if Array.length br = 0 then false (* empty match becomes MLexn *) + else + try + let get_r (ids,pat,c) = + match pat with + | Pusual r -> r + | Pcons (r,l) -> + if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l)) + then raise Impossible; + r + | _ -> raise Impossible + in + let ind = match get_r br.(0) with + | ConstructRef (ind,_) -> ind + | _ -> raise Impossible + in + array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br + with Impossible -> false + (*S Operations concerning lambdas. *) (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns @@ -577,7 +594,6 @@ let rec many_lams id a = function | 0 -> a | n -> many_lams id (MLlam (id,a)) (pred n) -let anonym_lams a n = many_lams anonymous a n let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n let dummy_lams a n = many_lams Dummy a n @@ -679,26 +695,31 @@ let rec ast_glob_subst s t = match t with expansion of type definitions. *) -(*s [branch_as_function b typs (r,l,c)] tries to see branch [c] +(*s [branch_as_function b typ (l,p,c)] tries to see branch [c] as a function [f] applied to [MLcons(r,l)]. For that it transforms any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] if any variable in [l] occurs outside such a [MLcons] *) -let branch_as_fun typs (r,l,c) = +let branch_as_fun typ (l,p,c) = let nargs = List.length l in + let cons = match p with + | Pusual r -> MLcons (typ, r, eta_args nargs) + | Pcons (r,pl) -> + let pat2rel = function Prel i -> MLrel i | _ -> raise Impossible in + MLcons (typ, r, List.map pat2rel pl) + | _ -> raise Impossible + in let rec genrec n = function | MLrel i as c -> let i' = i-n in if i'<1 then c else if i'>nargs then MLrel (i-nargs+1) else raise Impossible - | MLcons(i,r',args) when - r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs -> - MLrel (n+1) + | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1) | a -> ast_map_lift genrec n a in genrec 0 c -(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant +(*s [branch_as_cst (l,p,c)] tries to see branch [c] as a constant independent from the pattern [MLcons(r,l)]. For that is raises [Impossible] if any variable in [l] occurs in [c], and otherwise returns [c] lifted to appear like a function with one arg (for uniformity with [branch_as_fun]). @@ -706,7 +727,7 @@ let branch_as_fun typs (r,l,c) = empty, i.e. when [r] is a constant constructor *) -let branch_as_cst (_,l,c) = +let branch_as_cst (l,_,c) = let n = List.length l in if ast_occurs_itvl 1 n c then raise Impossible; ast_lift (1-n) c @@ -745,20 +766,27 @@ let census_add, census_max, census_clean = constant. *) -let factor_branches o typs br = - census_clean (); - for i = 0 to Array.length br - 1 do - if o.opt_case_idr then - (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ()); - if o.opt_case_cst then - (try census_add (branch_as_cst br.(i)) i with Impossible -> ()); - done; - let br_factor, br_set = census_max MLdummy in - census_clean (); - let n = Intset.cardinal br_set in - if n = 0 then None - else if Array.length br >= 2 && n < 2 then None - else Some (br_factor, br_set) +let is_opt_pat (_,p,_) = match p with + | Prel _ | Pwild -> true + | _ -> false + +let factor_branches o typ br = + if array_exists is_opt_pat br then None (* already optimized *) + else begin + census_clean (); + for i = 0 to Array.length br - 1 do + if o.opt_case_idr then + (try census_add (branch_as_fun typ br.(i)) i with Impossible -> ()); + if o.opt_case_cst then + (try census_add (branch_as_cst br.(i)) i with Impossible -> ()); + done; + let br_factor, br_set = census_max MLdummy in + census_clean (); + let n = Intset.cardinal br_set in + if n = 0 then None + else if Array.length br >= 2 && n < 2 then None + else Some (br_factor, br_set) + end (*s If all branches are functions, try to permut the case and the functions. *) @@ -781,14 +809,14 @@ let rec permut_case_fun br acc = let br = Array.copy br in let ids = ref [] in for i = 0 to Array.length br - 1 do - let (r,l,t) = br.(i) in + let (l,p,t) = br.(i) in let local_nb = nb_lams t in if local_nb < !nb then (* t = MLexn ... *) - br.(i) <- (r,l,remove_n_lams local_nb t) + br.(i) <- (l,p,remove_n_lams local_nb t) else begin let local_ids,t = collect_n_lams !nb t in ids := merge_ids !ids local_ids; - br.(i) <- (r,l,permut_rels !nb (List.length l) t) + br.(i) <- (l,p,permut_rels !nb (List.length l) t) end done; (!ids,br) @@ -796,32 +824,43 @@ let rec permut_case_fun br acc = (*S Generalized iota-reduction. *) -(* Definition of a generalized iota-redex: it's a [MLcase(e,_)] - with [(is_iota_gen e)=true]. Any generalized iota-redex is - transformed into beta-redexes. *) - -let rec is_iota_gen = function - | MLcons _ -> true - | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br - | _ -> false - -let constructor_index = function - | ConstructRef (_,j) -> pred j - | _ -> assert false - -let iota_gen br = +(* Definition of a generalized iota-redex: it's a [MLcase(e,br)] + where the head [e] is a [MLcons] or made of [MLcase]'s with + [MLcons] as leaf branches. + A generalized iota-redex is transformed into beta-redexes. *) + +(* In [iota_red], we try to simplify a [MLcase(_,MLcons(typ,r,a),br)]. + Argument [i] is the branch we consider, we should lift what + comes from [br] by [lift] *) + +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 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 + in MLapp (c,a) + | Prel 1 when List.length ids = 1 -> + let c = MLlam (List.hd ids, c) in + let c = ast_lift lift c + in MLapp(c,[MLcons(typ,r,a)]) + | Pwild when ids = [] -> ast_lift lift c + | _ -> raise Impossible (* TODO: handle some more cases *) + +(* [iota_gen] is an extension of [iota_red] where we allow to + traverse matches in the head of the first match *) + +let iota_gen br hd = let rec iota k = function - | MLcons (i,r,a) -> - let (_,ids,c) = br.(constructor_index r) in - let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in - let c = ast_lift k c in - MLapp (c,a) - | MLcase(i,e,br') -> + | MLcons (typ,r,a) -> iota_red 0 k br (typ,r,a) + | MLcase(typ,e,br') -> let new_br = - Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br' - in MLcase(i,e, new_br) - | _ -> assert false - in iota 0 + Array.map (fun (i,p,c)->(i,p,iota (k+(List.length i)) c)) br' + in MLcase(typ,e,new_br) + | _ -> raise Impossible + in iota 0 hd let is_atomic = function | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true @@ -853,9 +892,9 @@ let expand_linear_let o id e = let rec simpl o = function | MLapp (f, []) -> simpl o f | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f) - | 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) + | MLcase (typ,e,br) -> + let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in + simpl_case o typ br (simpl o e) | MLletin(Dummy,_,e) -> simpl o (ast_pop e) | MLletin(id,c,e) -> let e = simpl o e in @@ -891,40 +930,50 @@ and simpl_app o a = function | MLletin (id,e1,e2) when o.opt_let_app -> (* Application of a letin: we push arguments inside *) MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a))) - | MLcase (i,e,br) when o.opt_case_app -> + | MLcase (typ,e,br) when o.opt_case_app -> (* Application of a case: we push arguments inside *) let br' = Array.map - (fun (n,l,t) -> + (fun (l,p,t) -> let k = List.length l in let a' = List.map (ast_lift k) a in - (n, l, simpl o (MLapp (t,a')))) br - in simpl o (MLcase (i,e,br')) + (l, p, simpl o (MLapp (t,a')))) br + in simpl o (MLcase (typ,e,br')) | (MLdummy | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) (* Invariant : all empty matches should now be [MLexn] *) -and simpl_case o i br e = - if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *) +and simpl_case o typ br e = + try + (* Generalized iota-redex *) + if not o.opt_case_iot then raise Impossible; simpl o (iota_gen br e) - else + with Impossible -> (* Swap the case and the lam if possible *) let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in let n = List.length ids in if n <> 0 then - simpl o (named_lams ids (MLcase (i,ast_lift n e, br))) + simpl o (named_lams ids (MLcase (typ, ast_lift n e, br))) else (* Can we merge several branches as the same constant or function ? *) - match factor_branches o i.m_typs br with + if lang() = Scheme || is_custom_match br + then MLcase (typ, e, br) + else match factor_branches o typ br with | Some (f,ints) when Intset.cardinal ints = Array.length br -> - (* If all branches have been factorized, we remove the match *) - simpl o (MLletin (Tmp anonymous_name, e, f)) + (* If all branches have been factorized, we remove the match *) + simpl o (MLletin (Tmp anonymous_name, e, f)) | Some (f,ints) -> - let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints - in MLcase ({i with m_same=same}, e, br) - | None -> MLcase (i, e, br) + let last_br = + if ast_occurs 1 f then ([Tmp anonymous_name], Prel 1, f) + else ([], Pwild, ast_pop f) + in + let brl = Array.to_list br in + let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in + let brl_opt = brl_opt @ [last_br] in + MLcase (typ, e, Array.of_list brl_opt) + | None -> MLcase (typ, e, br) (*S Local prop elimination. *) (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *) @@ -1149,28 +1198,24 @@ let optimize_fix a = (* Utility functions used in the decision of inlining. *) +let ml_size_branch size pv = Array.fold_left (fun a (_,_,t) -> a + size t) 0 pv + let rec ml_size = function | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l | MLlam(_,t) -> 1 + ml_size t - | MLcons(_,_,l) -> ml_size_list l - | MLcase(_,t,pv) -> - 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0) + | MLcons(_,_,l) | MLtuple l -> ml_size_list l + | MLcase(_,t,pv) -> 1 + ml_size t + ml_size_branch ml_size pv | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | _ -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l -and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l +and ml_size_array a = Array.fold_left (fun a t -> a + ml_size t) 0 a let is_fix = function MLfix _ -> true | _ -> false -let rec is_constr = function - | MLcons _ -> true - | MLlam(_,t) -> is_constr t - | _ -> false - (*s Strictness *) (* A variable is strict if the evaluation of the whole term implies @@ -1219,7 +1264,7 @@ let rec non_stricts add cand = function (* so we make an union (in fact a merge). *) let cand = non_stricts false cand t in Array.fold_left - (fun c (_,i,t)-> + (fun c (i,_,t)-> let n = List.length i in let cand = lift n cand in let cand = pop n (non_stricts add cand t) in @@ -1265,12 +1310,14 @@ let inline_test r t = if not (auto_inline ()) then false else let c = match r with ConstRef c -> c | _ -> assert false in - let body = try (Global.lookup_constant c).const_body with _ -> None in - if body = None then false - else - let t1 = eta_red t in - let t2 = snd (collect_lams t1) in - not (is_fix t2) && ml_size t < 12 && is_not_strict t + let has_body = + try constant_has_body (Global.lookup_constant c) + with _ -> false + in + has_body && + (let t1 = eta_red t in + let t2 = snd (collect_lams t1) in + not (is_fix t2) && ml_size t < 12 && is_not_strict t) let con_of_string s = let null = empty_dirpath in diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 54a1baaa..029e8cf4 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val new_meta : 'a -> ml_type -val type_subst : int -> ml_type -> ml_type -> ml_type val type_subst_list : ml_type list -> ml_type -> ml_type val type_subst_vect : ml_type array -> ml_type -> ml_type @@ -118,9 +115,11 @@ val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool +val is_basic_pattern : ml_pattern -> bool +val has_deep_pattern : ml_branch array -> bool +val is_regular_match : ml_branch array -> bool + exception Impossible -val branch_as_fun : ml_type list -> ml_branch -> ml_ast -val branch_as_cst : ml_branch -> ml_ast (* Classification of signatures *) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index ffa38def..9e8dd828 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* () | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' @@ -58,7 +56,10 @@ let struct_iter do_decl do_spec s = | MEapply (me,me') -> me_iter me; me_iter me' | MEstruct (msid, sel) -> List.iter se_iter sel in - List.iter (function (_,sel) -> List.iter se_iter sel) s + se_iter + +let struct_iter do_decl do_spec s = + List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s (*s Apply some fonctions upon all references in [ml_type], [ml_ast], [ml_decl], [ml_spec] and [ml_structure]. *) @@ -76,18 +77,26 @@ let type_iter_references do_type t = | _ -> () in iter t +let patt_iter_references do_cons p = + let rec iter = function + | Pcons (r,l) -> do_cons r; List.iter iter l + | Pusual r -> do_cons r + | Ptuple l -> List.iter iter l + | Prel _ | Pwild -> () + in iter p + let ast_iter_references do_term do_cons do_type a = let rec iter a = ast_iter iter a; match a with | MLglob r -> do_term r - | MLcons (i,r,_) -> - if lang () = Ocaml then record_iter_references do_term i.c_kind; - do_cons r - | MLcase (i,_,v) -> - if lang () = Ocaml then record_iter_references do_term i.m_kind; - Array.iter (fun (r,_,_) -> do_cons r) v - | _ -> () + | MLcons (_,r,_) -> do_cons r + | MLcase (ty,_,v) -> + type_iter_references do_type ty; + Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v + + | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ + | MLdummy | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = @@ -108,15 +117,14 @@ let decl_iter_references do_term do_cons do_type = let type_iter = type_iter_references do_type and ast_iter = ast_iter_references do_term do_cons do_type in function - | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type - (mind_of_kn kn) ind + | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Dtype (r,_,t) -> do_type r; type_iter t | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t | Dfix(rv,c,t) -> Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t let spec_iter_references do_term do_cons do_type = function - | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn kn) ind + | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot | Sval (r,t) -> do_term r; type_iter_references do_type t @@ -236,7 +244,7 @@ let rec optim_se top to_appear s = function let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - if top && i && not (modular ()) && not (List.mem r to_appear) + if top && i && not (library ()) && not (List.mem r to_appear) then optim_se top to_appear s lse else let d = match optimize_fix a with @@ -254,7 +262,7 @@ let rec optim_se top to_appear s = function then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; - if !all && top && not (modular ()) + if !all && top && not (library ()) && (array_for_all (fun r -> not (List.mem r to_appear)) rv) then optim_se top to_appear s lse else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) @@ -271,7 +279,8 @@ and optim_me to_appear s = function | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) (* After these optimisations, some dependencies may not be needed anymore. - For monolithic extraction, we recompute a minimal set of dependencies. *) + For non-library extraction, we recompute a minimal set of dependencies + for first-level objects *) exception NoDepCheck @@ -281,15 +290,19 @@ let base_r = function | ConstructRef ((kn,_),_) -> IndRef (kn,0) | _ -> assert false -let reset_needed, add_needed, found_needed, is_needed = - let needed = ref Refset'.empty in - ((fun l -> needed := Refset'.empty), +let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = + let needed = ref Refset'.empty + and needed_mps = ref MPset.empty in + ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), + (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), - (fun r -> Refset'.mem (base_r r) !needed)) + (fun r -> + let r = base_r r in + Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps)) let declared_refs = function - | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)] + | Dind (kn,_) -> [IndRef (kn,0)] | Dtype (r,_,_) -> [r] | Dterm (r,_,_) -> [r] | Dfix (rv,_,_) -> Array.to_list rv @@ -300,7 +313,7 @@ let declared_refs = function let compute_deps_decl = function | Dind (kn,ind) -> (* Todo Later : avoid dependencies when Extract Inductive *) - ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind + ind_iter_references add_needed add_needed add_needed kn ind | Dtype (r,ids,t) -> if not (is_custom r) then type_iter_references add_needed t | Dterm (r,u,t) -> @@ -310,6 +323,15 @@ let compute_deps_decl = function | Dfix _ as d -> decl_iter_references add_needed add_needed add_needed d +let compute_deps_spec = function + | Sind (kn,ind) -> + (* Todo Later : avoid dependencies when Extract Inductive *) + ind_iter_references add_needed add_needed add_needed kn ind + | Stype (r,ids,t) -> + if not (is_custom r) then Option.iter (type_iter_references add_needed) t + | Sval (r,t) -> + type_iter_references add_needed t + let rec depcheck_se = function | [] -> [] | ((l,SEdecl d) as t) :: se -> @@ -317,7 +339,9 @@ let rec depcheck_se = function let refs = declared_refs d in let refs' = List.filter is_needed refs in if refs' = [] then - (List.iter remove_info_axiom refs; se') + (List.iter remove_info_axiom refs; + List.iter remove_opaque refs; + se') else begin List.iter found_needed refs'; (* Hack to avoid extracting unused part of a Dfix *) @@ -327,7 +351,10 @@ let rec depcheck_se = function ((l,SEdecl (Dfix (rv,trms',tys))) :: se') | _ -> (compute_deps_decl d; t::se') end - | _ -> raise NoDepCheck + | t :: se -> + let se' = depcheck_se se in + se_iter compute_deps_decl compute_deps_spec t; + t :: se' let rec depcheck_struct = function | [] -> [] @@ -350,13 +377,15 @@ let check_implicits = function let optimize_struct to_appear struc = let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in let opt_struc = - List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc + List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) + struc in let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in ignore (struct_ast_search check_implicits opt_struc); - try - if modular () then raise NoDepCheck; + if library () then opt_struc + else begin reset_needed (); - List.iter add_needed to_appear; + List.iter add_needed (fst to_appear); + List.iter add_needed_mp (snd to_appear); depcheck_struct opt_struc - with NoDepCheck -> opt_struc + end diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 26d07872..0565522b 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ml_structure -> ml_decl optimizations. The first argument is the list of objects we want to appear. *) -val optimize_struct : global_reference list -> ml_structure -> ml_structure +val optimize_struct : global_reference list * module_path list -> + ml_structure -> ml_structure diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index c07a1758..ed69ec45 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* mt () - | [x] -> f true x - | l -> - pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l) - -let pp_tuple f = function - | [] -> mt () - | [x] -> f x - | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l) - -let pp_boxed_tuple f = function - | [] -> mt () - | [x] -> f x - | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l)) - let pp_abst = function | [] -> mt () | l -> @@ -59,6 +41,10 @@ let pp_parameters l = let pp_string_parameters l = (pp_boxed_tuple str l ++ space_if (l<>[])) +let pp_letin pat def body = + let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in + hv 0 (hv 0 (hov 2 fstline ++ spc () ++ str "in") ++ spc () ++ hov 0 body) + (*s Ocaml renaming issues. *) let keywords = @@ -137,7 +123,8 @@ let rec pp_type par vl t = | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r - | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" -> + | Tglob (IndRef(kn,0),l) + when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" -> pp_tuple_light pp_rec l | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r @@ -154,10 +141,19 @@ let rec pp_type par vl t = de Bruijn variables. [args] is the list of collected arguments (already pretty-printed). *) +let is_bool_patt p s = + try + let r = match p with + | Pusual r -> r + | Pcons (r,[]) -> r + | _ -> raise Not_found + in + find_custom r = s + with Not_found -> false + + let is_ifthenelse = function - | [|(r1,[],_);(r2,[],_)|] -> - (try (find_custom r1 = "true") && (find_custom r2 = "false") - with Not_found -> false) + | [|([],p1,_);([],p2,_)|] -> is_bool_patt p1 "true" && is_bool_patt p2 "false" | _ -> false let expr_needs_par = function @@ -167,8 +163,8 @@ let expr_needs_par = function | _ -> false let rec pp_expr par env args = - let par' = args <> [] || par - and apply st = pp_apply st par args in + let apply st = pp_apply st par args + and apply2 st = pp_apply2 st par args in function | MLrel n -> let id = get_db_name n env in apply (pr_id id) @@ -179,109 +175,23 @@ let rec pp_expr par env args = 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) + let st = pp_abst (List.rev fl) ++ pp_expr false env' [] a' in + apply2 st | MLletin (id,a1,a2) -> 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 - hv 0 - (apply - (pp_par par' - (hv 0 - (hov 2 - (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ - spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2))) + hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2)) | MLglob r -> (try let args = list_skipn (projection_arity r) args in let record = List.hd args in pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) with _ -> apply (pp_global Term r)) - | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c - | MLcons ({c_kind = Coinductive},r,[]) -> - assert (args=[]); - pp_par par (str "lazy " ++ pp_global Cons r) - | MLcons ({c_kind = Coinductive},r,args') -> - assert (args=[]); - let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") - | MLcons (_,r,[]) -> - assert (args=[]); - pp_global Cons r - | MLcons ({c_kind = Record fields}, r, args') -> - assert (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 - ((pp_expr true env [] arg1) ++ str (get_infix r) ++ - (pp_expr true env [] arg2)) - | MLcons (_,r,args') -> - assert (args=[]); - let tuple = pp_tuple (pp_expr true env []) args' in - if str_global Cons r = "" (* hack Extract Inductive prod *) - then tuple - else pp_par par (pp_global Cons r ++ spc () ++ tuple) - | MLcase (_, t, pv) when is_custom_match pv -> - let mkfun (_,ids,e) = - if ids <> [] then named_lams (List.rev ids) e - else dummy_lams (ast_lift 1 e) 1 - in - apply - (pp_par par' - (hov 2 - (str (find_custom_match pv) ++ fnl () ++ - prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv - ++ pp_expr true env [] t))) - | MLcase (info, t, pv) -> - let expr = if info.m_kind = Coinductive then - (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) - else - (pp_expr false env [] t) - in - (try - (* 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' (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 - (hv 0 - (pp_par par' - (hv 0 - (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) - ++ spc () ++ str "in") ++ - spc () ++ hov 0 s2))) - else - (* Otherwise, standard match *) - apply - (pp_par par' - (try pp_ifthenelse par' env expr pv - with Not_found -> - v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ - pp_pat env info 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 + pp_fix par env' i (Array.of_list (List.rev ids'),defs) args | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)")) @@ -291,7 +201,96 @@ let rec pp_expr par env args = pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "failwith \"AXIOM TO BE REALIZED\"") - + | MLcons (_,r,a) as c -> + assert (args=[]); + begin match a with + | _ when is_native_char c -> pp_native_char c + | [a1;a2] when is_infix r -> + let pp = pp_expr true env [] in + pp_par par (pp a1 ++ str (get_infix r) ++ pp a2) + | _ when is_coinductive r -> + let ne = (a<>[]) in + let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in + pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple)) + | [] -> pp_global Cons r + | _ -> + let fds = get_record_fields r in + if fds <> [] then + pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a) + else + let tuple = pp_tuple (pp_expr true env []) a in + if str_global Cons r = "" (* hack Extract Inductive prod *) + then tuple + else pp_par par (pp_global Cons r ++ spc () ++ tuple) + end + | MLtuple l -> + assert (args = []); + pp_boxed_tuple (pp_expr true env []) l + | MLcase (_, t, pv) when is_custom_match pv -> + if not (is_regular_match pv) then + error "Cannot mix yet user-given match and general patterns."; + let mkfun (ids,_,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in + let inner = + str (find_custom_match pv) ++ fnl () ++ + prvect pp_branch pv ++ + pp_expr true env [] t + in + apply2 (hov 2 inner) + | MLcase (typ, t, pv) -> + let head = + if not (is_coinductive_type typ) then pp_expr false env [] t + else (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) + in + (* First, can this match be printed as a mere record projection ? *) + (try pp_record_proj par env typ t pv args + 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 pv.(0) in + hv 0 (apply2 (pp_letin s1 head s2)) + else + (* Third, can this match be printed as [if ... then ... else] ? *) + (try apply2 (pp_ifthenelse env head pv) + with Not_found -> + (* Otherwise, standard match *) + apply2 + (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++ + pp_pat env pv)))) + +and pp_record_proj par env typ t pv args = + (* Can a match be printed as a mere record projection ? *) + let fields = record_fields_of_type typ in + if fields = [] then raise Impossible; + if Array.length pv <> 1 then raise Impossible; + if has_deep_pattern pv then raise Impossible; + let (ids,pat,body) = pv.(0) in + let n = List.length ids in + let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in + let rel_i,a = match body with + | MLrel i when i <= n -> i,[] + | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a + | _ -> raise Impossible + in + let rec lookup_rel i idx = function + | Prel j :: l -> if i = j then idx else lookup_rel i (idx+1) l + | Pwild :: l -> lookup_rel i (idx+1) l + | _ -> raise Impossible + in + let r,idx = match pat with + | Pusual r -> r, n-rel_i + | Pcons (r,l) -> r, lookup_rel rel_i 0 l + | _ -> raise Impossible + in + if is_infix r then raise Impossible; + let env' = snd (push_vars (List.rev_map id_of_mlid ids) env) in + let pp_args = (List.map (pp_expr true env' []) a) @ args in + let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx + in + pp_apply pp_head par pp_args and pp_record_pat (fields, args) = str "{ " ++ @@ -300,9 +299,27 @@ and pp_record_pat (fields, args) = (List.combine fields args) ++ str " }" -and pp_ifthenelse par env expr pv = match pv with - | [|(tru,[],the);(fal,[],els)|] when - (find_custom tru = "true") && (find_custom fal = "false") +and pp_cons_pat r ppl = + if is_infix r && List.length ppl = 2 then + List.hd ppl ++ str (get_infix r) ++ List.hd (List.tl ppl) + else + let fields = get_record_fields r in + if fields <> [] then pp_record_pat (pp_fields r fields, ppl) + else if str_global Cons r = "" then + pp_boxed_tuple identity ppl (* Hack Extract Inductive prod *) + else + pp_global Cons r ++ space_if (ppl<>[]) ++ pp_boxed_tuple identity ppl + +and pp_gen_pat ids env = function + | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l) + | Pusual r -> pp_cons_pat r (List.map pr_id ids) + | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l + | Pwild -> str "_" + | Prel n -> pr_id (get_db_name n env) + +and pp_ifthenelse env expr pv = match pv with + | [|([],tru,the);([],fal,els)|] when + (is_bool_patt tru "true") && (is_bool_patt fal "false") -> hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ hov 2 (str "then " ++ @@ -311,66 +328,34 @@ and pp_ifthenelse par env expr pv = match pv with hov 2 (pp_expr (expr_needs_par els) env [] els))) | _ -> raise Not_found -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 - 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 - in - patt, expr - -and pp_pat env info pv = - let factor_br, factor_set = try match info.m_same with - | BranchFun ints -> - let i = Intset.choose ints in - branch_as_fun info.m_typs pv.(i), ints - | BranchCst ints -> - let i = Intset.choose ints in - ast_pop (branch_as_cst pv.(i)), ints - | BranchNone -> MLdummy, Intset.empty - with _ -> MLdummy, Intset.empty - in - let last = Array.length pv - 1 in +and pp_one_pat env (ids,p,t) = + let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in + pp_gen_pat (List.rev ids') env' p, + pp_expr (expr_needs_par t) env' [] t + +and pp_pat env pv = prvecti - (fun i x -> if Intset.mem i factor_set then mt () else - let s1,s2 = pp_one_pat env info x in + (fun i x -> + let s1,s2 = pp_one_pat env x in hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++ - if i = last && Intset.is_empty factor_set then mt () else fnl ()) + if i = Array.length pv - 1 then mt () else fnl ()) pv - ++ - if Intset.is_empty factor_set then mt () else - let par = expr_needs_par factor_br in - match info.m_same with - | BranchFun _ -> - let ids, env' = push_vars [anonymous_name] env in - hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - hov 2 (pp_expr par env' [] factor_br)) - | BranchCst _ -> - hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br)) - | BranchNone -> mt () and pp_function env t = let bl,t' = collect_lams t in let bl,env' = push_vars (List.map id_of_mlid bl) env in match t' with - | MLcase(i,MLrel 1,pv) when - i.m_kind = Standard && not (is_custom_match pv) -> - if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then + | MLcase(Tglob(r,_),MLrel 1,pv) when + not (is_coinductive r) && get_record_fields r = [] && + not (is_custom_match pv) -> + if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ - v 0 (pp_pat env' i pv) + v 0 (pp_pat env' pv) else pr_binding (List.rev bl) ++ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (pp_pat env' i pv) + v 0 (pp_pat env' pv) | _ -> pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ @@ -451,7 +436,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (IndRef (mind_of_kn kn,0)) in + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -459,7 +444,7 @@ let pp_singleton kn packet = pr_id packet.ip_consnames.(0))) let pp_record kn fields ip_equiv packet = - let ind = IndRef (mind_of_kn kn,0) in + 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 @@ -482,20 +467,20 @@ let pp_ind co kn ind = let init= ref (str "type ") in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (IndRef (mind_of_kn kn,i))) + pp_global Type (IndRef (kn,i))) ind.ind_packets in let cnames = Array.mapi (fun i p -> if p.ip_logical then [||] else - Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1))) + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) p.ip_types) ind.ind_packets in let rec pp i = if i >= Array.length ind.ind_packets then mt () else - let ip = (mind_of_kn kn,i) in + let ip = (kn,i) in let ip_equiv = ind.ind_equiv, i in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli index c0b4e5b3..fd60c69d 100644 --- a/plugins/extraction/ocaml.mli +++ b/plugins/extraction/ocaml.mli @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* apply (pp_global Term r) - | MLcons (info,r,args') -> + | MLcons (_,r,args') -> assert (args=[]); let st = str "`" ++ @@ -95,9 +93,12 @@ let rec pp_expr env args = (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in - if info.c_kind = Coinductive then paren (str "delay " ++ st) else st + if is_coinductive r then paren (str "delay " ++ st) else st + | MLtuple _ -> error "Cannot handle tuples in Scheme yet." + | MLcase (_,_,pv) when not (is_regular_match pv) -> + error "Cannot handle general patterns in Scheme yet." | MLcase (_,t,pv) when is_custom_match pv -> - let mkfun (_,ids,e) = + let mkfun (ids,_,e) = if ids <> [] then named_lams (List.rev ids) e else dummy_lams (ast_lift 1 e) 1 in @@ -107,9 +108,9 @@ let rec pp_expr env args = (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv ++ pp_expr env [] t))) - | MLcase (info,t, pv) -> - let e = - if info.m_kind <> Coinductive then pp_expr env [] t + | MLcase (typ,t, pv) -> + let e = + if not (is_coinductive_type typ) then pp_expr env [] t else paren (str "force" ++ spc () ++ pp_expr env [] t) in apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv))) @@ -126,14 +127,18 @@ let rec pp_expr env args = | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") and pp_cons_args env = function - | MLcons (info,r,args) when info.c_kind<>Coinductive -> + | MLcons (_,r,args) when is_coinductive r -> paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) | e -> str "," ++ pp_expr env [] e - -and pp_one_pat env (r,ids,t) = +and pp_one_pat env (ids,p,t) = + let r = match p with + | Pusual r -> r + | Pcons (r,l) -> r (* cf. the check [is_regular_match] above *) + | _ -> assert false + in let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let args = if ids = [] then mt () diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli index c7c3d8b5..eeca083c 100644 --- a/plugins/extraction/scheme.mli +++ b/plugins/extraction/scheme.mli @@ -1,11 +1,9 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ConstRef(constant_of_kn(user_con con)) - | IndRef (kn,i) -> IndRef(mind_of_kn(user_mind kn),i) - | ConstructRef ((kn,i),j)-> ConstructRef((mind_of_kn(user_mind kn),i),j) - | VarRef id -> VarRef id - in - Pervasives.compare (make_name x) (make_name y) -end +(** Sets and maps for [global_reference] that use the "user" [kernel_name] + instead of the canonical one *) -module Refmap' = Map.Make(RefOrd) -module Refset' = Set.Make(RefOrd) +module Refmap' = Map.Make(RefOrdered_env) +module Refset' = Set.Make(RefOrdered_env) (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) @@ -71,11 +57,6 @@ let raw_string_of_modfile = function | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) | _ -> assert false -let rec modfile_of_mp = function - | (MPfile _) as mp -> mp - | MPdot (mp,_) -> modfile_of_mp mp - | _ -> raise Not_found - let current_toplevel () = fst (Lib.current_prefix ()) let is_toplevel mp = @@ -109,12 +90,6 @@ let common_prefix_from_list mp0 mpl = | mp :: l -> if MPset.mem mp prefixes then Some mp else f l in f mpl -let rec parse_labels ll = function - | MPdot (mp,l) -> parse_labels (l::ll) mp - | mp -> mp,ll - -let labels_of_mp mp = parse_labels [] mp - let rec parse_labels2 ll mp1 = function | mp when mp1=mp -> mp,ll | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp @@ -125,10 +100,6 @@ let labels_of_ref r = let mp,_,l = repr_of_r r in parse_labels2 [l] mp_top mp -let rec add_labels_mp mp = function - | [] -> mp - | l :: ll -> add_labels_mp (MPdot (mp,l)) ll - (*S The main tables: constants, inductives, records, ... *) @@ -156,6 +127,39 @@ let add_ind kn mib ml_ind = inductives := Mindmap_env.add kn (mib,ml_ind) !inductives let lookup_ind kn = Mindmap_env.find kn !inductives +let inductive_kinds = + ref (Mindmap_env.empty : inductive_kind Mindmap_env.t) +let init_inductive_kinds () = inductive_kinds := Mindmap_env.empty +let add_inductive_kind kn k = + inductive_kinds := Mindmap_env.add kn k !inductive_kinds +let is_coinductive r = + let kn = match r with + | ConstructRef ((kn,_),_) -> kn + | IndRef (kn,_) -> kn + | _ -> assert false + in + try Mindmap_env.find kn !inductive_kinds = Coinductive + with Not_found -> false + +let is_coinductive_type = function + | Tglob (r,_) -> is_coinductive r + | _ -> false + +let get_record_fields r = + let kn = match r with + | ConstructRef ((kn,_),_) -> kn + | IndRef (kn,_) -> kn + | _ -> assert false + in + try match Mindmap_env.find kn !inductive_kinds with + | Record f -> f + | _ -> [] + with Not_found -> [] + +let record_fields_of_type = function + | Tglob (r,_) -> get_record_fields r + | _ -> [] + (*s Recursors table. *) (* NB: here we can use the equivalence between canonical @@ -203,25 +207,51 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms let add_log_axiom r = log_axioms := Refset'.add r !log_axioms -(*s Extraction mode: modular or monolithic *) +let opaques = ref Refset'.empty +let init_opaques () = opaques := Refset'.empty +let add_opaque r = opaques := Refset'.add r !opaques +let remove_opaque r = opaques := Refset'.remove r !opaques + +(*s Extraction modes: modular or monolithic, library or minimal ? + +Nota: + - Recursive Extraction : monolithic, minimal + - Separate Extraction : modular, minimal + - Extraction Library : modular, library +*) let modular_ref = ref false +let library_ref = ref false let set_modular b = modular_ref := b let modular () = !modular_ref +let set_library b = library_ref := b +let library () = !library_ref + (*s Printing. *) (* The following functions work even on objects not in [Global.env ()]. - WARNING: for inductive objects, an extract_inductive must have been - done before. *) - -let safe_basename_of_global = function - | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l - | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename - | ConstructRef ((kn,i),j) -> - (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) - | _ -> assert false + Warning: for inductive objects, this only works if an [extract_inductive] + have been done earlier, otherwise we can only ask the Nametab about + currently visible objects. *) + +let safe_basename_of_global r = + let last_chance r = + try Nametab.basename_of_global r + with Not_found -> + anomaly "Inductive object unknown to extraction and not globally visible" + in + match r with + | ConstRef kn -> id_of_label (con_label kn) + | IndRef (kn,0) -> id_of_label (mind_label kn) + | IndRef (kn,i) -> + (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename + with Not_found -> last_chance r) + | ConstructRef ((kn,i),j) -> + (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) + with Not_found -> last_chance r) + | VarRef _ -> assert false let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) @@ -272,7 +302,28 @@ let warning_axioms () = str "Having invalid logical axiom in the environment when extracting" ++ spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ fnl ()) - end + end; + if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then + msg_warning + (str "Some of these axioms might be due to option -dont-load-proofs.") + +let warning_opaques accessed = + let opaques = Refset'.elements !opaques in + if opaques = [] then () + else + let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in + if accessed then + msg_warning + (str "The extraction is currently set to bypass opacity,\n" ++ + str "the following opaque constant bodies have been accessed :" ++ + lst ++ str "." ++ fnl ()) + else + msg_warning + (str "The extraction now honors the opacity constraints by default,\n" ++ + str "the following opaque constants have been extracted as axioms :" ++ + lst ++ str "." ++ fnl () ++ + str "If necessary, use \"Set Extraction AccessOpaque\" to change this." + ++ fnl ()) let warning_both_mod_and_cst q mp r = msg_warning @@ -386,31 +437,34 @@ let info_file f = (* The objects defined below should survive an arbitrary time, so we register them to coq save/undo mechanism. *) -(*s Extraction AutoInline *) +let my_bool_option name initval = + let flag = ref initval in + let access = fun () -> !flag in + let _ = declare_bool_option + {optsync = true; + optdepr = false; + optname = "Extraction "^name; + optkey = ["Extraction"; name]; + optread = access; + optwrite = (:=) flag } + in + access -let auto_inline_ref = ref false +(*s Extraction AccessOpaque *) -let auto_inline () = !auto_inline_ref +let access_opaque = my_bool_option "AccessOpaque" false -let _ = declare_bool_option - {optsync = true; - optname = "Extraction AutoInline"; - optkey = ["Extraction"; "AutoInline"]; - optread = auto_inline; - optwrite = (:=) auto_inline_ref} +(*s Extraction AutoInline *) + +let auto_inline = my_bool_option "AutoInline" false (*s Extraction TypeExpand *) -let type_expand_ref = ref true +let type_expand = my_bool_option "TypeExpand" true -let type_expand () = !type_expand_ref +(*s Extraction KeepSingleton *) -let _ = declare_bool_option - {optsync = true; - optname = "Extraction TypeExpand"; - optkey = ["Extraction"; "TypeExpand"]; - optread = type_expand; - optwrite = (:=) type_expand_ref} +let keep_singleton = my_bool_option "KeepSingleton" false (*s Extraction Optimize *) @@ -461,6 +515,7 @@ let optims () = !opt_flag_ref let _ = declare_bool_option {optsync = true; + optdepr = false; optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> !int_flag_ref <> 0); @@ -468,6 +523,7 @@ let _ = declare_bool_option let _ = declare_int_option { optsync = true; + optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); @@ -484,7 +540,7 @@ let lang_ref = ref Ocaml let lang () = !lang_ref -let (extr_lang,_) = +let extr_lang : lang -> obj = declare_object {(default_object "Extraction Lang") with cache_function = (fun (_,l) -> lang_ref := l); @@ -516,12 +572,14 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let (inline_extraction,_) = +let inline_extraction : bool * global_reference list -> obj = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); classify_function = (fun o -> Substitute o); + discharge_function = + (fun (_,(b,l)) -> Some (b, List.map pop_global_reference l)); subst_function = (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) } @@ -534,8 +592,7 @@ let _ = declare_summary "Extraction Inline" (* Grammar entries. *) let extraction_inline b l = - check_inside_section (); - let refs = List.map Nametab.global l in + let refs = List.map Smartlocate.global_with_alias l in List.iter (fun r -> match r with | ConstRef _ -> () @@ -559,7 +616,7 @@ let print_extraction_inline () = (* Reset part *) -let (reset_inline,_) = +let reset_inline : unit -> obj = declare_object {(default_object "Reset Extraction Inline") with cache_function = (fun (_,_)-> inline_table := empty_inline_table); @@ -598,7 +655,7 @@ let add_implicits r l = (* Registration of operations for rollback. *) -let (implicit_extraction,_) = +let implicit_extraction : global_reference * int_or_id list -> obj = declare_object {(default_object "Extraction Implicit") with cache_function = (fun (_,(r,l)) -> add_implicits r l); @@ -616,7 +673,7 @@ let _ = declare_summary "Extraction Implicit" let extraction_implicit r l = check_inside_section (); - Lib.add_anonymous_leaf (implicit_extraction (Nametab.global r,l)) + Lib.add_anonymous_leaf (implicit_extraction (Smartlocate.global_with_alias r,l)) (*s Extraction Blacklist of filenames not to use while extracting *) @@ -658,12 +715,11 @@ let add_blacklist_entries l = (* Registration of operations for rollback. *) -let (blacklist_extraction,_) = +let blacklist_extraction : string list -> obj = declare_object {(default_object "Extraction Blacklist") with cache_function = (fun (_,l) -> add_blacklist_entries l); load_function = (fun _ (_,l) -> add_blacklist_entries l); - classify_function = (fun o -> Libobject.Keep o); subst_function = (fun (_,x) -> x) } @@ -686,7 +742,7 @@ let print_extraction_blacklist () = (* Reset part *) -let (reset_blacklist,_) = +let reset_blacklist : unit -> obj = declare_object {(default_object "Reset Extraction Blacklist") with cache_function = (fun (_,_)-> blacklist_table := Idset.empty); @@ -719,8 +775,10 @@ let add_custom_match r s = let indref_of_match pv = if Array.length pv = 0 then raise Not_found; - match pv.(0) with - | (ConstructRef (ip,_), _, _) -> IndRef ip + let (_,pat,_) = pv.(0) in + match pat with + | Pusual (ConstructRef (ip,_)) -> IndRef ip + | Pcons (ConstructRef (ip,_),_) -> IndRef ip | _ -> raise Not_found let is_custom_match pv = @@ -732,7 +790,7 @@ let find_custom_match pv = (* Registration of operations for rollback. *) -let (in_customs,_) = +let in_customs : global_reference * string list * string -> obj = declare_object {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); @@ -747,7 +805,7 @@ let _ = declare_summary "ML extractions" unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap'.empty) } -let (in_custom_matchs,_) = +let in_custom_matchs : global_reference * string -> obj = declare_object {(default_object "ML extractions custom matchs") with cache_function = (fun (_,(r,s)) -> add_custom_match r s); @@ -765,7 +823,7 @@ let _ = declare_summary "ML extractions custom match" let extract_constant_inline inline r ids s = check_inside_section (); - let g = Nametab.global r in + let g = Smartlocate.global_with_alias r in match g with | ConstRef kn -> let env = Global.env () in @@ -783,7 +841,7 @@ let extract_constant_inline inline r ids s = let extract_inductive r s l optstr = check_inside_section (); - let g = Nametab.global r in + let g = Smartlocate.global_with_alias r in match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in @@ -805,5 +863,6 @@ let extract_inductive r s l optstr = (*s Tables synchronization. *) let reset_tables () = - init_terms (); init_types (); init_inductives (); init_recursors (); - init_projs (); init_axioms (); reset_modfile () + init_terms (); init_types (); init_inductives (); + init_inductive_kinds (); init_recursors (); + init_projs (); init_axioms (); init_opaques (); reset_modfile () diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index b70d3efa..a3b7124e 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* identifier (*s Warning and Error messages. *) val warning_axioms : unit -> unit +val warning_opaques : bool -> unit val warning_both_mod_and_cst : qualid -> module_path -> global_reference -> unit val warning_id : string -> unit @@ -59,10 +58,8 @@ val at_toplevel : module_path -> bool val visible_con : constant -> bool val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t -val modfile_of_mp : module_path -> module_path val common_prefix_from_list : module_path -> module_path list -> module_path option -val add_labels_mp : module_path -> label list -> module_path val get_nth_label_mp : int -> module_path -> label val labels_of_ref : global_reference -> module_path * label list @@ -77,6 +74,14 @@ val lookup_type : constant -> ml_schema val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind +val add_inductive_kind : mutual_inductive -> inductive_kind -> unit +val is_coinductive : global_reference -> bool +val is_coinductive_type : ml_type -> bool +(* What are the fields of a record (empty for a non-record) *) +val get_record_fields : + global_reference -> global_reference option list +val record_fields_of_type : ml_type -> global_reference option list + val add_recursors : Environ.env -> mutual_inductive -> unit val is_recursor : global_reference -> bool @@ -88,8 +93,15 @@ val add_info_axiom : global_reference -> unit val remove_info_axiom : global_reference -> unit val add_log_axiom : global_reference -> unit +val add_opaque : global_reference -> unit +val remove_opaque : global_reference -> unit + val reset_tables : unit -> unit +(*s AccessOpaque parameter *) + +val access_opaque : unit -> bool + (*s AutoInline parameter *) val auto_inline : unit -> bool @@ -98,6 +110,10 @@ val auto_inline : unit -> bool val type_expand : unit -> bool +(*s KeepSingleton parameter *) + +val keep_singleton : unit -> bool + (*s Optimize parameter *) type opt_flag = @@ -120,11 +136,20 @@ val optims : unit -> opt_flag type lang = Ocaml | Haskell | Scheme val lang : unit -> lang -(*s Extraction mode: modular or monolithic *) +(*s Extraction modes: modular or monolithic, library or minimal ? + +Nota: + - Recursive Extraction : monolithic, minimal + - Separate Extraction : modular, minimal + - Extraction Library : modular, library +*) val set_modular : bool -> unit val modular : unit -> bool +val set_library : bool -> unit +val library : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool @@ -158,6 +183,7 @@ val extract_constant_inline : val extract_inductive : reference -> string -> string list -> string option -> unit + type int_or_id = ArgInt of int | ArgId of identifier val extraction_implicit : reference -> int_or_id list -> unit -- cgit v1.2.3