X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=bfbfdb2a37c0a1113336f9b2d8dec4339f799859;hb=6a9d597352e104434a1a7f371fdd1bbdac5e50a3;hp=d356499a1d50fccad761e5c7ed7d3adb8d2ae6f6;hpb=d9bd1adaa8588112818d3b6977a5c42a03755a21;p=helm.git diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index d356499a1..bfbfdb2a3 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -42,76 +42,96 @@ let reduction_tac ~reduction (proof,goal) = *) (* The default of term is the thesis of the goal to be prooved *) -let reduction_tac ~also_in_hypotheses ~reduction ~terms (proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let terms = - match terms with None -> [ty] | Some l -> l - in +let reduction_tac ~reduction ~pattern:(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= -(*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' = List.map (reduction context) terms in - ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' - ~where:where - with - _ -> where - in - let ty' = replace context ty in - let context' = - if also_in_hypotheses then - List.fold_right - (fun entry context -> - match entry with - Some (name,Cic.Def (t,None)) -> - (Some (name,Cic.Def ((replace context t),None)))::context - | Some (name,Cic.Decl t) -> - (Some (name,Cic.Decl (replace context t)))::context - | None -> None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context [] - else - context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv + 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) in - (curi,metasenv',pbo,pty), [metano] + 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 + 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 + in + let metasenv' = + List.map (function + | (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] ;; -let simpl_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.simpl - ~also_in_hypotheses ~terms);; +let simpl_tac ~pattern = + mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);; -let reduce_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:ProofEngineReduction.reduce - ~also_in_hypotheses ~terms);; +let reduce_tac ~pattern = + mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);; -let whd_tac ~also_in_hypotheses ~terms = - mk_tactic ( reduction_tac ~reduction:CicReduction.whd - ~also_in_hypotheses ~terms);; +let whd_tac ~pattern = + mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);; -let fold_tac ~reduction ~also_in_hypotheses ~term = - let fold_tac ~reduction ~also_in_hypotheses ~term (proof,goal) = +let normalize_tac ~pattern = + mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );; + +let fold_tac ~reduction ~pattern ~term = +(* + 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 @@ -138,5 +158,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 ;;