helm/gTopLevel/proofEngine.ml

   1 type binder_type =
   2    Declaration of Cic.name * Cic.term
   3  | Definition of Cic.name * Cic.term
   4 ;;
   5
   6 type metasenv = (int * Cic.term) list;;
   7
   8 type named_context = binder_type list;;
   9
  10 type sequent = named_context * Cic.term;;
  11
  12 let proof =
  13  ref (None : (UriManager.uri * metasenv * Cic.term * Cic.term) option)
  14 ;;
  15 (*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
  16 (* Note: the sequent is redundant: it can be computed from the type of the   *)
  17 (* metavariable and its context in the proof. We keep it just for efficiency *)
  18 (* because computing the context of a term may be quite expensive.           *)
  19 let goal = ref (None : (int * sequent) option);;
  20
  21 exception NotImplemented
  22
  23 let cic_context_of_named_context =
  24  List.map
  25   (function
  26       Declaration (_,t) -> Cic.Decl t
  27     | Definition (_,t) -> Cic.Def t
  28   )
  29 ;;
  30
  31 let refine_meta_with_brand_new_metasenv meta term newmetasenv =
  32  let (uri,bo,ty) =
  33   match !proof with
  34      None -> assert false
  35    | Some (uri,_,bo,ty) -> uri,bo,ty
  36  in
  37   let subst_in t =
  38    ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
  39   in
  40    let bo' = subst_in bo in
  41    let metasenv' = List.remove_assoc meta newmetasenv in
  42     proof := Some (uri,metasenv',bo',ty)
  43 ;;
  44
  45 let refine_meta meta term newmetasenv =
  46  let (uri,metasenv,bo,ty) =
  47   match !proof with
  48      None -> assert false
  49    | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
  50  in
  51   let subst_in t =
  52    ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
  53   in
  54    let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
  55     let metasenv'' = List.map (function i,ty -> i,(subst_in ty)) metasenv' in
  56     let bo' = subst_in bo in
  57      proof := Some (uri,metasenv'',bo',ty)
  58 ;;
  59
  60 (* Returns the first meta whose number is above the *)
  61 (* number of the higher meta.                       *)
  62 let new_meta () =
  63  let metasenv =
  64   match !proof with
  65      None -> assert false
  66    | Some (_,metasenv,_,_) -> metasenv
  67  in
  68   let rec aux =
  69    function
  70       None,[] -> 1
  71     | Some n,[] -> n
  72     | None,(n,_)::tl -> aux (Some n,tl)
  73     | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  74   in
  75    1 + aux (None,metasenv)
  76 ;;
  77
  78 (* metas_in_term term                                                *)
  79 (* Returns the ordered list of the metas that occur in [term].       *)
  80 (* Duplicates are removed. The implementation is not very efficient. *)
  81 let metas_in_term term =
  82  let module C = Cic in
  83   let rec aux =
  84    function
  85       C.Rel _
  86     | C.Var _ -> []
  87     | C.Meta n -> [n]
  88     | C.Sort _
  89     | C.Implicit -> []
  90     | C.Cast (te,ty) -> (aux te) @ (aux ty)
  91     | C.Prod (_,s,t) -> (aux s) @ (aux t)
  92     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
  93     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
  94     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
  95     | C.Const _
  96     | C.Abst _
  97     | C.MutInd _
  98     | C.MutConstruct _ -> []
  99     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 100        (aux outt) @ (aux t) @
 101         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
 102     | C.Fix (i,fl) ->
 103         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 104     | C.CoFix (i,fl) ->
 105         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 106   in
 107    let metas = aux term in
 108     let rec elim_duplicates =
 109      function
 110         [] -> []
 111       | he::tl ->
 112          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
 113     in
 114      elim_duplicates metas
 115 ;;
 116
 117 (* perforate context term ty                                                 *)
 118 (* replaces the term [term] in the proof with a new metavariable whose type  *)
 119 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
 120 (* could be easily computed; so the only reasons to have it as an argument   *)
 121 (* are efficiency reasons.                                                   *)
 122 let perforate context term ty =
 123  let module C = Cic in
 124   let newmeta = new_meta () in
 125    match !proof with
 126       None -> assert false
 127     | Some (uri,metasenv,bo,gty) ->
 128        (* We push the new meta at the end of the list for pretty-printing *)
 129        (* purposes: in this way metas are ordered.                        *)
 130        let metasenv' = metasenv@[newmeta,ty] in
 131         let bo' = ProofEngineReduction.replace term (C.Meta newmeta) bo in
 132         (* It may be possible that some metavariables occurred only in *)
 133         (* the term we are perforating and they now occurs no more. We *)
 134         (* get rid of them, collecting the really useful metavariables *)
 135         (* in metasenv''.                                              *)
 136          let newmetas = metas_in_term bo' in
 137           let metasenv'' =
 138            List.filter (function (n,_) -> List.mem n newmetas) metasenv'
 139           in
 140            proof := Some (uri,metasenv'',bo',gty) ;
 141            goal := Some (newmeta,(context,ty)) ;
 142            newmeta
 143 ;;
 144
 145 (************************************************************)
 146 (*                  Some easy tactics.                      *)
 147 (************************************************************)
 148
 149 exception Fail of string;;
 150
 151 let intros () =
 152  let module C = Cic in
 153  let module R = CicReduction in
 154   let metasenv =
 155    match !proof with
 156       None -> assert false
 157     | Some (_,metasenv,_,_) -> metasenv
 158   in
 159   let (metano,context,ty) =
 160    match !goal with
 161       None -> assert false
 162     | Some (metano,(context,ty)) -> metano,context,ty
 163   in
 164    let newmeta = new_meta () in
 165     let rec collect_context =
 166      function
 167         C.Cast (te,_)   -> collect_context te
 168       | C.Prod (n,s,t)  ->
 169          let (ctx,ty,bo) = collect_context t in
 170           let n' =
 171            match n with
 172               C.Name _ -> n
 173 (*CSC: generatore di nomi? Chiedere il nome? *)
 174             | C.Anonimous -> C.Name "fresh_name"
 175           in
 176            ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
 177       | C.LetIn (n,s,t) ->
 178          let (ctx,ty,bo) = collect_context t in
 179           ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
 180       | _ as t -> [], t, (C.Meta newmeta)
 181     in
 182      let revcontext',ty',bo' = collect_context ty in
 183       let context'' = (List.rev revcontext') @ context in
 184        refine_meta metano bo' [newmeta,ty'] ;
 185        goal := Some (newmeta,(context'',ty'))
 186 ;;
 187
 188 (* The term bo must be closed in the current context *)
 189 let exact bo =
 190  let module T = CicTypeChecker in
 191  let module R = CicReduction in
 192   let metasenv =
 193    match !proof with
 194       None -> assert false
 195     | Some (_,metasenv,_,_) -> metasenv
 196   in
 197   let (metano,context,ty) =
 198    match !goal with
 199       None -> assert false
 200     | Some (metano,(context,ty)) ->
 201        assert (ty = List.assoc metano metasenv) ;
 202        (* Invariant: context is the actual context of the meta in the proof *)
 203        metano,context,ty
 204   in
 205    let context = cic_context_of_named_context context in
 206     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
 207      begin
 208       refine_meta metano bo [] ;
 209       goal := None
 210      end
 211     else
 212      raise (Fail "The type of the provided term is not the one expected.")
 213 ;;
 214
 215 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 216 (* head, a META environment in which there is a META for each hypothesis and *)
 217 (* the indexes of the first and last new METAs introduced.                   *)
 218 let new_metasenv_for_apply ty =
 219  let module C = Cic in
 220  let module S = CicSubstitution in
 221   let rec aux newmeta =
 222    function
 223       C.Cast (he,_) -> aux newmeta he
 224     | C.Prod (_,s,t) ->
 225        let (res,newmetasenv,lastmeta) =
 226         aux (newmeta + 1) (S.subst (C.Meta newmeta) t)
 227        in
 228         res,(newmeta,s)::newmetasenv,lastmeta
 229     | t -> t,[],newmeta
 230   in
 231    let newmeta = new_meta () in
 232     (* WARNING: here we are using the invariant that above the most *)
 233     (* recente new_meta() there are no used metas.                  *)
 234     let (res,newmetasenv,lastmeta) = aux newmeta ty in
 235      res,newmetasenv,newmeta,lastmeta
 236 ;;
 237
 238 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 239 let classify_metas newmeta in_subst_domain apply_subst =
 240  List.fold_left
 241   (fun (old_uninst,new_uninst) (i,ty) ->
 242     if in_subst_domain i then
 243      old_uninst,new_uninst
 244     else
 245      let ty' = apply_subst ty in
 246       if i < newmeta then
 247        ((i,ty')::old_uninst),new_uninst
 248       else
 249        old_uninst,((i,ty')::new_uninst)
 250   ) ([],[])
 251 ;;
 252
 253 (* The term bo must be closed in the current context *)
 254 let apply term =
 255  let module T = CicTypeChecker in
 256  let module R = CicReduction in
 257  let module C = Cic in
 258   let metasenv =
 259    match !proof with
 260       None -> assert false
 261     | Some (_,metasenv,_,_) -> metasenv
 262   in
 263   let (metano,context,ty) =
 264    match !goal with
 265       None -> assert false
 266     | Some (metano,(context,ty)) ->
 267        assert (ty = List.assoc metano metasenv) ;
 268        (* Invariant: context is the actual context of the meta in the proof *)
 269        metano,context,ty
 270   in
 271    let ciccontext = cic_context_of_named_context context in
 272     let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
 273      (* newmeta is the lowest index of the new metas introduced *)
 274      let (consthead,newmetas,newmeta,_) = new_metasenv_for_apply termty in
 275       let newmetasenv = newmetas@metasenv in
 276        let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
 277         let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
 278         let apply_subst = CicUnification.apply_subst subst in
 279          let old_uninstantiatedmetas,new_uninstantiatedmetas =
 280           classify_metas newmeta in_subst_domain apply_subst newmetasenv
 281          in
 282           let bo' =
 283            if List.length newmetas = 0 then
 284             term
 285            else
 286             let arguments =
 287              List.map apply_subst
 288               (List.map (function (i,_) -> C.Meta i) newmetas)
 289             in
 290              Cic.Appl (term::arguments)
 291           in
 292            refine_meta_with_brand_new_metasenv metano bo'
 293             (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
 294            match new_uninstantiatedmetas with
 295               [] -> goal := None
 296             | (i,ty)::_ -> goal := Some (i,(context,ty))
 297 ;;
 298
 299 let eta_expand metasenv ciccontext t arg =
 300  let module T = CicTypeChecker in
 301  let module S = CicSubstitution in
 302  let module C = Cic in
 303   let rec aux n =
 304    function
 305       t' when t' = S.lift n arg -> C.Rel (1 + n)
 306     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
 307     | C.Var _
 308     | C.Meta _
 309     | C.Sort _
 310     | C.Implicit as t -> t
 311     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
 312     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
 313     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
 314     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
 315     | C.Appl l -> C.Appl (List.map (aux n) l)
 316     | C.Const _ as t -> t
 317     | C.Abst _ -> assert false
 318     | C.MutInd _
 319     | C.MutConstruct _ as t -> t
 320     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 321        C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
 322         List.map (aux n) pl)
 323     | C.Fix (i,fl) ->
 324        let tylen = List.length fl in
 325         let substitutedfl =
 326          List.map
 327           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 328            fl
 329         in
 330          C.Fix (i, substitutedfl)
 331     | C.CoFix (i,fl) ->
 332        let tylen = List.length fl in
 333         let substitutedfl =
 334          List.map
 335           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 336            fl
 337         in
 338          C.CoFix (i, substitutedfl)
 339   in
 340    let argty =
 341     T.type_of_aux' metasenv ciccontext arg
 342    in
 343     (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
 344 ;;
 345
 346 exception NotAnInductiveTypeToEliminate;;
 347 exception NotTheRightEliminatorShape;;
 348 exception NoHypothesesFound;;
 349
 350 let elim term =
 351  let module T = CicTypeChecker in
 352  let module U = UriManager in
 353  let module R = CicReduction in
 354  let module C = Cic in
 355   let curi,metasenv =
 356    match !proof with
 357       None -> assert false
 358     | Some (curi,metasenv,_,_) -> curi,metasenv
 359   in
 360   let (metano,context,ty) =
 361    match !goal with
 362       None -> assert false
 363     | Some (metano,(context,ty)) ->
 364        assert (ty = List.assoc metano metasenv) ;
 365        (* Invariant: context is the actual context of the meta in the proof *)
 366        metano,context,ty
 367   in
 368    let ciccontext = cic_context_of_named_context context in
 369     let termty = T.type_of_aux' metasenv ciccontext term in
 370     let uri,cookingno,typeno,args =
 371      match termty with
 372         C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
 373       | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
 374           (uri,cookingno,typeno,args)
 375       | _ -> raise NotAnInductiveTypeToEliminate
 376     in
 377      let eliminator_uri =
 378       let buri = U.buri_of_uri uri in
 379       let name =
 380        match CicEnvironment.get_cooked_obj uri cookingno with
 381           C.InductiveDefinition (tys,_,_) ->
 382            let (name,_,_,_) = List.nth tys typeno in
 383             name
 384         | _ -> assert false
 385       in
 386       let ext =
 387        match T.type_of_aux' metasenv ciccontext ty with
 388           C.Sort C.Prop -> "_ind"
 389         | C.Sort C.Set  -> "_rec"
 390         | C.Sort C.Type -> "_rect"
 391         | _ -> assert false
 392       in
 393        U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
 394      in
 395       let eliminator_cookingno =
 396        UriManager.relative_depth curi eliminator_uri 0
 397       in
 398       let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
 399        let ety =
 400         T.type_of_aux' [] [] eliminator_ref
 401        in
 402         let (econclusion,newmetas,newmeta,lastmeta) =
 403          new_metasenv_for_apply ety
 404         in
 405          (* Here we assume that we have only one inductive hypothesis to *)
 406          (* eliminate and that it is the last hypothesis of the theorem. *)
 407          (* A better approach would be fingering the hypotheses in some  *)
 408          (* way.                                                         *)
 409          let meta_of_corpse = Cic.Meta (lastmeta - 1) in
 410          let newmetasenv = newmetas @ metasenv in
 411 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
 412 flush stderr ;
 413          let subst1 =
 414           CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
 415          in
 416           let ueconclusion = CicUnification.apply_subst subst1 econclusion in
 417 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
 418 flush stderr ;
 419            (* The conclusion of our elimination principle is *)
 420            (*  (?i farg1 ... fargn)                         *)
 421            (* The conclusion of our goal is ty. So, we can   *)
 422            (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
 423            (* a new ty equal to (P farg1 ... fargn). Now     *)
 424            (* ?i can be instantiated with P and we are ready *)
 425            (* to refine the term.                            *)
 426            let emeta, fargs =
 427             match ueconclusion with
 428                C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
 429              | _ -> raise NotTheRightEliminatorShape
 430            in
 431             let ty' = CicUnification.apply_subst subst1 ty in
 432             let eta_expanded_ty =
 433              List.fold_left (eta_expand metasenv ciccontext) ty' fargs
 434             in
 435 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
 436              let subst2 =
 437 (*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
 438 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
 439               CicUnification.fo_unif
 440                newmetasenv ciccontext ueconclusion eta_expanded_ty
 441              in
 442 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
 443 prerr_endline "unwind"; flush stderr;
 444               let in_subst_domain i =
 445                let eq_to_i = function (j,_) -> i=j in
 446                 List.exists eq_to_i subst1 ||
 447                 List.exists eq_to_i subst2
 448               in
 449                (* When unwinding the META that corresponds to the elimination *)
 450                (* predicate (which is emeta), we must also perform one-step   *)
 451                (* beta-reduction.                                             *)
 452                let apply_subst =
 453                 function t ->
 454                  let t' = CicUnification.apply_subst subst1 t in
 455                   CicUnification.apply_subst_reducing
 456                    subst2 (Some (emeta,List.length fargs)) t'
 457                in
 458                 let newmetasenv' =
 459                  List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
 460                 in
 461                  let old_uninstantiatedmetas,new_uninstantiatedmetas =
 462                   classify_metas newmeta in_subst_domain apply_subst newmetasenv
 463                  in
 464                   let arguments =
 465                    List.map apply_subst
 466                     (List.map (function (i,_) -> C.Meta i) newmetas)
 467                   in
 468                    let bo' = Cic.Appl (eliminator_ref::arguments) in
 469 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
 470 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
 471                     refine_meta_with_brand_new_metasenv metano bo'
 472                      (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
 473                     match new_uninstantiatedmetas with
 474                        [] -> goal := None
 475                      | (i,ty)::_ -> goal := Some (i,(context,ty))
 476 ;;
 477
 478 let elim_intros term =
 479  elim term ;
 480  intros ()
 481 ;;
 482
 483 let reduction_tactic reduction_function term =
 484  let curi,metasenv,pbo,pty =
 485   match !proof with
 486      None -> assert false
 487    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 488  in
 489  let (metano,context,ty) =
 490   match !goal with
 491      None -> assert false
 492    | Some (metano,(context,ty)) -> metano,context,ty
 493  in
 494   let term' = reduction_function term in
 495    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 496    (* the type of one metavariable. So we replace it everywhere.   *)
 497    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 498    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 499    let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
 500     let ty' = replace ty in
 501     let context' =
 502      List.map
 503       (function
 504           Definition  (n,t) -> Definition  (n,replace t)
 505         | Declaration (n,t) -> Declaration (n,replace t)
 506       ) context
 507     in
 508      let metasenv' =
 509       List.map
 510        (function
 511            (n,_) when n = metano -> (metano,ty')
 512          | _ as t -> t
 513        ) metasenv
 514      in
 515       proof := Some (curi,metasenv',pbo,pty) ;
 516       goal := Some (metano,(context',ty'))
 517 ;;
 518
 519 let reduction_tactic_in_scratch reduction_function ty term =
 520  let metasenv =
 521   match !proof with
 522      None -> []
 523    | Some (_,metasenv,_,_) -> metasenv
 524  in
 525  let context =
 526   match !goal with
 527      None -> []
 528    | Some (_,(context,_)) -> context
 529  in
 530   let term' = reduction_function term in
 531    ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
 532 ;;
 533
 534 let whd    = reduction_tactic CicReduction.whd;;
 535 let reduce = reduction_tactic ProofEngineReduction.reduce;;
 536 let simpl  = reduction_tactic ProofEngineReduction.simpl;;
 537
 538 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd;;
 539 let reduce_in_scratch =
 540  reduction_tactic_in_scratch ProofEngineReduction.reduce;;
 541 let simpl_in_scratch  =
 542  reduction_tactic_in_scratch ProofEngineReduction.simpl;;
 543
 544 (* It is just the opposite of whd. The code should probably be merged. *)
 545 let fold term =
 546  let curi,metasenv,pbo,pty =
 547   match !proof with
 548      None -> assert false
 549    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 550  in
 551  let (metano,context,ty) =
 552   match !goal with
 553      None -> assert false
 554    | Some (metano,(context,ty)) -> metano,context,ty
 555  in
 556   let term' = CicReduction.whd term in
 557    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 558    (* the type of one metavariable. So we replace it everywhere.   *)
 559    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 560    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 561    let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
 562     let ty' = replace ty in
 563     let context' =
 564      List.map
 565       (function
 566           Declaration (n,t) -> Declaration (n,replace t)
 567         | Definition  (n,t) -> Definition (n,replace t)
 568       ) context
 569     in
 570      let metasenv' =
 571       List.map
 572        (function
 573            (n,_) when n = metano -> (metano,ty')
 574          | _ as t -> t
 575        ) metasenv
 576      in
 577       proof := Some (curi,metasenv',pbo,pty) ;
 578       goal := Some (metano,(context',ty'))
 579 ;;
 580
 581 let cut term =
 582  let module C = Cic in
 583   let curi,metasenv,pbo,pty =
 584    match !proof with
 585       None -> assert false
 586     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 587   in
 588   let (metano,context,ty) =
 589    match !goal with
 590       None -> assert false
 591     | Some (metano,(context,ty)) -> metano,context,ty
 592   in
 593    let newmeta1 = new_meta () in
 594    let newmeta2 = newmeta1 + 1 in
 595     let newmeta1ty = CicSubstitution.lift 1 ty in
 596     let bo' =
 597      C.Appl
 598       [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
 599        C.Meta newmeta2]
 600     in
 601 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
 602      refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
 603      goal :=
 604       Some
 605        (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
 606         newmeta1ty))
 607 ;;
 608
 609 let letin term =
 610  let module C = Cic in
 611   let curi,metasenv,pbo,pty =
 612    match !proof with
 613       None -> assert false
 614     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 615   in
 616   let (metano,context,ty) =
 617    match !goal with
 618       None -> assert false
 619     | Some (metano,(context,ty)) -> metano,context,ty
 620   in
 621    let ciccontext = cic_context_of_named_context context in
 622    let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
 623     let newmeta = new_meta () in
 624      let newmetaty = CicSubstitution.lift 1 ty in
 625      let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
 626       refine_meta metano bo' [newmeta,newmetaty];
 627       goal :=
 628        Some
 629         (newmeta,
 630          ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
 631 ;;
 632
 633 exception NotConvertible;;
 634
 635 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
 636 (*CSC: while [goal_input] can have a richer context (because of binders) *)
 637 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
 638 (*CSC: Is that evident? Is that right? Or should it be changed?          *)
 639 let change ~goal_input ~input =
 640  let curi,metasenv,pbo,pty =
 641   match !proof with
 642      None -> assert false
 643    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 644  in
 645  let (metano,context,ty) =
 646   match !goal with
 647      None -> assert false
 648    | Some (metano,(context,ty)) -> metano,context,ty
 649  in
 650   let ciccontext = cic_context_of_named_context context in
 651    (* are_convertible works only on well-typed terms *)
 652    ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
 653    if CicReduction.are_convertible goal_input input then
 654     begin
 655      let ty' = ProofEngineReduction.replace goal_input input ty in
 656       let metasenv' =
 657        List.map
 658         (function
 659             (n,_) when n = metano -> (metano,ty')
 660           | _ as t -> t
 661         ) metasenv
 662       in
 663        proof := Some (curi,metasenv',pbo,pty) ;
 664        goal := Some (metano,(context,ty'))
 665     end
 666   else
 667    raise NotConvertible
 668 ;;