diff options
author | 2010-05-21 16:13:58 +0000 | |
---|---|---|
committer | 2010-05-21 16:13:58 +0000 | |
commit | 9545a01076cc7b79d0d3278b1ba12e3249149716 (patch) | |
tree | b66405b976619de4a3d2d45369c034629c06ac87 /plugins/extraction | |
parent | 63fe9ca9438693fcf4d601c05f77a4db50588b40 (diff) |
Extract Inductive is now possible toward non-inductive types (e.g. nat => int)
For instance:
Extract Inductive nat => int [ "0" "succ" ]
"(fun fO fS n => if n=0 then fO () else fS (n-1))".
See Extraction.v for more details and caveat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 5 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 8 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 7 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 2 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 36 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 6 |
8 files changed, 74 insertions, 10 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index f8354f52e..b2256c471 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -124,6 +124,7 @@ VERNAC COMMAND EXTEND ExtractionInlinedConstant END VERNAC COMMAND EXTEND ExtractionInductive -| [ "Extract" "Inductive" global(x) "=>" mlname(id) "[" mlname_list(idl) "]" ] - -> [ extract_inductive x (id,idl) ] +| [ "Extract" "Inductive" global(x) "=>" + mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] + -> [ extract_inductive x id idl o ] END diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 84202d539..c1ed62b34 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -146,6 +146,14 @@ let rec pp_expr par env args = assert (args=[]); pp_par par (pp_global Cons r ++ spc () ++ prlist_with_sep spc (pp_expr true env []) args') + | MLcase (_,t, pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr true env [] t) | MLcase ((_,factors),t, pv) -> apply (pp_par par' (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index e936d2dbf..a1e59e2a0 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -96,15 +96,16 @@ type ml_ident = | Id of identifier | Tmp of identifier -type ml_ast = +type ml_branch = global_reference * ml_ident list * ml_ast + +and ml_ast = | MLrel of int | MLapp of ml_ast * ml_ast list | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference | MLcons of inductive_info * global_reference * ml_ast list - | MLcase of (inductive_info*case_info) * ml_ast * - (global_reference * ml_ident list * ml_ast) array + | MLcase of (inductive_info*case_info) * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 42787a540..7e9cfbeed 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -88,7 +88,7 @@ val collect_lams : ml_ast -> ml_ident list * ml_ast val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast val remove_n_lams : int -> ml_ast -> ml_ast val nb_lams : ml_ast -> int - +val named_lams : ml_ident list -> ml_ast -> ml_ast val dummy_lams : ml_ast -> int -> ml_ast val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 3d980e65f..137ae9047 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -219,6 +219,14 @@ let rec pp_expr par env args = if str_global Cons r = "" (* hack Extract Inductive prod *) then tuple else pp_par par (pp_global Cons r ++ spc () ++ tuple) + | MLcase (_, t, pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr true env [] t) | MLcase ((i,factors), t, pv) -> let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) @@ -328,7 +336,7 @@ and pp_function env t = let bl,t' = collect_lams t in let bl,env' = push_vars (List.map id_of_mlid bl) env in match t' with - | MLcase(i,MLrel 1,pv) when fst i=Standard -> + | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) -> if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 6a44812da..f7a0b5a53 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -94,7 +94,15 @@ let rec pp_expr env args = prlist_with_sep spc (pp_cons_args env) args') in if i = Coinductive then paren (str "delay " ++ st) else st - | MLcase ((i,_),t, pv) -> + | MLcase (_,t,pv) when is_custom_match pv -> + let mkfun (_,ids,e) = + if ids <> [] then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + hov 2 (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr env [] t) + | MLcase ((i,_),t, pv) -> let e = if i <> Coinductive then pp_expr env [] t else paren (str "force" ++ spc () ++ pp_expr env [] t) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 8ac6545bb..df61375c5 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -646,6 +646,24 @@ let find_custom r = snd (Refmap.find r !customs) let find_type_custom r = Refmap.find r !customs +let custom_matchs = ref Refmap.empty + +let add_custom_match r s = + custom_matchs := Refmap.add r s !custom_matchs + +let indref_of_match pv = + if Array.length pv = 0 then raise Not_found; + match pv.(0) with + | (ConstructRef (ip,_), _, _) -> IndRef ip + | _ -> raise Not_found + +let is_custom_match pv = + try Refmap.mem (indref_of_match pv) !custom_matchs + with Not_found -> false + +let find_custom_match pv = + Refmap.find (indref_of_match pv) !custom_matchs + (* Registration of operations for rollback. *) let (in_customs,_) = @@ -663,6 +681,20 @@ let _ = declare_summary "ML extractions" unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap.empty) } +let (in_custom_matchs,_) = + declare_object + {(default_object "ML extractions custom matchs") with + cache_function = (fun (_,(r,s)) -> add_custom_match r s); + load_function = (fun _ (_,(r,s)) -> add_custom_match r s); + classify_function = (fun o -> Substitute o); + subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s)) + } + +let _ = declare_summary "ML extractions custom match" + { freeze_function = (fun () -> !custom_matchs); + unfreeze_function = ((:=) custom_matchs); + init_function = (fun () -> custom_matchs := Refmap.empty) } + (* Grammar entries. *) let extract_constant_inline inline r ids s = @@ -683,7 +715,7 @@ let extract_constant_inline inline r ids s = | _ -> error_constant g -let extract_inductive r (s,l) = +let extract_inductive r s l optstr = check_inside_section (); let g = Nametab.global r in match g with @@ -693,6 +725,8 @@ let extract_inductive r (s,l) = 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)); + Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s))) + optstr; list_iter_i (fun j s -> let g = ConstructRef (ip,succ j) in diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index f02e73190..49108cf52 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -135,6 +135,9 @@ val is_inline_custom : global_reference -> bool val find_custom : global_reference -> string val find_type_custom : global_reference -> string list * string +val is_custom_match : ml_branch array -> bool +val find_custom_match : ml_branch array -> string + (*s Extraction commands. *) val extraction_language : lang -> unit @@ -143,7 +146,8 @@ val print_extraction_inline : unit -> unit val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit -val extract_inductive : reference -> string * string list -> unit +val extract_inductive : + reference -> string -> string list -> string option -> unit val extraction_implicit : reference -> int list -> unit (*s Table of blacklisted filenames *) |