diff options
| -rw-r--r-- | contrib/extraction/extraction.ml | 16 | ||||
| -rw-r--r-- | contrib/extraction/g_extraction.ml4 | 6 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 24 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 69 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 11 |
5 files changed, 69 insertions, 57 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index ba925b40b5..05ad8f48fe 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -88,6 +88,15 @@ let rec type_sign env c = (is_info_scheme env t)::(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 + | 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 + | _ -> 0 + +let _ = ugly_hack_arity_nb_args := type_scheme_nb_args + (*s [type_sign_vl] does the same, plus a type var list. *) let rec type_sign_vl env c = @@ -105,7 +114,6 @@ let rec nb_default_params env c = if is_default env t then n+1 else n | _ -> 0 - (*S Management of type variable contexts. *) (* A De Bruijn variable context (db) is a context for translating Coq [Rel] @@ -742,10 +750,8 @@ let extract_constant env kn cb = | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with | (Info,TypeScheme) -> - if isSort typ then - if is_custom (long_r r) then Dtype (r, [], Tunknown) - else error_axiom r - else error_axiom_scheme r + if is_custom (long_r r) then Dtype (r, [], Tunknown) + else error_axiom r | (Info,Default) -> if is_custom (long_r r) then let t = snd (record_constant_type env kn (Some typ)) in diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index 46021af732..ae79dda81e 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -82,13 +82,13 @@ END (* Overriding of a Coq object by an ML one *) VERNAC COMMAND EXTEND ExtractionConstant -| [ "Extract" "Constant" global(x) "=>" mlname(y) ] - -> [ extract_constant_inline false x y ] +| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ] + -> [ extract_constant_inline false x idl y ] END VERNAC COMMAND EXTEND ExtractionInlinedConstant | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ] - -> [ extract_constant_inline true x y ] + -> [ extract_constant_inline true x [] y ] END VERNAC COMMAND EXTEND ExtractionInductive diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index d65a467102..5fb08d091c 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -391,6 +391,9 @@ let rec pp_Dfix init i ((rv,c,t) as fix) = let pp_parameters l = (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) +let pp_string_parameters l = + (pp_boxed_tuple str l ++ space_if (l<>[])) + let pp_one_ind prefix ip pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = @@ -485,9 +488,12 @@ let pp_decl mp = if is_inline_custom r then failwith "empty phrase" else let l = rename_tvars keywords l in - let def = try str (find_custom r) with not_found -> pp_type false l t + let ids, def = try + let ids,s = find_type_custom r in + pp_string_parameters ids, str s + with not_found -> pp_parameters l, pp_type false l t in - hov 2 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ + hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ str "=" ++ spc () ++ def) | Dterm (r, a, t) -> if is_inline_custom r then failwith "empty phrase" @@ -519,15 +525,17 @@ let pp_spec mp = if is_inline_custom r then failwith "empty phrase" else let l = rename_tvars keywords vl in - let def = - try str "= " ++ str (find_custom r) + let ids, def = + try + let ids, s = find_type_custom r in + pp_string_parameters ids, str "= " ++ str s with not_found -> + let ids = pp_parameters l in match ot with - | None -> mt () - | Some t -> str "=" ++ spc () ++ pp_type false l t + | None -> ids, mt () + | Some t -> ids, str "=" ++ spc () ++ pp_type false l t in - hov 2 (str "type" ++ spc () ++ pp_parameters l ++ - pp_global r ++ spc () ++ def) + hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def) let rec pp_structure_elem mp = function | (_,SEdecl d) -> pp_decl mp d diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 9f0b2cf73a..189bcbbf6e 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -189,9 +189,10 @@ let pr_global r = pr_id (id_of_global r) let err s = errorlabstrm "Extraction" s -let error_axiom_scheme r = - err (str "Extraction cannot accept the type scheme axiom " ++ spc () ++ - pr_global r ++ spc () ++ str ".") +let error_axiom_scheme r i = + err (str "The type scheme axiom " ++ spc () ++ + pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ + str " type variable(s).") let error_axiom r = err (str "You must specify an extraction for axiom" ++ spc () ++ @@ -381,30 +382,22 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) (*s Extract Constant/Inductive. *) -type kind = Term | Type | Ind | Construct +let ugly_hack_arity_nb_args = ref (fun _ _ -> 0) -let check_term_or_type r = match r with +let check_term_or_type r ids = match r with | ConstRef sp -> let env = Global.env () in let typ = Environ.constant_type env sp in let typ = Reduction.whd_betadeltaiota env typ in - if isSort typ then (r,Type) - else if Reduction.is_arity env typ then error_type_scheme r - else (r,Term) + if Reduction.is_arity env typ + then + let nargs = !ugly_hack_arity_nb_args env typ in + if List.length ids <> nargs then error_axiom_scheme r nargs | _ -> error_constant r let customs = ref Refmap.empty -let all_customs () = - Refmap.fold (fun r _ -> Refset.add r) !customs Refset.empty - -let term_customs () = - Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l) !customs [] - -let type_customs () = - Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) !customs [] - -let add_custom r k s = customs := Refmap.add r (k,s) !customs +let add_custom r ids s = customs := Refmap.add r (ids,s) !customs let is_custom r = Refmap.mem (long_r r) !customs @@ -413,13 +406,15 @@ let is_inline_custom r = let find_custom r = snd (Refmap.find (long_r r) !customs) +let find_type_custom r = Refmap.find (long_r r) !customs + (* Registration of operations for rollback. *) let (in_customs,_) = declare_object {(default_object "ML extractions") with - cache_function = (fun (_,(r,k,s)) -> add_custom r k s); - load_function = (fun _ (_,(r,k,s)) -> add_custom r k s); + cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); + load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); export_function = (fun x -> Some x)} let _ = declare_summary "ML extractions" @@ -430,26 +425,28 @@ let _ = declare_summary "ML extractions" (* Grammar entries. *) -let extract_constant_inline inline r s = +let extract_constant_inline inline r ids s = if is_something_opened () then error_section (); - let g,k = check_term_or_type (Nametab.global r) in + let g = Nametab.global r in + check_term_or_type g ids; Lib.add_anonymous_leaf (inline_extraction (inline,[g])); - Lib.add_anonymous_leaf (in_customs (g,k,s)) + Lib.add_anonymous_leaf (in_customs (g,ids,s)) let extract_inductive r (s,l) = if is_something_opened () then error_section (); - let g = Nametab.global r in match g with - | IndRef ((kn,i) as ip) -> - let mib = Global.lookup_mind kn in - let n = Array.length mib.mind_packets.(i).mind_consnames in - if n <> List.length l then error_nb_cons (); - Lib.add_anonymous_leaf (inline_extraction (true,[g])); - Lib.add_anonymous_leaf (in_customs (g,Ind,s)); - list_iter_i - (fun j s -> - let g = ConstructRef (ip,succ j) in - Lib.add_anonymous_leaf (inline_extraction (true,[g])); - Lib.add_anonymous_leaf (in_customs (g,Construct,s))) l - | _ -> error_inductive g + let g = Nametab.global r in + match g with + | IndRef ((kn,i) as ip) -> + let mib = Global.lookup_mind kn in + let n = Array.length mib.mind_packets.(i).mind_consnames in + if n <> List.length l then error_nb_cons (); + Lib.add_anonymous_leaf (inline_extraction (true,[g])); + Lib.add_anonymous_leaf (in_customs (g,[],s)); + list_iter_i + (fun j s -> + let g = 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/contrib/extraction/table.mli b/contrib/extraction/table.mli index e4169a9bfe..3fbdbc209d 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -16,7 +16,7 @@ val id_of_global : global_reference -> identifier (*s Warning and Error messages. *) -val error_axiom_scheme : global_reference -> 'a +val error_axiom_scheme : global_reference -> int -> 'a val error_axiom : global_reference -> 'a val warning_axiom : global_reference -> unit val error_section : unit -> 'a @@ -94,12 +94,12 @@ val to_keep : global_reference -> bool (*s Table for user-given custom ML extractions. *) +val ugly_hack_arity_nb_args : (Environ.env -> Term.constr -> int) ref + val is_custom : global_reference -> bool val is_inline_custom : global_reference -> bool val find_custom : global_reference -> string -val all_customs : unit -> Refset.t -val type_customs : unit -> (global_reference * string) list -val term_customs : unit -> (global_reference * string) list +val find_type_custom : global_reference -> string list * string (*s Extraction commands. *) @@ -107,7 +107,8 @@ val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit val print_extraction_inline : unit -> unit val reset_extraction_inline : unit -> unit -val extract_constant_inline : bool -> reference -> string -> unit +val extract_constant_inline : + bool -> reference -> string list -> string -> unit val extract_inductive : reference -> string * string list -> unit |