diff options
Diffstat (limited to 'plugins/extraction')
34 files changed, 231 insertions, 197 deletions
diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES index 4bc3dba36e..bc7e1448f7 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -200,7 +200,7 @@ For the moment there are: Wf.well_founded_induction Wf.well_founded_induction_type Those constants does not match the auto-inlining criterion based on strictness. -Of course, you can still overide this behaviour via some Extraction NoInline. +Of course, you can still override this behaviour via some Extraction NoInline. * There is now a web page showing the extraction of all standard theories: http://www.lri.fr/~letouzey/extraction diff --git a/plugins/extraction/ExtrOCamlInt63.v b/plugins/extraction/ExtrOCamlInt63.v new file mode 100644 index 0000000000..a2ee602313 --- /dev/null +++ b/plugins/extraction/ExtrOCamlInt63.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extraction to OCaml of native 63-bit machine integers. *) + +From Coq Require Int63 Extraction. + +(** Basic data types used by some primitive operators. *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. +Extract Inductive comparison => int [ "0" "(-1)" "1" ]. +Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ]. + +(** Primitive types and operators. *) +Extract Constant Int63.int => "Uint63.t". +Extraction Inline Int63.int. +(* Otherwise, the name conflicts with the primitive OCaml type [int] *) + +Extract Constant Int63.lsl => "Uint63.l_sl". +Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Int63.land => "Uint63.l_and". +Extract Constant Int63.lor => "Uint63.l_or". +Extract Constant Int63.lxor => "Uint63.l_xor". + +Extract Constant Int63.add => "Uint63.add". +Extract Constant Int63.sub => "Uint63.sub". +Extract Constant Int63.mul => "Uint63.mul". +Extract Constant Int63.mulc => "Uint63.mulc". +Extract Constant Int63.div => "Uint63.div". +Extract Constant Int63.mod => "Uint63.rem". + +Extract Constant Int63.eqb => "Uint63.equal". +Extract Constant Int63.ltb => "Uint63.lt". +Extract Constant Int63.leb => "Uint63.le". + +Extract Constant Int63.addc => "Uint63.addc". +Extract Constant Int63.addcarryc => "Uint63.addcarryc". +Extract Constant Int63.subc => "Uint63.subc". +Extract Constant Int63.subcarryc => "Uint63.subcarryc". + +Extract Constant Int63.diveucl => "Uint63.diveucl". +Extract Constant Int63.diveucl_21 => "Uint63.div21". +Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". + +Extract Constant Int63.compare => "Uint63.compare". + +Extract Constant Int63.head0 => "Uint63.head0". +Extract Constant Int63.tail0 => "Uint63.tail0". diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 36bb1148b6..2f82b24862 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -(** Restore lazyness of andb, orb. +(** Restore laziness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined - by extraction in order to have lazyness, producing inelegant + by extraction in order to have laziness, producing inelegant (if ... then ... else false) and (if ... then true else ...). *) diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index 2d832799a3..f8bc86d087 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v index a3a4d45c13..2de1906323 100644 --- a/plugins/extraction/ExtrOcamlIntConv.v +++ b/plugins/extraction/ExtrOcamlIntConv.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index c403f7c5a1..a66d6e41fd 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index a2f809a0c1..406a7f0d2b 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v index f094d4860e..6265a67577 100644 --- a/plugins/extraction/ExtrOcamlString.v +++ b/plugins/extraction/ExtrOcamlString.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index f7746b3e3c..c36ea50755 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index f0e4b297e2..c7343d2468 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v index b79d32e650..207c95247e 100644 --- a/plugins/extraction/Extraction.v +++ b/plugins/extraction/Extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index c675eacc92..ef76154d75 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 59c57cc544..1c325a8d3a 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,7 +15,6 @@ open ModPath open Namegen open Nameops open Libnames -open Globnames open Table open Miniml open Mlutil @@ -125,7 +124,7 @@ module KOrd = struct type t = kind * string let compare (k1, s1) (k2, s2) = - let c = Pervasives.compare k1 k2 (* OK *) in + let c = pervasives_compare k1 k2 (* OK *) in if c = 0 then String.compare s1 s2 else c end @@ -573,7 +572,7 @@ let pp_ocaml_gen k mp rls olab = if is_mp_bound base then pp_ocaml_bound base rls else pp_ocaml_extern k base rls -(* For Haskell, things are simplier: we have removed (almost) all structures *) +(* For Haskell, things are simpler: we have removed (almost) all structures *) let pp_haskell_gen k mp rls = match rls with | [] -> assert false @@ -590,7 +589,7 @@ let pp_global k r = let s = List.hd ls in let mp,l = repr_of_r r in if ModPath.equal mp (top_visible_mp ()) then - (* simpliest situation: definition of r (or use in the same context) *) + (* simplest situation: definition of r (or use in the same context) *) (* we update the visible environment *) (add_visible (k,s) l; unquote s) else @@ -607,7 +606,7 @@ let pp_module mp = let ls = mp_renaming mp in match mp with | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) -> - (* simpliest situation: definition of mp (or use in the same context) *) + (* simplest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in add_visible (Mod,s) l; s @@ -629,21 +628,21 @@ let check_extract_ascii () = | Haskell -> "Prelude.Char" | _ -> raise Not_found in - String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type) + String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type) with Not_found -> false let is_list_cons l = - List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l + List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l let is_native_char = function - | MLcons(_,ConstructRef ((kn,0),1),l) -> + | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) -> MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l | _ -> false let get_native_char c = let rec cumul = function | [] -> 0 - | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) + | MLcons(_,GlobRef.ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l) | _ -> assert false in let l = match c with MLcons(_,_,l) -> l | _ -> assert false in diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 07237d7504..e4e9c4c527 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 8f17f7b2dd..551dbdc6fb 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -14,7 +14,6 @@ open Declarations open Names open ModPath open Libnames -open Globnames open Pp open CErrors open Util @@ -29,24 +28,27 @@ open Common let toplevel_env () = let get_reference = function - | (_,kn), Lib.Leaf o -> - let mp,l = KerName.repr kn in - begin match Libobject.object_tag o with - | "CONSTANT" -> - let constant = Global.lookup_constant (Constant.make1 kn) in - Some (l, SFBconst constant) - | "INDUCTIVE" -> - let inductive = Global.lookup_mind (MutInd.make1 kn) in - Some (l, SFBmind inductive) - | "MODULE" -> - let modl = Global.lookup_module (MPdot (mp, l)) in - Some (l, SFBmodule modl) - | "MODULE TYPE" -> - let modtype = Global.lookup_modtype (MPdot (mp, l)) in - Some (l, SFBmodtype modtype) - | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.") - | _ -> None - end + | (_,kn), Lib.Leaf Libobject.AtomicObject o -> + let mp,l = KerName.repr kn in + begin match Libobject.object_tag o with + | "CONSTANT" -> + let constant = Global.lookup_constant (Constant.make1 kn) in + Some (l, SFBconst constant) + | "INDUCTIVE" -> + let inductive = Global.lookup_mind (MutInd.make1 kn) in + Some (l, SFBmind inductive) + | _ -> None + end + | (_,kn), Lib.Leaf Libobject.ModuleObject _ -> + let mp,l = KerName.repr kn in + let modl = Global.lookup_module (MPdot (mp, l)) in + Some (l, SFBmodule modl) + | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ -> + let mp,l = KerName.repr kn in + let modtype = Global.lookup_modtype (MPdot (mp, l)) in + Some (l, SFBmodtype modtype) + | (_,kn), Lib.Leaf Libobject.IncludeObject _ -> + user_err Pp.(str "No extraction of toplevel Include yet.") | _ -> None in List.rev (List.map_filter get_reference (Lib.contents ())) @@ -115,7 +117,7 @@ module Visit : VISIT = struct v.mp <- MPset.union (prefixes_mp mp) v.mp; v.mp_all <- MPset.add mp v.mp_all let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn) - let add_ref = function + let add_ref = let open GlobRef in function | ConstRef c -> add_kn (Constant.user c) | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind) | VarRef _ -> assert false @@ -645,7 +647,6 @@ let separate_extraction lr = is \verb!Extraction! [qualid]. *) let simple_extraction r = - Vernacentries.dump_global CAst.(make (Constrexpr.AN r)); match locate_ref [r] with | ([], [mp]) as p -> full_extr None p | [r],[] -> @@ -751,19 +752,15 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = - let pstate = match pstate with - | None -> CErrors.user_err Pp.(str "No ongoing proof") - | Some pstate -> pstate - in init ~inner:true false false; - let prf = Proof_global.give_me_the_proof pstate in + let prf = Proof_global.get_proof pstate in let sigma, env = Pfedit.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Proof_global.get_current_proof_name pstate) in - let fake_ref = ConstRef (Constant.make2 mp l) in + let l = Label.of_id (Proof_global.get_proof_name pstate) in + let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7ba7e05019..927b10729f 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.t option -> unit +val show_extraction : pstate:Proof_global.t -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c9cfd74362..cca212f332 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -24,7 +24,6 @@ open Termops open Inductiveops open Recordops open Namegen -open Globnames open Miniml open Table open Mlutil @@ -115,7 +114,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) let get_opaque env c = EConstr.of_constr - (Opaqueproof.force_proof (Environ.opaque_tables env) c) + (fst (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c)) let applistc c args = EConstr.mkApp (c, Array.of_list args) @@ -303,7 +302,7 @@ let rec extract_type env sg db j c args = else let n' = List.nth db (n-1) in if Int.equal n' 0 then Tunknown else Tvar n') | Const (kn,u) -> - let r = ConstRef kn in + let r = GlobRef.ConstRef kn in let typ = type_of env sg (EConstr.mkConstU (kn,u)) in (match flag_of_type env sg typ with | (Logic,_) -> assert false (* Cf. logical cases above *) @@ -311,7 +310,7 @@ let rec extract_type env sg db j c args = let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ | Primitive _ -> mlt - | Def _ when is_custom (ConstRef kn) -> mlt + | Def _ when is_custom (GlobRef.ConstRef kn) -> mlt | Def lbody -> let newc = applistc (get_body lbody) args in let mlt' = extract_type env sg db j newc [] in @@ -331,7 +330,7 @@ let rec extract_type env sg db j c args = extract_type env sg db j newc [])) | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in - extract_type_app env sg db (IndRef (kn,i),s) args + extract_type_app env sg db (GlobRef.IndRef (kn,i),s) args | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown @@ -346,7 +345,7 @@ let rec extract_type env sg db j c args = | LocalDef (_,body,_) -> extract_type env sg db j (EConstr.applist (body,args)) [] | LocalAssum (_,ty) -> - let r = VarRef v in + let r = GlobRef.VarRef v in (match flag_of_type env sg ty with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> @@ -405,7 +404,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) extract_really_ind env kn mib with SingletonInductiveBecomesProp id -> (* TODO : which inductive is concerned in the block ? *) - error_singleton_become_prop id (Some (IndRef (kn,0))) + error_singleton_become_prop id (Some (GlobRef.IndRef (kn,0))) (* Then the real function *) @@ -481,7 +480,7 @@ and extract_really_ind env kn mib = let ind_info = try let ip = (kn, 0) in - let r = IndRef ip in + let r = GlobRef.IndRef ip in if is_custom r then raise (I Standard); if mib.mind_finite == CoFinite then raise (I Coinductive); if not (Int.equal mib.mind_ntypes 1) then raise (I Standard); @@ -519,7 +518,7 @@ and extract_really_ind env kn mib = (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((==) Keep) (type2signature env typ) then projs := Cset.add knp !projs; - Some (ConstRef knp) :: (select_fields l typs) + Some (GlobRef.ConstRef knp) :: (select_fields l typs) | _ -> assert false in let field_glob = select_fields field_names typ @@ -565,7 +564,7 @@ and extract_type_cons env sg db dbmap c i = (*s Recording the ML type abbreviation of a Coq type scheme constant. *) -and mlt_env env r = match r with +and mlt_env env r = let open GlobRef in match r with | IndRef _ | ConstructRef _ | VarRef _ -> None | ConstRef kn -> let cb = Environ.lookup_constant kn env in @@ -688,7 +687,7 @@ let rec extract_term env sg mle mlt c args = | LocalDef (_,_,ty) -> ty in let vty = extract_type env sg [] 0 ty [] in - let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in + let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in extract_app env sg mle mlt extract_var args | Int i -> assert (args = []); MLuint i | Ind _ | Prod _ | Sort _ -> assert false @@ -746,27 +745,15 @@ and extract_cst_app env sg mle mlt kn args = (* Second, is the resulting type compatible with the expected type [mlt] ? *) let magic2 = needs_magic (a, mlt) in (* The internal head receives a magic if [magic1] *) - let head = put_magic_if magic1 (MLglob (ConstRef kn)) in + let head = put_magic_if magic1 (MLglob (GlobRef.ConstRef kn)) in (* Now, the extraction of the arguments. *) let s_full = type2signature env (snd schema) in - let s_full = sign_with_implicits (ConstRef kn) s_full 0 in + let s_full = sign_with_implicits (GlobRef.ConstRef kn) s_full 0 in let s = sign_no_final_keeps s_full in let ls = List.length s in let la = List.length args in (* The ml arguments, already expunged from known logical ones *) let mla = make_mlargs env sg mle s args metas in - let mla = - if magic1 || lang () != Ocaml then mla - else - try - (* for better optimisations later, we discard dependent args - of projections and replace them by fake args that will be - removed during final pretty-print. *) - let l,l' = List.chop (projection_arity (ConstRef kn)) mla in - if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l' - else mla - with e when CErrors.noncritical e -> mla - in (* For strict languages, purely logical signatures lead to a dummy lam (except when [Kill Ktype] everywhere). So a [MLdummy] is left accordingly. *) @@ -807,11 +794,11 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = let nb_tvars = List.length oi.ip_vars and types = List.map (expand env) oi.ip_types.(j-1) in let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in - let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in + let type_cons = type_recomp (types, Tglob (GlobRef.IndRef ip, list_tvar)) in let type_cons = instantiation (nb_tvars, type_cons) in (* Then, the usual variables [s], [ls], [la], ... *) let s = List.map (type2sign env) types in - let s = sign_with_implicits (ConstructRef cp) s params_nb in + let s = sign_with_implicits (GlobRef.ConstructRef cp) s params_nb in let ls = List.length s in let la = List.length args in assert (la <= ls + params_nb); @@ -831,8 +818,8 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = | Tglob (_,l) -> List.map type_simpl l | _ -> assert false in - let typ = Tglob(IndRef ip, typeargs) in - put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla)) + let typ = Tglob(GlobRef.IndRef ip, typeargs) in + put_magic_if magic1 (MLcons (typ, GlobRef.ConstructRef cp, mla)) in (* Different situations depending of the number of arguments: *) if la < params_nb then @@ -854,7 +841,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = constructors_nrealargs_env env ip in + let ni = constructors_nrealargs env ip in let br_size = Array.length br in assert (Int.equal (Array.length ni) br_size); if Int.equal br_size 0 then begin @@ -880,11 +867,11 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt = let oi = mi.ind_packets.(i) in let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) - let type_head = Tglob (IndRef ip, Array.to_list metas) in + let type_head = Tglob (GlobRef.IndRef ip, Array.to_list metas) in let a = extract_term env sg mle type_head c [] in (* The extraction of each branch. *) let extract_branch i = - let r = ConstructRef (ip,i+1) in + let r = GlobRef.ConstructRef (ip,i+1) in (* The types of the arguments of the corresponding constructor. *) let f t = type_subst_vect metas (expand env t) in let l = List.map f oi.ip_types.(i) in @@ -909,7 +896,7 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt = else (* Standard case: we apply [extract_branch]. *) let typs = List.map type_simpl (Array.to_list metas) in - let typ = Tglob (IndRef ip,typs) in + let typ = Tglob (GlobRef.IndRef ip,typs) in MLcase (typ, a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) @@ -960,7 +947,7 @@ let extract_std_constant env sg kn body typ = let l,t' = type_decomp (expand env (var2var' t)) in let s = List.map (type2sign env) l in (* Check for user-declared implicit information *) - let s = sign_with_implicits (ConstRef kn) s 0 in + let s = sign_with_implicits (GlobRef.ConstRef kn) s 0 in (* Decomposing the top level lambdas of [body]. If there isn't enough, it's ok, as long as remaining args aren't to be pruned (and initial lambdas aren't to be all @@ -1015,7 +1002,7 @@ let extract_axiom env sg kn typ = let l,_ = type_decomp (expand env (var2var' t)) in let s = List.map (type2sign env) l in (* Check for user-declared implicit information *) - let s = sign_with_implicits (ConstRef kn) s 0 in + let s = sign_with_implicits (GlobRef.ConstRef kn) s 0 in type_expunge_from_sign env s t let extract_fixpoint env sg vkn (fi,ti,ci) = @@ -1034,10 +1021,10 @@ let extract_fixpoint env sg vkn (fi,ti,ci) = terms.(i) <- e; types.(i) <- t; with SingletonInductiveBecomesProp id -> - error_singleton_become_prop id (Some (ConstRef vkn.(i))) + error_singleton_become_prop id (Some (GlobRef.ConstRef vkn.(i))) done; current_fixpoints := []; - Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) + Dfix (Array.map (fun kn -> GlobRef.ConstRef kn) vkn, terms, types) (** Because of automatic unboxing the easy way [mk_def c] on the constant body of primitive projections doesn't work. We pretend @@ -1095,7 +1082,7 @@ let fake_match_projection env p = let extract_constant env kn cb = let sg = Evd.from_env env in - let r = ConstRef kn in + let r = GlobRef.ConstRef kn in let typ = EConstr.of_constr cb.const_type in 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 @@ -1150,11 +1137,11 @@ let extract_constant env kn cb = if access_opaque () then mk_def (get_opaque env c) else mk_ax ()) with SingletonInductiveBecomesProp id -> - error_singleton_become_prop id (Some (ConstRef kn)) + error_singleton_become_prop id (Some (GlobRef.ConstRef kn)) let extract_constant_spec env kn cb = let sg = Evd.from_env env in - let r = ConstRef kn in + let r = GlobRef.ConstRef kn in let typ = EConstr.of_constr cb.const_type in try match flag_of_type env sg typ with @@ -1173,7 +1160,7 @@ let extract_constant_spec env kn cb = let t = snd (record_constant_type env sg kn (Some typ)) in Sval (r, type_expunge env t) with SingletonInductiveBecomesProp id -> - error_singleton_become_prop id (Some (ConstRef kn)) + error_singleton_become_prop id (Some (GlobRef.ConstRef kn)) let extract_with_type env sg c = try @@ -1205,7 +1192,7 @@ let extract_inductive env kn = let ind = extract_ind env kn in add_recursors env kn; let f i j l = - let implicits = implicits_of_global (ConstructRef ((kn,i),j+1)) in + let implicits = implicits_of_global (GlobRef.ConstructRef ((kn,i),j+1)) in let rec filter i = function | [] -> [] | t::l -> diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index d27c79cb62..c2919d09f5 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -16,9 +16,9 @@ open Environ open Evd open Miniml -val extract_constant : env -> Constant.t -> constant_body -> ml_decl +val extract_constant : env -> Constant.t -> Opaqueproof.opaque constant_body -> ml_decl -val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec +val extract_constant_spec : env -> Constant.t -> 'a constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d7bb27f121..4f077b08b6 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY -(* Same, with content splitted in several files *) +(* Same, with content split in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] -> { separate_extraction l } END @@ -128,7 +128,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> {Feedback. msg_info (print_extraction_inline ()) } + -> {Feedback.msg_notice (print_extraction_inline ()) } END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF @@ -150,7 +150,7 @@ END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> { Feedback.msg_info (print_extraction_blacklist ()) } + -> { Feedback.msg_notice (print_extraction_blacklist ()) } END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF @@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF END (* Show the extraction of the current proof *) -VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query +| [ "Show" "Extraction" ] + -> { show_extraction } END diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index a3cd92d556..e4efbcff0c 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -14,7 +14,6 @@ open Pp open CErrors open Util open Names -open Globnames open Table open Miniml open Mlutil @@ -110,7 +109,7 @@ let rec pp_type par vl t = (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (IndRef(kn,0),l) + | Tglob (GlobRef.IndRef(kn,0),l) when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> pp_type true vl (List.hd l) | Tglob (r,l) -> @@ -271,7 +270,7 @@ let pp_logical_ind packet = prvect_with_sep spc Id.print packet.ip_consnames) let pp_singleton kn packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ name ++ spc () ++ prlist_with_sep spc Id.print l ++ @@ -291,14 +290,14 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.is_empty cv then "type " else "data ") ++ - pp_global Type (IndRef ip) ++ + pp_global Type (GlobRef.IndRef ip) ++ prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++ if Array.is_empty cv then str " () -- empty inductive" else (fnl () ++ str " " ++ v 0 (str " " ++ prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor - (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) + (Array.mapi (fun i c -> GlobRef.ConstructRef (ip,i+1),c) cv))) let rec pp_ind first kn i ind = if i >= Array.length ind.ind_packets then @@ -306,7 +305,7 @@ let rec pp_ind first kn i ind = else let ip = (kn,i) in let p = ind.ind_packets.(i) in - if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind + if is_custom (GlobRef.IndRef (kn,i)) then pp_ind first kn (i+1) ind else if p.ip_logical then pp_logical_ind p ++ pp_ind first kn (i+1) ind diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli index 27cb6b9460..26f54de7d6 100644 --- a/plugins/extraction/haskell.mli +++ b/plugins/extraction/haskell.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index f88d29e9ed..fba6b7c780 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,7 +1,6 @@ open Pp open Util open Names -open Globnames open Table open Miniml open Mlutil @@ -200,10 +199,10 @@ and json_function env t = let json_ind ip pl cv = json_dict [ ("what", json_str "decl:ind"); - ("name", json_global Type (IndRef ip)); + ("name", json_global Type (GlobRef.IndRef ip)); ("argnames", json_list (List.map json_id pl)); ("constructors", json_listarr (Array.mapi (fun idx c -> json_dict [ - ("name", json_global Cons (ConstructRef (ip, idx+1))); + ("name", json_global Cons (GlobRef.ConstructRef (ip, idx+1))); ("argtypes", json_list (List.map (json_type pl) c)) ]) cv)) ] diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index b7f80d543b..8b69edbe4c 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 9df0f4964e..e3c9635c55 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 2432887673..000df26858 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,7 +12,6 @@ open Util open Names open Libnames -open Globnames open Table open Miniml (*i*) @@ -668,11 +667,11 @@ let is_regular_match br = | _ -> raise Impossible in let ind = match get_r br.(0) with - | ConstructRef (ind,_) -> ind + | GlobRef.ConstructRef (ind,_) -> ind | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br @@ -780,7 +779,7 @@ let eta_red e = else e | _ -> e -(* Performs an eta-reduction when the core is atomic, +(* Performs an eta-reduction when the core is atomic and value, or otherwise returns None *) let atomic_eta_red e = @@ -790,7 +789,7 @@ let atomic_eta_red e = | MLapp (f,a) when test_eta_args_lift 0 n a -> (match f with | MLrel k when k>n -> Some (MLrel (k-n)) - | MLglob _ | MLexn _ | MLdummy _ -> Some f + | MLglob _ | MLdummy _ -> Some f | _ -> None) | _ -> None @@ -819,11 +818,11 @@ let rec tmp_head_lams = function *) let rec ast_glob_subst s t = match t with - | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> + | MLapp ((MLglob ((GlobRef.ConstRef kn) as refe)) as f, a) -> let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in (try linear_beta_red a (Refmap'.find refe s) with Not_found -> MLapp (f, a)) - | MLglob ((ConstRef kn) as refe) -> + | MLglob ((GlobRef.ConstRef kn) as refe) -> (try Refmap'.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -1504,7 +1503,7 @@ open Declareops let inline_test r t = if not (auto_inline ()) then false else - let c = match r with ConstRef c -> c | _ -> assert false in + let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in let has_body = try constant_has_body (Global.lookup_constant c) with Not_found -> false @@ -1534,7 +1533,7 @@ let manual_inline_set = Cset_env.empty let manual_inline = function - | ConstRef c -> Cset_env.mem c manual_inline_set + | GlobRef.ConstRef c -> Cset_env.mem c manual_inline_set | _ -> false (* If the user doesn't say he wants to keep [t], we inline in two cases: @@ -1548,6 +1547,7 @@ let inline r t = not (to_keep r) (* The user DOES want to keep it *) && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) - || (lang () != Haskell && not (is_projection r) && - (is_recursor r || manual_inline r || inline_test r t))) + || (lang () != Haskell && + (is_projection r || is_recursor r || + manual_inline r || inline_test r t))) diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index d23fdb3d53..2567804db6 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 654695c232..6b1eef7abb 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -10,7 +10,6 @@ open Names open ModPath -open Globnames open CErrors open Util open Miniml @@ -42,7 +41,7 @@ let se_iter do_decl do_spec do_mp = let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in + let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l')) in mt_iter mt; do_spec (Stype(r,l,Some t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in @@ -113,12 +112,12 @@ let ast_iter_references do_term do_cons do_type a = let ind_iter_references do_term do_cons do_type kn ind = let type_iter = type_iter_references do_type in - let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in + let cons_iter cp l = do_cons (GlobRef.ConstructRef cp); List.iter type_iter l in let packet_iter ip p = - do_type (IndRef ip); + do_type (GlobRef.IndRef ip); if lang () == Ocaml then (match ind.ind_equiv with - | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip)); + | Miniml.Equiv kne -> do_type (GlobRef.IndRef (MutInd.make1 kne, snd ip)); | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in @@ -258,7 +257,7 @@ let dfix_to_mlfix rv av i = let s = make_subst (Array.length rv - 1) Refmap'.empty in let rec subst n t = match t with - | MLglob ((ConstRef kn) as refe) -> + | MLglob ((GlobRef.ConstRef kn) as refe) -> (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in @@ -309,7 +308,7 @@ and optim_me to_appear s = function For non-library extraction, we recompute a minimal set of dependencies for first-level definitions (no module pruning yet). *) -let base_r = function +let base_r = let open GlobRef in function | ConstRef c as r -> r | IndRef (kn,_) -> IndRef (kn,0) | ConstructRef ((kn,_),_) -> IndRef (kn,0) @@ -327,7 +326,7 @@ let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps)) let declared_refs = function - | Dind (kn,_) -> [IndRef (kn,0)] + | Dind (kn,_) -> [GlobRef.IndRef (kn,0)] | Dtype (r,_,_) -> [r] | Dterm (r,_,_) -> [r] | Dfix (rv,_,_) -> Array.to_list rv diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index f45773f095..d0c90d83bb 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 8940aedd6d..e7004fe9af 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,7 +15,6 @@ open CErrors open Util open Names open ModPath -open Globnames open Table open Miniml open Mlutil @@ -142,7 +141,7 @@ let get_infix r = let s = find_custom r in String.sub s 1 (String.length s - 2) -let get_ind = function +let get_ind = let open GlobRef in function | IndRef _ as r -> r | ConstructRef (ind,_) -> IndRef ind | _ -> assert false @@ -166,7 +165,7 @@ let 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) + | Tglob (GlobRef.IndRef(kn,0),l) when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> pp_tuple_light pp_rec l | Tglob (r,l) -> @@ -230,12 +229,7 @@ let rec pp_expr par env args = and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in 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 e when CErrors.noncritical e -> apply (pp_global Term r)) + | MLglob r -> apply (pp_global Term r) | 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 @@ -325,10 +319,14 @@ and pp_record_proj par env typ t pv args = 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 + | MLrel i | MLmagic(MLrel i) when i <= n -> i,[] + | MLapp(MLrel i, a) | MLmagic(MLapp(MLrel i, a)) + | MLapp(MLmagic(MLrel i), a) when i<=n && no_patvar a -> i,a | _ -> raise Impossible in + let magic = + match body with MLmagic _ | MLapp(MLmagic _, _) -> true | _ -> false + in let rec lookup_rel i idx = function | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l | Pwild :: l -> lookup_rel i (idx+1) l @@ -344,7 +342,10 @@ and pp_record_proj par env typ t pv args = 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 + if magic then + pp_apply (str "Obj.magic") par (pp_head :: pp_args) + else + pp_apply pp_head par pp_args and pp_record_pat (fields, args) = str "{ " ++ @@ -467,7 +468,7 @@ let pp_Dfix (rv,c,t) = let pp_equiv param_list name = function | NoEquiv, _ -> mt () | Equiv kn, i -> - str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i)) + str " = " ++ pp_parameters param_list ++ pp_global Type (GlobRef.IndRef (MutInd.make1 kn,i)) | RenEquiv ren, _ -> str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name @@ -494,7 +495,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (GlobRef.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 () ++ @@ -502,7 +503,7 @@ let pp_singleton kn packet = Id.print packet.ip_consnames.(0))) let pp_record kn fields ip_equiv packet = - let ind = IndRef (kn,0) in + let ind = GlobRef.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 @@ -525,13 +526,13 @@ let pp_ind co kn ind = 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))) + pp_global Type (GlobRef.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 ((kn,i),j+1))) + Array.mapi (fun j _ -> pp_global Cons (GlobRef.ConstructRef ((kn,i),j+1))) p.ip_types) ind.ind_packets in @@ -541,7 +542,7 @@ let pp_ind co kn ind = 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) kwd + if is_custom (GlobRef.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 ()) ++ @@ -580,14 +581,10 @@ let pp_decl = function | Dterm (r, a, t) -> let def = if is_custom r then str (" = " ^ find_custom r) - else if is_projection r then - (prvect str (Array.make (projection_arity r) " _")) ++ - str " x = x." else pp_function (empty_env ()) a in let name = pp_global Term r in - let postdef = if is_projection r then name else mt () in - pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ()) | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) @@ -672,7 +669,7 @@ and pp_module_type params = function let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in + let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli index 96d123444f..e145673473 100644 --- a/plugins/extraction/ocaml.mli +++ b/plugins/extraction/ocaml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 6aa3a6220e..dd840cd929 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli index defd81846b..25aabea1e7 100644 --- a/plugins/extraction/scheme.mli +++ b/plugins/extraction/scheme.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 399a77c596..96a3d00dc2 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -30,12 +30,12 @@ module Refset' = GlobRef.Set_env (*S Utilities about [module_path] and [kernel_names] and [global_reference] *) -let occur_kn_in_ref kn = function +let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' | ConstRef _ | VarRef _ -> false -let repr_of_r = function +let repr_of_r = let open GlobRef in function | ConstRef kn -> Constant.repr2 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr2 kn @@ -101,7 +101,7 @@ let labels_of_ref r = (*S The main tables: constants, inductives, records, ... *) -(* Theses tables are not registered within coq save/undo mechanism +(* These tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum @@ -109,7 +109,7 @@ let labels_of_ref r = (*s Constants tables. *) -let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t) +let typedefs = ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_type) Cmap_env.t) let init_typedefs () = typedefs := Cmap_env.empty let add_typedef kn cb t = typedefs := Cmap_env.add kn (cb,t) !typedefs @@ -120,7 +120,7 @@ let lookup_typedef kn cb = with Not_found -> None let cst_types = - ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t) + ref (Cmap_env.empty : (Opaqueproof.opaque constant_body * ml_schema) Cmap_env.t) let init_cst_types () = cst_types := Cmap_env.empty let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types let lookup_cst_type kn cb = @@ -151,7 +151,7 @@ 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 + let kn = let open GlobRef in match r with | ConstructRef ((kn,_),_) -> kn | IndRef (kn,_) -> kn | _ -> assert false @@ -164,7 +164,7 @@ let is_coinductive_type = function | _ -> false let get_record_fields r = - let kn = match r with + let kn = let open GlobRef in match r with | ConstructRef ((kn,_),_) -> kn | IndRef (kn,_) -> kn | _ -> assert false @@ -201,7 +201,7 @@ let add_recursors env ind = mib.mind_packets let is_recursor = function - | ConstRef c -> KNset.mem (Constant.canonical c) !recursors + | GlobRef.ConstRef c -> KNset.mem (Constant.canonical c) !recursors | _ -> false (*s Record tables. *) @@ -210,7 +210,7 @@ let is_recursor = function let projs = ref (GlobRef.Map.empty : (inductive*int) GlobRef.Map.t) let init_projs () = projs := GlobRef.Map.empty -let add_projection n kn ip = projs := GlobRef.Map.add (ConstRef kn) (ip,n) !projs +let add_projection n kn ip = projs := GlobRef.Map.add (GlobRef.ConstRef kn) (ip,n) !projs let is_projection r = GlobRef.Map.mem r !projs let projection_arity r = snd (GlobRef.Map.find r !projs) let projection_info r = GlobRef.Map.find r !projs @@ -264,6 +264,7 @@ let safe_basename_of_global r = with Not_found -> anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in + let open GlobRef in match r with | ConstRef kn -> Label.to_id (Constant.label kn) | IndRef (kn,0) -> Label.to_id (MutInd.label kn) @@ -286,7 +287,7 @@ let safe_pr_global r = str (string_of_global r) let safe_pr_long_global r = try Printer.pr_global r with Not_found -> match r with - | ConstRef kn -> + | GlobRef.ConstRef kn -> let mp,l = Constant.repr2 kn in str ((ModPath.to_string mp)^"."^(Label.to_string l)) | _ -> assert false @@ -658,7 +659,7 @@ let extraction_inline b l = let refs = List.map Smartlocate.global_with_alias l in List.iter (fun r -> match r with - | ConstRef _ -> () + | GlobRef.ConstRef _ -> () | _ -> error_constant r) refs; Lib.add_anonymous_leaf (inline_extraction (b,refs)) @@ -666,7 +667,7 @@ let extraction_inline b l = let print_extraction_inline () = let (i,n)= !inline_table in - let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in + let i'= Refset'.filter (function GlobRef.ConstRef _ -> true | _ -> false) i in (str "Extraction Inline:" ++ fnl () ++ Refset'.fold (fun r p -> @@ -823,8 +824,8 @@ let indref_of_match pv = if Array.is_empty pv then raise Not_found; let (_,pat,_) = pv.(0) in match pat with - | Pusual (ConstructRef (ip,_)) -> IndRef ip - | Pcons (ConstructRef (ip,_),_) -> IndRef ip + | Pusual (GlobRef.ConstructRef (ip,_)) -> GlobRef.IndRef ip + | Pcons (GlobRef.ConstructRef (ip,_),_) -> GlobRef.IndRef ip | _ -> raise Not_found let is_custom_match pv = @@ -842,7 +843,7 @@ let in_customs : GlobRef.t * string list * string -> obj = ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + declare_object @@ superglobal_object_nodischarge "ML extractions custom matches" ~cache:(fun (_,(r,s)) -> add_custom_match r s) ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) @@ -852,9 +853,9 @@ let extract_constant_inline inline r ids s = check_inside_section (); let g = Smartlocate.global_with_alias r in match g with - | ConstRef kn -> + | GlobRef.ConstRef kn -> let env = Global.env () in - let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in + let typ, _ = Typeops.type_of_global_in_context env (GlobRef.ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin @@ -871,7 +872,7 @@ let extract_inductive r s l optstr = let g = Smartlocate.global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc g; match g with - | IndRef ((kn,i) as ip) -> + | GlobRef.IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets.(i).mind_consnames in if not (Int.equal n (List.length l)) then error_nb_cons (); @@ -881,7 +882,7 @@ let extract_inductive r s l optstr = optstr; List.iteri (fun j s -> - let g = ConstructRef (ip,succ j) in + let g = GlobRef.ConstructRef (ip,succ j) in Lib.add_anonymous_leaf (inline_extraction (true,[g])); Lib.add_anonymous_leaf (in_customs (g,[],s))) l | _ -> error_inductive g diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index acc1bfee8a..93f1629c4d 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -72,11 +72,11 @@ val labels_of_ref : GlobRef.t -> ModPath.t * Label.t list [mutual_inductive_body] as checksum. In both case, we should ideally also check the env *) -val add_typedef : Constant.t -> constant_body -> ml_type -> unit -val lookup_typedef : Constant.t -> constant_body -> ml_type option +val add_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type -> unit +val lookup_typedef : Constant.t -> Opaqueproof.opaque constant_body -> ml_type option -val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit -val lookup_cst_type : Constant.t -> constant_body -> ml_schema option +val add_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema -> unit +val lookup_cst_type : Constant.t -> Opaqueproof.opaque constant_body -> ml_schema option val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option |