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