aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/extraction/common.ml31
-rw-r--r--plugins/extraction/common.mli10
-rw-r--r--plugins/extraction/extract_env.mli5
-rw-r--r--plugins/extraction/extraction.ml15
-rw-r--r--plugins/extraction/haskell.ml122
-rw-r--r--plugins/extraction/miniml.mli39
-rw-r--r--plugins/extraction/mlutil.ml242
-rw-r--r--plugins/extraction/mlutil.mli6
-rw-r--r--plugins/extraction/modutil.ml22
-rw-r--r--plugins/extraction/ocaml.ml310
-rw-r--r--plugins/extraction/scheme.ml25
-rw-r--r--plugins/extraction/table.ml71
-rw-r--r--plugins/extraction/table.mli8
-rw-r--r--test-suite/success/extraction.v2
14 files changed, 536 insertions, 372 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 66ec446f0..0bd5b8434 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -33,17 +33,41 @@ let is_mp_bound = function MPbound _ -> true | _ -> false
let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
+
let pp_apply st par args = match args with
| [] -> st
| _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+(** Same as [pp_apply], but with also protection of the head by parenthesis *)
+
+let pp_apply2 st par args =
+ let par' = args <> [] || par in
+ pp_apply (pp_par par' st) par args
+
let pr_binding = function
| [] -> mt ()
| l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+let pp_tuple_light f = function
+ | [] -> mt ()
+ | [x] -> f true x
+ | l ->
+ pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
+
+let pp_tuple f = function
+ | [] -> mt ()
+ | [x] -> f x
+ | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
+
+let pp_boxed_tuple f = function
+ | [] -> mt ()
+ | [x] -> f x
+ | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
+
(** By default, in module Format, you can do horizontal placing of blocks
even if they include newlines, as long as the number of chars in the
- blocks are less that a line length. To avoid this awkward situation,
+ blocks is less that a line length. To avoid this awkward situation,
we attach a big virtual size to [fnl] newlines. *)
let fnl () = stras (1000000,"") ++ fnl ()
@@ -348,12 +372,13 @@ let ref_renaming_fun (k,r) =
let l = mp_renaming mp in
let l = if lang () <> Ocaml && not (modular ()) then [""] else l in
let s =
+ let idg = safe_basename_of_global r in
if l = [""] (* this happens only at toplevel of the monolithic case *)
then
let globs = Idset.elements (get_global_ids ()) in
- let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in
+ let id = next_ident_away (kindcase_id k idg) globs in
string_of_id id
- else modular_rename k (safe_basename_of_global r)
+ else modular_rename k idg
in
add_global_ids (id_of_string s);
s::l
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 1d8fe77ab..02a496bec 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -22,7 +22,17 @@ val fnl2 : unit -> std_ppcmds
val space_if : bool -> std_ppcmds
val pp_par : bool -> std_ppcmds -> std_ppcmds
+
+(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+
+(** Same as [pp_apply], but with also protection of the head by parenthesis *)
+val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+
+val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+
val pr_binding : identifier list -> std_ppcmds
val rename_id : identifier -> Idset.t -> identifier
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 70783b4f9..e587bf212 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -20,3 +20,8 @@ val extraction_library : bool -> identifier -> unit
val mono_environment :
global_reference list -> module_path list -> Miniml.ml_structure
+
+(* Used by the Relation Extraction plugin *)
+
+val print_one_decl :
+ Miniml.ml_structure -> module_path -> Miniml.ml_decl -> unit
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b780b64bb..549830fe7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -476,6 +476,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
ind_equiv = equiv }
in
add_ind kn mib i;
+ add_inductive_kind kn i.ind_kind;
i
(*s [extract_type_cons] extracts the type of an inductive
@@ -572,6 +573,8 @@ let rec extract_term env mle mlt c args =
| LetIn (n, c1, t1, c2) ->
let id = id_of_name n in
let env' = push_rel (Name id, Some 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
(try
check_default env t1;
@@ -735,8 +738,8 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
| Tglob (_,l) -> List.map type_simpl l
| _ -> assert false
in
- let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
- put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
+ let typ = Tglob(IndRef ip, typeargs) in
+ put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla))
in
(* Different situations depending of the number of arguments: *)
if la < params_nb then
@@ -800,22 +803,22 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
(* We suppress dummy arguments according to signature. *)
let ids,e = case_expunge s e in
let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
- (r, List.rev ids, e')
+ (List.rev ids, Pusual r, e')
in
if mi.ind_kind = Singleton then
begin
(* Informative singleton case: *)
(* [match c with C i -> t] becomes [let i = c' in t'] *)
assert (br_size = 1);
- let (_,ids,e') = extract_branch 0 in
+ let (ids,_,e') = extract_branch 0 in
assert (List.length ids = 1);
MLletin (tmp_id (List.hd ids),a,e')
end
else
(* Standard case: we apply [extract_branch]. *)
let typs = List.map type_simpl (Array.to_list metas) in
- let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
- in MLcase (info, a, Array.init br_size extract_branch)
+ let typ = Tglob (IndRef ip,typs) in
+ MLcase (typ, a, Array.init br_size extract_branch)
(*s Extraction of a (co)-fixpoint. *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 32ad45c93..96731ed27 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -111,8 +111,8 @@ let expr_needs_par = function
let rec pp_expr par env args =
- let par' = args <> [] || par
- and apply st = pp_apply st par args in
+ let apply st = pp_apply st par args
+ and apply2 st = pp_apply2 st par args in
function
| MLrel n ->
let id = get_db_name n env in apply (pr_id id)
@@ -123,7 +123,7 @@ let rec pp_expr par env args =
let fl,a' = collect_lams a in
let fl,env' = push_vars (List.map id_of_mlid fl) env in
let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
- apply (pp_par par' st)
+ apply2 st
| MLletin (id,a1,a2) ->
let i,env' = push_vars [id_of_mlid id] env in
let pp_id = pr_id (List.hd i)
@@ -133,37 +133,42 @@ let rec pp_expr par env args =
str "let {" ++ cut () ++
hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
in
- apply
- (pp_par par'
- (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
- spc () ++ hov 0 pp_a2)))
+ apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
+ spc () ++ hov 0 pp_a2))
| MLglob r ->
apply (pp_global Term r)
- | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
- | MLcons (_,r,[]) ->
- assert (args=[]); pp_global Cons r
- | MLcons (_,r,[a]) ->
- assert (args=[]);
- pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
- | MLcons (_,r,args') ->
- assert (args=[]);
- pp_par par (pp_global Cons r ++ spc () ++
- prlist_with_sep spc (pp_expr true env []) args')
+ | MLcons (_,r,a) as c ->
+ assert (args=[]);
+ begin match a with
+ | _ when is_native_char c -> pp_native_char c
+ | [] -> pp_global Cons r
+ | [a] ->
+ pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
+ | _ ->
+ pp_par par (pp_global Cons r ++ spc () ++
+ prlist_with_sep spc (pp_expr true env []) a)
+ end
+ | MLtuple l ->
+ assert (args=[]);
+ pp_boxed_tuple (pp_expr true env []) l
| MLcase (_,t, pv) when is_custom_match pv ->
- let mkfun (_,ids,e) =
+ if not (is_regular_match pv) then
+ error "Cannot mix yet user-given match and general patterns.";
+ let mkfun (ids,_,e) =
if ids <> [] then named_lams (List.rev ids) e
else dummy_lams (ast_lift 1 e) 1
in
- apply
- (pp_par par'
- (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 (info,t, pv) ->
- apply (pp_par par'
- (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
- fnl () ++ pp_pat env info pv)))
+ let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
+ let inner =
+ str (find_custom_match pv) ++ fnl () ++
+ prvect pp_branch pv ++
+ pp_expr true env [] t
+ in
+ apply2 (hov 2 inner)
+ | MLcase (typ,t,pv) ->
+ apply2
+ (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
+ fnl () ++ pp_pat env pv))
| 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
@@ -176,44 +181,31 @@ let rec pp_expr par env args =
pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
-and pp_pat env info pv =
- let pp_one_pat (name,ids,t) =
- let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
- let par = expr_needs_par t in
- hov 2 (str " " ++ pp_global Cons name ++
- (match ids with
- | [] -> mt ()
- | _ -> (str " " ++
- prlist_with_sep spc pr_id (List.rev ids))) ++
- str " ->" ++ spc () ++ pp_expr par env' [] t)
- in
- let factor_br, factor_set = try match info.m_same with
- | BranchFun ints ->
- let i = Intset.choose ints in
- branch_as_fun info.m_typs pv.(i), ints
- | BranchCst ints ->
- let i = Intset.choose ints in
- ast_pop (branch_as_cst pv.(i)), ints
- | BranchNone -> MLdummy, Intset.empty
- with _ -> MLdummy, Intset.empty
- in
- let last = Array.length pv - 1 in
+and pp_cons_pat par r ppl =
+ pp_par par
+ (pp_global Cons r ++ space_if (ppl<>[]) ++ prlist_with_sep spc identity ppl)
+
+and pp_gen_pat par ids env = function
+ | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l)
+ | Pusual r -> pp_cons_pat par r (List.map pr_id ids)
+ | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l
+ | Pwild -> str "_"
+ | Prel n -> pr_id (get_db_name n env)
+
+and pp_one_pat env (ids,p,t) =
+ let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
+ hov 2 (str " " ++
+ pp_gen_pat false (List.rev ids') env' p ++
+ str " ->" ++ spc () ++
+ pp_expr (expr_needs_par t) env' [] t)
+
+and pp_pat env pv =
prvecti
- (fun i x -> if Intset.mem i factor_set then mt () else
- (pp_one_pat pv.(i) ++
- if i = last && Intset.is_empty factor_set then str "}" else
- (str ";" ++ fnl ()))) pv
- ++
- if Intset.is_empty factor_set then mt () else
- let par = expr_needs_par factor_br in
- match info.m_same with
- | BranchFun _ ->
- let ids, env' = push_vars [anonymous_name] env in
- hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
- pp_expr par env' [] factor_br ++ str "}")
- | BranchCst _ ->
- hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}")
- | BranchNone -> mt ()
+ (fun i x ->
+ pp_one_pat env pv.(i) ++
+ if i = Array.length pv - 1 then str "}" else
+ (str ";" ++ fnl ()))
+ pv
(*s names of the functions ([ids]) are already pushed in [env],
and passed here just for convenience. *)
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index edff48c85..0bf1ff952 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -97,28 +97,17 @@ type ml_ident =
| Tmp of identifier
(** We now store some typing information on constructors
- and cases to avoid type-unsafe optimisations.
- For cases, we also store the set of branches to merge
- in a common pattern, either "_ -> c" or "x -> f x"
+ and cases to avoid type-unsafe optimisations. This will be
+ either the type of the applied constructor or the type
+ of the head of the match.
*)
-type constructor_info = {
- c_kind : inductive_kind;
- c_typs : ml_type list;
-}
-
-type branch_same =
- | BranchNone
- | BranchFun of Intset.t
- | BranchCst of Intset.t
+(** Nota : the constructor [MLtuple] and the extension of [MLcase]
+ to general patterns have been proposed by P.N. Tollitte for
+ his Relation Extraction plugin. [MLtuple] is currently not
+ used by the main extraction, as well as deep patterns. *)
-type match_info = {
- m_kind : inductive_kind;
- m_typs : ml_type list;
- m_same : branch_same
-}
-
-type ml_branch = global_reference * ml_ident list * ml_ast
+type ml_branch = ml_ident list * ml_pattern * ml_ast
and ml_ast =
| MLrel of int
@@ -126,14 +115,22 @@ and ml_ast =
| MLlam of ml_ident * ml_ast
| MLletin of ml_ident * ml_ast * ml_ast
| MLglob of global_reference
- | MLcons of constructor_info * global_reference * ml_ast list
- | MLcase of match_info * ml_ast * ml_branch array
+ | MLcons of ml_type * global_reference * ml_ast list
+ | MLtuple of ml_ast list
+ | MLcase of ml_type * ml_ast * ml_branch array
| MLfix of int * identifier array * ml_ast array
| MLexn of string
| MLdummy
| MLaxiom
| MLmagic of ml_ast
+and ml_pattern =
+ | Pcons of global_reference * ml_pattern list
+ | Ptuple of ml_pattern list
+ | Prel of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
+ | Pwild
+ | Pusual of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+
(*s ML declarations. *)
type ml_decl =
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 8a0d1a05f..5cef4764d 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -359,54 +359,61 @@ let ast_iter_rel f =
| MLlam (_,a) -> iter (n+1) a
| MLletin (_,a,b) -> iter n a; iter (n+1) b
| MLcase (_,a,v) ->
- iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
+ iter n a; Array.iter (fun (l,_,t) -> iter (n + (List.length l)) t) v
| MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
| MLapp (a,l) -> iter n a; List.iter (iter n) l
- | MLcons (_,_,l) -> List.iter (iter n) l
+ | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l
| MLmagic a -> iter n a
| MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
in iter 0
(*s Map over asts. *)
-let ast_map_case f (c,ids,a) = (c,ids,f a)
+let ast_map_branch f (c,ids,a) = (c,ids,f a)
+
+(* Warning: in [ast_map] we assume that [f] does not change the type
+ of [MLcons] and of [MLcase] heads *)
let ast_map f = function
| MLlam (i,a) -> MLlam (i, f a)
| MLletin (i,a,b) -> MLletin (i, f a, f b)
- | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
+ | MLcase (typ,a,v) -> MLcase (typ,f a, Array.map (ast_map_branch f) v)
| MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
| MLapp (a,l) -> MLapp (f a, List.map f l)
- | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
+ | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
+ | MLtuple l -> MLtuple (List.map f l)
| MLmagic a -> MLmagic (f a)
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
(*s Map over asts, with binding depth as parameter. *)
-let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
+let ast_map_lift_branch f n (ids,p,a) = (ids,p, f (n+(List.length ids)) a)
+
+(* Same warning as for [ast_map]... *)
let ast_map_lift f n = function
| MLlam (i,a) -> MLlam (i, f (n+1) a)
| MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
- | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
+ | MLcase (typ,a,v) -> MLcase (typ,f n a,Array.map (ast_map_lift_branch f n) v)
| MLfix (i,ids,v) ->
let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
| MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
- | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
+ | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
+ | MLtuple l -> MLtuple (List.map (f n) l)
| MLmagic a -> MLmagic (f n a)
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
(*s Iter over asts. *)
-let ast_iter_case f (c,ids,a) = f a
+let ast_iter_branch f (c,ids,a) = f a
let ast_iter f = function
| MLlam (i,a) -> f a
| MLletin (i,a,b) -> f a; f b
- | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
+ | MLcase (_,a,v) -> f a; Array.iter (ast_iter_branch f) v
| MLfix (i,ids,v) -> Array.iter f v
| MLapp (a,l) -> f a; List.iter f l
- | MLcons (_,c,l) -> List.iter f l
+ | MLcons (_,_,l) | MLtuple l -> List.iter f l
| MLmagic a -> f a
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
@@ -436,13 +443,13 @@ let nb_occur_match =
| MLcase(_,a,v) ->
(nb k a) +
Array.fold_left
- (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
+ (fun r (ids,_,a) -> max r (nb (k+(List.length ids)) a)) 0 v
| MLletin (_,a,b) -> (nb k a) + (nb (k+1) b)
| MLfix (_,ids,v) -> let k = k+(Array.length ids) in
Array.fold_left (fun r a -> r+(nb k a)) 0 v
| MLlam (_,a) -> nb (k+1) a
| MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
- | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
+ | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
| MLmagic a -> nb k a
| MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
in nb 1
@@ -502,6 +509,39 @@ let gen_subst v d t =
| a -> ast_map_lift subst n a
in subst 0 t
+(*S Operations concerning match patterns *)
+
+let is_basic_pattern = function
+ | Prel _ | Pwild -> true
+ | Pusual _ | Pcons _ | Ptuple _ -> false
+
+let has_deep_pattern br =
+ let deep = function
+ | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l)
+ | Pusual _ | Prel _ | Pwild -> false
+ in
+ array_exists (function (_,pat,_) -> deep pat) br
+
+let is_regular_match br =
+ if Array.length br <> 0 then false (* empty match becomes MLexn *)
+ else
+ try
+ let get_r (ids,pat,c) =
+ match pat with
+ | Pusual r -> r
+ | Pcons (r,l) ->
+ if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+ then raise Impossible;
+ r
+ | _ -> raise Impossible
+ in
+ let ind = match get_r br.(0) with
+ | ConstructRef (ind,_) -> ind
+ | _ -> raise Impossible
+ in
+ array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+ with Impossible -> false
+
(*S Operations concerning lambdas. *)
(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
@@ -650,26 +690,31 @@ let rec ast_glob_subst s t = match t with
expansion of type definitions.
*)
-(*s [branch_as_function b typs (r,l,c)] tries to see branch [c]
+(*s [branch_as_function b typ (l,p,c)] tries to see branch [c]
as a function [f] applied to [MLcons(r,l)]. For that it transforms
any [MLcons(r,l)] in [MLrel 1] and raises [Impossible]
if any variable in [l] occurs outside such a [MLcons] *)
-let branch_as_fun typs (r,l,c) =
+let branch_as_fun typ (l,p,c) =
let nargs = List.length l in
+ let cons = match p with
+ | Pusual r -> MLcons (typ, r, eta_args nargs)
+ | Pcons (r,pl) ->
+ let pat2rel = function Prel i -> MLrel i | _ -> raise Impossible in
+ MLcons (typ, r, List.map pat2rel pl)
+ | _ -> raise Impossible
+ in
let rec genrec n = function
| MLrel i as c ->
let i' = i-n in
if i'<1 then c
else if i'>nargs then MLrel (i-nargs+1)
else raise Impossible
- | MLcons(i,r',args) when
- r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs ->
- MLrel (n+1)
+ | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
| a -> ast_map_lift genrec n a
in genrec 0 c
-(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant
+(*s [branch_as_cst (l,p,c)] tries to see branch [c] as a constant
independent from the pattern [MLcons(r,l)]. For that is raises [Impossible]
if any variable in [l] occurs in [c], and otherwise returns [c] lifted to
appear like a function with one arg (for uniformity with [branch_as_fun]).
@@ -677,7 +722,7 @@ let branch_as_fun typs (r,l,c) =
empty, i.e. when [r] is a constant constructor
*)
-let branch_as_cst (_,l,c) =
+let branch_as_cst (l,_,c) =
let n = List.length l in
if ast_occurs_itvl 1 n c then raise Impossible;
ast_lift (1-n) c
@@ -716,20 +761,27 @@ let census_add, census_max, census_clean =
constant.
*)
-let factor_branches o typs br =
- census_clean ();
- for i = 0 to Array.length br - 1 do
- if o.opt_case_idr then
- (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ());
- if o.opt_case_cst then
- (try census_add (branch_as_cst br.(i)) i with Impossible -> ());
- done;
- let br_factor, br_set = census_max MLdummy in
- census_clean ();
- let n = Intset.cardinal br_set in
- if n = 0 then None
- else if Array.length br >= 2 && n < 2 then None
- else Some (br_factor, br_set)
+let is_opt_pat (_,p,_) = match p with
+ | Prel _ | Pwild -> true
+ | _ -> false
+
+let factor_branches o typ br =
+ if array_exists is_opt_pat br then None (* already optimized *)
+ else begin
+ census_clean ();
+ for i = 0 to Array.length br - 1 do
+ if o.opt_case_idr then
+ (try census_add (branch_as_fun typ br.(i)) i with Impossible -> ());
+ if o.opt_case_cst then
+ (try census_add (branch_as_cst br.(i)) i with Impossible -> ());
+ done;
+ let br_factor, br_set = census_max MLdummy in
+ census_clean ();
+ let n = Intset.cardinal br_set in
+ if n = 0 then None
+ else if Array.length br >= 2 && n < 2 then None
+ else Some (br_factor, br_set)
+ end
(*s If all branches are functions, try to permut the case and the functions. *)
@@ -752,14 +804,14 @@ let rec permut_case_fun br acc =
let br = Array.copy br in
let ids = ref [] in
for i = 0 to Array.length br - 1 do
- let (r,l,t) = br.(i) in
+ let (l,p,t) = br.(i) in
let local_nb = nb_lams t in
if local_nb < !nb then (* t = MLexn ... *)
- br.(i) <- (r,l,remove_n_lams local_nb t)
+ br.(i) <- (l,p,remove_n_lams local_nb t)
else begin
let local_ids,t = collect_n_lams !nb t in
ids := merge_ids !ids local_ids;
- br.(i) <- (r,l,permut_rels !nb (List.length l) t)
+ br.(i) <- (l,p,permut_rels !nb (List.length l) t)
end
done;
(!ids,br)
@@ -767,32 +819,43 @@ let rec permut_case_fun br acc =
(*S Generalized iota-reduction. *)
-(* Definition of a generalized iota-redex: it's a [MLcase(e,_)]
- with [(is_iota_gen e)=true]. Any generalized iota-redex is
- transformed into beta-redexes. *)
-
-let rec is_iota_gen = function
- | MLcons _ -> true
- | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
- | _ -> false
-
-let constructor_index = function
- | ConstructRef (_,j) -> pred j
- | _ -> assert false
-
-let iota_gen br =
+(* Definition of a generalized iota-redex: it's a [MLcase(e,br)]
+ where the head [e] is a [MLcons] or made of [MLcase]'s with
+ [MLcons] as leaf branches.
+ A generalized iota-redex is transformed into beta-redexes. *)
+
+(* In [iota_red], we try to simplify a [MLcase(_,MLcons(typ,r,a),br)].
+ Argument [i] is the branch we consider, we should lift what
+ comes from [br] by [lift] *)
+
+let rec iota_red i lift br ((typ,r,a) as cons) =
+ if i >= Array.length br then raise Impossible;
+ let (ids,p,c) = br.(i) in
+ match p with
+ | Pusual r' | Pcons (r',_) when r'<>r -> iota_red (i+1) lift br cons
+ | Pusual r' ->
+ let c = named_lams (List.rev ids) c in
+ let c = ast_lift lift c
+ in MLapp (c,a)
+ | Prel 1 when List.length ids = 1 ->
+ let c = MLlam (List.hd ids, c) in
+ let c = ast_lift lift c
+ in MLapp(c,[MLcons(typ,r,a)])
+ | Pwild when ids = [] -> ast_lift lift c
+ | _ -> raise Impossible (* TODO: handle some more cases *)
+
+(* [iota_gen] is an extension of [iota_red] where we allow to
+ traverse matches in the head of the first match *)
+
+let iota_gen br hd =
let rec iota k = function
- | MLcons (i,r,a) ->
- let (_,ids,c) = br.(constructor_index r) in
- let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
- let c = ast_lift k c in
- MLapp (c,a)
- | MLcase(i,e,br') ->
+ | MLcons (typ,r,a) -> iota_red 0 k br (typ,r,a)
+ | MLcase(typ,e,br') ->
let new_br =
- Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
- in MLcase(i,e, new_br)
- | _ -> assert false
- in iota 0
+ Array.map (fun (i,p,c)->(i,p,iota (k+(List.length i)) c)) br'
+ in MLcase(typ,e,new_br)
+ | _ -> raise Impossible
+ in iota 0 hd
let is_atomic = function
| MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
@@ -824,9 +887,9 @@ let expand_linear_let o id e =
let rec simpl o = function
| MLapp (f, []) -> simpl o f
| MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
- | MLcase (i,e,br) ->
- let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
- simpl_case o i br (simpl o e)
+ | MLcase (typ,e,br) ->
+ let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in
+ simpl_case o typ br (simpl o e)
| MLletin(Dummy,_,e) -> simpl o (ast_pop e)
| MLletin(id,c,e) ->
let e = simpl o e in
@@ -862,40 +925,50 @@ and simpl_app o a = function
| MLletin (id,e1,e2) when o.opt_let_app ->
(* Application of a letin: we push arguments inside *)
MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
- | MLcase (i,e,br) when o.opt_case_app ->
+ | MLcase (typ,e,br) when o.opt_case_app ->
(* Application of a case: we push arguments inside *)
let br' =
Array.map
- (fun (n,l,t) ->
+ (fun (l,p,t) ->
let k = List.length l in
let a' = List.map (ast_lift k) a in
- (n, l, simpl o (MLapp (t,a')))) br
- in simpl o (MLcase (i,e,br'))
+ (l, p, simpl o (MLapp (t,a')))) br
+ in simpl o (MLcase (typ,e,br'))
| (MLdummy | MLexn _) as e -> e
(* We just discard arguments in those cases. *)
| f -> MLapp (f,a)
(* Invariant : all empty matches should now be [MLexn] *)
-and simpl_case o i br e =
- if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
+and simpl_case o typ br e =
+ try
+ (* Generalized iota-redex *)
+ if not o.opt_case_iot then raise Impossible;
simpl o (iota_gen br e)
- else
+ with Impossible ->
(* Swap the case and the lam if possible *)
let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
let n = List.length ids in
if n <> 0 then
- simpl o (named_lams ids (MLcase (i,ast_lift n e, br)))
+ simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
else
(* Can we merge several branches as the same constant or function ? *)
- match factor_branches o i.m_typs br with
+ if lang() = Scheme || is_custom_match br
+ then MLcase (typ, e, br)
+ else match factor_branches o typ br with
| Some (f,ints) when Intset.cardinal ints = Array.length br ->
- (* If all branches have been factorized, we remove the match *)
- simpl o (MLletin (Tmp anonymous_name, e, f))
+ (* If all branches have been factorized, we remove the match *)
+ simpl o (MLletin (Tmp anonymous_name, e, f))
| Some (f,ints) ->
- let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints
- in MLcase ({i with m_same=same}, e, br)
- | None -> MLcase (i, e, br)
+ let last_br =
+ if ast_occurs 1 f then ([Tmp anonymous_name], Prel 1, f)
+ else ([], Pwild, ast_pop f)
+ in
+ let brl = Array.to_list br in
+ let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+ let brl_opt = brl_opt @ [last_br] in
+ MLcase (typ, e, Array.of_list brl_opt)
+ | None -> MLcase (typ, e, br)
(*S Local prop elimination. *)
(* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
@@ -1107,20 +1180,21 @@ let optimize_fix a =
(* Utility functions used in the decision of inlining. *)
+let ml_size_branch size pv = Array.fold_left (fun a (_,_,t) -> a + size t) 0 pv
+
let rec ml_size = function
| MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
| MLlam(_,t) -> 1 + ml_size t
- | MLcons(_,_,l) -> ml_size_list l
- | MLcase(_,t,pv) ->
- 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
+ | MLcons(_,_,l) | MLtuple l -> ml_size_list l
+ | MLcase(_,t,pv) -> 1 + ml_size t + ml_size_branch ml_size pv
| MLfix(_,_,f) -> ml_size_array f
| MLletin (_,_,t) -> ml_size t
| MLmagic t -> ml_size t
- | _ -> 0
+ | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0
and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
-and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
+and ml_size_array a = Array.fold_left (fun a t -> a + ml_size t) 0 a
let is_fix = function MLfix _ -> true | _ -> false
@@ -1172,7 +1246,7 @@ let rec non_stricts add cand = function
(* so we make an union (in fact a merge). *)
let cand = non_stricts false cand t in
Array.fold_left
- (fun c (_,i,t)->
+ (fun c (i,_,t)->
let n = List.length i in
let cand = lift n cand in
let cand = pop n (non_stricts add cand t) in
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index e8fa9c47b..452fd46c0 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -113,9 +113,11 @@ val normalize : ml_ast -> ml_ast
val optimize_fix : ml_ast -> ml_ast
val inline : global_reference -> ml_ast -> bool
+val is_basic_pattern : ml_pattern -> bool
+val has_deep_pattern : ml_branch array -> bool
+val is_regular_match : ml_branch array -> bool
+
exception Impossible
-val branch_as_fun : ml_type list -> ml_branch -> ml_ast
-val branch_as_cst : ml_branch -> ml_ast
(* Classification of signatures *)
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index a548c7866..9e8dd8286 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -77,18 +77,26 @@ let type_iter_references do_type t =
| _ -> ()
in iter t
+let patt_iter_references do_cons p =
+ let rec iter = function
+ | Pcons (r,l) -> do_cons r; List.iter iter l
+ | Pusual r -> do_cons r
+ | Ptuple l -> List.iter iter l
+ | Prel _ | Pwild -> ()
+ in iter p
+
let ast_iter_references do_term do_cons do_type a =
let rec iter a =
ast_iter iter a;
match a with
| MLglob r -> do_term r
- | MLcons (i,r,_) ->
- if lang () = Ocaml then record_iter_references do_term i.c_kind;
- do_cons r
- | MLcase (i,_,v) ->
- if lang () = Ocaml then record_iter_references do_term i.m_kind;
- Array.iter (fun (r,_,_) -> do_cons r) v
- | _ -> ()
+ | MLcons (_,r,_) -> do_cons r
+ | MLcase (ty,_,v) ->
+ type_iter_references do_type ty;
+ Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
+
+ | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
+ | MLdummy | MLaxiom | MLmagic _ -> ()
in iter a
let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9885c64b1..ed69ec457 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -29,22 +29,6 @@ let pp_tvar id =
then str ("'"^s)
else str ("' "^s)
-let pp_tuple_light f = function
- | [] -> mt ()
- | [x] -> f true x
- | l ->
- pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
-
-let pp_tuple f = function
- | [] -> mt ()
- | [x] -> f x
- | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
-
-let pp_boxed_tuple f = function
- | [] -> mt ()
- | [x] -> f x
- | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
-
let pp_abst = function
| [] -> mt ()
| l ->
@@ -57,6 +41,10 @@ let pp_parameters l =
let pp_string_parameters l =
(pp_boxed_tuple str l ++ space_if (l<>[]))
+let pp_letin pat def body =
+ let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in
+ hv 0 (hv 0 (hov 2 fstline ++ spc () ++ str "in") ++ spc () ++ hov 0 body)
+
(*s Ocaml renaming issues. *)
let keywords =
@@ -153,10 +141,19 @@ let rec pp_type par vl t =
de Bruijn variables. [args] is the list of collected arguments
(already pretty-printed). *)
+let is_bool_patt p s =
+ try
+ let r = match p with
+ | Pusual r -> r
+ | Pcons (r,[]) -> r
+ | _ -> raise Not_found
+ in
+ find_custom r = s
+ with Not_found -> false
+
+
let is_ifthenelse = function
- | [|(r1,[],_);(r2,[],_)|] ->
- (try (find_custom r1 = "true") && (find_custom r2 = "false")
- with Not_found -> false)
+ | [|([],p1,_);([],p2,_)|] -> is_bool_patt p1 "true" && is_bool_patt p2 "false"
| _ -> false
let expr_needs_par = function
@@ -166,8 +163,8 @@ let expr_needs_par = function
| _ -> false
let rec pp_expr par env args =
- let par' = args <> [] || par
- and apply st = pp_apply st par args in
+ let apply st = pp_apply st par args
+ and apply2 st = pp_apply2 st par args in
function
| MLrel n ->
let id = get_db_name n env in apply (pr_id id)
@@ -178,109 +175,23 @@ let rec pp_expr par env args =
let fl,a' = collect_lams a in
let fl = List.map id_of_mlid fl in
let fl,env' = push_vars fl env in
- let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
- apply (pp_par par' st)
+ let st = pp_abst (List.rev fl) ++ pp_expr false env' [] a' in
+ apply2 st
| MLletin (id,a1,a2) ->
let i,env' = push_vars [id_of_mlid id] env in
let pp_id = pr_id (List.hd i)
and pp_a1 = pp_expr false env [] a1
and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
- hv 0
- (apply
- (pp_par par'
- (hv 0
- (hov 2
- (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
- spc () ++ str "in") ++
- spc () ++ hov 0 pp_a2)))
+ hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
| MLglob r ->
(try
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 _ -> apply (pp_global Term r))
- | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
- | MLcons ({c_kind = Coinductive},r,[]) ->
- assert (args=[]);
- pp_par par (str "lazy " ++ pp_global Cons r)
- | MLcons ({c_kind = Coinductive},r,args') ->
- assert (args=[]);
- let tuple = pp_tuple (pp_expr true env []) args' in
- pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
- | MLcons (_,r,[]) ->
- assert (args=[]);
- pp_global Cons r
- | MLcons ({c_kind = Record fields}, r, args') ->
- assert (args=[]);
- pp_record_pat (pp_fields r fields, List.map (pp_expr true env []) args')
- | MLcons (_,r,[arg1;arg2]) when is_infix r ->
- assert (args=[]);
- pp_par par
- ((pp_expr true env [] arg1) ++ str (get_infix r) ++
- (pp_expr true env [] arg2))
- | MLcons (_,r,args') ->
- assert (args=[]);
- let tuple = pp_tuple (pp_expr true env []) args' in
- 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
- apply
- (pp_par par'
- (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 (info, t, pv) ->
- let expr = if info.m_kind = Coinductive then
- (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
- else
- (pp_expr false env [] t)
- in
- (try
- (* First, can this match be printed as a mere record projection ? *)
- let fields =
- match info.m_kind with Record f -> f | _ -> raise Impossible
- in
- let (r, ids, c) = pv.(0) in
- let n = List.length ids in
- let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
- let proj_hd i =
- pp_expr true env [] t ++ str "." ++ pp_field r fields i
- in
- match c with
- | MLrel i when i <= n -> apply (pp_par par' (proj_hd (n-i)))
- | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
- let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
- (pp_apply (proj_hd (n-i))
- par ((List.map (pp_expr true env' []) a) @ args))
- | _ -> raise Impossible
- with Impossible ->
- (* Second, can this match be printed as a let-in ? *)
- if Array.length pv = 1 then
- let s1,s2 = pp_one_pat env info pv.(0) in
- apply
- (hv 0
- (pp_par par'
- (hv 0
- (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
- ++ spc () ++ str "in") ++
- spc () ++ hov 0 s2)))
- else
- (* Otherwise, standard match *)
- apply
- (pp_par par'
- (try pp_ifthenelse par' env expr pv
- with Not_found ->
- v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
- pp_pat env info pv))))
| 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
+ pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
| MLexn s ->
(* An [MLexn] may be applied, but I don't really care. *)
pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
@@ -290,7 +201,96 @@ let rec pp_expr par env args =
pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
| MLaxiom ->
pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
-
+ | MLcons (_,r,a) as c ->
+ assert (args=[]);
+ begin match a with
+ | _ when is_native_char c -> pp_native_char c
+ | [a1;a2] when is_infix r ->
+ let pp = pp_expr true env [] in
+ pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)
+ | _ when is_coinductive r ->
+ let ne = (a<>[]) in
+ let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in
+ pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple))
+ | [] -> pp_global Cons r
+ | _ ->
+ let fds = get_record_fields r in
+ if fds <> [] then
+ pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a)
+ else
+ let tuple = pp_tuple (pp_expr true env []) a in
+ if str_global Cons r = "" (* hack Extract Inductive prod *)
+ then tuple
+ else pp_par par (pp_global Cons r ++ spc () ++ tuple)
+ end
+ | MLtuple l ->
+ assert (args = []);
+ pp_boxed_tuple (pp_expr true env []) l
+ | MLcase (_, t, pv) when is_custom_match pv ->
+ if not (is_regular_match pv) then
+ error "Cannot mix yet user-given match and general patterns.";
+ let mkfun (ids,_,e) =
+ if ids <> [] then named_lams (List.rev ids) e
+ else dummy_lams (ast_lift 1 e) 1
+ in
+ let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
+ let inner =
+ str (find_custom_match pv) ++ fnl () ++
+ prvect pp_branch pv ++
+ pp_expr true env [] t
+ in
+ apply2 (hov 2 inner)
+ | MLcase (typ, t, pv) ->
+ let head =
+ if not (is_coinductive_type typ) then pp_expr false env [] t
+ else (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
+ in
+ (* First, can this match be printed as a mere record projection ? *)
+ (try pp_record_proj par env typ t pv args
+ with Impossible ->
+ (* Second, can this match be printed as a let-in ? *)
+ if Array.length pv = 1 then
+ let s1,s2 = pp_one_pat env pv.(0) in
+ hv 0 (apply2 (pp_letin s1 head s2))
+ else
+ (* Third, can this match be printed as [if ... then ... else] ? *)
+ (try apply2 (pp_ifthenelse env head pv)
+ with Not_found ->
+ (* Otherwise, standard match *)
+ apply2
+ (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
+ pp_pat env pv))))
+
+and pp_record_proj par env typ t pv args =
+ (* Can a match be printed as a mere record projection ? *)
+ let fields = record_fields_of_type typ in
+ if fields = [] then raise Impossible;
+ if Array.length pv <> 1 then raise Impossible;
+ if has_deep_pattern pv then raise Impossible;
+ let (ids,pat,body) = pv.(0) in
+ let n = List.length ids in
+ let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
+ let rel_i,a = match body with
+ | MLrel i when i <= n -> i,[]
+ | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a
+ | _ -> raise Impossible
+ in
+ let rec lookup_rel i idx = function
+ | Prel j :: l -> if i = j then idx else lookup_rel i (idx+1) l
+ | Pwild :: l -> lookup_rel i (idx+1) l
+ | _ -> raise Impossible
+ in
+ let r,idx = match pat with
+ | Pusual r -> r, n-rel_i
+ | Pcons (r,l) -> r, lookup_rel rel_i 0 l
+ | _ -> raise Impossible
+ in
+ if is_infix r then raise Impossible;
+ let env' = snd (push_vars (List.rev_map id_of_mlid ids) env) in
+ let pp_args = (List.map (pp_expr true env' []) a) @ args in
+ let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx
+ in
+ pp_apply pp_head par pp_args
and pp_record_pat (fields, args) =
str "{ " ++
@@ -299,9 +299,27 @@ and pp_record_pat (fields, args) =
(List.combine fields args) ++
str " }"
-and pp_ifthenelse par env expr pv = match pv with
- | [|(tru,[],the);(fal,[],els)|] when
- (find_custom tru = "true") && (find_custom fal = "false")
+and pp_cons_pat r ppl =
+ if is_infix r && List.length ppl = 2 then
+ List.hd ppl ++ str (get_infix r) ++ List.hd (List.tl ppl)
+ else
+ let fields = get_record_fields r in
+ if fields <> [] then pp_record_pat (pp_fields r fields, ppl)
+ else if str_global Cons r = "" then
+ pp_boxed_tuple identity ppl (* Hack Extract Inductive prod *)
+ else
+ pp_global Cons r ++ space_if (ppl<>[]) ++ pp_boxed_tuple identity ppl
+
+and pp_gen_pat ids env = function
+ | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
+ | Pusual r -> pp_cons_pat r (List.map pr_id ids)
+ | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l
+ | Pwild -> str "_"
+ | Prel n -> pr_id (get_db_name n env)
+
+and pp_ifthenelse env expr pv = match pv with
+ | [|([],tru,the);([],fal,els)|] when
+ (is_bool_patt tru "true") && (is_bool_patt fal "false")
->
hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
hov 2 (str "then " ++
@@ -310,66 +328,34 @@ and pp_ifthenelse par env expr pv = match pv with
hov 2 (pp_expr (expr_needs_par els) env [] els)))
| _ -> raise Not_found
-and pp_one_pat env info (r,ids,t) =
- let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
- let expr = pp_expr (expr_needs_par t) env' [] t in
- let patt = match info.m_kind with
- | Record fields ->
- pp_record_pat (pp_fields r fields, List.rev_map pr_id ids)
- | _ -> match List.rev ids with
- | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
- | [] -> pp_global Cons r
- | ids ->
- (* hack Extract Inductive prod *)
- (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ())
- ++ pp_boxed_tuple pr_id ids
- in
- patt, expr
-
-and pp_pat env info pv =
- let factor_br, factor_set = try match info.m_same with
- | BranchFun ints ->
- let i = Intset.choose ints in
- branch_as_fun info.m_typs pv.(i), ints
- | BranchCst ints ->
- let i = Intset.choose ints in
- ast_pop (branch_as_cst pv.(i)), ints
- | BranchNone -> MLdummy, Intset.empty
- with _ -> MLdummy, Intset.empty
- in
- let last = Array.length pv - 1 in
+and pp_one_pat env (ids,p,t) =
+ let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
+ pp_gen_pat (List.rev ids') env' p,
+ pp_expr (expr_needs_par t) env' [] t
+
+and pp_pat env pv =
prvecti
- (fun i x -> if Intset.mem i factor_set then mt () else
- let s1,s2 = pp_one_pat env info x in
+ (fun i x ->
+ let s1,s2 = pp_one_pat env x in
hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
- if i = last && Intset.is_empty factor_set then mt () else fnl ())
+ if i = Array.length pv - 1 then mt () else fnl ())
pv
- ++
- if Intset.is_empty factor_set then mt () else
- let par = expr_needs_par factor_br in
- match info.m_same with
- | BranchFun _ ->
- let ids, env' = push_vars [anonymous_name] env in
- hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
- hov 2 (pp_expr par env' [] factor_br))
- | BranchCst _ ->
- hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br))
- | BranchNone -> mt ()
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
- i.m_kind = Standard && not (is_custom_match pv) ->
- if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
+ | MLcase(Tglob(r,_),MLrel 1,pv) when
+ not (is_coinductive r) && get_record_fields r = [] &&
+ not (is_custom_match pv) ->
+ if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then
pr_binding (List.rev (List.tl bl)) ++
str " = function" ++ fnl () ++
- v 0 (pp_pat env' i pv)
+ v 0 (pp_pat env' pv)
else
pr_binding (List.rev bl) ++
str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
- v 0 (pp_pat env' i pv)
+ v 0 (pp_pat env' pv)
| _ ->
pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 8a781a8d9..215076555 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -85,7 +85,7 @@ let rec pp_expr env args =
++ spc () ++ hov 0 (pp_expr env' [] a2)))))
| MLglob r ->
apply (pp_global Term r)
- | MLcons (info,r,args') ->
+ | MLcons (_,r,args') ->
assert (args=[]);
let st =
str "`" ++
@@ -93,9 +93,12 @@ let rec pp_expr env args =
(if args' = [] then mt () else spc ()) ++
prlist_with_sep spc (pp_cons_args env) args')
in
- if info.c_kind = Coinductive then paren (str "delay " ++ st) else st
+ if is_coinductive r then paren (str "delay " ++ st) else st
+ | MLtuple _ -> error "Cannot handle tuples in Scheme yet."
+ | MLcase (_,_,pv) when not (is_regular_match pv) ->
+ error "Cannot handle general patterns in Scheme yet."
| MLcase (_,t,pv) when is_custom_match pv ->
- let mkfun (_,ids,e) =
+ let mkfun (ids,_,e) =
if ids <> [] then named_lams (List.rev ids) e
else dummy_lams (ast_lift 1 e) 1
in
@@ -105,9 +108,9 @@ let rec pp_expr env args =
(str (find_custom_match pv) ++ fnl () ++
prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
++ pp_expr env [] t)))
- | MLcase (info,t, pv) ->
- let e =
- if info.m_kind <> Coinductive then pp_expr env [] t
+ | MLcase (typ,t, pv) ->
+ let e =
+ if not (is_coinductive_type typ) then pp_expr env [] t
else paren (str "force" ++ spc () ++ pp_expr env [] t)
in
apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
@@ -124,14 +127,18 @@ let rec pp_expr env args =
| MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
and pp_cons_args env = function
- | MLcons (info,r,args) when info.c_kind<>Coinductive ->
+ | MLcons (_,r,args) when is_coinductive r ->
paren (pp_global Cons r ++
(if args = [] then mt () else spc ()) ++
prlist_with_sep spc (pp_cons_args env) args)
| e -> str "," ++ pp_expr env [] e
-
-and pp_one_pat env (r,ids,t) =
+and pp_one_pat env (ids,p,t) =
+ let r = match p with
+ | Pusual r -> r
+ | Pcons (r,l) -> r (* cf. the check [is_regular_match] above *)
+ | _ -> assert false
+ in
let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
let args =
if ids = [] then mt ()
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 567b0727c..238befd25 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -127,6 +127,39 @@ let add_ind kn mib ml_ind =
inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
let lookup_ind kn = Mindmap_env.find kn !inductives
+let inductive_kinds =
+ ref (Mindmap_env.empty : inductive_kind Mindmap_env.t)
+let init_inductive_kinds () = inductive_kinds := Mindmap_env.empty
+let add_inductive_kind kn k =
+ inductive_kinds := Mindmap_env.add kn k !inductive_kinds
+let is_coinductive r =
+ let kn = match r with
+ | ConstructRef ((kn,_),_) -> kn
+ | IndRef (kn,_) -> kn
+ | _ -> assert false
+ in
+ try Mindmap_env.find kn !inductive_kinds = Coinductive
+ with Not_found -> false
+
+let is_coinductive_type = function
+ | Tglob (r,_) -> is_coinductive r
+ | _ -> false
+
+let get_record_fields r =
+ let kn = match r with
+ | ConstructRef ((kn,_),_) -> kn
+ | IndRef (kn,_) -> kn
+ | _ -> assert false
+ in
+ try match Mindmap_env.find kn !inductive_kinds with
+ | Record f -> f
+ | _ -> []
+ with Not_found -> []
+
+let record_fields_of_type = function
+ | Tglob (r,_) -> get_record_fields r
+ | _ -> []
+
(*s Recursors table. *)
(* NB: here we can use the equivalence between canonical
@@ -199,15 +232,26 @@ let library () = !library_ref
(*s Printing. *)
(* The following functions work even on objects not in [Global.env ()].
- WARNING: for inductive objects, an extract_inductive must have been
- done before. *)
-
-let safe_basename_of_global = function
- | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
- | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
- | ConstructRef ((kn,i),j) ->
- (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
- | _ -> assert false
+ Warning: for inductive objects, this only works if an [extract_inductive]
+ have been done earlier, otherwise we can only ask the Nametab about
+ currently visible objects. *)
+
+let safe_basename_of_global r =
+ let last_chance r =
+ try Nametab.basename_of_global r
+ with Not_found ->
+ anomaly "Inductive object unknown to extraction and not globally visible"
+ in
+ match r with
+ | ConstRef kn -> id_of_label (con_label kn)
+ | IndRef (kn,0) -> id_of_label (mind_label kn)
+ | IndRef (kn,i) ->
+ (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+ with Not_found -> last_chance r)
+ | ConstructRef ((kn,i),j) ->
+ (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
+ with Not_found -> last_chance r)
+ | VarRef _ -> assert false
let string_of_global r =
try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
@@ -731,8 +775,10 @@ let add_custom_match r s =
let indref_of_match pv =
if Array.length pv = 0 then raise Not_found;
- match pv.(0) with
- | (ConstructRef (ip,_), _, _) -> IndRef ip
+ let (_,pat,_) = pv.(0) in
+ match pat with
+ | Pusual (ConstructRef (ip,_)) -> IndRef ip
+ | Pcons (ConstructRef (ip,_),_) -> IndRef ip
| _ -> raise Not_found
let is_custom_match pv =
@@ -817,5 +863,6 @@ let extract_inductive r s l optstr =
(*s Tables synchronization. *)
let reset_tables () =
- init_terms (); init_types (); init_inductives (); init_recursors ();
+ init_terms (); init_types (); init_inductives ();
+ init_inductive_kinds (); init_recursors ();
init_projs (); init_axioms (); init_opaques (); reset_modfile ()
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index cdd792222..a3b7124e1 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -74,6 +74,14 @@ val lookup_type : constant -> ml_schema
val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind
+val add_inductive_kind : mutual_inductive -> inductive_kind -> unit
+val is_coinductive : global_reference -> bool
+val is_coinductive_type : ml_type -> bool
+(* What are the fields of a record (empty for a non-record) *)
+val get_record_fields :
+ global_reference -> global_reference option list
+val record_fields_of_type : ml_type -> global_reference option list
+
val add_recursors : Environ.env -> mutual_inductive -> unit
val is_recursor : global_reference -> bool
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 8123726a1..3f8a3bc49 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -342,7 +342,7 @@ case H1.
exact H0.
intros.
exact n.
-Qed.
+Defined.
Extraction oups.
(*
let oups h0 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 15:55:59 +0000