From 722d0c21cb2f8da64b1c54f854c8dc401edd25e6 Mon Sep 17 00:00:00 2001 From: corbinea Date: Tue, 27 Oct 2009 08:57:43 +0000 Subject: fixed czar bug with parametric inductives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12423 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/decl_interp.ml | 6 +++--- tactics/decl_proof_instr.ml | 44 ++++++++++++++++++++++++++++++-------------- tactics/decl_proof_instr.mli | 18 ++++++++++++------ tactics/refine.ml | 2 ++ 4 files changed, 47 insertions(+), 23 deletions(-) (limited to 'tactics') diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index 77357e3fa..bfb5039d5 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -327,9 +327,9 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let _ = let expected = mib.Declarations.mind_nparams - num_params in if List.length params <> expected then - errorlabstrm "suppose it is" - (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ + errorlabstrm "suppose it is" + (str "Wrong number of extra arguments: " ++ + (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index c2a32471e..bde403657 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -1151,9 +1151,9 @@ let case_tac params pat_info hyps gls0 = | _ -> anomaly "wrong place for cases" in let clause = build_dep_clause params pat_info per_info hyps gls0 in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in - let nek = - register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info - pat_info.pat_pat ek in + let nek = + register_dep_subcase (id,(List.length params,List.length hyps)) + (pf_env gls0) per_info pat_info.pat_pat ek in let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in tclTHENS (assert_postpone id clause) [tclTHENLIST @@ -1216,6 +1216,7 @@ let hrec_for fix_id per_info gls obj_id = let hd2 = applist (mkVar fix_id,args@[obj]) in compose_lam rc (whd_beta gls.sigma hd2) + let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with Close_patt t,_ -> @@ -1224,16 +1225,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | Skip_patt (_,t),skipped::next_objs -> let args0 = push_arg skipped args in execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls - | End_patt (id,nhyps),[] -> + | End_patt (id,(nparams,nhyps)),[] -> begin match List.assoc id args with - [None,br_args] -> - let metas = - list_tabulate (fun n -> mkMeta (succ n)) nhyps in + [None,br_args] -> + let all_metas = + list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + let param_metas,hyp_metas = list_chop nparams all_metas in tclTHEN (tclDO nhrec introf) - (tacnext - (applist (mkVar id,List.rev_append br_args metas))) gls + (tacnext + (applist (mkVar id, + List.append param_metas + (List.rev_append br_args hyp_metas)))) gls | _ -> anomaly "wrong stack size" end | Split_patt (ids,ind,br), casee::next_objs -> @@ -1307,7 +1311,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | End_patt (_,_) , _ :: _ -> anomaly "execute_cases : End of branch with garbage left" - +let understand_my_constr c gls = + let env = pf_env gls in + let nc = names_of_rel_context env in + let rawc = Detyping.detype false [] nc c in + let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in + Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + +let set_refine,my_refine = +let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in +((fun tac -> refine:= tac), +(fun c gls -> + let oc = understand_my_constr c gls in + !refine oc gls)) (* end focus/claim *) @@ -1348,9 +1364,9 @@ let end_tac et2 gls = simple_induct (AnonHyp (succ (List.length pi.per_args))); default_justification (List.map mkVar clauses)] | ET_Case_analysis,EK_dep tree -> - execute_cases Anonymous pi - (fun c -> tclTHENLIST - [refine c; + execute_cases Anonymous pi + (fun c -> tclTHENLIST + [my_refine c; clear clauses; justification assumption]) (initial_instance_stack clauses) [pi.per_casee] 0 tree @@ -1371,7 +1387,7 @@ let end_tac et2 gls = (fun c -> tclTHENLIST [clear [fix_id]; - refine c; + my_refine c; clear clauses; justification assumption]) (initial_instance_stack clauses) diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index a05c36e93..ada5e7448 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -42,21 +42,21 @@ val execute_cases : (Names.Idset.elt * (Term.constr option * Term.constr list) list) list -> Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic -val tree_of_pats : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> +val tree_of_pats : + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree -val add_branch : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> +val add_branch : + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> (Names.Idset.t * Decl_mode.split_tree) option -> (Names.Idset.t * Decl_mode.split_tree) option val append_tree : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> @@ -65,8 +65,13 @@ val build_dep_clause : Term.types Decl_expr.statement list -> (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types +<<<<<<< HEAD:tactics/decl_proof_instr.mli val register_dep_subcase : Names.identifier * int -> +======= +val register_dep_subcase : + Names.identifier * (int * int) -> +>>>>>>> ada3fb4... fixed czar bug with parametric inductives:tactics/decl_proof_instr.mli Environ.env -> Decl_mode.per_info -> Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind @@ -116,3 +121,4 @@ val init_tree: (Names.Idset.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree +val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit diff --git a/tactics/refine.ml b/tactics/refine.ml index 5258b319b..fe81dadce 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -379,3 +379,5 @@ let refine (evd,c) gl = complicated to update meta types when passing through a binder *) let th = compute_metamap (pf_env gl) evd c in tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl + +let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *) -- cgit v1.2.3