X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=65dc199124e576de389490937a666acb61be0802;hb=80fc89019bcb7fb7e0e1fb8bb111b708be49d19f;hp=bfbfdb2a37c0a1113336f9b2d8dec4339f799859;hpb=df0606d3bcbc41272fcde2d013bbe0b1aadf98af;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index bfbfdb2a3..65dc19912 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -25,81 +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, reduction (i @ context) 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 [[],ty]
-    | Some pat -> 
-        let terms = ProofEngineHelpers.select ~term:ty ~pattern: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 = 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)) ->
+              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 = 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
+              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
@@ -125,7 +139,7 @@ let whd_tac ~pattern =
 let normalize_tac ~pattern = 
  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern );;
 
-let fold_tac ~reduction ~pattern ~term =
+let fold_tac ~reduction ~pattern =
 (*
  let fold_tac ~reduction ~pattern:(hyp_patterns,goal_pattern) ~term (proof,goal)
  =