X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=ae99ecb33d486be1f0069a9fce4b46f076b3a5f5;hb=a3acd934eba07f24937e59c3c7a41db82d901025;hp=decb161f60ebb3533e8b2e978f706d0d77b8940b;hpb=e5efa2e0b70723b431cdc4cffe10b41167145ca4;p=helm.git diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index decb161f6..ae99ecb33 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -25,100 +25,71 @@ 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) +(* Note: this code is almost identical to PrimitiveTactics.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) as conjecture = CicUtil.lookup_meta goal metasenv in + let change where terms = + if terms = [] then where + else + 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 (selected_context,selected_ty) = + ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in + let ty' = change ty selected_ty in + let context' = + List.fold_right2 + (fun entry selected_entry context' -> + match entry,selected_entry with + None,None -> None::context' + | Some (name,Cic.Decl ty),Some (`Decl selected_ty) -> + let ty' = change ty selected_ty in + Some (name,Cic.Decl ty')::context' + | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) -> + let bo' = change bo selected_bo in + let ty' = + match ty,selected_ty with + None,None -> None + | Some ty,Some selected_ty -> Some (change ty selected_ty) + | _,_ -> assert false + in + Some (name,Cic.Def (bo',ty'))::context' + | _,_ -> assert false + ) context selected_context [] in + let metasenv' = + List.map (function + | (n,_,_) when n = metano -> (metano,context',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 ~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 - (* 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 lift 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.fold_left - (fun acc t -> - try - (CicSubstitution.delift lift t) :: acc - with Failure _ -> acc - ) [] terms - in - let terms' = List.map (reduction context) terms in - ProofEngineReduction.replace - ~equality:(=) ~what:terms ~with_what:terms' ~where:where - with - _ -> where - in - let ty' = replace 0 context ty in - let context', _ = - if also_in_hypotheses then - List.fold_right - (fun entry (context,i) -> - match entry with - | Some (name,Cic.Def (t,None)) -> - (Some (name,Cic.Def ((replace i context t),None)))::context, i-1 - | Some (name,Cic.Decl t) -> - (Some (name,Cic.Decl (replace i context t)))::context, i-1 - | None -> None::context, i-1 - | Some (_,Cic.Def (_,Some _)) -> assert false - ) context ([],(List.length context)) - else - context, 0 - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [metano] + (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 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 @@ -145,5 +116,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 ;;