X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=4fc192a5b261f48be145c3e21cc7268c14a47055;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bfbfdb2a37c0a1113336f9b2d8dec4339f799859;hpb=df0606d3bcbc41272fcde2d013bbe0b1aadf98af;p=helm.git diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index bfbfdb2a3..4fc192a5b 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -25,85 +25,61 @@ open ProofEngineTypes -(* -let reduction_tac ~reduction (proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let new_ty = reduction context ty in - let new_metasenv = - List.map - (function - (n,_,_) when n = metano -> (metano,context,new_ty) - | _ as t -> t - ) metasenv - in - (curi,new_metasenv,pbo,pty), [metano] -;; -*) - -(* The default of term is the thesis of the goal to be prooved *) -let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = +(* 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 = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: Il vero problema e' che non sapendo dove sia il term non *) - (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) - (*CSC: e' meglio prima cercare il termine e scoprirne il *) - (*CSC: contesto, poi ridurre e infine rimpiazzare. *) - let replace context where terms = - (*CSC: Per il momento se la riduzione fallisce significa solamente che *) - (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) - (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) - try - let terms, terms' = - List.split - (List.map - (fun i, t -> t, reduction (i @ context) t) - terms) + 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 + else + let pairs, metasenv, ugraph = + List.fold_left + (fun (pairs, metasenv, ugraph) (context, t) -> + let reduction, metasenv, ugraph = reduction context metasenv ugraph in + ((t, reduction context t) :: pairs), metasenv, ugraph) + ([], metasenv, ugraph) + terms in - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where - (* FIXME this is a catch ALL... bad thing *) - with exc -> (*prerr_endline (Printexc.to_string exc);*) where - in - let find_pattern_for name = - try Some (snd(List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns)) - with Not_found -> None + let terms, terms' = List.split pairs in + let where' = + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where + in + CicMetaSubst.apply_subst subst where', metasenv, ugraph in - let ty' = - match goal_pattern with - | None -> replace context ty [[],ty] - | Some pat -> - let terms = ProofEngineHelpers.select ~term:ty ~pattern:pat in - replace context ty terms - in - let context' = - if hyp_patterns <> [] then - List.fold_right - (fun entry context -> - match entry with - | Some (name,Cic.Decl term) -> - (match find_pattern_for name with - | None -> entry::context - | Some pat -> - let terms = ProofEngineHelpers.select ~term ~pattern:pat in - let where = replace context term terms in - let entry = Some (name,Cic.Decl where) in - entry::context) - | Some (name,Cic.Def (term, None)) -> - (match find_pattern_for name with - | None -> entry::context - | Some pat -> - let terms = ProofEngineHelpers.select ~term ~pattern:pat in - let where = replace context term terms in - let entry = Some (name,Cic.Def (where,None)) in - entry::context) - | _ -> entry::context - ) context [] - else - context + let (subst,metasenv,ugraph,selected_context,selected_ty) = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ~conjecture ~pattern in + let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in + let context', metasenv, ugraph = + List.fold_right2 + (fun entry selected_entry (context', metasenv, ugraph) -> + match entry,selected_entry with + None,None -> None::context', metasenv, ugraph + | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> + let ty', metasenv, ugraph = + change subst ty selected_ty metasenv ugraph + in + 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 + 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 + in + (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph + | _,_ -> assert false + ) context selected_context ([], metasenv, ugraph) in let metasenv' = List.map (function | (n,_,_) when n = metano -> (metano,context',ty') @@ -113,51 +89,130 @@ let reduction_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) (proof,goal) = (curi,metasenv',pbo,pty), [metano] ;; -let simpl_tac ~pattern = - mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);; +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 reduce_tac ~pattern = - mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; +let unfold_tac what ~pattern = + let reduction = + match what with + | None -> const_lazy_reduction (ProofEngineReduction.unfold ?what:None) + | Some lazy_term -> + (fun context metasenv ugraph -> + let what, metasenv, ugraph = lazy_term context metasenv ugraph in + ProofEngineReduction.unfold ~what, metasenv, ugraph) + in + mk_tactic (reduction_tac ~reduction ~pattern) -let whd_tac ~pattern = - mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);; +let whd_tac ~pattern = + mk_tactic (reduction_tac + ~reduction:(const_lazy_reduction CicReduction.whd) ~pattern) -let normalize_tac ~pattern = - mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; +let normalize_tac ~pattern = + mk_tactic (reduction_tac + ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern) -let fold_tac ~reduction ~pattern ~term = -(* - let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal) - = +exception NotConvertible + +(* Note: this code is almost identical to reduction_tac and +* it could be unified by making the change function a callback *) +(* CSC: with_what is parsed in the context of the goal, but it should replace + something that lives in a completely different context. Thus we + perform a delift + lift phase to move it in the right context. However, + in this way the tactic is less powerful than expected: with_what cannot + 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 ~pattern ~with_what (proof, goal) = let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let term' = reduction context term in - let replace = - ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term] + 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 + else + let pairs, metasenv, ugraph = + List.fold_left + (fun (pairs, metasenv, ugraph) (context_of_t, t) -> + let with_what, metasenv, ugraph = + with_what context_of_t metasenv ugraph + in + let _,u = + CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph + in + let b,_ = + CicReduction.are_convertible ~metasenv context_of_t t with_what u + in + if b then + ((t, with_what) :: pairs), metasenv, ugraph + else + raise NotConvertible) + ([], metasenv, ugraph) + terms in - let ty' = replace ty in - let metasenv' = - let context' = - if also_in_hypotheses then - List.map - (function - Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t)) - | Some (n,Cic.Def (t,None)) -> Some (n,Cic.Def ((replace t),None)) - | None -> None - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context - else - context - in - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - + let terms, terms' = List.split pairs in + let where' = + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where:where in - (curi,metasenv',pbo,pty), [metano] + CicMetaSubst.apply_subst subst where', metasenv, ugraph + in + let (subst,metasenv,ugraph,selected_context,selected_ty) = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture + ~pattern in + let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in + let context', metasenv, ugraph = + List.fold_right2 + (fun entry selected_entry (context', metasenv, ugraph) -> + match entry,selected_entry with + None,None -> (None::context'), metasenv, ugraph + | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> + let ty', metasenv, ugraph = + change subst ty selected_ty metasenv ugraph + in + (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 + 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 + in + (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph + | _,_ -> assert false + ) context selected_context ([], metasenv, ugraph) in + let metasenv' = + List.map + (function + | (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t) + metasenv + in + (curi,metasenv',pbo,pty), [metano] + in + mk_tactic (change_tac ~pattern ~with_what) + +let fold_tac ~reduction ~term ~pattern = + let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status = + assert (wanted = None); (* this should be checked syntactically *) + let reduced_term = + (fun context metasenv ugraph -> + let term, metasenv, ugraph = term context metasenv ugraph in + let reduction, metasenv, ugraph = reduction context metasenv ugraph in + reduction context term, metasenv, ugraph) + in + apply_tactic + (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status in - mk_tactic (fold_tac ~reduction ~pattern ~term) -*) assert false -;; + mk_tactic (fold_tac ~reduction ~term ~pattern) +