diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 40 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 10 | ||||
| -rw-r--r-- | plugins/extraction/extraction_plugin.mlpack (renamed from plugins/extraction/extraction_plugin.mllib) | 1 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 10 | ||||
| -rw-r--r-- | plugins/extraction/json.ml | 5 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 8 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 20 |
8 files changed, 42 insertions, 57 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index f2e7c3ede..3c5f6cb72 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -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 @@ -332,12 +333,9 @@ let reset_renaming_tables flag = let modular_rename k id = let s = ascii_of_id id in - let prefix,is_ok = - if upperkind k then "Coq_",is_upper else "coq_",is_lower + 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); - (Id.to_string nextcoq)^"_"^(ascii_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 = 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 ... *) @@ -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 41a068ff3..a03be5743 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 114c5149f..0153348de 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 @@ -76,7 +76,7 @@ type flag = info * scheme let rec flag_of_type env t : flag = let t = whd_betadeltaiota 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) @@ -249,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 @@ -573,7 +573,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 @@ -848,7 +848,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. *) diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack index ad3212434..9184f6501 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mlpack @@ -9,4 +9,3 @@ Scheme Json Extract_env G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index aec958689..19fda4aea 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/json.ml b/plugins/extraction/json.ml index df79c585e..8874afef3 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 b5e8b4804..bd4831130 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 5f83d2949..560fe5aea 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 = @@ -449,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,13 +459,13 @@ let check_loaded_modfile mp = match base_mp mp with 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.")) |