diff options
-rw-r--r-- | API/API.mli | 1 | ||||
-rw-r--r-- | CHANGES | 10 | ||||
-rw-r--r-- | interp/constrextern.ml | 8 | ||||
-rw-r--r-- | intf/glob_term.ml | 8 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
-rw-r--r-- | pretyping/detyping.ml | 102 | ||||
-rw-r--r-- | pretyping/detyping.mli | 10 | ||||
-rw-r--r-- | test-suite/output/Cases.out | 51 | ||||
-rw-r--r-- | test-suite/output/Cases.v | 32 | ||||
-rw-r--r-- | test-suite/output/Notations2.out | 11 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 7 |
11 files changed, 227 insertions, 17 deletions
diff --git a/API/API.mli b/API/API.mli index 99ba3eea4..089cf8b15 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4339,6 +4339,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref + val print_allow_match_default_clause : bool ref val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit @@ -12,6 +12,16 @@ Notations opened rather than to the latest notations defined independently of whether they are in an opened scope or not. +Specification language + +- When printing clauses of a "match", clauses with same right-hand + side are factorized and the last most factorized clause with no + variables, if it exists, is turned into a default clause. + Use "Unset Printing Allow Default Clause" do deactivate printing + of a default clause. + Use "Unset Printing Factorizable Match Patterns" to deactivate + factorization of clauses with same right-hand side. + Tactics - On Linux, "native_compute" calls can be profiled using the "perf" diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 6704ed4b7..1330b3741 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -852,7 +852,7 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) eqns in + let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> @@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes vars l in (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pl,c)) = - Loc.tag ?loc ([List.map (extern_cases_pattern_in_scope scopes vars) pl], - extern inctx scopes vars c) +and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + Loc.tag ?loc (pll,extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 72c91db6a..f311d33b8 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -93,6 +93,14 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located +type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list +type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list + +type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g +type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g +type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g + type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8bf6e48fd..5a9248d47 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -183,7 +183,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -197,6 +199,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -206,6 +209,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6527ba935..5906d5878 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -252,6 +252,89 @@ let lookup_index_as_renamed env sigma t n = in lookup n 1 t (**********************************************************************) +(* Factorization of match patterns *) + +let print_factorize_match_patterns = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "factorization of \"match\" patterns in printing"; + optkey = ["Printing";"Factorizable";"Match";"Patterns"]; + optread = (fun () -> !print_factorize_match_patterns); + optwrite = (fun b -> print_factorize_match_patterns := b) } + +let print_allow_match_default_clause = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "possible use of \"match\" default pattern in printing"; + optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; + optread = (fun () -> !print_allow_match_default_clause); + optwrite = (fun b -> print_allow_match_default_clause := b) } + +let rec join_eqns (ids,rhs as x) patll = function + | (loc,(ids',patl',rhs') as eqn')::rest -> + if not !Flags.raw_print && !print_factorize_match_patterns && + List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' + then + join_eqns x (patl'::patll) rest + else + let eqn,rest = join_eqns x patll rest in + eqn, eqn'::rest + | [] -> + patll, [] + +let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll + +let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = [] + +let rec move_more_factorized_default_candidate_to_end eqn n = function + | eqn' :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in + if isbest then false, dft, eqns else false, dft, eqn' :: eqns + else + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in + isbest, dft, eqn' :: eqns + | [] -> true, Some eqn, [] + +let rec select_default_clause = function + | eqn :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in + if isbest then dft, eqns else dft, eqn :: eqns + else + let dft, eqns = select_default_clause eqns in dft, eqn :: eqns + | [] -> None, [] + +let factorize_eqns eqns = + let rec aux found = function + | (loc,(ids,patl,rhs))::rest -> + let patll,rest = join_eqns (ids,rhs) [patl] rest in + aux ((loc,(ids,patll,rhs))::found) rest + | [] -> + found in + let eqns = aux [] (List.rev eqns) in + let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in + if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + match select_default_clause eqns with + (* At least two clauses and the last one is disjunctive with no variables *) + | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)] + (* Only one clause which is disjunctive with no variables: we keep at least one constructor *) + (* so that it is not interpreted as a dummy "match" *) + | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)] + | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false + | None, eqns -> eqns + else + eqns + +(**********************************************************************) (* Fragile algorithm to reverse pattern-matching compilation *) let update_name sigma na ((_,(e,_)),c) = @@ -290,7 +373,7 @@ let rec build_tree na isgoal e sigma ci cl = (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) sigma = match nal with - | [] -> [[],rhs] + | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with | Case (ci,p,c,cl) when @@ -300,19 +383,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e sigma ci cl in List.flatten - (List.map (fun (pat,rhs) -> + (List.map (fun (ids,pat,rhs) -> let lines = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) lines) + List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines) clauses) | _ -> - let pat = DAst.make @@ PatVar(update_name sigma na rhs) in + let na = update_name sigma na rhs in + let pat = DAst.make @@ PatVar na in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) mat + List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat -and contract_branch isgoal e sigma (cdn,can,mkpat,b) = - let nal,rhs = decomp_branch cdn [] isgoal e sigma b in +and contract_branch isgoal e sigma (cdn,can,mkpat,rhs) = + let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat + List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) @@ -648,7 +732,7 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c)) + List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cb1c0d8d4..f150cb195 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -26,10 +26,20 @@ val print_universes : bool ref (** If true, prints full local context of evars *) val print_evar_arguments : bool ref +(** If true, contract branches with same r.h.s. and same matching + variables in a disjunctive pattern *) +val print_factorize_match_patterns : bool ref + +(** If true and the last non unique clause of a "match" is a + variable-free disjunctive pattern, turn it into a catch-call case *) +val print_allow_match_default_clause : bool ref + val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern val subst_glob_constr : substitution -> glob_constr -> glob_constr +val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g + (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in [avoid] [isgoal] tells if naming must avoid global-level synonyms as intro does diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 97fa8e254..419dcadb4 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -95,8 +95,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl x : nat n, n0 := match x + 0 with - | 0 => 0 - | S _ => 0 + | 0 | S _ => 0 end : nat e, e0 := match x + 0 as y return (y = y) with @@ -104,8 +103,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl | S n => eq_refl end : x + 0 = x + 0 n1, n2 := match x with - | 0 => 0 - | S _ => 0 + | 0 | S _ => 0 end : nat e1, e2 := match x return (x = x) with | 0 => eq_refl @@ -126,3 +124,48 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl end : p = p /\ p = p ============================ eq_refl = eq_refl +fun x : comparison => match x with + | Eq => 1 + | _ => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt => 0 + | Gt => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt | Gt => 0 + end + : comparison -> nat +fun x : comparison => +match x return nat with +| Eq => S O +| Lt => O +| Gt => O +end + : forall _ : comparison, nat +fun x : K => match x with + | a3 | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a3 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a3 | a4 => 3 + | _ => 2 + end + : K -> nat diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 17fee3303..caf3b2870 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -1,5 +1,7 @@ (* Cases with let-in in constructors types *) +Unset Printing Allow Match Default Clause. + Inductive t : Set := k : let x := t in x -> x. @@ -184,3 +186,33 @@ let p := fresh "p" in |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) end. Show. + +Set Printing Allow Match Default Clause. + +(***************************************************) +(* Testing strategy for factorizing cases branches *) + +(* Factorization + default clause *) +Check fun x => match x with Eq => 1 | _ => 0 end. + +(* No factorization *) +Unset Printing Factorizable Match Patterns. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Factorizable Match Patterns. + +(* Factorization but no default clause *) +Unset Printing Allow Match Default Clause. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Allow Match Default Clause. + +(* No factorization in printing all mode *) +Set Printing All. +Check fun x => match x with Eq => 1 | _ => 0 end. +Unset Printing All. + +(* Several clauses *) +Inductive K := a1|a2|a3|a4|a5|a6. +Check fun x => match x with a3 | a4 => 3 | _ => 2 end. +Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index a1028bda0..121a369a9 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -37,6 +37,17 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat Notation plus2 n := (S(S(n))) +λ n : list(nat), match n with + | 1 :: nil => 0 + | _ => 2 + end + : list(nat) -> nat +λ n : list(nat), +match n with +| 1 :: nil => 0 +| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 +end + : list(nat) -> nat λ n : list(nat), match n with | nil => 2 diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 4c3eaa0c7..531398bb0 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -79,6 +79,13 @@ Notation plus2 n := (S (S n)). (* plus2 was not correctly printed in the two following tests in 8.3pl1 *) Print plus2. Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Allow Match Default Clause. +Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Factorizable Match Patterns. +Check fun n => match n with list1 => 0 | _ => 2 end. +Set Printing Allow Match Default Clause. +Set Printing Factorizable Match Patterns. + End A. (* This one is not fully satisfactory because binders in the same type |