diff options
author | 2010-12-21 11:31:57 +0000 | |
---|---|---|
committer | 2010-12-21 11:31:57 +0000 | |
commit | e3696e15775c44990018d1d4aea01c9bf662cd73 (patch) | |
tree | 6f14fb168ffe95ef0dd25984a99e0678f53bd89e /plugins | |
parent | b1ae368ec3228f7340076ba0d3bc465f79ed44fa (diff) |
Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/extraction.ml | 22 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 39 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 31 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 133 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 5 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 58 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 3 |
9 files changed, 166 insertions, 141 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 1e2793aa5..5131704a7 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -27,7 +27,7 @@ open Table open Mlutil (*i*) -exception I of inductive_info +exception I of inductive_kind (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : constant list) @@ -356,7 +356,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) in add_ind kn mib - {ind_info = Standard; + {ind_kind = Standard; ind_nparams = npar; ind_packets = packets; ind_equiv = equiv @@ -441,7 +441,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) Record field_glob with (I info) -> info in - let i = {ind_info = ind_info; + let i = {ind_kind = ind_info; ind_nparams = npar; ind_packets = packets; ind_equiv = equiv } @@ -699,9 +699,15 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in let magic2 = needs_magic (a, mlt) in let head mla = - if mi.ind_info = Singleton then + if mi.ind_kind = Singleton then put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *) - else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla)) + else + let typeargs = match snd (type_decomp type_cons) with + | 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)) in (* Different situations depending of the number of arguments: *) if la < params_nb then @@ -767,7 +773,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in (r, List.rev ids, e') in - if mi.ind_info = Singleton then + if mi.ind_kind = Singleton then begin (* Informative singleton case: *) (* [match c with C i -> t] becomes [let i = c' in t'] *) @@ -778,7 +784,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = end else (* Standard case: we apply [extract_branch]. *) - MLcase ((mi.ind_info,BranchNone), a, Array.init br_size 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) (*s Extraction of a (co)-fixpoint. *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 3d18431aa..6ca448826 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -154,10 +154,10 @@ let rec pp_expr par env args = 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) -> + | MLcase (info,t, pv) -> apply (pp_par par' (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ - fnl () ++ str " " ++ pp_pat env factors pv))) + fnl () ++ str " " ++ 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 @@ -170,7 +170,7 @@ 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 factors pv = +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 @@ -182,27 +182,32 @@ and pp_pat env factors pv = (fun () -> (spc ())) pr_id (List.rev ids))) ++ str " ->" ++ spc () ++ pp_expr par env' [] t) in - let factor_br, factor_l = try match factors with - | BranchFun (i::_ as l) -> check_function_branch pv.(i), l - | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l - | _ -> MLdummy, [] - with Impossible -> MLdummy, [] + 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 par = expr_needs_par factor_br in let last = Array.length pv - 1 in prvecti - (fun i x -> if List.mem i factor_l then mt () else + (fun i x -> if Intset.mem i factor_set then mt () else (pp_one_pat pv.(i) ++ - if i = last && factor_l = [] then mt () else + if i = last && Intset.is_empty factor_set then mt () else fnl () ++ str " ")) pv ++ - if factor_l = [] then mt () else match factors with + 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 - pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br + let ids, env' = push_vars [anonymous_name] env in + pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br | BranchCst _ -> - str "_ ->" ++ spc () ++ pp_expr par env [] factor_br + str "_ ->" ++ spc () ++ pp_expr par env [] factor_br | BranchNone -> mt () (*s names of the functions ([ids]) are already pushed in [env], @@ -282,7 +287,7 @@ let rec pp_ind first kn i ind = (*s Pretty-printing of a declaration. *) let pp_decl = function - | Dind (kn,i) when i.ind_info = Singleton -> + | Dind (kn,i) when i.ind_kind = Singleton -> pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i) | Dtype (r, l, t) -> diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index ea18cbee6..85cd4a42b 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -51,7 +51,7 @@ type ml_schema = int * ml_type (*s ML inductive types. *) -type inductive_info = +type inductive_kind = | Singleton | Coinductive | Standard @@ -83,7 +83,7 @@ type equiv = | RenEquiv of string type ml_ind = { - ind_info : inductive_info; + ind_kind : inductive_kind; ind_nparams : int; ind_packets : ml_ind_packet array; ind_equiv : equiv @@ -96,12 +96,27 @@ type ml_ident = | Id of identifier | Tmp of identifier -(* list of branches to merge in a common pattern *) +(** 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" +*) + +type constructor_info = { + c_kind : inductive_kind; + c_typs : ml_type list; +} -type case_info = +type branch_same = | BranchNone - | BranchFun of int list - | BranchCst of int list + | BranchFun of Intset.t + | BranchCst of Intset.t + +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 @@ -111,8 +126,8 @@ and ml_ast = | 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 * ml_branch array + | MLcons of constructor_info * global_reference * ml_ast list + | MLcase of match_info * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 29f9a817d..3036cb134 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -277,6 +277,8 @@ let type_expand env t = | a -> a in if Table.type_expand () then expand t else t +let type_simpl = type_expand (fun _ -> None) + (*s Generating a signature from a ML type. *) let type_to_sign env t = match type_expand env t with @@ -641,12 +643,23 @@ let rec ast_glob_subst s t = match t with (*S Auxiliary functions used in simplification of ML cases. *) -(*s [check_function_branch (r,l,c)] checks if branch [c] can be seen +(* Factorisation of some match branches into a common "x -> f x" + branch may break types sometimes. Example: [type 'x a = A]. + Then [let id = function A -> A] has type ['x a -> 'y a], + which is incompatible with the type of [let id x = x]. + We now check that the type arguments of the inductive are + preserved by our transformation. + + TODO: this verification should be done someday modulo + expansion of type definitions. +*) + +(*s [branch_as_function b typs (r,l,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] *) + any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] + if any variable in [l] occurs outside such a [MLcons] *) -let check_function_branch (r,l,c) = +let branch_as_fun typs (r,l,c) = let nargs = List.length l in let rec genrec n = function | MLrel i as c -> @@ -654,22 +667,32 @@ let check_function_branch (r,l,c) = if i'<1 then c else if i'>nargs then MLrel (i-nargs+1) else raise Impossible - | MLcons(_,r',args) when r=r' && (test_eta_args_lift n nargs args) -> + | MLcons(i,r',args) when + r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs -> MLrel (n+1) | a -> ast_map_lift genrec n a in genrec 0 c -(*s [check_constant_branch (r,l,c)] checks if branch [c] is 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 the - branch-as-function optimization) *) +(*s [branch_as_cst (r,l,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]). + NB: [MLcons(r,l)] might occur nonetheless in [c], but only when [l] is + empty, i.e. when [r] is a constant constructor +*) -let check_constant_branch (_,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 +(* A branch [MLcons(r,l)->c] can be seen at the same time as a function + branch and a constant branch, either because: + - [MLcons(r,l)] doesn't occur in [c]. For example : "A -> B" + - this constructor is constant (i.e. [l] is empty). For example "A -> A" + When searching for the best factorisation below, we'll try both. +*) + (* The following structure allows to record which element occurred at what position, and then finally return the most frequent element and its positions. *) @@ -678,61 +701,39 @@ let census_add, census_max, census_clean = let h = Hashtbl.create 13 in let clear () = Hashtbl.clear h in let add e i = - let l = try Hashtbl.find h e with Not_found -> [] in - Hashtbl.replace h e (i::l) + let s = try Hashtbl.find h e with Not_found -> Intset.empty in + Hashtbl.replace h e (Intset.add i s) in let max e0 = - let len = ref 0 and lst = ref [] and elm = ref e0 in + let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in Hashtbl.iter - (fun e l -> - let n = List.length l in - if n > !len then begin len := n; lst := l; elm := e end) + (fun e s -> + let n = Intset.cardinal s in + if n > !len then begin len := n; lst := s; elm := e end) h; (!elm,!lst) in (add,max,clear) -(* Given an abstraction function [abstr] (one of [check_*_branch]), - return the longest possible list of branches that have the - same abstraction, along with this abstraction. *) +(* [factor_branches] return the longest possible list of branches + that have the same factorization, either as a function or as a + constant. +*) -let factor_branches abstr br = +let factor_branches o typs br = census_clean (); for i = 0 to Array.length br - 1 do - try census_add (abstr br.(i)) i with Impossible -> () + 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_list = census_max MLdummy in - if br_list = [] then None - else if Array.length br >= 2 && List.length br_list < 2 then None - else Some (br_factor, br_list) - -(*s [check_generalizable_case] checks if all branches can be seen as the - same function [f] applied to the term matched. It is a generalized version - of both the identity case optimization and the constant case optimisation - ([f] can be a constant function) *) - -(* The optimisation [factor_branches check_function_branch] breaks types - in some special case. Example: [type 'x a = A]. - Then [let f = function A -> A] has type ['x a -> 'y a], - which is incompatible with the type of [let f x = x]. - We check first that there isn't such phantom variable in the inductive type - we're considering. *) - -let check_optim_id br = - let (kn,i) = - match br.(0) with (ConstructRef (c,_),_,_) -> c | _ -> assert false - in - let ip = (snd (lookup_ind kn)).ind_packets.(i) in - match ip.ip_optim_id_ok with - | Some ok -> ok - | None -> - let tvars = - intset_union_map_array (intset_union_map_list type_listvar) - ip.ip_types - in - let ok = (Intset.cardinal tvars = List.length ip.ip_vars) in - ip.ip_optim_id_ok <- Some ok; - ok + 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) (*s If all branches are functions, try to permut the case and the functions. *) @@ -873,26 +874,14 @@ and simpl_case o i br e = if n <> 0 then simpl o (named_lams ids (MLcase (i,ast_lift n e, br))) else - (* Does a term [f] exist such that many branches are [(f e)] ? *) - let opt1 = - if o.opt_case_idr && (o.opt_case_idg || check_optim_id br) then - factor_branches check_function_branch br - else None - in - (* Detect common constant branches. Often a particular case of - branch-as-function optim, but not always (e.g. A->A|B->A) *) - let opt2 = - if opt1 = None && o.opt_case_cst then - factor_branches check_constant_branch br - else opt1 - in - match opt2 with - | Some (f,ints) when List.length ints = Array.length br -> - (* if all branches have been factorized, we remove the match *) + (* Can we merge several branches as the same constant or function ? *) + match factor_branches o i.m_typs 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)) | Some (f,ints) -> - let ci = if ast_occurs 1 f then BranchFun ints else BranchCst ints - in MLcase ((fst i,ci), e, br) + 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) (*S Local prop elimination. *) diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index b4f3c4c18..e8fa9c47b 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -60,6 +60,7 @@ val var2var' : ml_type -> ml_type type abbrev_map = global_reference -> ml_type option val type_expand : abbrev_map -> ml_type -> ml_type +val type_simpl : ml_type -> ml_type val type_to_sign : abbrev_map -> ml_type -> sign val type_to_signature : abbrev_map -> ml_type -> signature val type_expunge : abbrev_map -> ml_type -> ml_type @@ -113,8 +114,8 @@ val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool exception Impossible -val check_function_branch : ml_branch -> ml_ast -val check_constant_branch : ml_branch -> ml_ast +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 bb880aeea..bff28aef1 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -80,10 +80,10 @@ let ast_iter_references do_term do_cons do_type a = match a with | MLglob r -> do_term r | MLcons (i,r,_) -> - if lang () = Ocaml then record_iter_references do_term i; + 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 (fst i); + if lang () = Ocaml then record_iter_references do_term i.m_kind; Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () in iter a @@ -99,7 +99,7 @@ let ind_iter_references do_term do_cons do_type kn ind = | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in - if lang () = Ocaml then record_iter_references do_term ind.ind_info; + if lang () = Ocaml then record_iter_references do_term ind.ind_kind; Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets let decl_iter_references do_term do_cons do_type = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index cf5acb3d9..b60eee381 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -216,17 +216,17 @@ let rec pp_expr par env args = when kn = ind_ascii && check_extract_ascii () & is_list_cons l -> assert (args=[]); pp_char l - | MLcons (Coinductive,r,[]) -> + | MLcons ({c_kind = Coinductive},r,[]) -> assert (args=[]); pp_par par (str "lazy " ++ pp_global Cons r) - | MLcons (Coinductive,r,args') -> + | 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 (Record projs, r, args') -> + | MLcons ({c_kind = Record projs}, r, args') -> assert (args=[]); pp_record_pat (projs, List.map (pp_expr true env []) args') | MLcons (_,r,[arg1;arg2]) when is_infix r -> @@ -248,14 +248,14 @@ let rec pp_expr par env args = 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 + | 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 - let projs = find_projections i in + let projs = find_projections info.m_kind in let (_, ids, c) = pv.(0) in let n = List.length ids in match c with @@ -275,7 +275,7 @@ let rec pp_expr par env args = | _ -> raise NoRecord with NoRecord -> if Array.length pv = 1 then - let s1,s2 = pp_one_pat env i pv.(0) in + let s1,s2 = pp_one_pat env info pv.(0) in apply (hv 0 (pp_par par' @@ -289,7 +289,7 @@ let rec pp_expr par env args = (try pp_ifthenelse par' env expr pv with Not_found -> v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ - str " | " ++ pp_pat env (i,factors) pv)))) + str " | " ++ 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 @@ -322,11 +322,11 @@ 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 i (r,ids,t) = +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 try - let projs = find_projections i in + let projs = find_projections info.m_kind in pp_record_pat (projs, List.rev_map pr_id ids), expr with NoRecord -> (match List.rev ids with @@ -338,36 +338,42 @@ and pp_one_pat env i (r,ids,t) = ++ pp_boxed_tuple pr_id ids), expr -and pp_pat env (info,factors) pv = - let factor_br, factor_l = try match factors with - | BranchFun (i::_ as l) -> check_function_branch pv.(i), l - | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l - | _ -> MLdummy, [] - with Impossible -> MLdummy, [] +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 par = expr_needs_par factor_br in let last = Array.length pv - 1 in prvecti - (fun i x -> if List.mem i factor_l then mt () else + (fun i x -> if Intset.mem i factor_set then mt () else let s1,s2 = pp_one_pat env info x in hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ - if i = last && factor_l = [] then mt () else + if i = last && Intset.is_empty factor_set then mt () else fnl () ++ str " | ") pv ++ - if factor_l = [] then mt () else match factors with + 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 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br) + let ids, env' = push_vars [anonymous_name] env in + hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br) | BranchCst _ -> - hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + hov 2 (str "_ ->" ++ spc () ++ 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 fst i=Standard && not (is_custom_match pv) -> + | 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 pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ @@ -517,7 +523,7 @@ let pp_ind co kn ind = (*s Pretty-printing of a declaration. *) let pp_mind kn i = - match i.ind_info with + match i.ind_kind with | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i | Record projs -> diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index eb7562609..77c8e944e 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 (i,r,args') -> + | MLcons (info,r,args') -> assert (args=[]); let st = str "`" ++ @@ -93,7 +93,7 @@ let rec pp_expr env args = (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in - if i = Coinductive then paren (str "delay " ++ st) else st + if info.c_kind = Coinductive then paren (str "delay " ++ st) else st | MLcase (_,t,pv) when is_custom_match pv -> let mkfun (_,ids,e) = if ids <> [] then named_lams (List.rev ids) e @@ -102,9 +102,9 @@ let rec pp_expr env args = 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) -> + | MLcase (info,t, pv) -> let e = - if i <> Coinductive then pp_expr env [] t + if info.m_kind <> Coinductive 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))) @@ -121,7 +121,7 @@ let rec pp_expr env args = | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") and pp_cons_args env = function - | MLcons (i,r,args) when i<>Coinductive -> + | MLcons (info,r,args) when info.c_kind<>Coinductive -> paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index c22bb17ea..b9081e286 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -404,7 +404,8 @@ let flag_of_int n = opt_lin_beta = kth_digit n 10 } (* For the moment, we allow by default everything except : - - the type-unsafe optimization [opt_case_idg] + - the type-unsafe optimization [opt_case_idg], which anyway + cannot be activated currently (cf [Mlutil.branch_as_fun]) - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta] (may lead to complexity blow-up, subsumed by finer reductions when inlining recursors). |