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 (* lambda_abstract newmeta ty *)
 166 (* returns a triple [bo],[context],[ty'] where              *)
 167 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
 168 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
 169 (* So, lambda_abstract is the core of the implementation of *)
 170 (* the Intros tactic.                                       *)
 171 let lambda_abstract newmeta ty =
 172  let module C = Cic in
 173   let rec collect_context =
 174    function
 175       C.Cast (te,_)   -> collect_context te
 176     | C.Prod (n,s,t)  ->
 177        let (ctx,ty,bo) = collect_context t in
 178         let n' =
 179          match n with
 180             C.Name _ -> n
 181 (*CSC: generatore di nomi? Chiedere il nome? *)
 182           | C.Anonimous -> C.Name "fresh_name"
 183         in
 184          ((Declaration (n',s))::ctx,ty,C.Lambda(n',s,bo))
 185     | C.LetIn (n,s,t) ->
 186        let (ctx,ty,bo) = collect_context t in
 187         ((Definition (n,s))::ctx,ty,C.LetIn(n,s,bo))
 188     | _ as t -> [], t, (C.Meta newmeta)
 189   in
 190    let revcontext,ty',bo = collect_context ty in
 191     bo,(List.rev revcontext),ty'
 192 ;;
 193
 194 let intros () =
 195  let module C = Cic in
 196  let module R = CicReduction in
 197   let metasenv =
 198    match !proof with
 199       None -> assert false
 200     | Some (_,metasenv,_,_) -> metasenv
 201   in
 202   let (metano,context,ty) =
 203    match !goal with
 204       None -> assert false
 205     | Some (metano,(context,ty)) -> metano,context,ty
 206   in
 207    let newmeta = new_meta () in
 208     let (bo',newcontext,ty') = lambda_abstract newmeta ty in
 209       let context'' = newcontext @ context in
 210        refine_meta metano bo' [newmeta,ty'] ;
 211        goal := Some (newmeta,(context'',ty'))
 212 ;;
 213
 214 (* The term bo must be closed in the current context *)
 215 let exact bo =
 216  let module T = CicTypeChecker in
 217  let module R = CicReduction in
 218   let metasenv =
 219    match !proof with
 220       None -> assert false
 221     | Some (_,metasenv,_,_) -> metasenv
 222   in
 223   let (metano,context,ty) =
 224    match !goal with
 225       None -> assert false
 226     | Some (metano,(context,ty)) ->
 227        assert (ty = List.assoc metano metasenv) ;
 228        (* Invariant: context is the actual context of the meta in the proof *)
 229        metano,context,ty
 230   in
 231    let context = cic_context_of_named_context context in
 232     if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
 233      begin
 234       refine_meta metano bo [] ;
 235       goal := None
 236      end
 237     else
 238      raise (Fail "The type of the provided term is not the one expected.")
 239 ;;
 240
 241 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
 242 (*CSC: Elim tactic. Do we already need tacticals?                       *)
 243 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 244 (* head, a META environment in which there is new a META for each hypothesis,*)
 245 (* a list of arguments for the new applications and the indexes of the first *)
 246 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 247 (* is the nth new META lambda-abstracted as much as possible. Hence, this    *)
 248 (* functions already provides the behaviour of Intros on the new goals.      *)
 249 let new_metasenv_for_apply_intros ty =
 250  let module C = Cic in
 251  let module S = CicSubstitution in
 252   let rec aux newmeta =
 253    function
 254       C.Cast (he,_) -> aux newmeta he
 255     | C.Prod (_,s,t) ->
 256        let newargument,newcontext,ty' = lambda_abstract newmeta s in
 257         let (res,newmetasenv,arguments,lastmeta) =
 258          aux (newmeta + 1) (S.subst newargument t)
 259         in
 260          res,(newmeta,ty')::newmetasenv,newargument::arguments,lastmeta
 261     | t -> t,[],[],newmeta
 262   in
 263    let newmeta = new_meta () in
 264     (* WARNING: here we are using the invariant that above the most *)
 265     (* recente new_meta() there are no used metas.                  *)
 266     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 267      res,newmetasenv,arguments,newmeta,lastmeta
 268 ;;
 269
 270 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 271 (* head, a META environment in which there is new a META for each hypothesis,*)
 272 (* a list of arguments for the new applications and the indexes of the first *)
 273 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 274 (* is just the nth new META.                                                 *)
 275 let new_metasenv_for_apply ty =
 276  let module C = Cic in
 277  let module S = CicSubstitution in
 278   let rec aux newmeta =
 279    function
 280       C.Cast (he,_) -> aux newmeta he
 281     | C.Prod (_,s,t) ->
 282        let newargument = C.Meta newmeta in
 283         let (res,newmetasenv,arguments,lastmeta) =
 284          aux (newmeta + 1) (S.subst newargument t)
 285         in
 286          res,(newmeta,s)::newmetasenv,newargument::arguments,lastmeta
 287     | t -> t,[],[],newmeta
 288   in
 289    let newmeta = new_meta () in
 290     (* WARNING: here we are using the invariant that above the most *)
 291     (* recente new_meta() there are no used metas.                  *)
 292     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 293      res,newmetasenv,arguments,newmeta,lastmeta
 294 ;;
 295
 296
 297 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 298 let classify_metas newmeta in_subst_domain apply_subst metasenv =
 299  List.fold_right
 300   (fun (i,ty) (old_uninst,new_uninst) ->
 301     if in_subst_domain i then
 302      old_uninst,new_uninst
 303     else
 304      let ty' = apply_subst ty in
 305       if i < newmeta then
 306        ((i,ty')::old_uninst),new_uninst
 307       else
 308        old_uninst,((i,ty')::new_uninst)
 309   ) metasenv ([],[])
 310 ;;
 311
 312 (* The term bo must be closed in the current context *)
 313 let apply term =
 314  let module T = CicTypeChecker in
 315  let module R = CicReduction in
 316  let module C = Cic in
 317   let metasenv =
 318    match !proof with
 319       None -> assert false
 320     | Some (_,metasenv,_,_) -> metasenv
 321   in
 322   let (metano,context,ty) =
 323    match !goal with
 324       None -> assert false
 325     | Some (metano,(context,ty)) ->
 326        assert (ty = List.assoc metano metasenv) ;
 327        (* Invariant: context is the actual context of the meta in the proof *)
 328        metano,context,ty
 329   in
 330    let ciccontext = cic_context_of_named_context context in
 331     let termty = CicTypeChecker.type_of_aux' metasenv ciccontext term in
 332      (* newmeta is the lowest index of the new metas introduced *)
 333      let (consthead,newmetas,arguments,newmeta,_) =
 334       new_metasenv_for_apply termty
 335      in
 336       let newmetasenv = newmetas@metasenv in
 337        let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
 338         let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
 339         let apply_subst = CicUnification.apply_subst subst in
 340 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
 341         let apply_subst_replacing t =
 342          List.fold_left
 343           (fun t (i,bo) ->
 344             ProofEngineReduction.replace
 345              ~what:(Cic.Meta i) ~with_what:bo ~where:t)
 346           t subst
 347         in
 348          let old_uninstantiatedmetas,new_uninstantiatedmetas =
 349           classify_metas newmeta in_subst_domain apply_subst newmetasenv
 350          in
 351           let bo' =
 352            if List.length newmetas = 0 then
 353             term
 354            else
 355             let arguments' = List.map apply_subst arguments in
 356              Cic.Appl (term::arguments')
 357           in
 358            refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
 359             (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
 360            match new_uninstantiatedmetas with
 361               [] -> goal := None
 362             | (i,ty)::_ -> goal := Some (i,(context,ty))
 363 ;;
 364
 365 let eta_expand metasenv ciccontext t arg =
 366  let module T = CicTypeChecker in
 367  let module S = CicSubstitution in
 368  let module C = Cic in
 369   let rec aux n =
 370    function
 371       t' when t' = S.lift n arg -> C.Rel (1 + n)
 372     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
 373     | C.Var _
 374     | C.Meta _
 375     | C.Sort _
 376     | C.Implicit as t -> t
 377     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
 378     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
 379     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
 380     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
 381     | C.Appl l -> C.Appl (List.map (aux n) l)
 382     | C.Const _ as t -> t
 383     | C.Abst _ -> assert false
 384     | C.MutInd _
 385     | C.MutConstruct _ as t -> t
 386     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 387        C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
 388         List.map (aux n) pl)
 389     | C.Fix (i,fl) ->
 390        let tylen = List.length fl in
 391         let substitutedfl =
 392          List.map
 393           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 394            fl
 395         in
 396          C.Fix (i, substitutedfl)
 397     | C.CoFix (i,fl) ->
 398        let tylen = List.length fl in
 399         let substitutedfl =
 400          List.map
 401           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 402            fl
 403         in
 404          C.CoFix (i, substitutedfl)
 405   in
 406    let argty =
 407     T.type_of_aux' metasenv ciccontext arg
 408    in
 409     (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
 410 ;;
 411
 412 exception NotAnInductiveTypeToEliminate;;
 413 exception NotTheRightEliminatorShape;;
 414 exception NoHypothesesFound;;
 415
 416 let elim_intros term =
 417  let module T = CicTypeChecker in
 418  let module U = UriManager in
 419  let module R = CicReduction in
 420  let module C = Cic in
 421   let curi,metasenv =
 422    match !proof with
 423       None -> assert false
 424     | Some (curi,metasenv,_,_) -> curi,metasenv
 425   in
 426   let (metano,context,ty) =
 427    match !goal with
 428       None -> assert false
 429     | Some (metano,(context,ty)) ->
 430        assert (ty = List.assoc metano metasenv) ;
 431        (* Invariant: context is the actual context of the meta in the proof *)
 432        metano,context,ty
 433   in
 434    let ciccontext = cic_context_of_named_context context in
 435     let termty = T.type_of_aux' metasenv ciccontext term in
 436     let uri,cookingno,typeno,args =
 437      match termty with
 438         C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
 439       | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
 440           (uri,cookingno,typeno,args)
 441       | _ -> raise NotAnInductiveTypeToEliminate
 442     in
 443      let eliminator_uri =
 444       let buri = U.buri_of_uri uri in
 445       let name =
 446        match CicEnvironment.get_cooked_obj uri cookingno with
 447           C.InductiveDefinition (tys,_,_) ->
 448            let (name,_,_,_) = List.nth tys typeno in
 449             name
 450         | _ -> assert false
 451       in
 452       let ext =
 453        match T.type_of_aux' metasenv ciccontext ty with
 454           C.Sort C.Prop -> "_ind"
 455         | C.Sort C.Set  -> "_rec"
 456         | C.Sort C.Type -> "_rect"
 457         | _ -> assert false
 458       in
 459        U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
 460      in
 461       let eliminator_cookingno =
 462        UriManager.relative_depth curi eliminator_uri 0
 463       in
 464       let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
 465        let ety =
 466         T.type_of_aux' [] [] eliminator_ref
 467        in
 468         let (econclusion,newmetas,arguments,newmeta,lastmeta) =
 469          new_metasenv_for_apply ety
 470         in
 471          (* Here we assume that we have only one inductive hypothesis to *)
 472          (* eliminate and that it is the last hypothesis of the theorem. *)
 473          (* A better approach would be fingering the hypotheses in some  *)
 474          (* way.                                                         *)
 475          let meta_of_corpse = Cic.Meta (lastmeta - 1) in
 476          let newmetasenv = newmetas @ metasenv in
 477 prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
 478 flush stderr ;
 479          let subst1 =
 480           CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
 481          in
 482           let ueconclusion = CicUnification.apply_subst subst1 econclusion in
 483 prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
 484 flush stderr ;
 485            (* The conclusion of our elimination principle is *)
 486            (*  (?i farg1 ... fargn)                         *)
 487            (* The conclusion of our goal is ty. So, we can   *)
 488            (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
 489            (* a new ty equal to (P farg1 ... fargn). Now     *)
 490            (* ?i can be instantiated with P and we are ready *)
 491            (* to refine the term.                            *)
 492            let emeta, fargs =
 493             match ueconclusion with
 494 (*CSC: Code to be used for Apply *)
 495                C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
 496              | C.Meta emeta -> emeta,[]
 497 (*CSC: Code to be used for ApplyIntros
 498                C.Appl (he::fargs) ->
 499                 let rec find_head =
 500                  function
 501                     C.Meta emeta -> emeta
 502                   | C.Lambda (_,_,t) -> find_head t
 503                   | C.LetIn (_,_,t) -> find_head t
 504                   | _ ->raise NotTheRightEliminatorShape
 505                 in
 506                  find_head he,fargs
 507 *)
 508              | _ -> raise NotTheRightEliminatorShape
 509            in
 510             let ty' = CicUnification.apply_subst subst1 ty in
 511             let eta_expanded_ty =
 512              List.fold_left (eta_expand metasenv ciccontext) ty' fargs
 513             in
 514 prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
 515              let subst2 =
 516 (*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
 517 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
 518               CicUnification.fo_unif
 519                newmetasenv ciccontext ueconclusion eta_expanded_ty
 520              in
 521 prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
 522 prerr_endline "unwind"; flush stderr;
 523               let in_subst_domain i =
 524                let eq_to_i = function (j,_) -> i=j in
 525                 List.exists eq_to_i subst1 ||
 526                 List.exists eq_to_i subst2
 527               in
 528                (* When unwinding the META that corresponds to the elimination *)
 529                (* predicate (which is emeta), we must also perform one-step   *)
 530                (* beta-reduction.                                             *)
 531                let apply_subst t =
 532                 let t' = CicUnification.apply_subst subst1 t in
 533                  CicUnification.apply_subst_reducing
 534                   subst2 (Some (emeta,List.length fargs)) t'
 535                in
 536 (*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
 537                let apply_subst_replacing t =
 538                 let t' =
 539                  List.fold_left
 540                   (fun t (i,bo) ->
 541                     ProofEngineReduction.replace
 542                      ~what:(Cic.Meta i) ~with_what:bo ~where:t)
 543                   t subst1
 544                 in
 545                  List.fold_left
 546                   (fun t (i,bo) ->
 547                     ProofEngineReduction.replace
 548                      ~what:(Cic.Meta i) ~with_what:bo ~where:t)
 549                   t' subst2
 550                in
 551                 let newmetasenv' =
 552                  List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
 553                 in
 554                  let old_uninstantiatedmetas,new_uninstantiatedmetas =
 555                   classify_metas newmeta in_subst_domain apply_subst newmetasenv
 556                  in
 557                   let arguments' = List.map apply_subst arguments in
 558                    let bo' = Cic.Appl (eliminator_ref::arguments') in
 559 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
 560 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
 561                     refine_meta_with_brand_new_metasenv metano bo'
 562                      apply_subst_replacing
 563                      (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
 564                     match new_uninstantiatedmetas with
 565                        [] -> goal := None
 566                      | (i,ty)::_ -> goal := Some (i,(context,ty))
 567 ;;
 568
 569 let reduction_tactic reduction_function term =
 570  let curi,metasenv,pbo,pty =
 571   match !proof with
 572      None -> assert false
 573    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 574  in
 575  let (metano,context,ty) =
 576   match !goal with
 577      None -> assert false
 578    | Some (metano,(context,ty)) -> metano,context,ty
 579  in
 580   let term' = reduction_function term in
 581    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 582    (* the type of one metavariable. So we replace it everywhere.   *)
 583    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 584    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 585    let replace = ProofEngineReduction.replace ~what:term ~with_what:term' in
 586     let ty' = replace ty in
 587     let context' =
 588      List.map
 589       (function
 590           Definition  (n,t) -> Definition  (n,replace t)
 591         | Declaration (n,t) -> Declaration (n,replace t)
 592       ) context
 593     in
 594      let metasenv' =
 595       List.map
 596        (function
 597            (n,_) when n = metano -> (metano,ty')
 598          | _ as t -> t
 599        ) metasenv
 600      in
 601       proof := Some (curi,metasenv',pbo,pty) ;
 602       goal := Some (metano,(context',ty'))
 603 ;;
 604
 605 let reduction_tactic_in_scratch reduction_function ty term =
 606  let metasenv =
 607   match !proof with
 608      None -> []
 609    | Some (_,metasenv,_,_) -> metasenv
 610  in
 611  let context =
 612   match !goal with
 613      None -> []
 614    | Some (_,(context,_)) -> context
 615  in
 616   let term' = reduction_function term in
 617    ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
 618 ;;
 619
 620 let whd    = reduction_tactic CicReduction.whd;;
 621 let reduce = reduction_tactic ProofEngineReduction.reduce;;
 622 let simpl  = reduction_tactic ProofEngineReduction.simpl;;
 623
 624 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd;;
 625 let reduce_in_scratch =
 626  reduction_tactic_in_scratch ProofEngineReduction.reduce;;
 627 let simpl_in_scratch  =
 628  reduction_tactic_in_scratch ProofEngineReduction.simpl;;
 629
 630 (* It is just the opposite of whd. The code should probably be merged. *)
 631 let fold term =
 632  let curi,metasenv,pbo,pty =
 633   match !proof with
 634      None -> assert false
 635    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 636  in
 637  let (metano,context,ty) =
 638   match !goal with
 639      None -> assert false
 640    | Some (metano,(context,ty)) -> metano,context,ty
 641  in
 642   let term' = CicReduction.whd term in
 643    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 644    (* the type of one metavariable. So we replace it everywhere.   *)
 645    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 646    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 647    let replace = ProofEngineReduction.replace ~what:term' ~with_what:term in
 648     let ty' = replace ty in
 649     let context' =
 650      List.map
 651       (function
 652           Declaration (n,t) -> Declaration (n,replace t)
 653         | Definition  (n,t) -> Definition (n,replace t)
 654       ) context
 655     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 ;;
 666
 667 let cut term =
 668  let module C = Cic in
 669   let curi,metasenv,pbo,pty =
 670    match !proof with
 671       None -> assert false
 672     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 673   in
 674   let (metano,context,ty) =
 675    match !goal with
 676       None -> assert false
 677     | Some (metano,(context,ty)) -> metano,context,ty
 678   in
 679    let newmeta1 = new_meta () in
 680    let newmeta2 = newmeta1 + 1 in
 681     let newmeta1ty = CicSubstitution.lift 1 ty in
 682     let bo' =
 683      C.Appl
 684       [C.Lambda (C.Name "dummy_for_cut",term,C.Meta newmeta1) ;
 685        C.Meta newmeta2]
 686     in
 687 prerr_endline ("BO': " ^ CicPp.ppterm bo') ; flush stderr ;
 688      refine_meta metano bo' [newmeta2,term; newmeta1,newmeta1ty];
 689      goal :=
 690       Some
 691        (newmeta1,((Declaration (C.Name "dummy_for_cut", term))::context,
 692         newmeta1ty))
 693 ;;
 694
 695 let letin term =
 696  let module C = Cic in
 697   let curi,metasenv,pbo,pty =
 698    match !proof with
 699       None -> assert false
 700     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 701   in
 702   let (metano,context,ty) =
 703    match !goal with
 704       None -> assert false
 705     | Some (metano,(context,ty)) -> metano,context,ty
 706   in
 707    let ciccontext = cic_context_of_named_context context in
 708    let _ = CicTypeChecker.type_of_aux' metasenv ciccontext term in
 709     let newmeta = new_meta () in
 710      let newmetaty = CicSubstitution.lift 1 ty in
 711      let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta newmeta) in
 712       refine_meta metano bo' [newmeta,newmetaty];
 713       goal :=
 714        Some
 715         (newmeta,
 716          ((Definition (C.Name "dummy_for_letin", term))::context, newmetaty))
 717 ;;
 718
 719 exception NotConvertible;;
 720
 721 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
 722 (*CSC: while [goal_input] can have a richer context (because of binders) *)
 723 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
 724 (*CSC: Is that evident? Is that right? Or should it be changed?          *)
 725 let change ~goal_input ~input =
 726  let curi,metasenv,pbo,pty =
 727   match !proof with
 728      None -> assert false
 729    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 730  in
 731  let (metano,context,ty) =
 732   match !goal with
 733      None -> assert false
 734    | Some (metano,(context,ty)) -> metano,context,ty
 735  in
 736   let ciccontext = cic_context_of_named_context context in
 737    (* are_convertible works only on well-typed terms *)
 738    ignore (CicTypeChecker.type_of_aux' metasenv ciccontext input) ;
 739    if CicReduction.are_convertible goal_input input then
 740     begin
 741      let ty' = ProofEngineReduction.replace goal_input input ty in
 742       let metasenv' =
 743        List.map
 744         (function
 745             (n,_) when n = metano -> (metano,ty')
 746           | _ as t -> t
 747         ) metasenv
 748       in
 749        proof := Some (curi,metasenv',pbo,pty) ;
 750        goal := Some (metano,(context,ty'))
 751     end
 752   else
 753    raise NotConvertible
 754 ;;