From d8b78f30453f93a413ca98c3e858363e9d13e47c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Apr 2007 14:53:04 +0000 Subject: [PATCH] one more step toward a decent destruct lifting should now be ok, but handling of wight params is still shaky --- .../tactics/discriminationTactics.ml | 43 +++++++++++++------ 1 file changed, 29 insertions(+), 14 deletions(-) diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 9bcdf6040..5a25c00fa 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/components/tactics/discriminationTactics.ml @@ -207,6 +207,11 @@ let exn_injwronggoal = let exn_noneqind = ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type");; +let pp ctx t = + let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in + CicPp.pp t names +;; + let rec injection_tac ~first_time ~term ~liftno ~continuation = let module C = Cic in let module CR = CicReduction in @@ -215,7 +220,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation = let module T = Tacticals in let module PST = ProofEngineStructuralRules in let module PET = ProofEngineTypes in - let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in +(* let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in *) let are_convertible hd1 hd2 metasenv context = fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph) in @@ -227,7 +232,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation = let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in - prerr_endline ("injection su: " ^ CicPp.ppterm termty); +(* prerr_endline ("\ninjection su: " ^ pp context termty); *) let tac = match termty with | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] @@ -317,7 +322,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = let module P = PrimitiveTactics in let module PET = ProofEngineTypes in let module T = Tacticals in - let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in +(* let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in *) let give_name seed = function | C.Name _ as name -> name | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed) @@ -334,7 +339,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in - prerr_endline ("injection1 su : " ^ CicPp.ppterm termty); +(* prerr_endline ("\ninjection1 su : " ^ pp context termty); *) match termty with (* an equality *) | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2] when LibraryObjects.is_eq_URI equri -> @@ -374,14 +379,15 @@ and injection1_tac ~term ~i ~liftno ~continuation = let binder' = give_name seed binder in C.Lambda (binder',source,(aux (k+1) target)) | _ -> - let nr_param_constr = k - paramsno in + let nr_param_constr = k - paramsno - 1 in if id = i_constr_id then C.Rel (k - i) else S.lift nr_param_constr t1' (* + 1 per liftare anche il lambda aggiunto * esternamente al case *) - in aux 1 reduced_cty) + in CicSubstitution.lift 1 (aux 1 reduced_cty)) constructor_list in + (* this code should be taken from cases_tac *) let outtype = let seed = ref 0 in let rec to_lambdas te head = @@ -399,7 +405,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = | _, _ -> assert false in let abstracted_tty = - match CicSubstitution.lift (paramsno(* + 1*)) tty with + match CicSubstitution.lift paramsno tty with | C.MutInd _ as tty' -> tty' | C.Appl l -> let keep,abstract = HExtlib.split_nth (paramsno +1) l in @@ -409,15 +415,20 @@ and injection1_tac ~term ~i ~liftno ~continuation = match ind_type_list with | [] -> assert false | (_,_,ty,_)::_ -> + (* this is in general wrong, do as in cases_tac *) to_lambdas (skip_prods left_params ty) (C.Lambda - (C.Name "x", abstracted_tty, S.lift 1 tty')) + (C.Name "x", abstracted_tty, + (* here we should capture right parameters *) + (* 1 for his Lambda, one for the Lambda outside the match + * and then one for each to_lambda *) + S.lift (2+List.length right_params) tty')) in patterns,outtype | _ -> raise exn_discrnonind in let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in - prerr_endline ("CUT: " ^ CicPp.ppterm cutted); +(* prerr_endline ("CUT: " ^ pp context cutted); *) PET.apply_tactic (T.thens ~start: (P.cut_tac cutted) ~continuations: @@ -430,7 +441,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = ;T.then_ ~start:(PET.mk_tactic (fun status -> - prerr_endline "riempo il cut"; +(* prerr_endline "riempo il cut"; *) let (proof, goal) = status in let _,metasenv,_,_, _ = proof in let _,context,gty =CicUtil.lookup_meta goal metasenv in @@ -446,14 +457,18 @@ and injection1_tac ~term ~i ~liftno ~continuation = C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1] in +(* prerr_endline - ("metto questo: " ^ CicPp.ppterm changed); + ("metto questo: " ^ pp context changed); prerr_endline - ("al posto di questo: " ^ CicPp.ppterm new_t1'); + ("al posto di questo: " ^ pp context new_t1'); prerr_endline - ("nel goal: " ^ CicPp.ppterm gty); + ("nel goal: " ^ pp context gty); prerr_endline ("nel contesto:\n" ^ CicPp.ppcontext context); + prerr_endline + ("e poi rewrite con: "^pp context term); +*) let rc = PET.apply_tactic (ReductionTactics.change_tac @@ -462,7 +477,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = ~term:gty [new_t1'])) (fun _ m u -> changed,m,u)) status - in prerr_endline "fine";rc + in rc )) ~continuation: (T.then_ -- 2.39.2