]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/proofEngine.ml
* Many improvements (expecially in exceptions handling)
[helm.git] / helm / gTopLevel / proofEngine.ml
index b676832c15d6e0d911e03122e4fefe1efe73f1bb..ac828a9598c794ca832edbfbc7a0c76e41b86d72 100644 (file)
@@ -1,15 +1,17 @@
 type binder_type =
-   Declaration
- | Definition
+   Declaration of Cic.name * Cic.term
+ | Definition of Cic.name * Cic.term
 ;;
 
-type metas_context = (int * Cic.term) list;;
+type metasenv = (int * Cic.term) list;;
 
-type context = (binder_type * Cic.name * Cic.term) list;;
+type named_context = binder_type list;;
 
-type sequent = context * Cic.term;;
+type sequent = named_context * Cic.term;;
 
-let proof = ref (None : (metas_context * Cic.term * Cic.term) option);;
+let proof =
+ ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
+;;
 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
 (* Note: the sequent is redundant: it can be computed from the type of the   *)
 (* metavariable and its context in the proof. We keep it just for efficiency *)
@@ -18,69 +20,64 @@ let goal = ref (None : (int * sequent) option);;
 
 exception NotImplemented
 
-(*CSC: Funzione che deve sparire!!! *)
-let cic_context_of_context =
+let cic_context_of_named_context =
  List.map
   (function
-      Declaration,_,t -> t
-    | Definition,_,_ -> raise NotImplemented
+      Declaration (_,t) -> Cic.Decl t
+    | Definition (_,t) -> Cic.Def t
   )
 ;;
 
+(* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing    *)
+(*   newmetasenv                                                          *)
+(* This (heavy) function must be called when a tactic can instantiate old *)
+(* metavariables (i.e. existential variables). It substitues the metasenv *)
+(* of the proof with the result of removing [meta] from the domain of     *)
+(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
+(* in the current proof. Finally it applies [apply_subst_replacing] to    *)
+(*  current proof.                                                        *)
+(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
+(*CSC: ci ripasso sopra apply_subst!!!                                     *)
+(*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
+(*CSC: newmetasenv!!!                                                      *)
+let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
+ newmetasenv
+=
+ let (uri,bo,ty) =
+  match !proof with
+     None -> assert false
+   | Some (uri,_,bo,ty) -> uri,bo,ty
+ in
+  let subst_in t =
+   ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
+  in
+   let bo' = apply_subst_replacing (subst_in bo) in
+   let metasenv' = List.remove_assoc meta newmetasenv in
+    proof := Some (uri,metasenv',bo',ty)
+;;
+
 let refine_meta meta term newmetasenv =
- let (metasenv,bo,ty) =
+ let (uri,metasenv,bo,ty) =
   match !proof with
      None -> assert false
-   | Some (metasenv,bo,ty) -> metasenv,bo,ty
+   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
  in
-  let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
-  let rec aux =
-   let module C = Cic in
-    function
-       C.Rel _ as t -> t
-     | C.Var _ as t  -> t
-     | C.Meta meta' when meta=meta' -> term
-     | C.Meta _ as t -> t
-     | C.Sort _ as t -> t
-     | C.Implicit as t -> t
-     | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
-     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
-     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
-     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-     | C.Appl l -> C.Appl (List.map aux l)
-     | C.Const _ as t -> t
-     | C.Abst _ as t -> t
-     | C.MutInd _ as t -> t
-     | C.MutConstruct _ as t -> t
-     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-        C.MutCase (sp,cookingsno,i,aux outt, aux t,
-         List.map aux pl)
-     | C.Fix (i,fl) ->
-        let substitutedfl =
-         List.map
-          (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
-           fl
-        in
-         C.Fix (i, substitutedfl)
-     | C.CoFix (i,fl) ->
-        let substitutedfl =
-         List.map
-          (fun (name,ty,bo) -> (name, aux ty, aux bo))
-           fl
-        in
-         C.CoFix (i, substitutedfl)
+  let subst_in t =
+   ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
   in
-   let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in
-   let bo' = aux bo in
-    proof := Some (metasenv'',bo',ty)
+   let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
+    let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in
+    let bo' = subst_in bo in
+     proof := Some (uri,metasenv'',bo',ty)
 ;;
 
-(* Returns the first meta whose number is above the number of the higher meta. *)
+(* Returns the first meta whose number is above the *)
+(* number of the higher meta.                       *)
 let new_meta () =
  let metasenv =
   match !proof with
      None -> assert false
-   | Some (metasenv,_,_) -> metasenv
+   | Some (_,metasenv,_,_) -> metasenv
  in
   let rec aux =
    function
@@ -141,47 +138,11 @@ let perforate context term ty =
   let newmeta = new_meta () in
    match !proof with
       None -> assert false
-    | Some (metasenv,bo,gty) ->
+    | Some (uri,metasenv,bo,gty) ->
        (* We push the new meta at the end of the list for pretty-printing *)
        (* purposes: in this way metas are ordered.                        *)
        let metasenv' = metasenv@[newmeta,ty] in
-       let rec aux =
-        function
-           (* Is == strong enough? *)
-           t when t == term -> C.Meta newmeta
-         | C.Rel _ as t -> t
-         | C.Var _ as t  -> t
-         | C.Meta _ as t -> t
-         | C.Sort _ as t -> t
-         | C.Implicit as t -> t
-         | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
-         | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
-         | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
-         | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-         | C.Appl l -> C.Appl (List.map aux l)
-         | C.Const _ as t -> t
-         | C.Abst _ as t -> t
-         | C.MutInd _ as t -> t
-         | C.MutConstruct _ as t -> t
-         | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-            C.MutCase (sp,cookingsno,i,aux outt, aux t,
-             List.map aux pl)
-         | C.Fix (i,fl) ->
-            let substitutedfl =
-             List.map
-              (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
-               fl
-            in
-             C.Fix (i, substitutedfl)
-         | C.CoFix (i,fl) ->
-            let substitutedfl =
-             List.map
-              (fun (name,ty,bo) -> (name, aux ty, aux bo))
-               fl
-            in
-             C.CoFix (i, substitutedfl)
-       in
-        let bo' = aux bo in
+        let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
         (* It may be possible that some metavariables occurred only in *)
         (* the term we are perforating and they now occurs no more. We *)
         (* get rid of them, collecting the really useful metavariables *)
@@ -190,7 +151,7 @@ let perforate context term ty =
           let metasenv'' =
            List.filter (function (n,_) -> List.mem n newmetas) metasenv'
           in
-           proof := Some (metasenv'',bo',gty) ;
+           proof := Some (uri,metasenv'',bo',gty) ;
            goal := Some (newmeta,(context,ty)) ;
            newmeta
 ;;
@@ -207,7 +168,7 @@ let intros () =
   let metasenv =
    match !proof with
       None -> assert false
-    | Some (metasenv,_,_) -> metasenv
+    | Some (_,metasenv,_,_) -> metasenv
   in
   let (metano,context,ty) =
    match !goal with
@@ -220,10 +181,16 @@ let intros () =
         C.Cast (te,_)   -> collect_context te
       | C.Prod (n,s,t)  ->
          let (ctx,ty,bo) = collect_context t in
-          ((Declaration,n,s)::ctx,ty,C.Lambda(n,s,bo))
+          let n' =
+           match n with
+              C.Name _ -> n
+(*CSC: generatore di nomi? Chiedere il nome? *)
+            | C.Anonimous -> C.Name "fresh_name"
+          in
+           ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
       | C.LetIn (n,s,t) ->
          let (ctx,ty,bo) = collect_context t in
-          ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo))
+          ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
       | _ as t -> [], t, (C.Meta newmeta)
     in
      let revcontext',ty',bo' = collect_context ty in
@@ -239,7 +206,7 @@ let exact bo =
   let metasenv =
    match !proof with
       None -> assert false
-    | Some (metasenv,_,_) -> metasenv
+    | Some (_,metasenv,_,_) -> metasenv
   in
   let (metano,context,ty) =
    match !goal with
@@ -249,8 +216,7 @@ let exact bo =
        (* Invariant: context is the actual context of the meta in the proof *)
        metano,context,ty
   in
-   (*CSC: deve sparire! *)
-   let context = cic_context_of_context context in
+   let context = cic_context_of_named_context context in
     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
      begin
       refine_meta metano bo [] ;
@@ -260,6 +226,44 @@ let exact bo =
      raise (Fail "The type of the provided term is not the one expected.")
 ;;
 
+(* Auxiliary function for apply: given a type (a backbone), it returns its   *)
+(* head, a META environment in which there is a META for each hypothesis and *)
+(* the indexes of the first and last new METAs introduced.                   *)
+let new_metasenv_for_apply ty =
+ let module C = Cic in
+ let module S = CicSubstitution in
+  let rec aux newmeta =
+   function
+      C.Cast (he,_) -> aux newmeta he
+    | C.Prod (_,s,t) ->
+       let (res,newmetasenv,lastmeta) =
+        aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
+       in
+        res,(newmeta,s)::newmetasenv,lastmeta
+    | t -> t,[],newmeta
+  in
+   let newmeta = new_meta () in
+    (* WARNING: here we are using the invariant that above the most *)
+    (* recente new_meta() there are no used metas.                  *)
+    let (res,newmetasenv,lastmeta) = aux newmeta ty in
+     res,newmetasenv,newmeta,lastmeta
+;;
+
+(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
+let classify_metas newmeta in_subst_domain apply_subst metasenv =
+ List.fold_right
+  (fun (i,ty) (old_uninst,new_uninst) ->
+    if in_subst_domain i then
+     old_uninst,new_uninst
+    else
+     let ty' = apply_subst ty in
+      if i < newmeta then
+       ((i,ty')::old_uninst),new_uninst
+      else
+       old_uninst,((i,ty')::new_uninst)
+  ) metasenv ([],[])
+;;
+
 (* The term bo must be closed in the current context *)
 let apply term =
  let module T = CicTypeChecker in
@@ -268,7 +272,7 @@ let apply term =
   let metasenv =
    match !proof with
       None -> assert false
-    | Some (metasenv,_,_) -> metasenv
+    | Some (_,metasenv,_,_) -> metasenv
   in
   let (metano,context,ty) =
    match !goal with
@@ -278,82 +282,431 @@ let apply term =
        (* Invariant: context is the actual context of the meta in the proof *)
        metano,context,ty
   in
-   (*CSC: deve sparire! *)
-   let ciccontext = cic_context_of_context context in
-    let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
-     let mgul  = Array.to_list mgu in
-     let mgutl = Array.to_list mgut in
-     let applymetas_to_metas =
-      let newmeta = new_meta () in
-       (* WARNING: here we are using the invariant that above the most *)
-       (* recente new_meta() there are no used metas.                  *)
-       Array.init (List.length mgul) (function i -> newmeta + i) in
-      (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!!                         *)
-      (* Here we assume that either a META has been instantiated with *)
-      (* a close term or with itself.                                 *)
-      let uninstantiatedmetas =
-       List.fold_right2
-        (fun bo ty newmetas ->
-          match bo with
-             Cic.Meta i ->
-              let newmeta = applymetas_to_metas.(i) in
-               (*CSC: se ty contiene metas, queste hanno il numero errato!!! *)
-               let ty_with_newmetas =
-                (* Substitues (META n) with (META (applymetas_to_metas.(n))) *)
-                let rec aux =
-                 function
-                    C.Rel _
-                  | C.Var _ as t  -> t
-                  | C.Meta n -> C.Meta (applymetas_to_metas.(n))
-                  | C.Sort _
-                  | C.Implicit as t -> t
-                  | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
-                  | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
-                  | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
-                  | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-                  | C.Appl l -> C.Appl (List.map aux l)
-                  | C.Const _ as t -> t
-                  | C.Abst _ -> assert false
-                  | C.MutInd _
-                  | C.MutConstruct _ as t -> t
-                  | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
-                     C.MutCase (sp,cookingsno,i,aux outt, aux t,
-                      List.map aux pl)
-                  | C.Fix (i,fl) ->
-                     let substitutedfl =
-                      List.map
-                       (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
-                        fl
-                     in
-                      C.Fix (i, substitutedfl)
-                  | C.CoFix (i,fl) ->
-                     let substitutedfl =
-                      List.map
-                       (fun (name,ty,bo) -> (name, aux ty, aux bo))
-                        fl
-                     in
-                      C.CoFix (i, substitutedfl)
+   let ciccontext = cic_context_of_named_context context in
+    let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
+     (* newmeta is the lowest index of the new metas introduced *)
+     let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in
+      let newmetasenv = newmetas@metasenv in
+       let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
+        let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
+        let apply_subst = CicUnification.apply_subst subst in
+(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
+        let apply_subst_replacing t =
+         List.fold_left
+          (fun t (i,bo) ->
+            ProofEngineReduction.replace
+             ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+          t subst
+        in
+         let old_uninstantiatedmetas,new_uninstantiatedmetas =
+          classify_metas newmeta in_subst_domain apply_subst newmetasenv
+         in
+         let bo' =
+          if List.length newmetas = 0 then
+           term
+          else
+            let arguments =
+             List.map apply_subst
+              (List.map (function (i,_) -> C.Meta i) newmetas)
+            in
+            Cic.Appl (term::arguments)
+         in
+          refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
+            (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
+prerr_endline "QUI4" ; flush stderr ; (
+          match new_uninstantiatedmetas with
+             [] -> goal := None
+           | (i,ty)::_ -> goal := Some (i,(context,ty))
+) ;
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas)
+; prerr_endline "FATTO" ; flush stderr ;
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ;
+prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b))
+; prerr_endline "FATTO2" ; flush stderr
+;;
+
+let eta_expand metasenv ciccontext t arg =
+ let module T = CicTypeChecker in
+ let module S = CicSubstitution in
+ let module C = Cic in
+  let rec aux n =
+   function
+      t' when t' = S.lift n arg -> C.Rel (1 + n)
+    | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
+    | C.Var _
+    | C.Meta _
+    | C.Sort _
+    | C.Implicit as t -> t
+    | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
+    | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
+    | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
+    | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
+    | C.Appl l -> C.Appl (List.map (aux n) l)
+    | C.Const _ as t -> t
+    | C.Abst _ -> assert false
+    | C.MutInd _
+    | C.MutConstruct _ as t -> t
+    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+       C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
+        List.map (aux n) pl)
+    | C.Fix (i,fl) ->
+       let tylen = List.length fl in
+        let substitutedfl =
+         List.map
+          (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
+           fl
+        in
+         C.Fix (i, substitutedfl)
+    | C.CoFix (i,fl) ->
+       let tylen = List.length fl in
+        let substitutedfl =
+         List.map
+          (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
+           fl
+        in
+         C.CoFix (i, substitutedfl)
+  in
+   let argty =
+    T.type_of_aux' metasenv ciccontext arg
+   in
+    (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
+;;
+
+exception NotAnInductiveTypeToEliminate;;
+exception NotTheRightEliminatorShape;;
+exception NoHypothesesFound;;
+
+let elim term =
+ let module T = CicTypeChecker in
+ let module U = UriManager in
+ let module R = CicReduction in
+ let module C = Cic in
+  let curi,metasenv =
+   match !proof with
+      None -> assert false
+    | Some (curi,metasenv,_,_) -> curi,metasenv
+  in
+  let (metano,context,ty) =
+   match !goal with
+      None -> assert false
+    | Some (metano,(context,ty)) ->
+       assert (ty = List.assoc metano metasenv) ;
+       (* Invariant: context is the actual context of the meta in the proof *)
+       metano,context,ty
+  in
+   let ciccontext = cic_context_of_named_context context in
+    let termty = T.type_of_aux' metasenv ciccontext term in
+    let uri,cookingno,typeno,args =
+     match termty with
+        C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
+      | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
+          (uri,cookingno,typeno,args)
+      | _ -> raise NotAnInductiveTypeToEliminate
+    in
+     let eliminator_uri =
+      let buri = U.buri_of_uri uri in
+      let name = 
+       match CicEnvironment.get_cooked_obj uri cookingno with
+          C.InductiveDefinition (tys,_,_) ->
+           let (name,_,_,_) = List.nth tys typeno in
+            name
+        | _ -> assert false
+      in
+      let ext =
+       match T.type_of_aux' metasenv ciccontext ty with
+          C.Sort C.Prop -> "_ind"
+        | C.Sort C.Set  -> "_rec"
+        | C.Sort C.Type -> "_rect"
+        | _ -> assert false
+      in
+       U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
+     in
+      let eliminator_cookingno =
+       UriManager.relative_depth curi eliminator_uri 0
+      in
+      let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
+       let ety =
+        T.type_of_aux' [] [] eliminator_ref
+       in
+        let (econclusion,newmetas,newmeta,lastmeta) =
+         new_metasenv_for_apply ety
+        in
+         (* Here we assume that we have only one inductive hypothesis to *)
+         (* eliminate and that it is the last hypothesis of the theorem. *)
+         (* A better approach would be fingering the hypotheses in some  *)
+         (* way.                                                         *)
+         let meta_of_corpse = Cic.Meta (lastmeta - 1) in
+         let newmetasenv = newmetas @ metasenv in
+prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
+flush stderr ;
+         let subst1 =
+          CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
+         in
+          let ueconclusion = CicUnification.apply_subst subst1 econclusion in
+prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
+flush stderr ;
+           (* The conclusion of our elimination principle is *)
+           (*  (?i farg1 ... fargn)                         *)
+           (* The conclusion of our goal is ty. So, we can   *)
+           (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
+           (* a new ty equal to (P farg1 ... fargn). Now     *)
+           (* ?i can be instantiated with P and we are ready *)
+           (* to refine the term.                            *)
+           let emeta, fargs =
+            match ueconclusion with
+               C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
+             | _ -> raise NotTheRightEliminatorShape
+           in
+            let ty' = CicUnification.apply_subst subst1 ty in
+            let eta_expanded_ty =
+             List.fold_left (eta_expand metasenv ciccontext) ty' fargs
+            in
+prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
+             let subst2 =
+(*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
+da subst1!!!! Dovrei rimuoverle o sono innocue?*)
+              CicUnification.fo_unif
+               newmetasenv ciccontext ueconclusion eta_expanded_ty
+             in
+prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
+prerr_endline "unwind"; flush stderr;
+              let in_subst_domain i =
+               let eq_to_i = function (j,_) -> i=j in
+                List.exists eq_to_i subst1 ||
+                List.exists eq_to_i subst2
+              in
+               (* When unwinding the META that corresponds to the elimination *)
+               (* predicate (which is emeta), we must also perform one-step   *)
+               (* beta-reduction.                                             *)
+               let apply_subst t =
+                let t' = CicUnification.apply_subst subst1 t in
+                 CicUnification.apply_subst_reducing
+                  subst2 (Some (emeta,List.length fargs)) t'
+               in
+(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
+               let apply_subst_replacing t =
+                let t' =
+                 List.fold_left
+                  (fun t (i,bo) ->
+                    ProofEngineReduction.replace
+                     ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+                  t subst1
                 in
-                 aux ty
+                 List.fold_left
+                  (fun t (i,bo) ->
+                    ProofEngineReduction.replace
+                     ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+                  t' subst2
                in
-                (newmeta,ty_with_newmetas)::newmetas
-           | _ -> newmetas
-        ) mgul mgutl []
-      in
-      let mgul' =
-       List.map 
+                let newmetasenv' =
+                 List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
+                in
+                 let old_uninstantiatedmetas,new_uninstantiatedmetas =
+                  classify_metas newmeta in_subst_domain apply_subst newmetasenv
+                 in
+                  let arguments =
+                   List.map apply_subst
+                    (List.map (function (i,_) -> C.Meta i) newmetas)
+                  in
+                   let bo' = Cic.Appl (eliminator_ref::arguments) in
+prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
+List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
+                   refine_meta_with_brand_new_metasenv metano bo'
+                     apply_subst_replacing
+                     (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
+                   match new_uninstantiatedmetas with
+                      [] -> goal := None
+                    | (i,ty)::_ -> goal := Some (i,(context,ty))
+;;
+
+let elim_intros term =
+ elim term ;
+ intros ()
+;;
+
+let reduction_tactic reduction_function term =
+ let curi,metasenv,pbo,pty =
+  match !proof with
+     None -> assert false
+   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let (metano,context,ty) =
+  match !goal with
+     None -> assert false
+   | Some (metano,(context,ty)) -> metano,context,ty
+ in
+  let term' = reduction_function 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 ~what:term ~with_what:term' in
+    let ty' = replace ty in
+    let context' =
+     List.map
+      (function
+          Definition  (n,t) -> Definition  (n,replace t)
+        | Declaration (n,t) -> Declaration (n,replace t)
+      ) context
+    in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_) when n = metano -> (metano,ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      proof := Some (curi,metasenv',pbo,pty) ;
+      goal := Some (metano,(context',ty'))
+;;
+
+let reduction_tactic_in_scratch reduction_function ty term =
+ let metasenv =
+  match !proof with
+     None -> []
+   | Some (_,metasenv,_,_) -> metasenv
+ in
+ let context =
+  match !goal with
+     None -> []
+   | Some (_,(context,_)) -> context
+ in
+  let term' = reduction_function term in
+   ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
+;;
+
+let whd    = reduction_tactic CicReduction.whd;;
+let reduce = reduction_tactic ProofEngineReduction.reduce;;
+let simpl  = reduction_tactic ProofEngineReduction.simpl;;
+
+let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd;;
+let reduce_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.reduce;;
+let simpl_in_scratch  =
+ reduction_tactic_in_scratch ProofEngineReduction.simpl;;
+
+(* It is just the opposite of whd. The code should probably be merged. *)
+let fold term =
+ let curi,metasenv,pbo,pty =
+  match !proof with
+     None -> assert false
+   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let (metano,context,ty) =
+  match !goal with
+     None -> assert false
+   | Some (metano,(context,ty)) -> metano,context,ty
+ in
+  let term' = CicReduction.whd 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 ~what:term' ~with_what:term in
+    let ty' = replace ty in
+    let context' =
+     List.map
+      (function
+          Declaration (n,t) -> Declaration (n,replace t)
+        | Definition  (n,t) -> Definition (n,replace t)
+      ) context
+    in
+     let metasenv' = 
+      List.map
+       (function
+           (n,_) when n = metano -> (metano,ty')
+         | _ as t -> t
+       ) metasenv
+     in
+      proof := Some (curi,metasenv',pbo,pty) ;
+      goal := Some (metano,(context',ty'))
+;;
+
+let cut term =
+ let module C = Cic in
+  let curi,metasenv,pbo,pty =
+   match !proof with
+      None -> assert false
+    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+  in
+  let (metano,context,ty) =
+   match !goal with
+      None -> assert false
+    | Some (metano,(context,ty)) -> metano,context,ty
+  in
+   let newmeta1 = new_meta () in
+   let newmeta2 = newmeta1 + 1 in
+    let newmeta1ty = CicSubstitution.lift 1 ty in
+    let bo' =
+     C.Appl
+      [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
+       C.Meta newmeta2]
+    in
+prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
+     refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
+     goal :=
+      Some
+       (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
+        newmeta1ty))
+;;
+
+let letin term =
+ let module C = Cic in
+  let curi,metasenv,pbo,pty =
+   match !proof with
+      None -> assert false
+    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+  in
+  let (metano,context,ty) =
+   match !goal with
+      None -> assert false
+    | Some (metano,(context,ty)) -> metano,context,ty
+  in
+   let ciccontext = cic_context_of_named_context context in
+   let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
+    let newmeta = new_meta () in
+     let newmetaty = CicSubstitution.lift 1 ty in
+     let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
+      refine_meta metano bo' [newmeta,newmetaty];
+      goal :=
+       Some
+        (newmeta,
+         ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
+;;
+
+exception NotConvertible;;
+
+(*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
+(*CSC: while [goal_input] can have a richer context (because of binders) *)
+(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
+(*CSC: Is that evident? Is that right? Or should it be changed?          *)
+let change ~goal_input ~input =
+ let curi,metasenv,pbo,pty =
+  match !proof with
+     None -> assert false
+   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let (metano,context,ty) =
+  match !goal with
+     None -> assert false
+   | Some (metano,(context,ty)) -> metano,context,ty
+ in
+  let ciccontext = cic_context_of_named_context context in
+   (* are_convertible works only on well-typed terms *)
+   ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
+   if CicReduction.are_convertible goal_input input then
+    begin
+     let ty' = ProofEngineReduction.replace goal_input input ty in
+      let metasenv' = 
+       List.map
         (function
-            Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i))
+            (n,_) when n = metano -> (metano,ty')
           | _ as t -> t
-        ) mgul in
-       let bo' =
-        if List.length mgul' = 0 then
-         term 
-        else
-         Cic.Appl (term::mgul')
-       in
-        refine_meta metano bo' uninstantiatedmetas ;
-        match uninstantiatedmetas with
-           (n,ty)::tl -> goal := Some (n,(context,ty))
-         | [] -> goal := None
+        ) metasenv
+      in
+       proof := Some (curi,metasenv',pbo,pty) ;
+       goal := Some (metano,(context,ty'))
+    end
+  else
+   raise NotConvertible
 ;;