From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/extraction/ExtrOcamlZBigInt.v | 2 +- plugins/extraction/common.ml | 54 +++++----- plugins/extraction/extract_env.ml | 11 +-- plugins/extraction/extraction.ml | 119 ++++++++++++++--------- plugins/extraction/extraction_plugin.mllib | 12 --- plugins/extraction/extraction_plugin.mlpack | 11 +++ plugins/extraction/g_extraction.ml4 | 10 +- plugins/extraction/haskell.ml | 6 +- plugins/extraction/json.ml | 8 +- plugins/extraction/modutil.ml | 12 +-- plugins/extraction/ocaml.ml | 4 +- plugins/extraction/scheme.ml | 2 +- plugins/extraction/table.ml | 146 ++++++++++++++++------------ plugins/extraction/table.mli | 5 +- 14 files changed, 220 insertions(+), 182 deletions(-) delete mode 100644 plugins/extraction/extraction_plugin.mllib create mode 100644 plugins/extraction/extraction_plugin.mlpack (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 9a1a4aa0..c9e8eac0 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -46,7 +46,7 @@ Extract Constant Pos.max => "Big.max". Extract Constant Pos.compare => "fun x y -> Big.compare_case Eq Lt Gt x y". Extract Constant Pos.compare_cont => - "fun x y c -> Big.compare_case c Lt Gt x y". + "fun c x y -> Big.compare_case c Lt Gt x y". Extract Constant N.add => "Big.add". Extract Constant N.succ => "Big.succ". diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bb9e8e5f..3c5f6cb7 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -17,8 +17,8 @@ open Table open Miniml open Mlutil -let string_of_id id = - let s = Names.Id.to_string id in +let ascii_of_id id = + let s = Id.to_string id in for i = 0 to String.length s - 2 do if s.[i] == '_' && s.[i+1] == '_' then warning_id s done; @@ -73,18 +73,19 @@ let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () -let is_digit = function - | '0'..'9' -> true - | _ -> false +let begins_with s prefix = + let len = String.length prefix in + String.length s >= len && String.equal (String.sub s 0 len) prefix let begins_with_CoqXX s = let n = String.length s in n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' && let i = ref 3 in try while !i < n do - if s.[!i] == '_' then i:=n (*Stop*) - else if is_digit s.[!i] then incr i - else raise Not_found + match s.[!i] with + | '_' -> i:=n (*Stop*) + | '0'..'9' -> incr i + | _ -> raise Not_found done; true with Not_found -> false @@ -109,9 +110,9 @@ let pseudo_qualify = qualify "__" let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false -let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id)) +let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id)) let uppercase_id id = - let s = string_of_id id in + let s = ascii_of_id id in assert (not (String.is_empty s)); if s.[0] == '_' then Id.of_string ("Coq_"^s) else Id.of_string (String.capitalize s) @@ -331,13 +332,10 @@ let reset_renaming_tables flag = existing. *) let modular_rename k id = - let s = string_of_id id in - let prefix,is_ok = - if upperkind k then "Coq_",is_upper else "coq_",is_lower + let s = ascii_of_id id in + let prefix,is_ok = if upperkind k then "Coq_",is_upper else "coq_",is_lower in - if not (is_ok s) || - (Id.Set.mem id (get_keywords ())) || - (String.length s >= 4 && String.equal (String.sub s 0 4) prefix) + if not (is_ok s) || Id.Set.mem id (get_keywords ()) || begins_with s prefix then prefix ^ s else s @@ -345,21 +343,20 @@ let modular_rename k id = with unique numbers *) let modfstlev_rename = - let add_prefixes,get_prefixes,_ = mktable_id true in + let add_index,get_index,_ = mktable_id true in fun l -> - let coqid = Id.of_string "Coq" in let id = Label.to_id l in try - let coqset = get_prefixes id in - let nextcoq = next_ident_away coqid coqset in - add_prefixes id (nextcoq::coqset); - (string_of_id nextcoq)^"_"^(string_of_id id) + let n = get_index id in + add_index id (n+1); + let s = if n == 0 then "" else string_of_int (n-1) in + "Coq"^s^"_"^(ascii_of_id id) with Not_found -> - let s = string_of_id id in + let s = ascii_of_id id in if is_lower s || begins_with_CoqXX s then - (add_prefixes id [coqid]; "Coq_"^s) + (add_index id 1; "Coq_"^s) else - (add_prefixes id []; s) + (add_index id 0; s) (*s Creating renaming for a [module_path] : first, the real function ... *) @@ -404,7 +401,7 @@ let ref_renaming_fun (k,r) = | [""] -> (* this happens only at toplevel of the monolithic case *) let globs = Id.Set.elements (get_global_ids ()) in let id = next_ident_away (kindcase_id k idg) globs in - string_of_id id + Id.to_string id | _ -> modular_rename k idg in add_global_ids (Id.of_string s); @@ -562,7 +559,7 @@ let pp_ocaml_extern k base rls = match rls with (* Standard situation : object in an opened file *) dottify rls' -(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *) +(* [pp_ocaml_gen] : choosing between [pp_ocaml_local] or [pp_ocaml_extern] *) let pp_ocaml_gen k mp rls olab = match common_prefix_from_list mp (get_visible_mps ()) with @@ -579,8 +576,7 @@ let pp_haskell_gen k mp rls = match rls with | s::rls' -> let str = pseudo_qualify rls' in let str = if is_upper str && not (upperkind k) then ("_"^str) else str in - let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in - prf ^ str + if ModPath.equal (base_mp mp) (top_visible_mp ()) then str else s^"."^str (* Main name printing function for a reference *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 41a068ff..52f22ee6 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -13,13 +13,12 @@ open Names open Libnames open Globnames open Pp -open Errors +open CErrors open Util open Table open Extraction open Modutil open Common -open Mod_subst (***************************************) (*S Part I: computing Coq environment. *) @@ -542,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) if not (Int.equal (Buffer.length buf) 0) then begin - Pp.msg_notice (str (Buffer.contents buf)); + Feedback.msg_notice (str (Buffer.contents buf)); Buffer.reset buf end @@ -584,8 +583,8 @@ let rec locate_ref = function | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_both_mod_and_cst q mp r; - let refs,mps = locate_ref l in refs,mp::mps + warning_ambiguous_name (q,mp,r); + let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when @@ -636,7 +635,7 @@ let simple_extraction r = in let ans = flag ++ print_one_decl struc (modpath_of_r r) d in reset (); - Pp.msg_notice ans + Feedback.msg_notice ans | _ -> assert false diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 10644da2..a980a43f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Declarations open Declareops open Environ @@ -26,6 +25,7 @@ open Globnames open Miniml open Table open Mlutil +open Context.Rel.Declaration (*i*) exception I of inductive_kind @@ -35,17 +35,18 @@ let current_fixpoints = ref ([] : constant list) let none = Evd.empty +(* NB: In OCaml, [type_of] and [get_of] might raise + [SingletonInductiveBecomeProp]. This exception will be caught + in late wrappers around the exported functions of this file, + in order to display the location of the issue. *) + let type_of env c = - try - let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast c) - with SingletonInductiveBecomesProp id -> error_singleton_become_prop id + let polyprop = (lang() == Haskell) in + Retyping.get_type_of ~polyprop env none (strip_outer_cast c) let sort_of env c = - try - let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) - with SingletonInductiveBecomesProp id -> error_singleton_become_prop id + let polyprop = (lang() == Haskell) in + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) (*S Generation of flags and signatures. *) @@ -73,9 +74,9 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_betadeltaiota env none t in + let t = whd_all env none t in match kind_of_term t with - | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c + | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) @@ -101,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -134,7 +135,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all 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 Kprop::s, vl @@ -142,7 +143,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -248,7 +249,7 @@ let rec extract_type env db j c args = | _ 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 + | LocalDef (_,t,_) -> extract_type env db j (lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown @@ -285,7 +286,7 @@ let rec extract_type env db j c args = | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args - | Case _ | Fix _ | CoFix _ -> Tunknown + | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown | _ -> assert false (*s Auxiliary function dealing with type application. @@ -328,11 +329,22 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) +(* First, a version with cache *) + and extract_ind env kn = (* kn is supposed to be in long form *) let mib = Environ.lookup_mind kn env in match lookup_ind kn mib with | Some ml_ind -> ml_ind | None -> + try + 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))) + +(* Then the real function *) + +and extract_really_ind env kn mib = (* First, if this inductive is aliased via a Module, we process the original inductive if possible. When at toplevel of the monolithic case, we cannot do much @@ -359,8 +371,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let packets = Array.mapi (fun i mip -> - let (ind,u), ctx = - Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in @@ -477,7 +488,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in @@ -561,7 +572,7 @@ let rec extract_term env mle mlt c args = put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (Name id, Some c1, t1) env in + let env' = push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) let args' = List.map (lift 1) args in @@ -579,10 +590,10 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const (kn,u) -> - extract_cst_app env mle mlt kn u args - | Construct (cp,u) -> - extract_cons_app env mle mlt cp u args + | Const (kn,_) -> + extract_cst_app env mle mlt kn args + | Construct (cp,_) -> + extract_cons_app env mle mlt cp args | Proj (p, c) -> let term = Retyping.expand_projection env (Evd.from_env env) p c [] in extract_term env mle mlt term args @@ -633,7 +644,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn u args = +and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -672,7 +683,7 @@ and extract_cst_app env mle mlt kn u args = 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 Errors.noncritical e -> 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 @@ -706,7 +717,7 @@ and extract_cst_app env mle mlt kn u args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in @@ -836,7 +847,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = let decomp_lams_eta_n n m env c t = let rels = fst (splay_prod_n env none n t) in - let rels = List.map (fun (id,_,c) -> (id,c)) rels in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) @@ -934,11 +945,13 @@ let extract_fixpoint env vkn (fi,ti,ci) = (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) let sub = List.rev_map mkConst kns in for i = 0 to n-1 do - if sort_of env ti.(i) != InProp then begin - let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in - terms.(i) <- e; - types.(i) <- t; - end + if sort_of env ti.(i) != InProp then + try + let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + terms.(i) <- e; + types.(i) <- t; + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef vkn.(i))) done; current_fixpoints := []; Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) @@ -968,13 +981,17 @@ let extract_constant env kn cb = let e,t = extract_std_constant env kn c typ in Dterm (r,e,t) in - match flag_of_type env typ with + try + match flag_of_type env typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_typ (Mod_subst.force_constr c) + | Some pb -> mk_typ pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then @@ -983,17 +1000,23 @@ let extract_constant env kn cb = | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_def (Mod_subst.force_constr c) + | Some pb -> mk_def pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) else mk_ax ()) + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef kn)) let extract_constant_spec env kn cb = let r = ConstRef kn in let typ = Typeops.type_of_constant_type env cb.const_type in - match flag_of_type env typ with + try + match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> @@ -1008,26 +1031,34 @@ let extract_constant_spec env kn cb = | (Info, Default) -> let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id (Some (ConstRef kn)) let extract_with_type env c = - let typ = type_of env c in - match flag_of_type env typ with + try + let typ = type_of env c in + match flag_of_type env typ with | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in let db = db_from_sign s in let t = extract_type_scheme env db c (List.length s) in Some (vl, t) | _ -> None + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id None let extract_constr env c = reset_meta_count (); - let typ = type_of env c in - match flag_of_type env typ with + try + let typ = type_of env c in + match flag_of_type env typ with | (_,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 + let mlt = extract_type env [] 1 typ [] in + extract_term env Mlenv.empty mlt c [], mlt + with SingletonInductiveBecomesProp id -> + error_singleton_become_prop id None let extract_inductive env kn = let ind = extract_ind env kn in diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mllib deleted file mode 100644 index ad321243..00000000 --- a/plugins/extraction/extraction_plugin.mllib +++ /dev/null @@ -1,12 +0,0 @@ -Table -Mlutil -Modutil -Extraction -Common -Ocaml -Haskell -Scheme -Json -Extract_env -G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/extraction_plugin.mlpack b/plugins/extraction/extraction_plugin.mlpack new file mode 100644 index 00000000..9184f650 --- /dev/null +++ b/plugins/extraction/extraction_plugin.mlpack @@ -0,0 +1,11 @@ +Table +Mlutil +Modutil +Extraction +Common +Ocaml +Haskell +Scheme +Json +Extract_env +G_extraction diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index aec95868..19fda4ae 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,9 +8,14 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "extraction_plugin" + (* ML names *) open Genarg +open Stdarg +open Constrarg +open Pcoq.Prim open Pp open Names open Nameops @@ -31,7 +36,6 @@ let pr_int_or_id _ _ _ = function | ArgId id -> pr_id id ARGUMENT EXTEND int_or_id - TYPED AS int_or_id PRINTED BY pr_int_or_id | [ preident(id) ] -> [ ArgId (Id.of_string id) ] | [ integer(i) ] -> [ ArgInt i ] @@ -99,7 +103,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> [ msg_info (print_extraction_inline ()) ] + -> [Feedback. msg_info (print_extraction_inline ()) ] END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF @@ -121,7 +125,7 @@ END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> [ msg_info (print_extraction_blacklist ()) ] + -> [ Feedback.msg_info (print_extraction_blacklist ()) ] END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 22519e34..0692c88c 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -9,7 +9,7 @@ (*s Production of Haskell syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -346,7 +346,7 @@ let pp_decl = function in if void then mt () else - names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++ + hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++ (if is_custom r then (names.(i) ++ str " = " ++ str (find_custom r)) else @@ -357,7 +357,7 @@ let pp_decl = function if is_inline_custom r then mt () else let e = pp_global Term r in - e ++ str " :: " ++ pp_type false [] t ++ fnl () ++ + hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++ if is_custom r then hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) else diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index df79c585..e43c47d0 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,8 +1,6 @@ open Pp -open Errors open Util open Names -open Nameops open Globnames open Table open Miniml @@ -18,9 +16,6 @@ let json_int i = let json_bool b = if b then str "true" else str "false" -let json_null = - str "null" - let json_global typ ref = json_str (Common.pp_global typ ref) @@ -147,7 +142,8 @@ let rec json_expr env = function ("what", json_str "fix:item"); ("name", json_id fi); ("body", json_function env' ti) - ]) (Array.map2 (fun a b -> a,b) ids' defs))) + ]) (Array.map2 (fun a b -> a,b) ids' defs))); + ("for", json_int i); ] | MLexn s -> json_dict [ ("what", json_str "expr:exception"); diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b5e8b480..60fe8e76 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -8,7 +8,7 @@ open Names open Globnames -open Errors +open CErrors open Util open Miniml open Table @@ -310,7 +310,7 @@ let base_r = function let reset_needed, add_needed, add_needed_mp, found_needed, is_needed = let needed = ref Refset'.empty and needed_mps = ref MPset.empty in - ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty), + ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty), (fun r -> needed := Refset'.add (base_r r) !needed), (fun mp -> needed_mps := MPset.add mp !needed_mps), (fun r -> needed := Refset'.remove (base_r r) !needed), @@ -380,14 +380,6 @@ let rec depcheck_struct = function let lse' = depcheck_se lse in if List.is_empty lse' then struc' else (mp,lse')::struc' -let is_prefix pre s = - let len = String.length pre in - let rec is_prefix_aux i = - if Int.equal i len then true - else pre.[i] == s.[i] && is_prefix_aux (succ i) - in - is_prefix_aux 0 - exception RemainingImplicit of kill_reason let check_for_remaining_implicits struc = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 3cb3810c..1c29a9bc 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -9,7 +9,7 @@ (*s Production of Ocaml syntax. *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -203,7 +203,7 @@ let rec pp_expr par env args = 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 Errors.noncritical e -> apply (pp_global Term r)) + with e when CErrors.noncritical e -> 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 diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 7b0f14df..a6309e61 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -9,7 +9,7 @@ (*s Production of Scheme syntax. *) open Pp -open Errors +open CErrors open Util open Names open Miniml diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index d7842e12..ff66d915 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -15,7 +15,7 @@ open Libobject open Goptions open Libnames open Globnames -open Errors +open CErrors open Util open Pp open Miniml @@ -295,81 +295,94 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) let err s = errorlabstrm "Extraction" s +let warn_extraction_axiom_to_realize = + CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" + (fun axioms -> + let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in + strbrk ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms) + ++ str "." ++ fnl ()) + +let warn_extraction_logical_axiom = + CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction" + (fun axioms -> + let s = + if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were" + in + (strbrk ("The following logical "^s^" encountered:") ++ + hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n") + ++ strbrk "Having invalid logical axiom in the environment when extracting" + ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++ + fnl ())) + let warning_axioms () = let info_axioms = Refset'.elements !info_axioms in - if List.is_empty info_axioms then () - else begin - let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in - msg_warning - (str ("The following "^s^" must be realized in the extracted code:") - ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) - ++ str "." ++ fnl ()) - end; + if not (List.is_empty info_axioms) then + warn_extraction_axiom_to_realize info_axioms; let log_axioms = Refset'.elements !log_axioms in - if List.is_empty log_axioms then () - else begin - let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were" - in - msg_warning - (str ("The following logical "^s^" encountered:") ++ - hov 1 - (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") - ++ - str "Having invalid logical axiom in the environment when extracting" ++ - spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ - fnl ()) - end + if not (List.is_empty log_axioms) then + warn_extraction_logical_axiom log_axioms + +let warn_extraction_opaque_accessed = + CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction" + (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++ + strbrk "the following opaque constant bodies have been accessed :" ++ + lst ++ str "." ++ fnl ()) + +let warn_extraction_opaque_as_axiom = + CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction" + (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++ + strbrk "the following opaque constants have been extracted as axioms :" ++ + lst ++ str "." ++ fnl () ++ + strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this." + ++ fnl ()) let warning_opaques accessed = let opaques = Refset'.elements !opaques in - if List.is_empty opaques then () - else + if not (List.is_empty opaques) then let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in - if accessed then - msg_warning - (str "The extraction is currently set to bypass opacity,\n" ++ - str "the following opaque constant bodies have been accessed :" ++ - lst ++ str "." ++ fnl ()) - else - msg_warning - (str "The extraction now honors the opacity constraints by default,\n" ++ - str "the following opaque constants have been extracted as axioms :" ++ - lst ++ str "." ++ fnl () ++ - str "If necessary, use \"Set Extraction AccessOpaque\" to change this." - ++ fnl ()) - -let warning_both_mod_and_cst q mp r = - msg_warning - (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ - str "do you mean module " ++ - pr_long_mp mp ++ - str " or object " ++ - pr_long_global r ++ str " ?" ++ fnl () ++ - str "First choice is assumed, for the second one please use " ++ - str "fully qualified name." ++ fnl ()) + if accessed then warn_extraction_opaque_accessed lst + else warn_extraction_opaque_as_axiom lst + +let warning_ambiguous_name = + CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction" + (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++ + strbrk "do you mean module " ++ + pr_long_mp mp ++ + strbrk " or object " ++ + pr_long_global r ++ str " ?" ++ fnl () ++ + strbrk "First choice is assumed, for the second one please use " ++ + strbrk "fully qualified name." ++ fnl ()) let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ safe_pr_global r ++ spc () ++ str "needs " ++ int i ++ str " type variable(s).") +let warn_extraction_inside_module = + CWarnings.create ~name:"extraction-inside-module" ~category:"extraction" + (fun () -> strbrk "Extraction inside an opened module is experimental." ++ + strbrk "In case of problem, close it first.") + + let check_inside_module () = if Lib.is_modtype () then err (str "You can't do that within a Module Type." ++ fnl () ++ str "Close it and try again.") else if Lib.is_module () then - msg_warning - (str "Extraction inside an opened module is experimental.\n" ++ - str "In case of problem, close it first.\n") + warn_extraction_inside_module () let check_inside_section () = if Lib.sections_are_opened () then err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") -let warning_id s = - msg_warning (str ("The identifier "^s^ - " contains __ which is reserved for the extraction")) +let warn_extraction_reserved_identifier = + CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction" + (fun s -> strbrk ("The identifier "^s^ + " contains __ which is reserved for the extraction")) + +let warning_id s = warn_extraction_reserved_identifier s let error_constant r = err (safe_pr_global r ++ str " is not a constant.") @@ -391,9 +404,15 @@ let error_no_module_expr mp = ++ str "some Declare Module outside any Module Type.\n" ++ str "This situation is currently unsupported by the extraction.") -let error_singleton_become_prop id = +let error_singleton_become_prop id og = + let loc = + match og with + | Some g -> fnl () ++ str "in " ++ safe_pr_global g ++ + str " (or in its mutual block)" + | None -> mt () + in err (str "The informative inductive type " ++ pr_id id ++ - str " has a Prop instance.\n" ++ + str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ str "The Ocaml extraction cannot handle this situation yet.\n" ++ @@ -422,7 +441,7 @@ let error_MPfile_as_mod mp b = 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 + decompose_prod (Reduction.whd_all (Global.env ()) typ) in List.rev_map fst rels let msg_of_implicit = function @@ -441,25 +460,28 @@ let error_remaining_implicit k = str "You might also try Unset Extraction SafeImplicits to force" ++ fnl() ++ str "the extraction of unsafe code and review it manually.") +let warn_extraction_remaining_implicit = + CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction" + (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ + strbrk "Extraction SafeImplicits is unset, extracting nonetheless," + ++ strbrk "but this code is potentially unsafe, please 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.") + warn_extraction_remaining_implicit s let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> if not (Library.library_is_loaded dp) then begin match base_mp (Lib.current_mp ()) with | MPfile dp' when not (DirPath.equal dp dp') -> - err (str ("Please load library "^(DirPath.to_string dp^" first."))) + err (str "Please load library " ++ pr_dirpath dp ++ str " first.") | _ -> () end | _ -> () let info_file f = - Flags.if_verbose msg_info + Flags.if_verbose Feedback.msg_info (str ("The file "^f^" has been created by extraction.")) @@ -858,7 +880,7 @@ let extract_constant_inline inline r ids s = | ConstRef kn -> let env = Global.env () in let typ = Global.type_of_global_unsafe (ConstRef kn) in - let typ = Reduction.whd_betadeltaiota env typ in + let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin let nargs = Hook.get use_type_scheme_nb_args env typ in diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b163610..15a08756 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_both_mod_and_cst : - qualid -> module_path -> global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit val warning_id : string -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a @@ -30,7 +29,7 @@ val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : module_path -> module_path -> 'a val error_no_module_expr : module_path -> 'a -val error_singleton_become_prop : Id.t -> 'a +val error_singleton_become_prop : Id.t -> global_reference option -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -- cgit v1.2.3