]> matita.cs.unibo.it Git - helm.git/commitdiff
simplify has a brand new semantics!
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 Apr 2007 21:15:44 +0000 (21:15 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 Apr 2007 21:15:44 +0000 (21:15 +0000)
replace_lifting passes a context to the comparison function
(but in the case Fix/CoFix is incomplete)

helm/software/components/tactics/inversion.ml
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/proofEngineReduction.ml
helm/software/components/tactics/proofEngineReduction.mli

index 5f8a9a37f91ab400b8574cea9f0afe7e1960f2ea..5f90c45ebbee4854c64ebe0e44c5883d7d1773ea 100644 (file)
@@ -123,7 +123,8 @@ let rec foo_prod nright right_param_tys rightparameters l2 base_rel goalty
      (CicSubstitution.lift 1 termty)
      isSetType (CicSubstitution.lift 1 term))
    | [] -> ProofEngineReduction.replace_lifting 
-    ~equality:(CicUtil.alpha_equivalence)
+    ~equality:(fun _ -> CicUtil.alpha_equivalence)
+    ~context:[]
     ~what: (if isSetType
      then (rightparameters_ @ [term] ) 
      else (rightparameters_ ) )
@@ -151,7 +152,8 @@ let rec foo_lambda nright right_param_tys nright_ right_param_tys_
    | [] when isSetType -> Cic.Lambda (
     (Cic.Name ("lambda" ^ (string_of_int nright))),
     (ProofEngineReduction.replace_lifting
-     ~equality:(CicUtil.alpha_equivalence)
+     ~equality:(fun _ -> CicUtil.alpha_equivalence)
+     ~context:[]
      ~what: (rightparameters_ ) 
      ~with_what: (List.map (CicSubstitution.lift (-1)) created_vars)
      ~where:termty), (* type of H with replaced right parameters *)
index fcb4586cb4d8b2e0ecb2e1831797f11a2ef49605..d9e16a255e362ed58d5592e1c9fe33e491e7f22a 100644 (file)
@@ -371,12 +371,12 @@ prerr_endline ("!!! RISPARMIO " ^ string_of_int (List.length acc) ^ " PASSI");
   
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
-    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+  ~equality:(fun _ ->(=)) ~context:[] ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
 ;;
 
 let put_in_ctx ctx t = 
   ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+  ~equality:(fun _ -> (=)) ~context:[] ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
 ;;
 
 let mk_eq uri ty l r =
@@ -581,8 +581,9 @@ let parametrize_proof p l r =
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(fun t1 t2 -> 
+    ~equality:(fun t1 t2 -> 
       match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
+    ~context:[]
     ~what ~with_what ~where:p
   in
   let ty_of_m _ = Cic.Implicit (Some `Type) in
index 50626aff0ed3f7d41b012a4483b106436d4569fe..cc16c203012101be0aff7f3657da38dded372b8d 100644 (file)
@@ -715,8 +715,9 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam
       in
       let replaced = ref false in
       let replace = ProofEngineReduction.replace_lifting
-       ~equality:(fun a b -> let rc = CicUtil.alpha_equivalence a b in 
+       ~equality:(fun a b -> let rc = CicUtil.alpha_equivalence a b in 
                   if rc then replaced := true; rc)
+       ~context:[]
       in
       let captured = 
         replace ~what:[CicSubstitution.lift n_lambdas term] 
index b55b92b9339da1e211acf65c7340511d480356d8..ec69074369663cabc55ba782f17cde1a9ef78d76 100644 (file)
@@ -49,6 +49,11 @@ exception RelToHiddenHypothesis;;
 module C = Cic
 module S = CicSubstitution
 
+let debug = false
+let prerr_endline =
+  if debug then prerr_endline else (fun x -> ())
+;;
+
 exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 (* Replaces "textually" in "where" every term in "what" with the corresponding
@@ -122,26 +127,28 @@ let replace ~equality ~what ~with_what ~where =
    Thus "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" is the
    inverse of subst up to the fact that free variables in "where" are NOT
    lifted.  *)
-let replace_lifting ~equality ~what ~with_what ~where =
-  let find_image what t =
+let replace_lifting ~equality ~context ~what ~with_what ~where =
+  let find_image ctx what t =
    let rec find_image_aux =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality what t then with_what else find_image_aux (tl1,tl2)
+        if equality ctx what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
   in
-  let rec substaux k what t =
+  let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
+  let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+  let rec substaux k ctx what t =
    try
-    S.lift (k-1) (find_image what t)
+    S.lift (k-1) (find_image ctx what t)
    with Not_found ->
     match t with
       C.Rel n as t -> t
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
     | C.Meta (i, l) -> 
@@ -149,56 +156,56 @@ let replace_lifting ~equality ~what ~with_what ~where =
         List.map
          (function
              None -> None
-           | Some t -> Some (substaux k what t)
+           | Some t -> Some (substaux k ctx what t)
          ) l
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
     | C.Implicit _ as t -> t
-    | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
+    | C.Cast (te,ty) -> C.Cast (substaux k ctx what te, substaux k ctx what ty)
     | C.Prod (n,s,t) ->
        C.Prod
-        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
+        (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
     | C.Lambda (n,s,t) ->
        C.Lambda
-        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
+        (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
     | C.LetIn (n,s,t) ->
        C.LetIn
-        (n, substaux k what s, substaux (k + 1) (List.map (S.lift 1) what) t)
+        (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
-       let tl' = List.map (substaux k what) tl in
+       let tl' = List.map (substaux k ctx what) tl in
         begin
-         match substaux k what he with
+         match substaux k ctx what he with
             C.Appl l -> C.Appl (l@tl')
           | _ as he' -> C.Appl (he'::tl')
         end
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
        in
        C.Const (uri,exp_named_subst')
     | C.MutInd (uri,i,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
        in
         C.MutInd (uri,i,exp_named_subst')
     | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
+        List.map (function (uri,t) -> uri,substaux k ctx what t) exp_named_subst
        in
         C.MutConstruct (uri,i,j,exp_named_subst')
     | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,substaux k what outt, substaux k what t,
-        List.map (substaux k what) pl)
+       C.MutCase (sp,i,substaux k ctx what outt, substaux k ctx what t,
+        List.map (substaux k ctx what) pl)
     | C.Fix (i,fl) ->
        let len = List.length fl in
        let substitutedfl =
         List.map
-         (fun (name,i,ty,bo) ->
-           (name, i, substaux k what ty,
-             substaux (k+len) (List.map (S.lift len) what) bo)
+         (fun (name,i,ty,bo) -> (* WRONG CTX *)
+           (name, i, substaux k ctx what ty,
+             substaux (k+len) ctx (List.map (S.lift len) what) bo)
          ) fl
        in
         C.Fix (i, substitutedfl)
@@ -206,14 +213,14 @@ let replace_lifting ~equality ~what ~with_what ~where =
        let len = List.length fl in
        let substitutedfl =
         List.map
-         (fun (name,ty,bo) ->
-           (name, substaux k what ty,
-             substaux (k+len) (List.map (S.lift len) what) bo)
+         (fun (name,ty,bo) -> (* WRONG CTX *)
+           (name, substaux k ctx what ty,
+             substaux (k+len) ctx (List.map (S.lift len) what) bo)
          ) fl
        in
         C.CoFix (i, substitutedfl)
  in
-  substaux 1 what where
+  substaux 1 context what where
 ;;
 
 (* Replaces in "where" every term in "what" with the corresponding
@@ -228,7 +235,7 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
     function
        [],[] -> raise Not_found
      | what::tl1,with_what::tl2 ->
-        if equality what t then with_what else find_image_aux (tl1,tl2)
+         if equality what t then with_what else find_image_aux (tl1,tl2)
      | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength
    in
     find_image_aux (what,with_what)
@@ -521,7 +528,7 @@ let reduce context =
           (fun (types,len) (n,_,ty,_) ->
              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
               len+1)
-         ) ([],0) fl
+         ) ([],0) fl 
        in
         let t' () =
          let fl' =
@@ -563,7 +570,7 @@ let reduce context =
           (fun (types,len) (n,ty,_) ->
              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
               len+1)
-         ) ([],0) fl
+         ) ([],0) fl
        in
         let t' =
          let fl' =
@@ -581,6 +588,94 @@ let reduce context =
   reduceaux context []
 ;;
 
+
+let unfold ?what context where =
+ let contextlen = List.length context in
+ let first_is_the_expandable_head_of_second context' t1 t2 =
+  match t1,t2 with
+     Cic.Const (uri,_), Cic.Const (uri',_)
+   | Cic.Var (uri,_), Cic.Var (uri',_)
+   | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
+   | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
+   | Cic.Const _, _
+   | Cic.Var _, _ -> false
+   | Cic.Rel n, Cic.Rel m
+   | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
+      n + (List.length context' - contextlen) = m
+   | Cic.Rel _, _ -> false
+   | _,_ ->
+     raise
+      (ProofEngineTypes.Fail
+        (lazy "The term to unfold is not a constant, a variable or a bound variable "))
+ in
+ let appl he tl =
+  if tl = [] then he else Cic.Appl (he::tl) in
+ let cannot_delta_expand t =
+  raise
+   (ProofEngineTypes.Fail
+     (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
+ let rec hd_delta_beta context tl =
+  function
+    Cic.Rel n as t ->
+     (try
+       match List.nth context (n-1) with
+          Some (_,Cic.Decl _) -> cannot_delta_expand t
+        | Some (_,Cic.Def (bo,_)) ->
+           CicReduction.head_beta_reduce
+            (appl (CicSubstitution.lift n bo) tl)
+        | None -> raise RelToHiddenHypothesis
+      with
+         Failure _ -> assert false)
+  | Cic.Const (uri,exp_named_subst) as t ->
+     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+      (match o with
+          Cic.Constant (_,Some body,_,_,_) ->
+           CicReduction.head_beta_reduce
+            (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
+        | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
+        | Cic.Variable _ -> raise ReferenceToVariable
+        | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
+        | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+      )
+  | Cic.Var (uri,exp_named_subst) as t ->
+     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+      (match o with
+          Cic.Constant _ -> raise ReferenceToConstant
+        | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
+        | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        | Cic.Variable (_,Some body,_,_,_) ->
+           CicReduction.head_beta_reduce
+            (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
+        | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
+      )
+   | Cic.Appl [] -> assert false
+   | Cic.Appl (he::tl) -> hd_delta_beta context tl he
+   | t -> cannot_delta_expand t
+ in
+ let context_and_matched_term_list =
+  match what with
+     None -> [context, where]
+   | Some what ->
+      let res =
+       ProofEngineHelpers.locate_in_term
+        ~equality:first_is_the_expandable_head_of_second
+        what ~where context
+      in
+       if res = [] then
+        raise
+         (ProofEngineTypes.Fail
+           (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
+       else
+        res
+ in
+  let reduced_terms =
+   List.map
+    (function (context,where) -> hd_delta_beta context [] where)
+    context_and_matched_term_list in
+  let whats = List.map snd context_and_matched_term_list in
+   replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
+;;
+
 exception WrongShape;;
 exception AlreadySimplified;;
 
@@ -761,7 +856,7 @@ let simpl context =
            (fun (types,len) (n,_,ty,_) ->
               (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
                len+1)
-          ) ([],0) fl
+          ) ([],0) fl 
        in
         let t' () =
          let fl' =
@@ -803,7 +898,7 @@ let simpl context =
           (fun (types,len) (n,ty,_) ->
              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
               len+1)
-         ) ([],0) fl
+         ) ([],0) fl
        in
         let t' =
          let fl' =
@@ -818,6 +913,15 @@ let simpl context =
  and reduceaux_exp_named_subst context l =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
+ and reduce_with_no_hope_to_fold_back t l =
+    prerr_endline "reduce_with_no_hope_to_fold_back";
+    let simplified = reduceaux context l t in
+    let t' = if l = [] then t else C.Appl (t::l) in
+    if t' = simplified then
+      raise AlreadySimplified
+    else
+      simplified
+
  and try_delta_expansion context l term body =
    try
     let res,constant_args =
@@ -871,28 +975,153 @@ let simpl context =
       let simplified_term_to_fold =
        reduceaux context [] delta_expanded_term_to_fold
       in
-       replace_lifting (=) [simplified_term_to_fold] [term_to_fold] res
+       replace_lifting ~equality:(fun _ x y -> x = y) ~context
+         ~what:[simplified_term_to_fold] ~with_what:[term_to_fold] ~where:res
    with
       WrongShape ->
+       let rec skip_lambda n = function
+         | Cic.Lambda (_,_,t) -> skip_lambda (n+1) t | t -> t, n
+       in
+       let is_fix uri = 
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
+         | Cic.Constant (_,Some bo, _, _,_) ->
+             (let t, _ = skip_lambda 0 bo in
+             match t with | Cic.Fix _ -> true | _ -> false) 
+         | _ -> false
+       in
+       let guess_recno uri = 
+         prerr_endline ("GUESS: " ^ UriManager.string_of_uri uri);
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
+         | Cic.Constant (_,Some bo, _, _,_ ) -> 
+             let t, n = skip_lambda 0 bo in
+             (match t with
+             | Cic.Fix (i,fl) ->
+                 let _,recno,_,_ = List.nth fl i in
+                 prerr_endline ("GUESSED: " ^ string_of_int recno ^ " after " ^
+                 string_of_int n ^ " lambdas");
+                 recno + n
+             | _ -> assert false)    
+         | _ -> assert false
+       in
+       let original_args = l in 
        (**** Step 3.2 ****)
        let rec aux l =
         function
-           C.Lambda (name,s,t) ->
+         | C.Lambda (name,s,t) ->
              (match l with
-                [] -> raise AlreadySimplified
+              | [] -> raise AlreadySimplified
               | he::tl ->
                  (* when name is Anonimous the substitution should *)
                  (* be superfluous                                 *)
                  aux tl (S.subst he t))
          | C.LetIn (_,s,t) -> aux l (S.subst s t)
-         | t ->
-            let simplified = reduceaux context l t in
-            let t' = if l = [] then t else C.Appl (t::l) in
-             if t' = simplified then
-              raise AlreadySimplified
+         | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
+             let recno =
+               prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
+                 ^ " in: " ^ String.concat " " 
+                 (List.map (fun x -> CicPp.ppterm x) args));
+               prerr_endline ("e piglio il rispettivo in :"^String.concat " " 
+                 (List.map (fun x -> CicPp.ppterm x) original_args));
+               (* look for args[regno] in saved_args *)
+               let wanted = List.nth args (guess_recno uri) in (* args@l ? *)
+               let rec aux n = function
+                 | [] -> n (* DA CAPIRE *)
+                 | t::_ when t = wanted -> n
+                 | _::tl -> aux (n+1) tl
+               in
+               aux 0 original_args
+             in
+             if recno = List.length original_args then
+               reduce_with_no_hope_to_fold_back t l
              else
-              simplified
-       in
+               let simplified = reduceaux context l t in
+               let rec mk_implicits = function
+                 | n,_::tl when n = recno -> 
+                     Cic.Implicit None :: (mk_implicits (n+1,tl))
+                 | n,arg::tl -> arg :: (mk_implicits (n+1,tl))
+                 | _,[] -> []
+               in
+               (* we try to fold back constant that do not expand to Fix *)
+               let _ = prerr_endline 
+                 ("INIZIO (" ^ string_of_int recno ^ ") : " ^ CicPp.ppterm
+                 simplified) in
+               let term_to_fold = 
+                 Cic.Appl (term:: mk_implicits (0,original_args)) 
+               in
+               (try
+                 let term_to_fold, _, metasenv, _ = 
+                   CicRefine.type_of_aux' [] context term_to_fold
+                     CicUniv.oblivion_ugraph
+                 in
+                 let _ = 
+                   prerr_endline ("RAFFINA: "^CicPp.ppterm term_to_fold) in
+                 let _ = 
+                   prerr_endline 
+                     ("RAFFINA: "^CicMetaSubst.ppmetasenv [] metasenv) in
+                 let simplified_term_to_fold = unfold context term_to_fold in
+                 let _ = 
+                   prerr_endline ("SEMPLIFICA: " ^ 
+                     CicPp.ppterm simplified_term_to_fold) 
+                 in
+                 let rec do_n f t = 
+                   let t1 = f t in
+                   if t1 = t then t else do_n f t1
+                 in
+                 do_n 
+                 (fun simplified -> 
+                   let subst = ref [] in
+                   let myunif ctx t1 t2 =
+                     if !subst <> [] then false 
+                     else
+                     try 
+                       prerr_endline "MUNIF";
+                       prerr_endline (CicPp.ppterm t1);
+                       prerr_endline "VS";
+                       prerr_endline (CicPp.ppterm t2 ^ "\n");
+                       let subst1, _, _ = 
+                         CicUnification.fo_unif metasenv ctx t1 t2
+                           CicUniv.empty_ugraph
+                       in
+                       prerr_endline "UNIFICANO\n\n\n";
+                       subst := subst1;
+                       true
+                     with 
+                     | CicUnification.UnificationFailure s
+                     | CicUnification.Uncertain s
+                     | CicUnification.AssertFailure s ->
+                         prerr_endline (Lazy.force s); false
+                     | CicUtil.Meta_not_found _ -> false
+                     (*
+                     | _ as exn -> 
+                         prerr_endline (Printexc.to_string exn);
+                         false*)
+                   in
+                   let t = 
+                     replace_lifting myunif context
+                       [simplified_term_to_fold] [term_to_fold] simplified
+                   in
+                   let _ = prerr_endline "UNIFICA" in
+                   if List.length metasenv <> List.length !subst then 
+                     let _ = prerr_endline ("SUBST CORTA " ^
+                       CicMetaSubst.ppsubst !subst ~metasenv) 
+                     in
+                       simplified 
+                   else
+                     if t = simplified then 
+                       let _ = prerr_endline "NULLA DI FATTO" in
+                       simplified 
+                     else
+                       let t = CicMetaSubst.apply_subst !subst t in
+                       prerr_endline ("ECCO: " ^ CicPp.ppterm t); t)
+                   simplified 
+               with 
+               | CicRefine.RefineFailure s 
+               | CicRefine.Uncertain s
+               | CicRefine.AssertFailure s ->
+                   prerr_endline (Lazy.force s); simplified 
+               (*| exn -> prerr_endline (Printexc.to_string exn); simplified*))
+         | t -> reduce_with_no_hope_to_fold_back t l
+      in
         (try aux l body
          with
           AlreadySimplified ->
@@ -905,90 +1134,3 @@ let simpl context =
  in
   reduceaux context []
 ;;
-
-let unfold ?what context where =
- let contextlen = List.length context in
- let first_is_the_expandable_head_of_second context' t1 t2 =
-  match t1,t2 with
-     Cic.Const (uri,_), Cic.Const (uri',_)
-   | Cic.Var (uri,_), Cic.Var (uri',_)
-   | Cic.Const (uri,_), Cic.Appl (Cic.Const (uri',_)::_)
-   | Cic.Var (uri,_), Cic.Appl (Cic.Var (uri',_)::_) -> UriManager.eq uri uri'
-   | Cic.Const _, _
-   | Cic.Var _, _ -> false
-   | Cic.Rel n, Cic.Rel m
-   | Cic.Rel n, Cic.Appl (Cic.Rel m::_) ->
-      n + (List.length context' - contextlen) = m
-   | Cic.Rel _, _ -> false
-   | _,_ ->
-     raise
-      (ProofEngineTypes.Fail
-        (lazy "The term to unfold is not a constant, a variable or a bound variable "))
- in
- let appl he tl =
-  if tl = [] then he else Cic.Appl (he::tl) in
- let cannot_delta_expand t =
-  raise
-   (ProofEngineTypes.Fail
-     (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in
- let rec hd_delta_beta context tl =
-  function
-    Cic.Rel n as t ->
-     (try
-       match List.nth context (n-1) with
-          Some (_,Cic.Decl _) -> cannot_delta_expand t
-        | Some (_,Cic.Def (bo,_)) ->
-           CicReduction.head_beta_reduce
-            (appl (CicSubstitution.lift n bo) tl)
-        | None -> raise RelToHiddenHypothesis
-      with
-         Failure _ -> assert false)
-  | Cic.Const (uri,exp_named_subst) as t ->
-     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-      (match o with
-          Cic.Constant (_,Some body,_,_,_) ->
-           CicReduction.head_beta_reduce
-            (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
-        | Cic.Constant (_,None,_,_,_) -> cannot_delta_expand t
-        | Cic.Variable _ -> raise ReferenceToVariable
-        | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
-        | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-      )
-  | Cic.Var (uri,exp_named_subst) as t ->
-     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-      (match o with
-          Cic.Constant _ -> raise ReferenceToConstant
-        | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
-        | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-        | Cic.Variable (_,Some body,_,_,_) ->
-           CicReduction.head_beta_reduce
-            (appl (CicSubstitution.subst_vars exp_named_subst body) tl)
-        | Cic.Variable (_,None,_,_,_) -> cannot_delta_expand t
-      )
-   | Cic.Appl [] -> assert false
-   | Cic.Appl (he::tl) -> hd_delta_beta context tl he
-   | t -> cannot_delta_expand t
- in
- let context_and_matched_term_list =
-  match what with
-     None -> [context, where]
-   | Some what ->
-      let res =
-       ProofEngineHelpers.locate_in_term
-        ~equality:first_is_the_expandable_head_of_second
-        what ~where context
-      in
-       if res = [] then
-        raise
-         (ProofEngineTypes.Fail
-           (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)))
-       else
-        res
- in
-  let reduced_terms =
-   List.map
-    (function (context,where) -> hd_delta_beta context [] where)
-    context_and_matched_term_list in
-  let whats = List.map snd context_and_matched_term_list in
-   replace ~equality:(==) ~what:whats ~with_what:reduced_terms ~where
-;;
index 2d04d39596ea4149042189b2187ffb1245928ebd..f8cdec89b74956f8e01bcef6bdbddb7529047ae2 100644 (file)
@@ -50,7 +50,8 @@ val replace :
    inverse of subst up to the fact that free variables in "where" are NOT
    lifted. *)
 val replace_lifting :
-  equality:(Cic.term -> Cic.term -> bool) ->
+  equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
+  context:Cic.context ->
   what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 
 (* Replaces in "where" every term in "what" with the corresponding