helm/gTopLevel/proofEngine.ml

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