X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FreductionTactics.ml;h=c943e7a19cafdf592426615182dfdd5cdd4bdf07;hb=eaf5880ed69963b3ad37cb1f8a1fd48b2918e58b;hp=754b2c0c5b49cca403f94a8e3bde1ee86f2c9798;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index 754b2c0c5..c943e7a19 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -30,7 +30,7 @@ open ProofEngineTypes (* Note: this code is almost identical to change_tac and * it could be unified by making the change function a callback *) let reduction_tac ~reduction ~pattern (proof,goal) = - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change subst where terms metasenv ugraph = if terms = [] then where, metasenv, ugraph @@ -51,7 +51,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) = CicMetaSubst.apply_subst subst where', metasenv, ugraph in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in @@ -67,17 +67,9 @@ let reduction_tac ~reduction ~pattern (proof,goal) = Some (name,Cic.Decl ty')::context', metasenv, ugraph | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> let bo', metasenv, ugraph = - change subst bo selected_bo metasenv ugraph - in + change subst bo selected_bo metasenv ugraph in let ty', metasenv, ugraph = - match ty,selected_ty with - None,None -> None, metasenv, ugraph - | Some ty,Some selected_ty -> - let ty', metasenv, ugraph = - change subst ty selected_ty metasenv ugraph - in - Some ty', metasenv, ugraph - | _,_ -> assert false + change subst ty selected_ty metasenv ugraph in (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph | _,_ -> assert false @@ -88,17 +80,13 @@ let reduction_tac ~reduction ~pattern (proof,goal) = | _ as t -> t ) metasenv in - (curi,metasenv',pbo,pty, attrs), [metano] + (curi,metasenv',_subst,pbo,pty, attrs), [metano] ;; let simpl_tac ~pattern = mk_tactic (reduction_tac ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern) -let reduce_tac ~pattern = - mk_tactic (reduction_tac - ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern) - let unfold_tac what ~pattern = let reduction = match what with @@ -106,7 +94,17 @@ let unfold_tac what ~pattern = | Some lazy_term -> (fun context metasenv ugraph -> let what, metasenv, ugraph = lazy_term context metasenv ugraph in - ProofEngineReduction.unfold ~what, metasenv, ugraph) + let unfold ctx t = + try + ProofEngineReduction.unfold ~what ctx t + with + (* Not what we would like to have; however, this is required + right now for the case of a definition in the context: + if it works only in the body (or only in the type), that should + be accepted *) + ProofEngineTypes.Fail _ -> t + in + unfold, metasenv, ugraph) in mk_tactic (reduction_tac ~reduction ~pattern) @@ -118,6 +116,12 @@ let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern) +let head_beta_reduce_tac ?delta ?upto ~pattern = + mk_tactic (reduction_tac + ~reduction: + (const_lazy_reduction + (fun _context -> CicReduction.head_beta_reduce ?delta ?upto)) ~pattern) + exception NotConvertible (* Note: this code is almost identical to reduction_tac and @@ -129,9 +133,9 @@ exception NotConvertible reference variables that are local to the term that is going to be replaced. To fix this we should parse with_what in the context of the term(s) to be replaced. *) -let change_tac ~pattern with_what = +let change_tac ?(with_cast=false) ~pattern with_what = let change_tac ~pattern ~with_what (proof, goal) = - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change subst where terms metasenv ugraph = if terms = [] then where, metasenv, ugraph @@ -163,7 +167,7 @@ let change_tac ~pattern with_what = CicMetaSubst.apply_subst subst where', metasenv, ugraph in let (subst,metasenv,ugraph,selected_context,selected_ty) = - ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern in let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in let context', metasenv, ugraph = @@ -178,17 +182,9 @@ let change_tac ~pattern with_what = (Some (name,Cic.Decl ty')::context'), metasenv, ugraph | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> let bo', metasenv, ugraph = - change subst bo selected_bo metasenv ugraph - in + change subst bo selected_bo metasenv ugraph in let ty', metasenv, ugraph = - match ty,selected_ty with - None,None -> None, metasenv, ugraph - | Some ty,Some selected_ty -> - let ty', metasenv, ugraph = - change subst ty selected_ty metasenv ugraph - in - Some ty', metasenv, ugraph - | _,_ -> assert false + change subst ty selected_ty metasenv ugraph in (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph | _,_ -> assert false @@ -200,7 +196,19 @@ let change_tac ~pattern with_what = | _ as t -> t) metasenv in - (curi,metasenv',pbo,pty, attrs), [metano] + let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in + if with_cast then + let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in + let (newproof,_) = + let irl= CicMkImplicit.identity_relocation_list_for_metavariable context' + in + ProofEngineHelpers.subst_meta_in_proof + proof metano + (Cic.Cast (Cic.Meta(metano',irl),ty')) [metano',context',ty'] + in + newproof, [metano'] + else + proof,[goal] in mk_tactic (change_tac ~pattern ~with_what)