diff options
31 files changed, 589 insertions, 395 deletions
@@ -15,6 +15,12 @@ Program Changes from V8.5beta3 ====================== +Vernacular commands +- Flag -compat 8.4 now loads Coq.Compat.Coq84. The standard way of putting Coq + in v8.4 compatibility mode is to pass the command line flag "-compat 8.4". It + can be followed by "-require Coq.Compat.AdmitAxiom" if 8.4 behavior of admit is + needed, in which case it uses an axiom. + Specification language - Syntax "$(tactic)$" changed to "ltac:(tactic)". @@ -22,7 +28,9 @@ Specification language Tactics - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly - for induction. + for induction (rare source of incompatibilities easily solvable by + removing parentheses around "hyp" when not for the purpose of keeping + the hypothesis). - Syntax "p/c" for on-the-fly application of a lemma c before introducing along pattern p changed to p%c1..%cn. The feature and syntax are in experimental stage. diff --git a/INSTALL.ide b/INSTALL.ide index b651e77db..6e41b2d05 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -39,7 +39,7 @@ COMPILATION REQUIREMENTS install GTK+ 2.x, should you need to force it for one reason or another.) - The OCaml bindings for GTK+ 2.x, lablgtk2 with support for gtksourceview2. - You need at least version 2.16. + You need at least version 2.14.2. Your distribution may contain precompiled packages. For example, for Debian, run diff --git a/configure.ml b/configure.ml index b8bb650b1..47721f778 100644 --- a/configure.ml +++ b/configure.ml @@ -670,18 +670,10 @@ let operating_system, osdeplibs = (** * lablgtk2 and CoqIDE *) -type source = Manual | OCamlFind | Stdlib - -let get_source = function -| Manual -> "manually provided" -| OCamlFind -> "via ocamlfind" -| Stdlib -> "in OCaml library" - (** Is some location a suitable LablGtk2 installation ? *) -let check_lablgtkdir ?(fatal=false) src dir = +let check_lablgtkdir ?(fatal=false) msg dir = let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in - let msg = get_source src in if not (dir_exists dir) then yell (sprintf "No such directory '%s' (%s)." dir msg) else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then @@ -695,11 +687,11 @@ let check_lablgtkdir ?(fatal=false) src dir = let get_lablgtkdir () = match !Prefs.lablgtkdir with | Some dir -> - let msg = Manual in + let msg = "manually provided" in if check_lablgtkdir ~fatal:true msg dir then dir, msg - else "", msg + else "", "" | None -> - let msg = OCamlFind in + let msg = "via ocamlfind" in let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in if d1 <> "" && check_lablgtkdir msg d1 then d1, msg else @@ -707,34 +699,10 @@ let get_lablgtkdir () = let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg else - let msg = Stdlib in + let msg = "in OCaml library" in let d3 = camllib^"/lablgtk2" in if check_lablgtkdir msg d3 then d3, msg - else "", msg - -(** Detect and/or verify the Lablgtk2 version *) - -let check_lablgtk_version src dir = match src with -| Manual | Stdlib -> - let test accu f = - if accu then - let test = sprintf "grep -q -w %s %S/glib.mli" f dir in - Sys.command test = 0 - else false - in - let heuristics = [ - "convert_with_fallback"; - "wrap_poll_func"; (** Introduced in lablgtk 2.16 *) - ] in - let ans = List.fold_left test true heuristics in - if ans then printf "Warning: could not check the version of lablgtk2.\n"; - (ans, "an unknown version") -| OCamlFind -> - let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in - try - let vi = List.map s2i (numeric_prefix_list v) in - ([2; 16] <= vi, v) - with _ -> (false, v) + else "", "" let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native" @@ -758,9 +726,9 @@ let check_coqide () = if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; let dir, via = get_lablgtkdir () in if dir = "" then set_ide No "LablGtk2 not found"; - let (ok, version) = check_lablgtk_version via dir in - let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in - if not ok then set_ide No (found^", but too old (required >= 2.16, found " ^ version ^ ")"); + let found = sprintf "LablGtk2 found (%s)" via in + let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in + if Sys.command test <> 0 then set_ide No (found^" but too old"); (* We're now sure to produce at least one kind of coqide *) lablgtkdir := shorten_camllib dir; if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 74c8374de..a963662f6 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -198,6 +198,11 @@ this constant is not declared in the generated file. \asubsection{Extra elimination of useless arguments} +The following command provides some extra manual control on the +code elimination performed during extraction, in a way which +is independent but complementary to the main elimination +principles of extraction (logical parts and types). + \begin{description} \item \comindex{Extraction Implicit} {\tt Extraction Implicit} \qualid\ [ \ident$_1$ \dots\ \ident$_n$ ]. @@ -207,12 +212,27 @@ This experimental command allows declaring some arguments of be removed by extraction. Here \qualid\ can be any function or inductive constructor, and \ident$_i$ are the names of the concerned arguments. In fact, an argument can also be referred by a number -indicating its position, starting from 1. When an actual extraction -takes place, an error is raised if the {\tt Extraction Implicit} +indicating its position, starting from 1. +\end{description} + +When an actual extraction takes place, an error is normally raised if the +{\tt Extraction Implicit} declarations cannot be honored, that is if any of the implicited -variables still occurs in the final code. This declaration of useless -arguments is independent but complementary to the main elimination -principles of extraction (logical parts and types). +variables still occurs in the final code. This behavior can be relaxed +via the following option: + +\begin{description} +\item \optindex{Extraction SafeImplicits} {\tt Unset Extraction SafeImplicits.} + +Default is Set. When this option is Unset, a warning is emitted +instead of an error if some implicited variables still occur in the +final code of an extraction. This way, the extracted code may be +obtained nonetheless and reviewed manually to locate the source of the issue +(in the code, some comments mark the location of these remaining +implicited variables). +Note that this extracted code might not compile or run properly, +depending of the use of these remaining implicited variables. + \end{description} \asubsection{Realizing axioms}\label{extraction:axioms} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index e3e49e115..1554ee04d 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -24,7 +24,7 @@ written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as The types of types are {\em sorts}. Types and sorts are themselves terms so that terms, types and sorts are all components of a common syntactic language of terms which is described in -Section~\label{cic:terms} but, first, we describe sorts. +Section~\ref{cic:terms} but, first, we describe sorts. \subsection[Sorts]{Sorts\label{Sorts} \index{Sorts}} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index a718a26ea..f2ab79dce 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -226,6 +226,7 @@ Definition c := {| y := 3; x := 5 |}. This syntax can be disabled globally for printing by \begin{quote} {\tt Unset Printing Records.} +\optindex{Printing Records} \end{quote} For a given type, one can override this using either \begin{quote} @@ -284,6 +285,9 @@ To deactivate the printing of projections, use {\tt Unset Printing Projections}. \subsection{Primitive Projections} +\optindex{Primitive Projections} +\optindex{Printing Primitive Projection Parameters} +\optindex{Printing Primitive Projection Compatibility} \index{Primitive projections} \label{prim-proj} @@ -314,6 +318,12 @@ for the usual defined ones. % - [pattern x at n], [rewrite x at n] and in general abstraction and selection % of occurrences may fail due to the disappearance of parameters. +For compatibility, the parameters still appear to the user when printing terms +even though they are absent in the actual AST manipulated by the kernel. This +can be changed by unsetting the {\tt Printing Primitive Projection Parameters} +flag. Further compatibility printing can be deactivated thanks to the +{\tt Printing Primitive Projection Compatibility} option which governs the +printing of pattern-matching over primitive records. \section{Variants and extensions of {\mbox{\tt match}} \label{Extensions-of-match} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 0e758bcab..fcccd9cb4 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -496,9 +496,8 @@ arguments is used for making explicit the value of implicit arguments The expression ``{\term}~{\tt :}~{\type}'' is a type cast expression. It enforces the type of {\term} to be {\type}. -``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine (as if option -{\tt Virtual Machine} were on, see \ref{SetVirtualMachine}) for checking that -{\term} has type {\type}. +``{\term}~{\tt <:}~{\type}'' locally sets up the virtual machine for checking +that {\term} has type {\type}. \subsection{Inferable subterms \label{hole} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 571e16d57..53aa6b86a 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -126,6 +126,8 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} +\optindex{Case Analysis Schemes} +\optindex{Decidable Equality Schemes} \label{set-nonrecursive-elimination-schemes} } @@ -139,6 +141,10 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. + +In addition, the {\tt Case Analysis Schemes} flag governs the generation of +case analysis lemmas for inductive types, i.e. corresponding to the +pattern-matching term alone and without fixpoint. \\ You can also activate the automatic declaration of those Boolean equalities diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index ea3cca77e..a08cd1475 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -159,6 +159,7 @@ unification can have different unfolding behaviors on the same development with universe polymorphism switched on or off. \asection{Minimization} +\optindex{Universe Minimization ToSet} Universe polymorphism with cumulativity tends to generate many useless inclusion constraints in general. Typically at each application of a @@ -248,7 +249,7 @@ User-named universes are considered rigid for unification and are never minimized. \subsection{\tt Unset Strict Universe Declaration. - \optindex{StrictUniverseDeclaration} + \optindex{Strict Universe Declaration} \label{StrictUniverseDeclaration}} The command \texttt{Unset Strict Universe Declaration} allows one to diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 33de399c0..a8bbdeb37 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -618,6 +618,7 @@ through the <tt>Require Import</tt> command.</p> Compatibility wrappers for previous versions of Coq </dt> <dd> + theories/Compat/AdmitAxiom.v theories/Compat/Coq84.v theories/Compat/Coq85.v </dd> diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index f7279f9cf..152f76cc0 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -28,6 +28,7 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) + | [< >] -> raise Parsing_error and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 0f846013b..7014df83f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -78,56 +78,51 @@ module type VISIT = sig (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) val add_ref : global_reference -> unit + val add_kn : kernel_name -> unit val add_decl_deps : ml_decl -> unit val add_spec_deps : ml_spec -> unit (* Test functions: is a particular object a needed dependency for the current extraction ? *) val needed_ind : mutual_inductive -> bool - val needed_con : constant -> bool + val needed_cst : constant -> bool val needed_mp : module_path -> bool val needed_mp_all : module_path -> bool end module Visit : VISIT = struct type must_visit = - { mutable ind : KNset.t; mutable con : KNset.t; - mutable mp : MPset.t; mutable mp_all : MPset.t } + { mutable kn : 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; mp_all = MPset.empty } + let v = { kn = KNset.empty; mp = MPset.empty; mp_all = MPset.empty } (* the accessor functions *) let reset () = - v.ind <- KNset.empty; - v.con <- KNset.empty; + v.kn <- 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_ind i = KNset.mem (user_mind i) v.kn + let needed_cst c = KNset.mem (user_con c) v.kn 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; + 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) - let add_con c = - let kn = user_con c in - v.con <- KNset.add kn v.con; add_mp (modpath kn) + let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) let add_ref = function - | ConstRef c -> add_con c - | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_ind ind + | ConstRef c -> add_kn (user_con c) + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind) | VarRef _ -> assert false let add_decl_deps = decl_iter_references add_ref add_ref add_ref let add_spec_deps = spec_iter_references add_ref add_ref add_ref end let add_field_label mp = function - | (lab, SFBconst _) -> Visit.add_ref (ConstRef (Constant.make2 mp lab)) - | (lab, SFBmind _) -> Visit.add_ref (IndRef (MutInd.make2 mp lab, 0)) + | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab) | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab)) let rec add_labels mp = function @@ -193,36 +188,44 @@ let rec mp_of_mexpr = function | MEwith (seb,_) -> mp_of_mexpr seb | _ -> assert false +let no_delta = Mod_subst.empty_delta_resolver + let env_for_mtb_with_def env mp me idl = let struc = Modops.destr_nofunctor me in let l = Label.of_id (List.hd idl) in let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in let before = fst (List.split_when spot struc) in - Modops.add_structure mp before empty_delta_resolver env + Modops.add_structure mp before no_delta env + +let make_cst resolver mp l = + Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l) + +let make_mind resolver mp l = + Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l) (* From a [structure_body] (i.e. a list of [structure_field_body]) to specifications. *) -let rec extract_structure_spec env mp = function +let rec extract_structure_spec env mp reso = function | [] -> [] | (l,SFBconst cb) :: msig -> - let kn = Constant.make2 mp l in - let s = extract_constant_spec env kn cb in - let specs = extract_structure_spec env mp msig in + let c = make_cst reso mp l in + let s = extract_constant_spec env c cb in + let specs = extract_structure_spec env mp reso msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let mind = MutInd.make2 mp l in + let mind = make_mind reso mp l in let s = Sind (mind, extract_inductive env mind) in - let specs = extract_structure_spec env mp msig in + let specs = extract_structure_spec env mp reso msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmodule mb) :: msig -> - let specs = extract_structure_spec env mp msig in + let specs = extract_structure_spec env mp reso msig in let spec = extract_mbody_spec env mb.mod_mp mb in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> - let specs = extract_structure_spec env mp msig in + let specs = extract_structure_spec env mp reso msig in let spec = extract_mbody_spec env mtb.mod_mp mtb in (l,Smodtype spec) :: specs @@ -244,7 +247,7 @@ and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with | MEwith(me',WithMod(idl,mp))-> Visit.add_mp_all mp; MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp)) - | MEapply _ -> extract_msignature_spec env mp1 me_struct + | MEapply _ -> extract_msignature_spec env mp1 no_delta (*TODO*) me_struct and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with | MoreFunctor (mbid, mtb, me_alg') -> @@ -258,19 +261,19 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with extract_mexpression_spec env' mp1 (me_struct',me_alg')) | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m) -and extract_msignature_spec env mp1 = function +and extract_msignature_spec env mp1 reso = function | NoFunctor struc -> - let env' = Modops.add_structure mp1 struc empty_delta_resolver env in - MTsig (mp1, extract_structure_spec env' mp1 struc) + let env' = Modops.add_structure mp1 struc reso env in + MTsig (mp1, extract_structure_spec env' mp1 reso struc) | MoreFunctor (mbid, mtb, me) -> let mp = MPbound mbid in let env' = Modops.add_module_type mp mtb env in MTfunsig (mbid, extract_mbody_spec env mp mtb, - extract_msignature_spec env' mp1 me) + extract_msignature_spec env' mp1 reso me) and extract_mbody_spec env mp mb = match mb.mod_type_alg with | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty) - | None -> extract_msignature_spec env mp mb.mod_type + | None -> extract_msignature_spec env mp mb.mod_delta mb.mod_type (* From a [structure_body] (i.e. a list of [structure_field_body]) to implementations. @@ -279,31 +282,31 @@ and extract_mbody_spec env mp mb = match mb.mod_type_alg with important: last to first ensures correct dependencies. *) -let rec extract_structure env mp ~all = function +let rec extract_structure env mp reso ~all = function | [] -> [] | (l,SFBconst cb) :: struc -> (try let vl,recd,struc = factor_fix env l cb struc in - let vc = Array.map (Constant.make2 mp) vl in - let ms = extract_structure env mp ~all struc in - let b = Array.exists Visit.needed_con vc in + let vc = Array.map (make_cst reso mp) vl in + let ms = extract_structure env mp reso ~all struc in + let b = Array.exists Visit.needed_cst vc in if all || b then let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_structure env mp ~all struc in - let c = Constant.make2 mp l in - let b = Visit.needed_con c in + let ms = extract_structure env mp reso ~all struc in + let c = make_cst reso mp l in + let b = Visit.needed_cst c in if all || b then let d = extract_constant env c cb in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) | (l,SFBmind mib) :: struc -> - let ms = extract_structure env mp ~all struc in - let mind = MutInd.make2 mp l in + let ms = extract_structure env mp reso ~all struc in + let mind = make_mind reso mp l in let b = Visit.needed_ind mind in if all || b then let d = Dind (mind, extract_inductive env mind) in @@ -311,14 +314,14 @@ let rec extract_structure env mp ~all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms | (l,SFBmodule mb) :: struc -> - let ms = extract_structure env mp ~all struc in + let ms = extract_structure env mp reso ~all struc in let mp = MPdot (mp,l) in let all' = all || Visit.needed_mp_all mp in if all' || Visit.needed_mp mp then (l,SEmodule (extract_module env mp ~all:all' mb)) :: ms else ms | (l,SFBmodtype mtb) :: struc -> - let ms = extract_structure env mp ~all struc in + let ms = extract_structure env mp reso ~all struc in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms @@ -332,7 +335,7 @@ and extract_mexpr env mp = function (* In Haskell/Scheme, we expand everything. For now, we also extract everything, dead code will be removed later (see [Modutil.optimize_struct]. *) - extract_msignature env mp ~all:true (expand_mexpr env mp me) + extract_msignature env mp no_delta ~all:true (expand_mexpr env mp me) | MEident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp_all mp; Miniml.MEident mp @@ -350,17 +353,17 @@ and extract_mexpression env mp = function extract_mbody_spec env mp1 mtb, extract_mexpression env' mp me) -and extract_msignature env mp ~all = function +and extract_msignature env mp reso ~all = function | NoFunctor struc -> - let env' = Modops.add_structure mp struc empty_delta_resolver env in - Miniml.MEstruct (mp,extract_structure env' mp ~all struc) + let env' = Modops.add_structure mp struc reso env in + Miniml.MEstruct (mp,extract_structure env' mp reso ~all struc) | MoreFunctor (mbid, mtb, me) -> let mp1 = MPbound mbid in let env' = Modops.add_module_type mp1 mtb env in Miniml.MEfunctor (mbid, extract_mbody_spec env mp1 mtb, - extract_msignature env' mp ~all me) + extract_msignature env' mp reso ~all me) and extract_module env mp ~all mb = (* A module has an empty [mod_expr] when : @@ -376,8 +379,8 @@ and extract_module env mp ~all mb = (* This module has a signature, otherwise it would be FullStruct. We extract just the elements required by this signature. *) let () = add_labels mp mb.mod_type in - extract_msignature env mp ~all:false sign - | FullStruct -> extract_msignature env mp ~all mb.mod_type + extract_msignature env mp mb.mod_delta ~all:false sign + | FullStruct -> extract_msignature env mp mb.mod_delta ~all mb.mod_type in (* Slight optimization: for modules without explicit signatures ([FullStruct] case), we build the type out of the extracted @@ -399,7 +402,7 @@ let mono_environment refs mpl = let l = List.rev (environment_until None) in List.rev_map (fun (mp,struc) -> - mp, extract_structure env mp ~all:(Visit.needed_mp_all mp) struc) + mp, extract_structure env mp no_delta ~all:(Visit.needed_mp_all mp) struc) l (**************************************) @@ -455,7 +458,7 @@ let print_one_decl struc mp decl = push_visible mp []; let ans = d.pp_decl decl in pop_visible (); - ans + v 0 ans (*s Extraction of a ml struct to a file. *) @@ -495,8 +498,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let d = descr () in reset_renaming_tables AllButExternal; let unsafe_needs = { - mldummy = struct_ast_search ((==) MLdummy) struc; - tdummy = struct_type_search Mlutil.isDummy struc; + mldummy = struct_ast_search Mlutil.isMLdummy struc; + tdummy = struct_type_search Mlutil.isTdummy struc; tunknown = struct_type_search ((==) Tunknown) struc; magic = if lang () != Haskell then false @@ -650,7 +653,7 @@ let extraction_library is_rec m = let l = List.rev (environment_until (Some dir_m)) in let select l (mp,struc) = if Visit.needed_mp mp - then (mp, extract_structure env mp true struc) :: l + then (mp, extract_structure env mp no_delta true struc) :: l else l in let struc = List.fold_left select [] l in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 1112c3b89..f4d14af62 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -91,7 +91,7 @@ exception NotDefault of kill_reason let check_default env t = match flag_of_type env t with | _,TypeScheme -> raise (NotDefault Ktype) - | Logic,_ -> raise (NotDefault Kother) + | Logic,_ -> raise (NotDefault Kprop) | _ -> () let is_info_scheme env t = match flag_of_type env t with @@ -103,7 +103,7 @@ let is_info_scheme env t = match flag_of_type env t with let rec type_sign env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> - (if is_info_scheme env t then Keep else Kill Kother) + (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] @@ -137,7 +137,7 @@ let rec type_sign_vl env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then Kill Kother::s, vl + if not (is_info_scheme env t) then Kill Kprop::s, vl else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] @@ -154,25 +154,12 @@ let sign_with_implicits r s nb_params = let implicits = implicits_of_global r in let rec add_impl i = function | [] -> [] - | sign::s -> - let sign' = - if sign == Keep && Int.List.mem i implicits - then Kill Kother else sign - in sign' :: add_impl (succ i) s + | Keep::s when Int.Set.mem i implicits -> + Kill (Kimplicit (r,i)) :: add_impl (i+1) s + | sign::s -> sign :: add_impl (i+1) s in add_impl (1+nb_params) s -(* Enriching a exception message *) - -let rec handle_exn r n fn_name = function - | MLexn s -> - (try Scanf.sscanf s "UNBOUND %d%!" - (fun i -> - assert ((0 < i) && (i <= n)); - MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) - with Scanf.Scan_failure _ | End_of_file -> MLexn s) - | a -> ast_map (handle_exn r n fn_name) a - (*S Management of type variable contexts. *) (* A De Bruijn variable context (db) is a context for translating Coq [Rel] @@ -285,10 +272,10 @@ let rec extract_type env db j c args = (match expand env mld with | Tdummy d -> Tdummy d | _ -> - let reason = if lvl == TypeScheme then Ktype else Kother in + let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother + | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop | Rel n -> (match lookup_rel n env with | (_,Some t,_) -> extract_type env db j (lift n t) args @@ -458,7 +445,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if p.ip_logical then raise (I Standard); if not (Int.equal (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 + let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in if not (keep_singleton ()) && Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); @@ -479,7 +466,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let mp = MutInd.modpath kn in let rec select_fields l typs = match l,typs with | [],[] -> [] - | _::l, typ::typs when isDummy (expand env typ) -> + | _::l, typ::typs when isTdummy (expand env typ) -> select_fields l typs | Anonymous::l, typ::typs -> None :: (select_fields l typs) @@ -655,7 +642,7 @@ and extract_maybe_term env mle mlt c = try check_default env (type_of env c); extract_term env mle mlt c [] with NotDefault d -> - put_magic (mlt, Tdummy d) MLdummy + put_magic (mlt, Tdummy d) (MLdummy d) (*s Generic way to deal with an application. *) @@ -723,11 +710,11 @@ and extract_cst_app env mle mlt kn u args = else mla with e when Errors.noncritical e -> mla in - (* For strict languages, purely logical signatures with at least - one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left + (* For strict languages, purely logical signatures lead to a dummy lam + (except when [Kill Ktype] everywhere). So a [MLdummy] is left accordingly. *) let optdummy = match sign_kind s_full with - | UnsafeLogicalSig when lang () != Haskell -> [MLdummy] + | UnsafeLogicalSig when lang () != Haskell -> [MLdummy Kprop] | _ -> [] in (* Different situations depending of the number of arguments: *) @@ -826,8 +813,8 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* Logical singleton case: *) (* [match c with C i j k -> t] becomes [t'] *) assert (Int.equal br_size 1); - let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in - let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in + let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in + let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in let e = extract_maybe_term env mle mlt br.(0) in snd (case_expunge s e) end @@ -851,8 +838,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in (* 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 - (List.rev ids, Pusual r, e') + (List.rev ids, Pusual r, e) in if mi.ind_kind == Singleton then begin @@ -960,8 +946,6 @@ let extract_std_constant env kn body typ = let e = extract_term env mle t' c [] in (* Expunging term and type from dummy lambdas. *) let trm = term_expunge s (ids,e) in - let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm - in trm, type_expunge_from_sign env s t (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) @@ -979,8 +963,8 @@ let extract_axiom env kn typ = let extract_fixpoint env vkn (fi,ti,ci) = let n = Array.length vkn in - let types = Array.make n (Tdummy Kother) - and terms = Array.make n MLdummy in + let types = Array.make n (Tdummy Kprop) + and terms = Array.make n (MLdummy Kprop) in let kns = Array.to_list vkn in current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) @@ -1022,7 +1006,7 @@ let extract_constant env kn cb = 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) + | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () @@ -1047,7 +1031,7 @@ let extract_constant_spec env kn cb = let typ = Typeops.type_of_constant_type env cb.const_type in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) - | (Logic, Default) -> Sval (r, Tdummy Kother) + | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in (match cb.const_body with @@ -1075,8 +1059,8 @@ let extract_constr env c = reset_meta_count (); let typ = type_of env c in match flag_of_type env typ with - | (_,TypeScheme) -> MLdummy, Tdummy Ktype - | (Logic,_) -> MLdummy, Tdummy Kother + | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype + | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> let mlt = extract_type env [] 1 typ [] in extract_term env Mlenv.empty mlt c [], mlt @@ -1090,7 +1074,7 @@ let extract_inductive env kn = | [] -> [] | t::l -> let l' = filter (succ i) l in - if isDummy (expand env t) || Int.List.mem i implicits then l' + if isTdummy (expand env t) || Int.Set.mem i implicits then l' else t::l' in filter (1+ind.ind_nparams) l in @@ -1102,11 +1086,11 @@ let extract_inductive env kn = (*s Is a [ml_decl] logical ? *) let logical_decl = function - | Dterm (_,MLdummy,Tdummy _) -> true + | Dterm (_,MLdummy _,Tdummy _) -> true | Dtype (_,[],Tdummy _) -> true | Dfix (_,av,tv) -> - (Array.for_all ((==) MLdummy) av) && - (Array.for_all isDummy tv) + (Array.for_all isMLdummy av) && + (Array.for_all isTdummy tv) | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 37b414207..00259750d 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -35,56 +35,59 @@ let keywords = let pp_comment s = str "-- " ++ s ++ fnl () let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}" +(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"], + the '\n' character interacts badly with the Format boxing mechanism *) + let preamble mod_name comment used_modules usf = - let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") + let pp_import mp = str ("import qualified "^ string_of_modfile mp) ++ fnl () in (if not (usf.magic || usf.tunknown) then mt () else str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++ - str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}") - ++ fnl () ++ fnl () + str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}" ++ fnl2 ()) ++ (match comment with | None -> mt () - | Some com -> pp_bracket_comment com ++ fnl () ++ fnl ()) + | Some com -> pp_bracket_comment com ++ fnl2 ()) ++ str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++ str "import qualified Prelude" ++ fnl () ++ - prlist pp_import used_modules ++ fnl () ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ + prlist pp_import used_modules ++ fnl () + ++ (if not (usf.magic || usf.tunknown) then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\nimport qualified GHC.Base\ -\nimport qualified GHC.Prim\ -\n#else\ -\n-- HUGS\ -\nimport qualified IOExts\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "import qualified GHC.Base" ++ fnl () ++ + str "import qualified GHC.Prim" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "import qualified IOExts" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.magic then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\nunsafeCoerce :: a -> b\ -\nunsafeCoerce = GHC.Base.unsafeCoerce#\ -\n#else\ -\n-- HUGS\ -\nunsafeCoerce :: a -> b\ -\nunsafeCoerce = IOExts.unsafeCoerce\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "unsafeCoerce :: a -> b" ++ fnl () ++ + str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "unsafeCoerce :: a -> b" ++ fnl () ++ + str "unsafeCoerce = IOExts.unsafeCoerce" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.tunknown then mt () - else str "\ -\n#ifdef __GLASGOW_HASKELL__\ -\ntype Any = GHC.Prim.Any\ -\n#else\ -\n-- HUGS\ -\ntype Any = ()\ -\n#endif" ++ fnl2 ()) + else + str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++ + str "type Any = GHC.Prim.Any" ++ fnl () ++ + str "#else" ++ fnl () ++ + str "-- HUGS" ++ fnl () ++ + str "type Any = ()" ++ fnl () ++ + str "#endif" ++ fnl2 ()) ++ (if not usf.mldummy then mt () - else str "__ :: any" ++ fnl () ++ - str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) + else + str "__ :: any" ++ fnl () ++ + str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) let pp_abst = function | [] -> (mt ()) @@ -120,7 +123,7 @@ let rec pp_type par vl t = (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy _ -> str "()" | Tunknown -> str "Any" - | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" + | Taxiom -> str "() -- AXIOM TO BE REALIZED" ++ fnl () in hov 0 (pp_rec par t) @@ -200,8 +203,11 @@ let rec pp_expr par env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "Prelude.error" ++ spc () ++ qs s) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ pp_bracket_comment (str s)) | MLmagic a -> pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") @@ -320,7 +326,7 @@ let pp_decl = function prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s with Not_found -> prlist (fun id -> pr_id id ++ str " ") l ++ - if t == Taxiom then str "= () -- AXIOM TO BE REALIZED\n" + if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () else str "=" ++ spc () ++ pp_type false l t in hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () @@ -331,7 +337,8 @@ let pp_decl = function prvecti (fun i r -> let void = is_inline_custom r || - (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom r) && + match defs.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then mt () else diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 125dc86b8..df79c585e 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -153,7 +153,7 @@ let rec json_expr env = function ("what", json_str "expr:exception"); ("msg", json_str s) ] - | MLdummy -> json_dict [("what", json_str "expr:dummy")] + | MLdummy _ -> json_dict [("what", json_str "expr:dummy")] | MLmagic a -> json_dict [ ("what", json_str "expr:coerce"); ("value", json_expr env a) diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index b7dee6cb1..681dceaa0 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -16,11 +16,16 @@ open Globnames object expects, and what these arguments will become in the ML object. *) -(* We eliminate from terms: 1) types 2) logical parts. - [Kother] stands both for logical or other reasons - (for instance user-declared implicit arguments w.r.t. extraction). *) +(* We eliminate from terms: + 1) types + 2) logical parts + 3) user-declared implicit arguments of a constant of constructor +*) -type kill_reason = Ktype | Kother +type kill_reason = + | Ktype + | Kprop + | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -118,7 +123,7 @@ and ml_ast = | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array | MLexn of string - | MLdummy + | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 6fc1195fb..bfd0794de 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -299,10 +299,12 @@ let type_to_signature env t = let isKill = function Kill _ -> true | _ -> false -let isDummy = function Tdummy _ -> true | _ -> false +let isTdummy = function Tdummy _ -> true | _ -> false + +let isMLdummy = function MLdummy _ -> true | _ -> false let sign_of_id = function - | Dummy -> Kill Kother + | Dummy -> Kill Kprop | _ -> Keep (* Classification of signatures *) @@ -310,45 +312,44 @@ let sign_of_id = function type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) let rec sign_kind = function | [] -> EmptySig | Keep :: _ -> NonLogicalSig | Kill k :: s -> - match sign_kind s with - | NonLogicalSig -> NonLogicalSig - | UnsafeLogicalSig -> UnsafeLogicalSig - | SafeLogicalSig | EmptySig -> - if k == Kother then UnsafeLogicalSig else SafeLogicalSig + match k, sign_kind s with + | _, NonLogicalSig -> NonLogicalSig + | Ktype, (SafeLogicalSig | EmptySig) -> SafeLogicalSig + | _, _ -> UnsafeLogicalSig (* Removing the final [Keep] in a signature *) let rec sign_no_final_keeps = function | [] -> [] | k :: s -> - let s' = k :: sign_no_final_keeps s in - match s' with [Keep] -> [] | _ -> s' + match k, sign_no_final_keeps s with + | Keep, [] -> [] + | k, l -> k::l (*s Removing [Tdummy] from the top level of a ML type. *) let type_expunge_from_sign env s t = - let rec expunge s t = - if List.is_empty s then t else match t with - | Tmeta {contents = Some t} -> expunge s t - | Tarr (a,b) -> - let t = expunge (List.tl s) b in - if List.hd s == Keep then Tarr (a, t) else t - | Tglob (r,l) -> - (match env r with - | Some mlt -> expunge s (type_subst_list l mlt) - | None -> assert false) - | _ -> assert false + let rec expunge s t = match s, t with + | [], _ -> t + | Keep :: s, Tarr(a,b) -> Tarr (a, expunge s b) + | Kill _ :: s, Tarr(a,b) -> expunge s b + | _, Tmeta {contents = Some t} -> expunge s t + | _, Tglob (r,l) -> + (match env r with + | Some mlt -> expunge s (type_subst_list l mlt) + | None -> assert false) + | _ -> assert false in let t = expunge (sign_no_final_keeps s) t in if lang () != Haskell && sign_kind s == UnsafeLogicalSig then - Tarr (Tdummy Kother, t) + Tarr (Tdummy Kprop, t) else t let type_expunge env t = @@ -385,7 +386,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLfix (i1, id1, t1), MLfix (i2, id2, t2) -> Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2 | MLexn e1, MLexn e2 -> String.equal e1 e2 -| MLdummy, MLdummy -> true +| MLdummy k1, MLdummy k2 -> k1 == k2 | MLaxiom, MLaxiom -> true | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | _ -> false @@ -420,7 +421,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () in iter 0 (*s Map over asts. *) @@ -439,7 +440,7 @@ let ast_map f = function | 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 + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -457,7 +458,7 @@ let ast_map_lift f n = function | 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 + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a (*s Iter over asts. *) @@ -471,7 +472,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) @@ -507,7 +508,7 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) 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 + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0 in nb 1 (*s Lifting on terms. @@ -559,7 +560,7 @@ let gen_subst v d t = if i' < 1 then a else if i' <= Array.length v then match v.(i'-1) with - | None -> MLexn ("UNBOUND " ^ string_of_int i') + | None -> assert false | Some u -> ast_lift n u else MLrel (i+d) | a -> ast_map_lift subst n a @@ -813,8 +814,8 @@ let census_add, census_max, census_clean = try h := add k i !h with Not_found -> h := (k, Int.Set.singleton i) :: !h in - let maxf k = - let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in + let maxf () = + let len = ref 0 and lst = ref Int.Set.empty and elm = ref MLaxiom in List.iter (fun (e, s) -> let n = Int.Set.cardinal s in @@ -843,7 +844,7 @@ let factor_branches o typ br = 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 + let br_factor, br_set = census_max () in census_clean (); let n = Int.Set.cardinal br_set in if Int.equal n 0 then None @@ -926,7 +927,7 @@ let iota_gen br hd = in iota 0 hd let is_atomic = function - | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ -> true | _ -> false let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false @@ -986,6 +987,10 @@ and simpl_app o a = function | _ -> let a' = List.map (ast_lift 1) (List.tl a) in simpl o (MLletin (id, List.hd a, MLapp (t, a')))) + | MLmagic (MLlam (id,t)) -> + (* When we've at least one argument, we permute the magic + and the lambda, to simplify things a bit (see #2795) *) + simpl_app o a (MLlam (id,MLmagic t)) | 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))) @@ -998,7 +1003,7 @@ and simpl_app o a = function let a' = List.map (ast_lift k) a in (l, p, simpl o (MLapp (t,a')))) br in simpl o (MLcase (typ,e,br')) - | (MLdummy | MLexn _) as e -> e + | (MLdummy _ | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) @@ -1049,20 +1054,26 @@ let rec select_via_bl l args = match l,args with (*s [kill_some_lams] removes some head lambdas according to the signature [bl]. This list is build on the identifier list model: outermost lambda is on the right. - [Rels] corresponding to removed lambdas are supposed not to occur, and + [Rels] corresponding to removed lambdas are not supposed to occur + (except maybe in the case of Kimplicit), and the other [Rels] are made correct via a [gen_subst]. Output is not directly a [ml_ast], compose with [named_lams] if needed. *) +let is_impl_kill = function Kill (Kimplicit _) -> true | _ -> false + let kill_some_lams bl (ids,c) = let n = List.length bl in let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in if Int.equal n n' then ids,c - else if Int.equal n' 0 then [],ast_lift (-n) c + else if Int.equal n' 0 && not (List.exists is_impl_kill bl) + then [],ast_lift (-n) c else begin let v = Array.make n None in let rec parse_ids i j = function | [] -> () | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l + | Kill (Kimplicit _ as k) :: l -> + v.(i) <- Some (MLdummy k); parse_ids (i+1) j l | Kill _ :: l -> parse_ids (i+1) j l in parse_ids 0 1 bl; select_via_bl bl ids, gen_subst v (n'-n) c @@ -1070,11 +1081,19 @@ let kill_some_lams bl (ids,c) = (*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or - if there is no lambda left at all. *) + if there is no lambda left at all. In addition, it now accepts a signature + that may mention some implicits. *) -let kill_dummy_lams c = +let rec merge_implicits ids s = match ids, s with + | [],_ -> [] + | _,[] -> List.map sign_of_id ids + | Dummy::ids, _::s -> Kill Kprop :: merge_implicits ids s + | _::ids, (Kill (Kimplicit _) as k)::s -> k :: merge_implicits ids s + | _::ids, _::s -> Keep :: merge_implicits ids s + +let kill_dummy_lams sign c = let ids,c = collect_lams c in - let bl = List.map sign_of_id ids in + let bl = merge_implicits ids (List.rev sign) in if not (List.memq Keep bl) then raise Impossible; let rec fst_kill n = function | [] -> raise Impossible @@ -1086,7 +1105,7 @@ let kill_dummy_lams c = let _, bl = List.chop skip bl in let c = named_lams ids_skip c in let ids',c = kill_some_lams bl (ids,c) in - ids, named_lams ids' c + (ids,bl), named_lams ids' c (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] and a signature [s] and builds a eta-long version. *) @@ -1100,12 +1119,12 @@ let eta_expansion_sign s (ids,c) = let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels in ids, MLapp (ast_lift (i-1) c, a) | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l - | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l + | Kill k :: l -> abs (Dummy :: ids) (MLdummy k :: rels) (i+1) l in abs ids [] 1 s (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas - corresponding to [Del] in [s]. *) + corresponding to [Kill _] in [s]. *) let case_expunge s e = let m = List.length s in @@ -1123,17 +1142,18 @@ let term_expunge s (ids,c) = if List.is_empty s then c else let ids,c = kill_some_lams (List.rev s) (ids,c) in - if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then - MLlam (Dummy, ast_lift 1 c) + if List.is_empty ids && lang () != Haskell && + sign_kind s == UnsafeLogicalSig + then MLlam (Dummy, ast_lift 1 c) else named_lams ids c -(*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and - purge the args of [MLrel r] corresponding to a [dummy_name]. +(*s [kill_dummy_args (ids,bl) r t] looks for occurrences of [MLrel r] in [t] + and purge the args of [MLrel r] corresponding to a [Kill] in [bl]. It makes eta-expansion if needed. *) -let kill_dummy_args ids r t = +let kill_dummy_args (ids,bl) r t = let m = List.length ids in - let bl = List.rev_map sign_of_id ids in + let sign = List.rev bl in let rec found n = function | MLrel r' when Int.equal r' (r + n) -> true | MLmagic e -> found n e @@ -1144,41 +1164,46 @@ let kill_dummy_args ids r t = let k = max 0 (m - (List.length a)) in let a = List.map (killrec n) a in let a = List.map (ast_lift k) a in - let a = select_via_bl bl (a @ (eta_args k)) in + let a = select_via_bl sign (a @ (eta_args k)) in named_lams (List.firstn k ids) (MLapp (ast_lift k e, a)) | e when found n e -> - let a = select_via_bl bl (eta_args m) in + let a = select_via_bl sign (eta_args m) in named_lams ids (MLapp (ast_lift m e, a)) | e -> ast_map_lift killrec n e in killrec 0 t (*s The main function for local [dummy] elimination. *) +let sign_of_args a = + List.map (function MLdummy k -> Kill k | _ -> Keep) a + let rec kill_dummy = function | MLfix(i,fi,c) -> (try - let ids,c = kill_dummy_fix i c in - ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1)) + let k,c = kill_dummy_fix i c [] in + ast_subst (MLfix (i,fi,c)) (kill_dummy_args k 1 (MLrel 1)) with Impossible -> MLfix (i,fi,Array.map kill_dummy c)) | MLapp (MLfix (i,fi,c),a) -> let a = List.map kill_dummy a in + (* Heuristics: if some arguments are implicit args, we try to + eliminate the corresponding arguments of the fixpoint *) (try - let ids,c = kill_dummy_fix i c in + let k,c = kill_dummy_fix i c (sign_of_args a) in let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in - let fake' = kill_dummy_args ids 1 fake in + let fake' = kill_dummy_args k 1 fake in ast_subst (MLfix (i,fi,c)) fake' with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a)) | MLletin(id, MLfix (i,fi,c),e) -> (try - let ids,c = kill_dummy_fix i c in - let e = kill_dummy (kill_dummy_args ids 1 e) in + let k,c = kill_dummy_fix i c [] in + let e = kill_dummy (kill_dummy_args k 1 e) in MLletin(id, MLfix(i,fi,c),e) with Impossible -> MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e)) | MLletin(id,c,e) -> (try - let ids,c = kill_dummy_lams (kill_dummy_hd c) in - let e = kill_dummy (kill_dummy_args ids 1 e) in + let k,c = kill_dummy_lams [] (kill_dummy_hd c) in + let e = kill_dummy (kill_dummy_args k 1 e) in let c = kill_dummy c in if is_atomic c then ast_subst c e else MLletin (id, c, e) with Impossible -> MLletin(id,kill_dummy c,kill_dummy e)) @@ -1190,21 +1215,21 @@ and kill_dummy_hd = function | MLlam(id,e) -> MLlam(id, kill_dummy_hd e) | MLletin(id,c,e) -> (try - let ids,c = kill_dummy_lams (kill_dummy_hd c) in - let e = kill_dummy_hd (kill_dummy_args ids 1 e) in + let k,c = kill_dummy_lams [] (kill_dummy_hd c) in + let e = kill_dummy_hd (kill_dummy_args k 1 e) in let c = kill_dummy c in if is_atomic c then ast_subst c e else MLletin (id, c, e) with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e)) | a -> a -and kill_dummy_fix i c = +and kill_dummy_fix i c s = let n = Array.length c in - let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in + let k,ci = kill_dummy_lams s (kill_dummy_hd c.(i)) in let c = Array.copy c in c.(i) <- ci; for j = 0 to (n-1) do - c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j)) + c.(j) <- kill_dummy (kill_dummy_args k (n-i) c.(j)) done; - ids,c + k,c (*s Putting things together. *) @@ -1267,7 +1292,7 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 0a71d2c83..c380dfb3e 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type val eq_ml_type : ml_type -> ml_type -> bool -val isDummy : ml_type -> bool +val isTdummy : ml_type -> bool +val isMLdummy : ml_ast -> bool val isKill : sign -> bool val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast @@ -125,8 +126,8 @@ exception Impossible type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) val sign_kind : signature -> sign_kind diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8158ac647..e8383bda5 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -100,7 +100,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy | MLaxiom | MLmagic _ -> () + | MLdummy _ | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = @@ -387,16 +387,15 @@ let is_prefix pre s = in is_prefix_aux 0 -let check_implicits = function - | MLexn s -> - if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then - begin - if is_prefix "UNBOUND" s then assert false; - if is_prefix "IMPLICIT" s then - error_non_implicit (String.sub s 9 (String.length s - 9)); - end; - false - | _ -> false +exception RemainingImplicit of kill_reason + +let check_for_remaining_implicits struc = + let check = function + | MLdummy (Kimplicit _ as k) -> raise (RemainingImplicit k) + | _ -> false + in + try ignore (struct_ast_search check struc) + with RemainingImplicit k -> err_or_warn_remaining_implicit k let optimize_struct to_appear struc = let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in @@ -404,12 +403,16 @@ let optimize_struct to_appear struc = List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) struc in - ignore (struct_ast_search check_implicits opt_struc); - if library () then - List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc - else begin - reset_needed (); - List.iter add_needed (fst to_appear); - List.iter add_needed_mp (snd to_appear); - depcheck_struct opt_struc - end + let mini_struc = + if library () then + List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc + else + begin + reset_needed (); + List.iter add_needed (fst to_appear); + List.iter add_needed_mp (snd to_appear); + depcheck_struct opt_struc + end + in + let () = check_for_remaining_implicits mini_struc in + mini_struc diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 8c482b4b1..6ff4c25ec 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -55,29 +55,36 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Id.Set.empty -let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") +(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"], + the '\n' character interacts badly with the Format boxing mechanism *) + +let pp_open mp = str ("open "^ string_of_modfile mp) ++ fnl () let pp_comment s = str "(* " ++ hov 0 s ++ str " *)" let pp_header_comment = function | None -> mt () - | Some com -> pp_comment com ++ fnl () ++ fnl () + | Some com -> pp_comment com ++ fnl2 () + +let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl () + +let pp_tdummy usf = + if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt () + +let pp_mldummy usf = + if usf.mldummy then + str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl () + else mt () let preamble _ comment used_modules usf = pp_header_comment comment ++ - prlist pp_open used_modules ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ - (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++ - (if usf.mldummy then - str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n" - else mt ()) ++ - (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ()) + then_nl (prlist pp_open used_modules) ++ + then_nl (pp_tdummy usf ++ pp_mldummy usf) let sig_preamble _ comment used_modules usf = - pp_header_comment comment ++ fnl () ++ fnl () ++ - prlist pp_open used_modules ++ - (if List.is_empty used_modules then mt () else fnl ()) ++ - (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt()) + pp_header_comment comment ++ + then_nl (prlist pp_open used_modules) ++ + then_nl (pp_tdummy usf) (*s The pretty-printer for Ocaml syntax*) @@ -199,8 +206,11 @@ let rec pp_expr par env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)")) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ str ("(* "^s^" *)")) | MLmagic a -> pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) | MLaxiom -> @@ -352,7 +362,7 @@ and pp_function env t = | MLcase(Tglob(r,_),MLrel 1,pv) when not (is_coinductive r) && List.is_empty (get_record_fields r) && not (is_custom_match pv) -> - if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then + if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ v 0 (pp_pat env' pv) @@ -378,9 +388,14 @@ and pp_fix par env i (ids,bl) args = fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) +(* Ad-hoc double-newline in v boxes, with enough negative whitespace + to avoid indenting the intermediate blank line *) + +let cut2 () = brk (0,-100000) ++ brk (0,0) + let pp_val e typ = hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ - str " **)") ++ fnl2 () + str " **)") ++ cut2 () (*s Pretty-printing of [Dfix] *) @@ -389,11 +404,11 @@ let pp_Dfix (rv,c,t) = (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv in let rec pp init i = - if i >= Array.length rv then - (if init then failwith "empty phrase" else mt ()) + if i >= Array.length rv then mt () else let void = is_inline_custom rv.(i) || - (not (is_custom rv.(i)) && match c.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom rv.(i)) && + match c.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then pp init (i+1) else @@ -401,7 +416,7 @@ let pp_Dfix (rv,c,t) = if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) else pp_function (empty_env ()) c.(i) in - (if init then mt () else fnl2 ()) ++ + (if init then mt () else cut2 ()) ++ pp_val names.(i) t.(i) ++ str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ pp false (i+1) @@ -466,8 +481,8 @@ let pp_coind pl name = let pp_ind co kn ind = let prefix = if co then "__" else "" in - let some = ref false in - let init= ref (str "type ") in + let initkwd = str "type " in + let nextkwd = fnl () ++ str "and " in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else pp_global Type (IndRef (kn,i))) @@ -480,29 +495,20 @@ let pp_ind co kn ind = p.ip_types) ind.ind_packets in - let rec pp i = + let rec pp i kwd = if i >= Array.length ind.ind_packets then mt () else 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) - else begin - some := true; - if p.ip_logical then pp_logical_ind p ++ pp (i+1) - else - let s = !init in - begin - init := (fnl () ++ str "and "); - s ++ - (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ - pp_one_ind - prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ - pp (i+1) - end - end + if is_custom (IndRef ip) then pp (i+1) kwd + else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd + else + kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ + pp_one_ind prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ + pp (i+1) nextkwd in - let st = pp 0 in if !some then st else failwith "empty phrase" + pp 0 initkwd (*s Pretty-printing of a declaration. *) @@ -515,8 +521,8 @@ let pp_mind kn i = | Standard -> pp_ind false kn i let pp_decl = function - | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase" - | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dtype (r,_,_) when is_inline_custom r -> mt () + | Dterm (r,_,_) when is_inline_custom r -> mt () | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> let name = pp_global Type r in @@ -524,13 +530,13 @@ let pp_decl = function let ids, def = try let ids,s = find_type_custom r in - pp_string_parameters ids, str "=" ++ spc () ++ str s + pp_string_parameters ids, str " =" ++ spc () ++ str s with Not_found -> pp_parameters l, - if t == Taxiom then str "(* AXIOM TO BE REALIZED *)" - else str "=" ++ spc () ++ pp_type false l t + if t == Taxiom then str " (* AXIOM TO BE REALIZED *)" + else str " =" ++ spc () ++ pp_type false l t in - hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + hov 2 (str "type " ++ ids ++ name ++ def) | Dterm (r, a, t) -> let def = if is_custom r then str (" = " ^ find_custom r) @@ -564,8 +570,8 @@ let pp_alias_decl ren = function rv let pp_spec = function - | Sval (r,_) when is_inline_custom r -> failwith "empty phrase" - | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Sval (r,_) when is_inline_custom r -> mt () + | Stype (r,_,_) when is_inline_custom r -> mt () | Sind (kn,i) -> pp_mind kn i | Sval (r,t) -> let def = pp_type false [] t in @@ -577,15 +583,15 @@ let pp_spec = function let ids, def = try let ids, s = find_type_custom r in - pp_string_parameters ids, str "= " ++ str s + pp_string_parameters ids, str " =" ++ spc () ++ str s with Not_found -> let ids = pp_parameters l in match ot with | None -> ids, mt () - | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" - | Some t -> ids, str "=" ++ spc () ++ pp_type false l t + | Some Taxiom -> ids, str " (* AXIOM TO BE REALIZED *)" + | Some t -> ids, str " =" ++ spc () ++ pp_type false l t in - hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + hov 2 (str "type " ++ ids ++ name ++ def) let pp_alias_spec ren = function | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } @@ -602,7 +608,7 @@ let rec pp_specif = function | (l,Spec s) -> (try let ren = Common.check_duplicate (top_visible_mp ()) l in - hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++ + hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ pp_alias_spec ren s with Not_found -> pp_spec s) @@ -610,15 +616,15 @@ let rec pp_specif = function let def = pp_module_type [] mt in let def' = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in - hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ + hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') + fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def') with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in - hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in fnl () ++ str ("module type "^ren^" = ") ++ name @@ -635,14 +641,15 @@ and pp_module_type params = function | MTsig (mp, sign) -> push_visible mp params; let try_pp_specif l x = - try pp_specif x :: l with Failure "empty phrase" -> l + let px = pp_specif x in + if Pp.is_empty px then l else px::l in (* We cannot use fold_right here due to side effects in pp_specif *) let l = List.fold_left try_pp_specif [] sign in let l = List.rev l in pop_visible (); - str "sig " ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + str "sig" ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl () ++ str "end" | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in @@ -672,7 +679,7 @@ let rec pp_structure_elem = function | (l,SEdecl d) -> (try let ren = Common.check_duplicate (top_visible_mp ()) l in - hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++ + hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++ fnl () ++ str "end" ++ fnl () ++ pp_alias_decl ren d with Not_found -> pp_decl d) @@ -686,8 +693,8 @@ let rec pp_structure_elem = function let def = pp_module_expr [] m.ml_mod_expr in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 - (str "module " ++ name ++ typ ++ str " = " ++ - (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ + (str "module " ++ name ++ typ ++ str " =" ++ + (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in fnl () ++ str ("module "^ren^" = ") ++ name @@ -695,7 +702,7 @@ let rec pp_structure_elem = function | (l,SEmodtype m) -> let def = pp_module_type [] m in let name = pp_modname (MPdot (top_visible_mp (), l)) in - hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ (try let ren = Common.check_duplicate (top_visible_mp ()) l in fnl () ++ str ("module type "^ren^" = ") ++ name @@ -713,36 +720,42 @@ and pp_module_expr params = function | MEstruct (mp, sel) -> push_visible mp params; let try_pp_structure_elem l x = - try pp_structure_elem x :: l with Failure "empty phrase" -> l + let px = pp_structure_elem x in + if Pp.is_empty px then l else px::l in (* We cannot use fold_right here due to side effects in pp_structure_elem *) let l = List.fold_left try_pp_structure_elem [] sel in let l = List.rev l in pop_visible (); - str "struct " ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ + str "struct" ++ fnl () ++ + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl () ++ str "end" +let rec prlist_sep_nonempty sep f = function + | [] -> mt () + | [h] -> f h + | h::t -> + let e = f h in + let r = prlist_sep_nonempty sep f t in + if Pp.is_empty e then r + else e ++ sep () ++ r + let do_struct f s = - let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt () - in let ppl (mp,sel) = push_visible mp []; - let p = prlist_strict pp sel in + let p = prlist_sep_nonempty cut2 f sel in (* for monolithic extraction, we try to simulate the unavailability of [MPfile] in names by artificially nesting these [MPfile] *) (if modular () then pop_visible ()); p in - let p = prlist_strict ppl s in + let p = prlist_sep_nonempty cut2 ppl s in (if not (modular ()) then repeat (List.length s) pop_visible ()); - p + v 0 p ++ fnl () let pp_struct s = do_struct pp_structure_elem s let pp_signature s = do_struct pp_specif s -let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt () - let ocaml_descr = { keywords = keywords; file_suffix = ".ml"; @@ -754,5 +767,3 @@ let ocaml_descr = { pp_sig = pp_signature; pp_decl = pp_decl; } - - diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index cc8b6d8e7..0b2a04d3f 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -126,7 +126,7 @@ let rec pp_expr env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) paren (str "error" ++ spc () ++ qs s) - | MLdummy -> + | MLdummy _ -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> pp_expr env args a @@ -183,7 +183,8 @@ let pp_decl = function prvecti (fun i r -> let void = is_inline_custom r || - (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false) + (not (is_custom r) && + match defs.(i) with MLexn "UNUSED" -> true | _ -> false) in if void then mt () else diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a57c39eef..63d792e36 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -401,16 +401,34 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let msg_non_implicit r n id = - let name = match id with - | Anonymous -> "" - | Name id -> "(" ^ Id.to_string id ^ ") " - in - "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) - -let error_non_implicit msg = - err (str (msg ^ " still occurs after extraction.") ++ - fnl () ++ str "Please check the Extraction Implicit declarations.") +let argnames_of_global r = + let typ = Global.type_of_global_unsafe r in + let rels,_ = + decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + List.rev_map fst rels + +let msg_of_implicit = function + | Kimplicit (r,i) -> + let name = match List.nth (argnames_of_global r) (i-1) with + | Anonymous -> "" + | Name id -> "(" ^ Id.to_string id ^ ") " + in + (String.ordinal i)^" argument "^name^"of "^(string_of_global r) + | Ktype | Kprop -> "" + +let error_remaining_implicit k = + let s = msg_of_implicit k in + err (str ("An implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Please check your Extraction Implicit declarations." ++ fnl() ++ + str "You might also try Unset Extraction SafeImplicits to force" ++ + fnl() ++ str "the extraction of unsafe code and review it manually.") + +let warning_remaining_implicit k = + let s = msg_of_implicit k in + msg_warning + (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl () + ++ str "but this code is potentially unsafe, please review it manually.") let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> @@ -635,32 +653,39 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) (*s Extraction Implicit *) +let safe_implicit = my_bool_option "SafeImplicits" true + +let err_or_warn_remaining_implicit k = + if safe_implicit () then + error_remaining_implicit k + else + warning_remaining_implicit k + type int_or_id = ArgInt of int | ArgId of Id.t let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit" let implicits_of_global r = - try Refmap'.find r !implicits_table with Not_found -> [] + try Refmap'.find r !implicits_table with Not_found -> Int.Set.empty let add_implicits r l = - let typ = Global.type_of_global_unsafe r in - let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in - let names = List.rev_map fst rels in + let names = argnames_of_global r in let n = List.length names in - let check = function + let add_arg s = function | ArgInt i -> - if 1 <= i && i <= n then i + if 1 <= i && i <= n then Int.Set.add i s else err (int i ++ str " is not a valid argument number for " ++ safe_pr_global r) | ArgId id -> - (try List.index Name.equal (Name id) names - with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ - safe_pr_global r)) + try + let i = List.index Name.equal (Name id) names in + Int.Set.add i s + with Not_found -> + err (str "No argument " ++ pr_id id ++ str " for " ++ + safe_pr_global r) in - let l' = List.map check l in - implicits_table := Refmap'.add r l' !implicits_table + let ints = List.fold_left add_arg Int.Set.empty l in + implicits_table := Refmap'.add r ints !implicits_table (* Registration of operations for rollback. *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 648f23211..a6734dae8 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -38,8 +38,8 @@ val error_MPfile_as_mod : module_path -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -val msg_non_implicit : global_reference -> int -> Name.t -> string -val error_non_implicit : string -> 'a +val msg_of_implicit : kill_reason -> string +val err_or_warn_remaining_implicit : kill_reason -> unit val info_file : string -> unit @@ -166,7 +166,7 @@ val to_keep : global_reference -> bool (*s Table for implicits arguments *) -val implicits_of_global : global_reference -> int list +val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aeb2445d1..fe26dcd28 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1286,10 +1286,16 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | l -> evd let occur_evar_upto_types sigma n c = + let seen = ref Evar.Set.empty in let rec occur_rec c = match kind_of_term c with | Evar (sp,_) when Evar.equal sp n -> raise Occur - | Evar e -> Option.iter occur_rec (existential_opt_value sigma e); - occur_rec (existential_type sigma e) + | Evar (sp,args as e) -> + if Evar.Set.mem sp !seen then + Array.iter occur_rec args + else ( + seen := Evar.Set.add sp !seen; + Option.iter occur_rec (existential_opt_value sigma e); + occur_rec (existential_type sigma e)) | _ -> iter_constr occur_rec c in try occur_rec c; false with Occur -> true diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 31706b3d0..24c0c4749 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -341,7 +341,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) - let ctx_body = restrict_universe_context ctx used_univs_body in + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx_body = restrict_universe_context ctx used_univs in (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v new file mode 100644 index 000000000..9895548c1 --- /dev/null +++ b/test-suite/bugs/closed/4363.v @@ -0,0 +1,9 @@ +Set Printing Universes. +Definition foo : Type. +Proof. + assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat). + exact bar. +Defined. (* Toplevel input, characters 0-8: +Error: +The term "(fun _ : Set => bar) foo_subproof" has type +"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *) diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v new file mode 100644 index 000000000..dfdeff82f --- /dev/null +++ b/test-suite/success/extraction_impl.v @@ -0,0 +1,82 @@ + +(** Examples of extraction with manually-declared implicit arguments *) + +(** NB: we should someday check the produced code instead of + simply running the commands. *) + +(** Bug #4243, part 1 *) + +Inductive dnat : nat -> Type := +| d0 : dnat 0 +| ds : forall n m, n = m -> dnat n -> dnat (S n). + +Extraction Implicit ds [m]. + +Lemma dnat_nat: forall n, dnat n -> nat. +Proof. + intros n d. + induction d as [| n m Heq d IHn]. + exact 0. exact (S IHn). +Defined. + +Recursive Extraction dnat_nat. + +Extraction Implicit dnat_nat [n]. +Recursive Extraction dnat_nat. + +(** Same, with a Fixpoint *) + +Fixpoint dnat_nat' n (d:dnat n) := + match d with + | d0 => 0 + | ds n m _ d => S (dnat_nat' n d) + end. + +Recursive Extraction dnat_nat'. + +Extraction Implicit dnat_nat' [n]. +Recursive Extraction dnat_nat'. + +(** Bug #4243, part 2 *) + +Inductive enat: nat -> Type := + e0: enat 0 +| es: forall n, enat n -> enat (S n). + +Lemma enat_nat: forall n, enat n -> nat. +Proof. + intros n e. + induction e as [| n e IHe]. + exact (O). + exact (S IHe). +Defined. + +Extraction Implicit es [n]. +Extraction Implicit enat_nat [n]. +Recursive Extraction enat_nat. + +(** Same, with a Fixpoint *) + +Fixpoint enat_nat' n (e:enat n) : nat := + match e with + | e0 => 0 + | es n e => S (enat_nat' n e) + end. + +Extraction Implicit enat_nat' [n]. +Recursive Extraction enat_nat'. + +(** Bug #4228 *) + +Module Food. +Inductive Course := +| main: nat -> Course +| dessert: nat -> Course. + +Inductive Meal : Course -> Type := +| one_course : forall n:nat, Meal (main n) +| two_course : forall n m, Meal (main n) -> Meal (dessert m). +Extraction Implicit two_course [n]. +End Food. + +Recursive Extraction Food.Meal. diff --git a/theories/Compat/AdmitAxiom.v b/theories/Compat/AdmitAxiom.v new file mode 100644 index 000000000..68607f6b2 --- /dev/null +++ b/theories/Compat/AdmitAxiom.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Compatibility file for making the admit tactic act similar to Coq v8.4. In +8.4, [admit] created a new axiom; in 8.5, it just shelves the goal. This +compatibility definition is not in the Coq84.v file to avoid loading an +inconsistent axiom implicitly. *) + +Axiom proof_admitted : False. +Ltac admit := clear; abstract case proof_admitted. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index b04d5168f..1c70a894a 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -18,10 +18,6 @@ Global Set Asymmetric Patterns. (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. -(** In 8.4, [admit] created a new axiom; in 8.5, it just shelves the goal. *) -Axiom proof_admitted : False. -Ltac admit := clear; abstract case proof_admitted. - (** In 8.5, [refine] leaves over dependent subgoals. *) Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable. diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget index c0c40ab1c..43b197004 100644 --- a/theories/Compat/vo.itarget +++ b/theories/Compat/vo.itarget @@ -1,2 +1,3 @@ +AdmitAxiom.vo Coq84.vo Coq85.vo diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4852a6d33..5e782233f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -196,6 +196,11 @@ let require () = let map dir = Qualid (Loc.ghost, qualid_of_string dir) in Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) +let add_compat_require v = + match v with + | Flags.V8_4 -> add_require "Coq.Compat.Coq84" + | _ -> () + let compile_list = ref ([] : (bool * string) list) let glob_opt = ref false @@ -475,7 +480,7 @@ let parse_args arglist = |"-async-proofs-private-flags" -> Flags.async_proofs_private_flags := Some (next ()); |"-worker-id" -> set_worker_id opt (next ()) - |"-compat" -> Flags.compat_version := get_compat_version (next ()) + |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |