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