X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=65dc199124e576de389490937a666acb61be0802;hb=80fc89019bcb7fb7e0e1fb8bb111b708be49d19f;hp=c641cbf653af905c3b4689b5f4407dc6bdb6ecaa;hpb=caaca5ed51e45a023ccb1244fd5cbbb32d233e2e;p=helm.git diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index c641cbf65..65dc19912 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -25,84 +25,95 @@ 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) = +let reduction_tac ~reduction ~pattern:(what,hyp_patterns,goal_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, - (let x, _, _ = CicMetaSubst.delift_rels [] metasenv i t in - let t' = reduction context x in - CicSubstitution.lift i t')) - 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 replace where terms = + let terms, terms' = + List.split (List.map (fun (context, t) -> t, reduction context t) terms) + in + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' + ~where: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 - in + with Not_found -> None in let ty' = - match goal_pattern with - | None -> replace context ty [0,ty] - | Some pat -> - let terms = CicUtil.select ~term:ty ~context:pat in - replace context ty terms - in + let terms = + ProofEngineHelpers.select ~context ~term:ty ~pattern:(what,goal_pattern) + in + replace ty terms in + let context_len = List.length context in let context' = if hyp_patterns <> [] then List.fold_right (fun entry context -> match entry with + None -> None::context | Some (name,Cic.Decl term) -> (match find_pattern_for name with | None -> entry::context | Some pat -> - let terms = CicUtil.select ~term ~context: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)) -> + try + let what = + match what with + None -> None + | Some what -> + let what,subst',metasenv' = + CicMetaSubst.delift_rels [] metasenv + (context_len - List.length context) what + in + assert (subst' = []); + assert (metasenv' = metasenv); + Some what in + let terms = + ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in + let term' = replace term terms in + Some (name,Cic.Decl term') :: context + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise + (ProofEngineTypes.Fail + ("The term the user wants to convert is not closed " ^ + "in the context of the position of the substitution."))) + | Some (name,Cic.Def (term, ty)) -> (match find_pattern_for name with | None -> entry::context | Some pat -> - let terms = CicUtil.select ~term ~context:pat in - let where = replace context term terms in - let entry = Some (name,Cic.Def (where,None)) in - entry::context) - | _ -> entry::context + try + let what = + match what with + None -> None + | Some what -> + let what,subst',metasenv' = + CicMetaSubst.delift_rels [] metasenv + (context_len - List.length context) what + in + assert (subst' = []); + assert (metasenv' = metasenv); + Some what in + let terms = + ProofEngineHelpers.select ~context ~term ~pattern:(what,pat) in + let term' = replace term terms in + let ty' = + match ty with + None -> None + | Some ty -> + let terms = + ProofEngineHelpers.select + ~context ~term:ty ~pattern:(what,pat) + in + Some (replace ty terms) + in + Some (name,Cic.Def (term',ty')) :: context + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + raise + (ProofEngineTypes.Fail + ("The term the user wants to convert is not closed " ^ + "in the context of the position of the substitution."))) ) context [] else context @@ -128,15 +139,13 @@ let whd_tac ~pattern = let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; -let fold_tac ~reduction ~also_in_hypotheses ~term = - let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = +let fold_tac ~reduction ~pattern = +(* + let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (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 - (* 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: ma si potrebbe ovviare al problema. Ma non credo *) - (*CSC: che si guadagni nulla in fatto di efficienza. *) let replace = ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term] in @@ -163,5 +172,6 @@ let fold_tac ~reduction ~also_in_hypotheses ~term = in (curi,metasenv',pbo,pty), [metano] in - mk_tactic (fold_tac ~reduction ~also_in_hypotheses ~term) + mk_tactic (fold_tac ~reduction ~pattern ~term) +*) assert false ;;