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