diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 54 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 80 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 5 | ||||
| -rw-r--r-- | plugins/extraction/haskell.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/json.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 8 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 28 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 2 |
9 files changed, 105 insertions, 86 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bb9e8e5f5b..3c5f6cb720 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 41a068ff38..a03be5743f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -19,7 +19,6 @@ 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 @@ -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 6c57bc2bbd..e40621965f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -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 catched + 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. *) @@ -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 @@ -934,11 +946,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 +982,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 +1001,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 +1032,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/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index ca4e13e125..0a8cb0ccd3 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -14,7 +14,6 @@ open Genarg open Stdarg open Constrarg open Pcoq.Prim -open Pcoq.Constr open Pp open Names open Nameops @@ -102,7 +101,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 @@ -124,7 +123,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 22519e3471..764223621e 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -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 df79c585e5..8874afef33 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) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b5e8b48044..bd48311308 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -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/table.ml b/plugins/extraction/table.ml index 466c8054b8..560fe5aea8 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -300,7 +300,7 @@ let warning_axioms () = 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 + Feedback.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 ()) @@ -310,7 +310,7 @@ let warning_axioms () = else begin let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were" in - msg_warning + Feedback.msg_warning (str ("The following logical "^s^" encountered:") ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") @@ -326,12 +326,12 @@ let warning_opaques accessed = else let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in if accessed then - msg_warning + Feedback.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 + Feedback.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 () ++ @@ -339,7 +339,7 @@ let warning_opaques accessed = ++ fnl ()) let warning_both_mod_and_cst q mp r = - msg_warning + Feedback.msg_warning (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ str "do you mean module " ++ pr_long_mp mp ++ @@ -358,7 +358,7 @@ let check_inside_module () = 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 + Feedback.msg_warning (str "Extraction inside an opened module is experimental.\n" ++ str "In case of problem, close it first.\n") @@ -368,7 +368,7 @@ let check_inside_section () = str "Close it and try again.") let warning_id s = - msg_warning (str ("The identifier "^s^ + Feedback.msg_warning (str ("The identifier "^s^ " contains __ which is reserved for the extraction")) let error_constant r = @@ -391,9 +391,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" ++ @@ -443,7 +449,7 @@ let error_remaining_implicit k = let warning_remaining_implicit k = let s = msg_of_implicit k in - msg_warning + Feedback.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.") @@ -459,7 +465,7 @@ let check_loaded_modfile mp = match base_mp mp with | _ -> () let info_file f = - Flags.if_verbose msg_info + Flags.if_verbose Feedback.msg_info (str ("The file "^f^" has been created by extraction.")) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b163610e9..62c20bd3a7 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -30,7 +30,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 |