From 5a88ca4db8f9d97a58add90a8a23f06960d9364f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 18 Oct 2011 09:40:12 +0000 Subject: [PATCH] Changes in "destruct" tactic (allowing performance improvements): 1) discrimination principles are now generated upon definition of an inductive type I and recorded as objects I_discr and I_jmdiscr (resp. leibniz and john major's principles); in case JMeq wasn't loaded at that time, it is possible to explicitly request the definition by means of the command discriminator I. 2) destruct uses the aforementioned principle rather than generating a cut at each discrimination step 3) destruct performs generalizations using the basic generalize0_tac, rather than generalize_tac: this should bring small performance improvements. --- .../grafite_engine/grafiteEngine.ml | 69 +++- matita/components/ng_kernel/nCic.ml | 1 + matita/components/ng_kernel/nCicPp.ml | 1 + matita/components/ng_tactics/nDestructTac.ml | 350 +++++++++--------- matita/components/ng_tactics/nDestructTac.mli | 6 + matita/components/ng_tactics/nTactics.ml | 2 +- matita/components/ng_tactics/nTactics.mli | 1 + matita/matita/matita.lang | 1 + 8 files changed, 248 insertions(+), 183 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index f286cf6b8..9c0f456b2 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -603,6 +603,57 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) | _ -> status in + let status = match nobj with + NCic.Inductive (is_ind,leftno,itl,_) -> + (* first leibniz *) + let status' = List.fold_left + (fun status it -> + let _,ind_name,ty,cl = it in + let status = status#set_ng_mode `ProofMode in + try + (let status,invobj = + NDestructTac.mk_discriminator ~use_jmeq:false + (ind_name ^ "_discr") + it leftno status status#baseuri in + let _,_,menv,_,_ = invobj in + (match menv with + [] -> eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status)) + (* XXX *) + with + | NDestructTac.ConstructorTooBig k -> + HLog.warn (Printf.sprintf + "unable to generate leibniz discrimination principle (constructor %s too big)" + k); + let status = status#set_ng_mode `CommandMode in status + | _ -> (*HLog.warn "error in generating discrimination principle"; *) + let status = status#set_ng_mode `CommandMode in + status) + status itl + in + (* then JMeq *) + List.fold_left + (fun status it -> + let _,ind_name,ty,cl = it in + let status = status#set_ng_mode `ProofMode in + try + (let status,invobj = + NDestructTac.mk_discriminator ~use_jmeq:true + (ind_name ^ "_jmdiscr") + it leftno status status#baseuri in + let _,_,menv,_,_ = invobj in + (match menv with + [] -> eval_ncommand ~include_paths opts status + ("",0,GrafiteAst.NQed Stdpp.dummy_loc) + | _ -> status)) + (* XXX *) + with _ -> (*HLog.warn "error in generating discrimination principle"; *) + let status = status#set_ng_mode `CommandMode in + status) + status' itl + | _ -> status + in let coercions = match obj with _,_,_,_,NCic.Inductive @@ -684,24 +735,26 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> status) - | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> + | GrafiteAst.NDiscriminator (loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") else let status = status#set_ng_mode `ProofMode in let metasenv,subst,status,indty = - GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in - let indtyno, (_,_,tys,_,_) = match indty with - NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) -> - indtyno, NCicEnvironment.get_checked_indtys r + GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in + let indtyno, (_,_,tys,_,_),leftno = match indty with + NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) -> + indtyno, NCicEnvironment.get_checked_indtys status r, leftno | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in - let it = List.nth tys indtyno in - let status,obj = NDestructTac.mk_discriminator it status in + let (_,ind_name,_,_ as it) = List.nth tys indtyno in + let status,obj = + NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr") + it leftno status status#baseuri in let _,_,menv,_,_ = obj in (match menv with [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> prerr_endline ("Discriminator: non empty metasenv"); - status, []) *) + status) | GrafiteAst.NInverter (loc, name, indty, selection, sort) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml index 7e4e4f855..94dc827c8 100644 --- a/matita/components/ng_kernel/nCic.ml +++ b/matita/components/ng_kernel/nCic.ml @@ -94,6 +94,7 @@ type def_pragma = (* pragmatic of the object *) | `Elim of sort (* elimination principle; universe is not relevant *) | `Projection (* record projection *) | `InversionPrinciple (* inversion principle *) + | `DiscriminationPrinciple (* discrimination principle *) | `Variant | `Local | `Regular ] (* Local = hidden technicality *) diff --git a/matita/components/ng_kernel/nCicPp.ml b/matita/components/ng_kernel/nCicPp.ml index 0d78c4971..11ba55e78 100644 --- a/matita/components/ng_kernel/nCicPp.ml +++ b/matita/components/ng_kernel/nCicPp.ml @@ -280,6 +280,7 @@ let string_of_pragma = function | `Elim _sort -> "Elim _" | `Projection -> "Projection" | `InversionPrinciple -> "InversionPrinciple" + | `DiscriminationPrinciple -> "DiscriminationPrinciple" | `Variant -> "Variant" | `Local -> "Local" | `Regular -> "Regular" diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index dd7a2c3c4..de4c23a1c 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -44,6 +44,8 @@ let mk_id id = NotationPt.Ident (id,None) ;; +let mk_sym s = NotationPt.Symbol (s,0);; + let rec mk_prods l t = match l with [] -> t @@ -71,6 +73,14 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o) ;; +(* needed to workaround a weakness of the refiner? *) +let rec generalize0_tac tl s = + match tl with + | [] -> s + | t0::tl0 -> NTactics.generalize0_tac [t0] (generalize0_tac tl0 s) +;; + + (* input: nome della variabile riscritta * output: lista dei nomi delle variabili il cui tipo dipende dall'input *) let cascade_select_in_ctx status ~subst ctx skip iname = @@ -161,11 +171,18 @@ let hp_pattern_jm n = ; NotationPt.Implicit `JustOne ] ], None);; -(* returns the discrimination = injection+contradiction principle *) +(* creates the discrimination = injection+contradiction principle *) +exception ConstructorTooBig of string;; -let mk_discriminator it ~use_jmeq nleft xyty status = - let _,indname,_,cl = it in +let mk_discriminator ~use_jmeq name it leftno status baseuri = + let itnargs = + let _,_,arity,_ = it in + List.length (arg_list 0 arity) in + let _,itname,_,_ = it in + let params = List.map (fun x -> "a" ^ string_of_int x) (HExtlib.list_seq 1 (itnargs+1)) in + let xyty = mk_appl (List.map mk_id (itname::params)) in + (* PHASE 1: derive the type of the discriminator (we'll name it "principle") *) let mk_eq tys ts us es n = if use_jmeq then @@ -192,15 +209,16 @@ let mk_discriminator it ~use_jmeq nleft xyty status = List.nth us n] in + + let _,_,_,cl = it in - let kname it j = - let _,_,_,cl = it in + let kname (*it*) j = let _,name,_ = List.nth cl j in name in let branch i j ts us = - let nargs = nargs it nleft i in + let nargs = nargs it leftno i in let es = List.map (fun x -> mk_id ("e" ^ string_of_int x)) (HExtlib.list_seq 0 nargs) in let tys = List.map (fun x -> iter @@ -216,10 +234,10 @@ let mk_discriminator it ~use_jmeq nleft xyty status = NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), acc))) (nargs-1) (mk_appl [mk_id "eq"; NotationPt.Implicit `JustOne; - mk_appl (mk_id (kname it i):: + mk_appl (mk_id (kname i):: List.map (fun x -> mk_id ("x" ^string_of_int x)) (HExtlib.list_seq 0 (List.length ts))); - mk_appl (mk_id (kname it j)::us)])] + mk_appl (mk_id (kname j)::us)])] in (** NotationPt.Binder (`Lambda, (mk_id "e", Some (mk_appl @@ -256,12 +274,12 @@ let mk_discriminator it ~use_jmeq nleft xyty status = None, List.map (fun j -> - let nargs_kty = nargs it nleft j in + let nargs_kty = nargs it leftno j in let us = iter (fun m acc -> mk_id ("u" ^ (string_of_int m))::acc) (nargs_kty - 1) [] in let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in - NotationPt.Pattern (kname it j, + NotationPt.Pattern (kname j, None, List.combine us nones), branch i j ts us) @@ -272,42 +290,50 @@ let mk_discriminator it ~use_jmeq nleft xyty status = None , List.map (fun i -> - let nargs_kty = nargs it nleft i in + let nargs_kty = nargs it leftno i in + if (nargs_kty > 5 && not use_jmeq) then raise (ConstructorTooBig (kname i)); let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc) (nargs_kty - 1) [] in let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in - NotationPt.Pattern (kname it i, + NotationPt.Pattern (kname i, None, List.combine ts nones), inner i ts) (HExtlib.list_seq 0 (List.length cl))) in - let principle = NotationPt.Binder (`Lambda, (mk_id "x", Some xyty), - NotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer)) + let principle = + mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", + Some xyty), + NotationPt.Binder (`Forall, (mk_id "y", Some xyty), + (if use_jmeq then + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl + [mk_sym "jmsimeq"; NotationPt.Implicit `JustOne; mk_id "x"; + NotationPt.Implicit `JustOne; mk_id "y"])), + outer) + else + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl [mk_sym "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), + outer))))) in pp (lazy ("discriminator = " ^ (NotationPp.pp_term status principle))); - - status, principle -;; - -let hd_of_term = function - | NCic.Appl (hd::_) -> hd - | t -> t -;; - -let name_of_rel ~context rel = - let s, _ = List.nth context (rel-1) in s -;; - -(* let lookup_in_ctx ~context n = - List.nth context ((List.length context) - n - 1) -;;*) - -let mk_sym s = NotationPt.Symbol (s,0);; - -let discriminate_tac ~context cur_eq status = - pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq))); + (* PHASE 2: create the object for the proof of the principle: we'll name it + * "theorem" *) + let status, theorem = + GrafiteDisambiguate.disambiguate_nobj status ~baseuri + (baseuri ^ name ^ ".def",0, + NotationPt.Theorem + (`Theorem,name,principle, + Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple)) + in + let uri,height,nmenv,nsubst,nobj = theorem in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = status#set_obj theorem in + let status = status#set_stack ninitial_stack in + let status = subst_metasenv_and_fix_names status in + + (* PHASE 3: we finally prove the discrimination principle *) let dbranch it ~use_jmeq leftno consno = let refl_id = mk_sym "refl" in pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno)); @@ -323,7 +349,6 @@ let discriminate_tac ~context cur_eq status = ] in let dbranches it ~use_jmeq leftno = pp (lazy (Printf.sprintf "dbranches %d" leftno)); - let _,_,_,cl = it in let nbranches = List.length cl in let branches = iter (fun n acc -> let m = nbranches - n - 1 in @@ -335,15 +360,49 @@ let discriminate_tac ~context cur_eq status = NTactics.branch_tac ~force:false:: branches @ [NTactics.merge_tac] else branches in + let print_tac s status = pp s ; status in + + let status = + NTactics.block_tac ( + [print_tac (lazy "ci sono"); + NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern + ] + @ List.map (fun x -> NTactics.intro_tac x) params @ + [NTactics.intro_tac "x"; + NTactics.intro_tac "y"; + NTactics.intro_tac "Deq"; + print_tac (lazy "ci sono 2"); + NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern; + NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern] + @ dbranches it ~use_jmeq leftno) status + in status, status#obj +;; + +let hd_of_term = function + | NCic.Appl (hd::_) -> hd + | t -> t +;; + +let name_of_rel ~context rel = + let s, _ = List.nth context (rel-1) in s +;; + +(* let lookup_in_ctx ~context n = + List.nth context ((List.length context) - n - 1) +;;*) + +let discriminate_tac ~context cur_eq status = + pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq))); + let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in let _,ctx' = HExtlib.split_nth cur_eq context in let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in let status, s = term_of_cic_term status s ctx' in - let status, leftno, it, use_jmeq = - let it, t1, t2, use_jmeq = match s with - | NCic.Appl [_;it;t1;t2] -> it,t1,t2,false - | NCic.Appl [_;it;t1;_;t2] -> it,t1,t2,true + let status,it,use_jmeq = + let it,use_jmeq = match s with + | NCic.Appl [_;it;_;_] -> it,false + | NCic.Appl [_;it;_;_;_] -> it,true | _ -> assert false in (* XXX: serve? ho già fatto whd *) let status, it = whd status ctx' (mk_cic_term ctx' it) in @@ -355,8 +414,8 @@ let discriminate_tac ~context cur_eq status = uri, indtyno, NCicEnvironment.get_checked_indtys status r | _ -> pp (lazy ("discriminate: indty =" ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] it)) ; assert false in - let _,leftno,its,_,_ = its in - status, leftno, List.nth its indtyno, use_jmeq + let _,_,its,_,_ = its in + status,List.nth its indtyno, use_jmeq in let itnargs = @@ -364,48 +423,16 @@ let discriminate_tac ~context cur_eq status = List.length (arg_list 0 arity) in let _,itname,_,_ = it in let params = List.map (fun x -> "a" ^ string_of_int x) (HExtlib.list_seq 1 (itnargs+1)) in - let xyty = mk_appl (List.map mk_id (itname::params)) in - let print_tac s status = pp s ; status in - NTactics.block_tac ( - [(fun status -> - let status, discr = mk_discriminator it ~use_jmeq leftno xyty status in - let cut_term = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", - Some xyty), - NotationPt.Binder (`Forall, (mk_id "y", Some xyty), - (if use_jmeq then fun tgt -> - NotationPt.Binder (`Forall, (mk_id "e", - Some (mk_appl - [mk_sym "jmsimeq"; NotationPt.Implicit `JustOne; mk_id "x"; - NotationPt.Implicit `JustOne; mk_id "y"])),tgt) - else fun tgt -> - NotationPt.Binder (`Forall, (mk_id "e", - Some (mk_appl [mk_sym "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])),tgt)) - (mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in - let status = print_tac (lazy ("cut_term = "^ NotationPp.pp_term status cut_term)) status in - NTactics.cut_tac ("",0, cut_term) - status); - NTactics.branch_tac; - print_tac (lazy "ci sono"); - NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern - ] - @ List.map (fun x -> NTactics.intro_tac x) params @ - [NTactics.intro_tac "x"; - NTactics.intro_tac "y"; - NTactics.intro_tac "Deq"; - print_tac (lazy "ci sono 2"); - NTactics.rewrite_tac ~dir:`RightToLeft ~what:("",0,mk_id "Deq") ~where:default_pattern; - NTactics.cases_tac ~what:("",0,mk_id "x") ~where:default_pattern] - @ dbranches it ~use_jmeq leftno @ - [NTactics.shift_tac; - print_tac (lazy "ci sono 3"); - NTactics.intro_tac "#discriminate"; - NTactics.apply_tac ("",0,mk_appl ([mk_id "#discriminate"]@ + let principle_name = + if use_jmeq then itname ^ "_jmdiscr" + else itname ^ "_discr" + in + pp (lazy ("apply (" ^ principle_name ^ " " ^ + (String.concat "" (HExtlib.mk_list "?" (List.length params + 2))) ^ + " " ^ eq_name ^ ")")); + NTactics.apply_tac ("",0,mk_appl ([mk_id principle_name]@ HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length params + 2) @ - [mk_id eq_name ])); -(* NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern; *) - NTactics.clear_tac ["#discriminate"]; - NTactics.merge_tac; print_tac (lazy "the end of discriminate")] - ) status + [mk_id eq_name ])) status ;; let saturate_skip status context skip = @@ -445,16 +472,22 @@ let subst_tac ~context ~dir skip cur_eq = if (List.exists (fun x -> List.mem x skip) names_to_gen) then oldstatus else - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@ - [NTactics.clear_tac names_to_gen; + let gen_tac x = + (fun s -> + let x' = String.concat " " x in + let x = List.map mk_id x in + (* let s = NTactics.print_tac false ("@generalize " ^ x') s in *) + generalize0_tac x s) in + NTactics.block_tac ( + (* (List.map gen_tac names_to_gen)@ *) + [gen_tac (List.rev names_to_gen); + NTactics.clear_tac names_to_gen; NTactics.rewrite_tac ~dir ~what:("",0,mk_id eq_name) ~where:default_pattern; (* NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern;*) - NTactics.try_tac (NTactics.clear_tac [eq_name])]@ + NTactics.try_tac (NTactics.clear_tac [eq_name]); +]@ (List.map NTactics.intro_tac (List.rev names_to_gen))) status ;; @@ -465,93 +498,62 @@ let clearid_tac ~context skip cur_eq = let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) in let status, s = term_of_cic_term status s ctx' in let skip = saturate_skip status context skip in - (* - let streicher_id = - match s with - | NCic.Appl [_;_;_;_] -> mk_id "streicherK" - | NCic.Appl [_;_;_;_;_] -> mk_id "streicherKjmeq" - | _ -> assert false - in - pp (lazy (Printf.sprintf "clearid: equation %s" eq_name)); - let names_to_gen, _ = - cascade_select_in_ctx ~subst:(get_subst status) context cur_eq in - let names_to_gen = names_to_gen @ [eq_name] in - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@ - [NTactics.clear_tac names_to_gen; - NTactics.apply_tac ("",0, mk_appl [streicher_id; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne]); - NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern] @ - (let names_to_intro = - match List.rev names_to_gen with - | [] -> [] - | _::tl -> tl in - List.map NTactics.intro_tac names_to_intro)) status -*) pp (lazy (Printf.sprintf "clearid: equation %s" eq_name)); - match s with - | NCic.Appl [_;_;_;_] -> - (* leibniz *) - let streicher_id = mk_id "streicherK" - in - let names_to_gen, _ = - cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in - let names_to_gen = names_to_gen @ [eq_name] in - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@ - [NTactics.clear_tac names_to_gen; - NTactics.apply_tac ("",0, mk_appl [streicher_id; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne]); -(* NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern *) - ] @ - (let names_to_intro = - match List.rev names_to_gen with - | [] -> [] - | _::tl -> tl in - List.map NTactics.intro_tac names_to_intro)) status - | NCic.Appl [_;_;_;_;_] -> - (* JMeq *) - let streicher_id = mk_id "streicherK" - in - let names_to_gen, _ = - cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in - let names_to_gen = names_to_gen (* @ [eq_name]*) in - let gen_tac x = - NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in - let gen_eq = NTactics.generalize_tac - ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq"; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - mk_id eq_name]),[], Some NotationPt.UserInput)) in - NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq:: - [NTactics.clear_tac names_to_gen; - NTactics.try_tac (NTactics.clear_tac [eq_name]); - NTactics.apply_tac ("",0, mk_appl [streicher_id; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne; - NotationPt.Implicit `JustOne]); -(* NTactics.reduce_tac ~reduction:(`Normalize true) - ~where:default_pattern *) - ] @ - (let names_to_intro = List.rev names_to_gen in - List.map NTactics.intro_tac names_to_intro)) status - | _ -> assert false + let streicher_id = mk_id "streicherK" in + let names_to_gen, _ = + cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in + let gen_tac x = generalize0_tac (List.map mk_id x) in + + match s with + (* jmeq *) + | NCic.Appl [_;_;_;_;_] -> + let names_to_gen = List.rev names_to_gen in + (*let gen_eq = NTactics.generalize_tac + ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq"; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + mk_id eq_name]),[], Some + NotationPt.UserInput)) in*) + let gen_eq = generalize0_tac + [mk_appl [mk_id "jmeq_to_eq"; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + mk_id eq_name]] in + NTactics.block_tac ((gen_tac (List.rev names_to_gen))::gen_eq:: + [NTactics.clear_tac names_to_gen; + NTactics.try_tac (NTactics.clear_tac [eq_name]); + NTactics.apply_tac ("",0, mk_appl [streicher_id; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]); + ] @ + (List.map NTactics.intro_tac names_to_gen)) status + + (* leibniz *) + | NCic.Appl [_;_;_;_] -> + begin + let names_to_gen, _ = + cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in + let names_to_gen = eq_name :: (List.rev names_to_gen) in + NTactics.block_tac ((gen_tac names_to_gen):: + [NTactics.clear_tac names_to_gen; + NTactics.apply_tac ("",0, mk_appl [streicher_id; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]) + (* NTactics.reduce_tac ~reduction:(`Normalize true) + ~where:default_pattern *) + ] @ + let names_to_intro = List.tl names_to_gen in + (List.map NTactics.intro_tac names_to_intro)) status + end + | _ -> assert false + ;; let get_ctx st goal = diff --git a/matita/components/ng_tactics/nDestructTac.mli b/matita/components/ng_tactics/nDestructTac.mli index 714638d24..f753fa61e 100644 --- a/matita/components/ng_tactics/nDestructTac.mli +++ b/matita/components/ng_tactics/nDestructTac.mli @@ -13,3 +13,9 @@ val destruct_tac : string list option -> string list -> 's NTacStatus.tactic +val mk_discriminator: (use_jmeq: bool) -> + string -> NCic.inductiveType -> int -> + (#NTacStatus.tac_status as 's) -> string -> 's * NCic.obj + +exception ConstructorTooBig of string + diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index dbc134319..104a044f6 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -390,7 +390,7 @@ let select0_tac ~where ~job = let status, instance = mk_meta status newgoalctx (`Decl newgoalty) `IsTerm in - instantiate ~refine:false status goal instance) + instantiate ~refine:false status goal instance) ;; let select_tac ~where:((txt,txtlen,(wanted,hyps,path)) as where) ~job diff --git a/matita/components/ng_tactics/nTactics.mli b/matita/components/ng_tactics/nTactics.mli index 985849b63..5290a322e 100644 --- a/matita/components/ng_tactics/nTactics.mli +++ b/matita/components/ng_tactics/nTactics.mli @@ -54,6 +54,7 @@ val rewrite_tac: dir:[ `LeftToRight | `RightToLeft ] -> what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic +val generalize0_tac : NotationPt.term list -> 's NTacStatus.tactic val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic val clear_tac : string list -> 's NTacStatus.tactic val reduce_tac: diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang index 62bfaccee..be110b9ba 100644 --- a/matita/matita/matita.lang +++ b/matita/matita/matita.lang @@ -114,6 +114,7 @@ coinductive corec default + discriminator for include include' -- 2.39.2