From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:30:41 +0000 (+0000) Subject: - attributes support X-Git-Tag: V_0_1_0~105 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=883bfac8ffa054608e4923d185405dbcb0a06f0f;p=helm.git - attributes support - removed ancient debug prints --- diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 781e6f5c8..cfed56c95 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -99,30 +99,21 @@ and injection1_tac ~term ~i = match tty with (* some inductive type *) (C.MutInd (turi,typeno,exp_named_subst)) | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> - prerr_endline ("XXXX term " ^ CicPp.ppterm term) ; - prerr_endline ("XXXX termty " ^ CicPp.ppterm termty) ; - prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; - prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; - prerr_endline ("XXXX tty " ^ CicPp.ppterm tty) ; let t1',t2',consno = (* sono i due sottotermini che differiscono *) match t1,t2 with ((C.Appl ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1))::applist1)), (C.Appl ((C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))::applist2))) when (uri1 = uri2) && (typeno1 = typeno2) && (consno1 = consno2) && (exp_named_subst1 = exp_named_subst2) -> (* controllo ridondante *) (List.nth applist1 (i-1)),(List.nth applist2 (i-1)),consno2 - | _ -> raise (ProofEngineTypes.Fail "Injection: qui non dovrei capitarci mai") + | _ -> assert false in let tty',_ = CicTypeChecker.type_of_aux' metasenv context t1' CicUniv.empty_ugraph in - prerr_endline ("XXXX tty' " ^ CicPp.ppterm tty') ; - prerr_endline ("XXXX t1' " ^ CicPp.ppterm t1') ; - prerr_endline ("XXXX t2' " ^ CicPp.ppterm t2') ; - prerr_endline ("XXXX consno " ^ string_of_int consno) ; let pattern = match fst(CicEnvironment.get_obj CicUniv.empty_ugraph turi ) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx) -> + C.InductiveDefinition (ind_type_list,_,nr_ind_params_dx,_) -> let _,_,_,constructor_list = (List.nth ind_type_list typeno) in let i_constr_id,_ = List.nth constructor_list (consno - 1) in List.map @@ -149,7 +140,6 @@ and injection1_tac ~term ~i = constructor_list | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible") in - prerr_endline ("XXXX cominciamo!") ; ProofEngineTypes.apply_tactic (T.thens ~start:(P.cut_tac (C.Appl [(C.MutInd (equri,0,[])) ; tty' ; t1' ; t2'])) @@ -164,17 +154,12 @@ and injection1_tac ~term ~i = let (proof, goal) = status in let _,metasenv,_,_ = proof in let _,context,gty = CicUtil.lookup_meta goal metasenv in - prerr_endline ("XXXX goal " ^ string_of_int goal) ; - prerr_endline ("XXXX gty " ^ CicPp.ppterm gty) ; - prerr_endline ("XXXX old t1' " ^ CicPp.ppterm t1') ; - prerr_endline ("XXXX change " ^ CicPp.ppterm (C.Appl [ C.Lambda (C.Name "x", tty, C.MutCase (turi, typeno, (C.Lambda ((C.Name "x"),(S.lift 1 tty),(S.lift 2 tty'))), (C.Rel 1), pattern)); t1])) ; let new_t1' = match gty with (C.Appl (C.MutInd (_,_,_)::arglist)) -> List.nth arglist 1 | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") in - prerr_endline ("XXXX new t1' " ^ CicPp.ppterm new_t1') ; ProofEngineTypes.apply_tactic (P.change_tac ~what:new_t1' @@ -237,8 +222,6 @@ let discriminate'_tac ~term = let consno2 = (* bruuutto: uso un eccezione per terminare con successo! buuu!! :-/ *) try let rec traverse t1 t2 = -prerr_endline ("XXXX t1 " ^ CicPp.ppterm t1) ; -prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; match t1,t2 with ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) @@ -268,7 +251,6 @@ prerr_endline ("XXXX t2 " ^ CicPp.ppterm t2) ; in traverse t1 t2 with (TwoDifferentSubtermsFound consno2) -> consno2 in -prerr_endline ("XXXX consno2 " ^ (string_of_int consno2)) ; if consno2 = 0 then raise (ProofEngineTypes.Fail "Discriminate: Discriminating terms are structurally equal") else @@ -277,12 +259,9 @@ prerr_endline ("XXXX consno2 " ^ (string_of_int consno2)) ; (* a list of "True" except for the element in position consno2 which is "False" *) match fst(CicEnvironment.get_obj CicUniv.empty_ugraph turi) with - C.InductiveDefinition (ind_type_list,_,nr_ind_params) -> -prerr_endline ("XXXX nth " ^ (string_of_int (List.length ind_type_list)) ^ " " ^ (string_of_int typeno)) ; + C.InductiveDefinition (ind_type_list,_,nr_ind_params,_) -> let _,_,_,constructor_list = (List.nth ind_type_list typeno) in -prerr_endline ("XXXX nth " ^ (string_of_int (List.length constructor_list)) ^ " " ^ (string_of_int consno2)) ; let false_constr_id,_ = List.nth constructor_list (consno2 - 1) in -prerr_endline ("XXXX nth funzionano ") ; List.map (function (id,cty) -> let red_ty = CicReduction.whd context cty in (* dubbio: e' corretto ridurre in questo context ??? *) @@ -334,21 +313,6 @@ prerr_endline ("XXXX nth funzionano ") ; ) ~continuation: ( -let u = CicUniv.empty_ugraph in -prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2]) u))); -prerr_endline ("XXXX rewrite<-: " ^ CicPp.ppterm (C.Appl [(C.MutInd (equri,0,[])) ; tty ; t1 ; t2])) ; -prerr_endline ("XXXX equri: " ^ U.string_of_uri equri) ; -prerr_endline ("XXXX tty : " ^ CicPp.ppterm tty) ; -prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ; -prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ; -if (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <> tty then -prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst (CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ; -if (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u)) <> tty then -prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ; -if (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u)) <> -(fst (CicTypeChecker.type_of_aux' metasenv' context' t2 u)) - then prerr_endline ("XXXX tt1': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t1 u))) ; prerr_endline ("XXXX tt2': " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' t2 u))) ; -prerr_endline ("XXXX rewrite<- " ^ CicPp.ppterm term ^ " : " ^ CicPp.ppterm (fst(CicTypeChecker.type_of_aux' metasenv' context' term u))); T.then_ ~start:(EqualityTactics.rewrite_back_simpl_tac ~term) ~continuation:(IntroductionTactics.constructor_tac ~n:1) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 92b89a679..66a9c0930 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -205,11 +205,7 @@ let let module C = Cic in let params = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.Constant (_,_,_,params) - | C.CurrentProof (_,_,_,_,params) - | C.Variable (_,_,_,params) - | C.InductiveDefinition (_,params,_) -> params + CicUtil.params_of_obj o in let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'= let next_fresh_meta = ref newmeta in @@ -222,7 +218,7 @@ let let ty = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.Variable (_,_,ty,_) -> + C.Variable (_,_,ty,_,_) -> CicSubstitution.subst_vars !exp_named_subst_diff ty | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) in @@ -386,7 +382,7 @@ let intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub in mk_tactic (intros_tac ~mk_fresh_name_callback ()) -let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term= +let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term= let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term (proof, goal) @@ -494,7 +490,7 @@ let elim_tac ~term = let name = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tys,_,_) -> + C.InductiveDefinition (tys,_,_,_) -> let (name,_,_,_) = List.nth tys typeno in name | _ -> assert false diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index e53d69048..e43f9221c 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -394,10 +394,10 @@ let reduce context = C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> + | C.Variable (_,None,_,_,_) -> let t' = C.Var (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> + | C.Variable (_,Some body,_,_,_) -> (reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body)) ) @@ -432,14 +432,14 @@ let reduce context = in (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.Constant (_,Some body,_,_) -> + C.Constant (_,Some body,_,_,_) -> (reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body)) - | C.Constant (_,None,_,_) -> + | C.Constant (_,None,_,_,_) -> let t' = C.Const (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> + | C.CurrentProof (_,_,body,_,_,_) -> (reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body)) | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition @@ -494,7 +494,7 @@ let reduce context = let (arity, r) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (tl,_,r) -> + C.InductiveDefinition (tl,_,r,_) -> let (_,_,arity,_) = List.nth tl i in (arity,r) | _ -> raise WrongUriToInductiveDefinition @@ -620,10 +620,10 @@ let simpl context = C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_) -> + | C.Variable (_,None,_,_,_) -> let t' = C.Var (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_) -> + | C.Variable (_,Some body,_,_,_) -> reduceaux context l (CicSubstitution.subst_vars exp_named_subst' body) ) @@ -658,15 +658,15 @@ let simpl context = in (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.Constant (_,Some body,_,_) -> + C.Constant (_,Some body,_,_,_) -> try_delta_expansion l (C.Const (uri,exp_named_subst')) (CicSubstitution.subst_vars exp_named_subst' body) - | C.Constant (_,None,_,_) -> + | C.Constant (_,None,_,_,_) -> let t' = C.Const (uri,exp_named_subst') in if l = [] then t' else C.Appl (t'::l) | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body + | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition ) | C.MutInd (uri,i,exp_named_subst) -> @@ -717,7 +717,7 @@ let simpl context = let (arity, r) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (tl,ingredients,r) -> + C.InductiveDefinition (tl,ingredients,r,_) -> let (_,_,arity,_) = List.nth tl i in (arity,r) | _ -> raise WrongUriToInductiveDefinition