helm/gTopLevel/proofEngine.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 let proof =
  27  ref (None : (UriManager.uri * Cic.metasenv * Cic.term * Cic.term) option)
  28 ;;
  29 let goal = ref (None : int option);;
  30
  31 (*CSC: commento vecchio *)
  32 (* refine_meta_with_brand_new_metasenv meta term subst_in 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: Attenzione! Ora questa funzione applica anche [subst_in] a *)
  42 (*CSC: [newmetasenv].                                             *)
  43 let subst_meta_and_metasenv_in_current_proof meta subst_in newmetasenv =
  44  let (uri,bo,ty) =
  45   match !proof with
  46      None -> assert false
  47    | Some (uri,_,bo,ty) -> uri,bo,ty
  48  in
  49   let bo' = subst_in bo in
  50   let metasenv' =
  51    List.fold_right
  52     (fun metasenv_entry i ->
  53       match metasenv_entry with
  54          (m,canonical_context,ty) when m <> meta ->
  55            let canonical_context' =
  56             List.map
  57              (function
  58                  None -> None
  59                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
  60                | Some (i,Cic.Def t)  -> Some (i,Cic.Def (subst_in t))
  61              ) canonical_context
  62            in
  63             (m,canonical_context',subst_in ty)::i
  64        | _ -> i
  65     ) newmetasenv []
  66   in
  67    proof := Some (uri,metasenv',bo',ty) ;
  68    metasenv'
  69 ;;
  70
  71 let subst_meta_in_current_proof meta term newmetasenv =
  72  let (uri,metasenv,bo,ty) =
  73   match !proof with
  74      None -> assert false
  75    | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
  76  in
  77   let subst_in = CicUnification.apply_subst [meta,term] in
  78    let metasenv' =
  79     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
  80    in
  81     let metasenv'' =
  82      List.map
  83       (function i,canonical_context,ty ->
  84         let canonical_context' =
  85          List.map
  86           (function
  87               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
  88             | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
  89             | None -> None
  90           ) canonical_context
  91         in
  92          i,canonical_context',(subst_in ty)
  93       ) metasenv'
  94     in
  95      let bo' = subst_in bo in
  96       proof := Some (uri,metasenv'',bo',ty) ;
  97       metasenv''
  98 ;;
  99
 100 (* Returns the first meta whose number is above the *)
 101 (* number of the higher meta.                       *)
 102 let new_meta () =
 103  let metasenv =
 104   match !proof with
 105      None -> assert false
 106    | Some (_,metasenv,_,_) -> metasenv
 107  in
 108   let rec aux =
 109    function
 110       None,[] -> 1
 111     | Some n,[] -> n
 112     | None,(n,_,_)::tl -> aux (Some n,tl)
 113     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
 114   in
 115    1 + aux (None,metasenv)
 116 ;;
 117
 118 (* metas_in_term term                                                *)
 119 (* Returns the ordered list of the metas that occur in [term].       *)
 120 (* Duplicates are removed. The implementation is not very efficient. *)
 121 let metas_in_term term =
 122  let module C = Cic in
 123   let rec aux =
 124    function
 125       C.Rel _
 126     | C.Var _ -> []
 127     | C.Meta (n,_) -> [n]
 128     | C.Sort _
 129     | C.Implicit -> []
 130     | C.Cast (te,ty) -> (aux te) @ (aux ty)
 131     | C.Prod (_,s,t) -> (aux s) @ (aux t)
 132     | C.Lambda (_,s,t) -> (aux s) @ (aux t)
 133     | C.LetIn (_,s,t) -> (aux s) @ (aux t)
 134     | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
 135     | C.Const _
 136     | C.Abst _
 137     | C.MutInd _
 138     | C.MutConstruct _ -> []
 139     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 140        (aux outt) @ (aux t) @
 141         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
 142     | C.Fix (i,fl) ->
 143         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 144     | C.CoFix (i,fl) ->
 145         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 146   in
 147    let metas = aux term in
 148     let rec elim_duplicates =
 149      function
 150         [] -> []
 151       | he::tl ->
 152          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
 153     in
 154      elim_duplicates metas
 155 ;;
 156
 157 (* identity_relocation_list_for_metavariable i canonical_context         *)
 158 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 159 (* where n = List.length [canonical_context]                             *)
 160 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
 161 let identity_relocation_list_for_metavariable canonical_context =
 162  let canonical_context_length = List.length canonical_context in
 163   let rec aux =
 164    function
 165       (_,[]) -> []
 166     | (n,None::tl) -> None::(aux ((n+1),tl))
 167     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
 168   in
 169    aux (1,canonical_context)
 170 ;;
 171
 172 (* perforate context term ty                                                 *)
 173 (* replaces the term [term] in the proof with a new metavariable whose type  *)
 174 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
 175 (* could be easily computed; so the only reasons to have it as an argument   *)
 176 (* are efficiency reasons.                                                   *)
 177 let perforate context term ty =
 178  let module C = Cic in
 179   let newmeta = new_meta () in
 180    match !proof with
 181       None -> assert false
 182     | Some (uri,metasenv,bo,gty) ->
 183        (* We push the new meta at the end of the list for pretty-printing *)
 184        (* purposes: in this way metas are ordered.                        *)
 185        let metasenv' = metasenv@[newmeta,context,ty] in
 186         let irl = identity_relocation_list_for_metavariable context in
 187 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
 188         let bo' =
 189          ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
 190         in
 191         (* It may be possible that some metavariables occurred only in *)
 192         (* the term we are perforating and they now occurs no more. We *)
 193         (* get rid of them, collecting the really useful metavariables *)
 194         (* in metasenv''.                                              *)
 195 (*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
 196 (*CSC: di una metavariabile che compare in bo'!!!!!!!                     *)
 197          let newmetas = metas_in_term bo' in
 198           let metasenv'' =
 199            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
 200           in
 201            proof := Some (uri,metasenv'',bo',gty) ;
 202            goal := Some newmeta
 203 ;;
 204
 205 (************************************************************)
 206 (*                  Some easy tactics.                      *)
 207 (************************************************************)
 208
 209 exception Fail of string;;
 210
 211 (*CSC: generatore di nomi? Chiedere il nome? *)
 212 let fresh_name =
 213  let next_fresh_index = ref 0
 214 in
 215  function () ->
 216   incr next_fresh_index ;
 217   "fresh_name" ^ string_of_int !next_fresh_index
 218 ;;
 219
 220 (* lambda_abstract newmeta ty *)
 221 (* returns a triple [bo],[context],[ty'] where              *)
 222 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
 223 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
 224 (* So, lambda_abstract is the core of the implementation of *)
 225 (* the Intros tactic.                                       *)
 226 let lambda_abstract context newmeta ty =
 227  let module C = Cic in
 228   let rec collect_context context =
 229    function
 230       C.Cast (te,_)   -> collect_context context te
 231     | C.Prod (n,s,t)  ->
 232        let n' =
 233         match n with
 234            C.Name _ -> n
 235 (*CSC: generatore di nomi? Chiedere il nome? *)
 236          | C.Anonimous -> C.Name (fresh_name ())
 237        in
 238         let (context',ty,bo) =
 239          collect_context ((Some (n',(C.Decl s)))::context) t
 240         in
 241          (context',ty,C.Lambda(n',s,bo))
 242     | C.LetIn (n,s,t) ->
 243        let (context',ty,bo) =
 244         collect_context ((Some (n,(C.Def s)))::context) t
 245        in
 246         (context',ty,C.LetIn(n,s,bo))
 247     | _ as t ->
 248       let irl = identity_relocation_list_for_metavariable context in
 249        context, t, (C.Meta (newmeta,irl))
 250   in
 251    collect_context context ty
 252 ;;
 253
 254 let intros () =
 255  let module C = Cic in
 256  let module R = CicReduction in
 257   let metasenv =
 258    match !proof with
 259       None -> assert false
 260     | Some (_,metasenv,_,_) -> metasenv
 261   in
 262   let metano,context,ty =
 263    match !goal with
 264       None -> assert false
 265     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 266   in
 267    let newmeta = new_meta () in
 268     let (context',ty',bo') = lambda_abstract context newmeta ty in
 269      let _ = subst_meta_in_current_proof metano bo' [newmeta,context',ty'] in
 270       goal := Some newmeta
 271 ;;
 272
 273 (* The term bo must be closed in the current context *)
 274 let exact bo =
 275  let module T = CicTypeChecker in
 276  let module R = CicReduction in
 277   let metasenv =
 278    match !proof with
 279       None -> assert false
 280     | Some (_,metasenv,_,_) -> metasenv
 281   in
 282   let metano,context,ty =
 283    match !goal with
 284       None -> assert false
 285     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 286   in
 287    if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then
 288     begin
 289      let metasenv' = subst_meta_in_current_proof metano bo [] in
 290       goal :=
 291        match metasenv' with
 292           [] -> None
 293         | (n,_,_)::_ -> Some n
 294     end
 295    else
 296     raise (Fail "The type of the provided term is not the one expected.")
 297 ;;
 298
 299 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
 300 (*CSC: Elim tactic. Do we already need tacticals?                       *)
 301 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 302 (* head, a META environment in which there is new a META for each hypothesis,*)
 303 (* a list of arguments for the new applications and the indexes of the first *)
 304 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 305 (* is the nth new META lambda-abstracted as much as possible. Hence, this    *)
 306 (* functions already provides the behaviour of Intros on the new goals.      *)
 307 let new_metasenv_for_apply_intros context ty =
 308  let module C = Cic in
 309  let module S = CicSubstitution in
 310   let rec aux newmeta =
 311    function
 312       C.Cast (he,_) -> aux newmeta he
 313     | C.Prod (name,s,t) ->
 314        let newcontext,ty',newargument = lambda_abstract context newmeta s in
 315         let (res,newmetasenv,arguments,lastmeta) =
 316          aux (newmeta + 1) (S.subst newargument t)
 317         in
 318          res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta
 319     | t -> t,[],[],newmeta
 320   in
 321    let newmeta = new_meta () in
 322     (* WARNING: here we are using the invariant that above the most *)
 323     (* recente new_meta() there are no used metas.                  *)
 324     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 325      res,newmetasenv,arguments,newmeta,lastmeta
 326 ;;
 327
 328 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 329 (* head, a META environment in which there is new a META for each hypothesis,*)
 330 (* a list of arguments for the new applications and the indexes of the first *)
 331 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 332 (* is just the nth new META.                                                 *)
 333 let new_metasenv_for_apply context ty =
 334  let module C = Cic in
 335  let module S = CicSubstitution in
 336   let rec aux newmeta =
 337    function
 338       C.Cast (he,_) -> aux newmeta he
 339     | C.Prod (name,s,t) ->
 340        let irl = identity_relocation_list_for_metavariable context in
 341         let newargument = C.Meta (newmeta,irl) in
 342          let (res,newmetasenv,arguments,lastmeta) =
 343           aux (newmeta + 1) (S.subst newargument t)
 344          in
 345           res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
 346     | t -> t,[],[],newmeta
 347   in
 348    let newmeta = new_meta () in
 349     (* WARNING: here we are using the invariant that above the most *)
 350     (* recente new_meta() there are no used metas.                  *)
 351     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 352      res,newmetasenv,arguments,newmeta,lastmeta
 353 ;;
 354
 355
 356 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 357 let classify_metas newmeta in_subst_domain subst_in metasenv =
 358  List.fold_right
 359   (fun (i,canonical_context,ty) (old_uninst,new_uninst) ->
 360     if in_subst_domain i then
 361      old_uninst,new_uninst
 362     else
 363      let ty' = subst_in canonical_context ty in
 364       let canonical_context' =
 365        List.fold_right
 366         (fun entry canonical_context' ->
 367           let entry' =
 368            match entry with
 369               Some (n,Cic.Decl s) ->
 370                Some (n,Cic.Decl (subst_in canonical_context' s))
 371             | Some (n,Cic.Def s) ->
 372                Some (n,Cic.Def (subst_in canonical_context' s))
 373             | None -> None
 374           in
 375            entry'::canonical_context'
 376         ) canonical_context []
 377      in
 378       if i < newmeta then
 379        ((i,canonical_context',ty')::old_uninst),new_uninst
 380       else
 381        old_uninst,((i,canonical_context',ty')::new_uninst)
 382   ) metasenv ([],[])
 383 ;;
 384
 385 (* The term bo must be closed in the current context *)
 386 let apply term =
 387  let module T = CicTypeChecker in
 388  let module R = CicReduction in
 389  let module C = Cic in
 390   let metasenv =
 391    match !proof with
 392       None -> assert false
 393     | Some (_,metasenv,_,_) -> metasenv
 394   in
 395   let metano,context,ty =
 396    match !goal with
 397       None -> assert false
 398     | Some metano ->
 399        List.find (function (m,_,_) -> m=metano) metasenv
 400   in
 401    let termty = CicTypeChecker.type_of_aux' metasenv context term in
 402     (* newmeta is the lowest index of the new metas introduced *)
 403     let (consthead,newmetas,arguments,newmeta,_) =
 404      new_metasenv_for_apply context termty
 405     in
 406      let newmetasenv = newmetas@metasenv in
 407       let subst,newmetasenv' =
 408        CicUnification.fo_unif newmetasenv context consthead ty
 409       in
 410        let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
 411        let apply_subst = CicUnification.apply_subst subst in
 412         let old_uninstantiatedmetas,new_uninstantiatedmetas =
 413          (* subst_in doesn't need the context. Hence the underscore. *)
 414          let subst_in _ = CicUnification.apply_subst subst in
 415           classify_metas newmeta in_subst_domain subst_in newmetasenv'
 416         in
 417          let bo' =
 418           if List.length newmetas = 0 then
 419            term
 420           else
 421            let arguments' = List.map apply_subst arguments in
 422             Cic.Appl (term::arguments')
 423          in
 424           let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
 425           let newmetasenv''' =
 426            let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in
 427             subst_meta_and_metasenv_in_current_proof metano subst_in
 428              newmetasenv''
 429           in
 430            match newmetasenv''' with
 431               [] -> goal := None
 432             | (i,_,_)::_ -> goal := Some i
 433 ;;
 434
 435 let eta_expand metasenv context t arg =
 436  let module T = CicTypeChecker in
 437  let module S = CicSubstitution in
 438  let module C = Cic in
 439   let rec aux n =
 440    function
 441       t' when t' = S.lift n arg -> C.Rel (1 + n)
 442     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
 443     | C.Var _
 444     | C.Meta _
 445     | C.Sort _
 446     | C.Implicit as t -> t
 447     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
 448     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
 449     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
 450     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
 451     | C.Appl l -> C.Appl (List.map (aux n) l)
 452     | C.Const _ as t -> t
 453     | C.Abst _ -> assert false
 454     | C.MutInd _
 455     | C.MutConstruct _ as t -> t
 456     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 457        C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
 458         List.map (aux n) pl)
 459     | C.Fix (i,fl) ->
 460        let tylen = List.length fl in
 461         let substitutedfl =
 462          List.map
 463           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 464            fl
 465         in
 466          C.Fix (i, substitutedfl)
 467     | C.CoFix (i,fl) ->
 468        let tylen = List.length fl in
 469         let substitutedfl =
 470          List.map
 471           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 472            fl
 473         in
 474          C.CoFix (i, substitutedfl)
 475   in
 476    let argty =
 477     T.type_of_aux' metasenv context arg
 478    in
 479     (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
 480 ;;
 481
 482 exception NotAnInductiveTypeToEliminate;;
 483 exception NotTheRightEliminatorShape;;
 484 exception NoHypothesesFound;;
 485
 486 let elim_intros_simpl term =
 487  let module T = CicTypeChecker in
 488  let module U = UriManager in
 489  let module R = CicReduction in
 490  let module C = Cic in
 491   let curi,metasenv =
 492    match !proof with
 493       None -> assert false
 494     | Some (curi,metasenv,_,_) -> curi,metasenv
 495   in
 496   let metano,context,ty =
 497    match !goal with
 498       None -> assert false
 499     | Some metano ->
 500        List.find (function (m,_,_) -> m=metano) metasenv
 501   in
 502    let termty = T.type_of_aux' metasenv context term in
 503    let uri,cookingno,typeno,args =
 504     match termty with
 505        C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
 506      | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
 507          (uri,cookingno,typeno,args)
 508      | _ -> raise NotAnInductiveTypeToEliminate
 509    in
 510     let eliminator_uri =
 511      let buri = U.buri_of_uri uri in
 512      let name =
 513       match CicEnvironment.get_cooked_obj uri cookingno with
 514          C.InductiveDefinition (tys,_,_) ->
 515           let (name,_,_,_) = List.nth tys typeno in
 516            name
 517        | _ -> assert false
 518      in
 519      let ext =
 520       match T.type_of_aux' metasenv context ty with
 521          C.Sort C.Prop -> "_ind"
 522        | C.Sort C.Set  -> "_rec"
 523        | C.Sort C.Type -> "_rect"
 524        | _ -> assert false
 525      in
 526       U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
 527     in
 528      let eliminator_cookingno =
 529       UriManager.relative_depth curi eliminator_uri 0
 530      in
 531      let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
 532       let ety =
 533        T.type_of_aux' [] [] eliminator_ref
 534       in
 535        let (econclusion,newmetas,arguments,newmeta,lastmeta) =
 536 (*
 537         new_metasenv_for_apply context ety
 538 *)
 539         new_metasenv_for_apply_intros context ety
 540        in
 541         (* Here we assume that we have only one inductive hypothesis to *)
 542         (* eliminate and that it is the last hypothesis of the theorem. *)
 543         (* A better approach would be fingering the hypotheses in some  *)
 544         (* way.                                                         *)
 545         let meta_of_corpse =
 546          let (_,canonical_context,_) =
 547           List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas
 548          in
 549           let irl =
 550            identity_relocation_list_for_metavariable canonical_context
 551           in
 552            Cic.Meta (lastmeta - 1, irl)
 553         in
 554         let newmetasenv = newmetas @ metasenv in
 555         let subst1,newmetasenv' =
 556          CicUnification.fo_unif newmetasenv context term meta_of_corpse
 557         in
 558          let ueconclusion = CicUnification.apply_subst subst1 econclusion in
 559           (* The conclusion of our elimination principle is *)
 560           (*  (?i farg1 ... fargn)                         *)
 561           (* The conclusion of our goal is ty. So, we can   *)
 562           (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
 563           (* a new ty equal to (P farg1 ... fargn). Now     *)
 564           (* ?i can be instantiated with P and we are ready *)
 565           (* to refine the term.                            *)
 566           let emeta, fargs =
 567            match ueconclusion with
 568 (*CSC: Code to be used for Apply
 569               C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
 570             | C.Meta (emeta,_) -> emeta,[]
 571 *)
 572 (*CSC: Code to be used for ApplyIntros *)
 573               C.Appl (he::fargs) ->
 574                let rec find_head =
 575                 function
 576                    C.Meta (emeta,_) -> emeta
 577                  | C.Lambda (_,_,t) -> find_head t
 578                  | C.LetIn (_,_,t) -> find_head t
 579                  | _ ->raise NotTheRightEliminatorShape
 580                in
 581                 find_head he,fargs
 582 (* *)
 583             | _ -> raise NotTheRightEliminatorShape
 584           in
 585            let ty' = CicUnification.apply_subst subst1 ty in
 586            let eta_expanded_ty =
 587 (*CSC: newmetasenv' era metasenv ??????????? *)
 588             List.fold_left (eta_expand newmetasenv' context) ty' fargs
 589            in
 590             let subst2,newmetasenv'' =
 591 (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
 592 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
 593              CicUnification.fo_unif
 594               newmetasenv' context ueconclusion eta_expanded_ty
 595             in
 596              let in_subst_domain i =
 597               let eq_to_i = function (j,_) -> i=j in
 598                List.exists eq_to_i subst1 ||
 599                List.exists eq_to_i subst2
 600              in
 601 (*CSC: codice per l'elim
 602               (* When unwinding the META that corresponds to the elimination *)
 603               (* predicate (which is emeta), we must also perform one-step   *)
 604               (* beta-reduction. apply_subst doesn't need the context. Hence *)
 605               (* the underscore.                                             *)
 606               let apply_subst _ t =
 607                let t' = CicUnification.apply_subst subst1 t in
 608                 CicUnification.apply_subst_reducing
 609                  subst2 (Some (emeta,List.length fargs)) t'
 610               in
 611 *)
 612 (*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *)
 613               let apply_subst context t =
 614                let t' = CicUnification.apply_subst (subst1@subst2) t in
 615                 ProofEngineReduction.simpl context t'
 616               in
 617 (* *)
 618                 let old_uninstantiatedmetas,new_uninstantiatedmetas =
 619                  classify_metas newmeta in_subst_domain apply_subst
 620                   newmetasenv''
 621                 in
 622                  let arguments' = List.map (apply_subst context) arguments in
 623                   let bo' = Cic.Appl (eliminator_ref::arguments') in
 624                    let newmetasenv''' =
 625                     new_uninstantiatedmetas@old_uninstantiatedmetas
 626                    in
 627                     let newmetasenv'''' =
 628                      (* When unwinding the META that corresponds to the *)
 629                      (* elimination predicate (which is emeta), we must *)
 630                      (* also perform one-step beta-reduction.           *)
 631                      (* The only difference w.r.t. apply_subst is that  *)
 632                      (* we also substitute metano with bo'.             *)
 633                      (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
 634                      (*CSC: no?                                              *)
 635 (*CSC: codice per l'elim
 636                      let apply_subst' t =
 637                       let t' = CicUnification.apply_subst subst1 t in
 638                        CicUnification.apply_subst_reducing
 639                         ((metano,bo')::subst2)
 640                         (Some (emeta,List.length fargs)) t'
 641                      in
 642 *)
 643 (*CSC: codice per l'elim_intros_simpl *)
 644                      let apply_subst' t =
 645                       CicUnification.apply_subst
 646                        ((metano,bo')::(subst1@subst2)) t
 647                      in
 648 (* *)
 649                       subst_meta_and_metasenv_in_current_proof metano
 650                        apply_subst' newmetasenv'''
 651                     in
 652                      match newmetasenv'''' with
 653                         [] -> goal := None
 654                       | (i,_,_)::_ -> goal := Some i
 655 ;;
 656
 657 let reduction_tactic reduction_function term =
 658  let curi,metasenv,pbo,pty =
 659   match !proof with
 660      None -> assert false
 661    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 662  in
 663  let metano,context,ty =
 664   match !goal with
 665      None -> assert false
 666    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 667  in
 668   let term' = reduction_function context term in
 669    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 670    (* the type of one metavariable. So we replace it everywhere.   *)
 671    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 672    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 673    let replace =
 674     ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
 675    in
 676     let ty' = replace ty in
 677     let context' =
 678      List.map
 679       (function
 680           Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
 681         | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
 682         | None -> None
 683       ) context
 684     in
 685      let metasenv' =
 686       List.map
 687        (function
 688            (n,_,_) when n = metano -> (metano,context',ty')
 689          | _ as t -> t
 690        ) metasenv
 691      in
 692       proof := Some (curi,metasenv',pbo,pty) ;
 693       goal := Some metano
 694 ;;
 695
 696 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 697 let reduction_tactic_in_scratch reduction_function term ty =
 698  let metasenv =
 699   match !proof with
 700      None -> []
 701    | Some (_,metasenv,_,_) -> metasenv
 702  in
 703  let metano,context,_ =
 704   match !goal with
 705      None -> assert false
 706    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 707  in
 708   let term' = reduction_function context term in
 709    ProofEngineReduction.replace
 710     ~equality:(==) ~what:term ~with_what:term' ~where:ty
 711 ;;
 712
 713 let whd    = reduction_tactic CicReduction.whd;;
 714 let reduce = reduction_tactic ProofEngineReduction.reduce;;
 715 let simpl  = reduction_tactic ProofEngineReduction.simpl;;
 716
 717 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd;;
 718 let reduce_in_scratch =
 719  reduction_tactic_in_scratch ProofEngineReduction.reduce;;
 720 let simpl_in_scratch  =
 721  reduction_tactic_in_scratch ProofEngineReduction.simpl;;
 722
 723 (* It is just the opposite of whd. The code should probably be merged. *)
 724 let fold term =
 725  let curi,metasenv,pbo,pty =
 726   match !proof with
 727      None -> assert false
 728    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 729  in
 730  let metano,context,ty =
 731   match !goal with
 732      None -> assert false
 733    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 734  in
 735   let term' = CicReduction.whd context term in
 736    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 737    (* the type of one metavariable. So we replace it everywhere.   *)
 738    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 739    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 740    let replace = ProofEngineReduction.replace
 741     ~equality:(==) ~what:term' ~with_what:term
 742    in
 743     let ty' = replace ty in
 744     let context' =
 745      List.map
 746       (function
 747           Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
 748         | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
 749         | None -> None
 750       ) context
 751     in
 752      let metasenv' =
 753       List.map
 754        (function
 755            (n,_,_) when n = metano -> (metano,context',ty')
 756          | _ as t -> t
 757        ) metasenv
 758      in
 759       proof := Some (curi,metasenv',pbo,pty) ;
 760       goal := Some metano
 761 ;;
 762
 763 let cut term =
 764  let module C = Cic in
 765   let curi,metasenv,pbo,pty =
 766    match !proof with
 767       None -> assert false
 768     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 769   in
 770   let metano,context,ty =
 771    match !goal with
 772       None -> assert false
 773     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 774   in
 775    let newmeta1 = new_meta () in
 776    let newmeta2 = newmeta1 + 1 in
 777    let context_for_newmeta1 =
 778     (Some (C.Name "dummy_for_cut",C.Decl term))::context in
 779    let irl1 =
 780     identity_relocation_list_for_metavariable context_for_newmeta1 in
 781    let irl2 = identity_relocation_list_for_metavariable context in
 782     let newmeta1ty = CicSubstitution.lift 1 ty in
 783     let bo' =
 784      C.Appl
 785       [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ;
 786        C.Meta (newmeta2,irl2)]
 787     in
 788      let _ =
 789       subst_meta_in_current_proof metano bo'
 790        [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
 791      in
 792       goal := Some newmeta1
 793 ;;
 794
 795 let letin term =
 796  let module C = Cic in
 797   let curi,metasenv,pbo,pty =
 798    match !proof with
 799       None -> assert false
 800     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 801   in
 802   let metano,context,ty =
 803    match !goal with
 804       None -> assert false
 805     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 806   in
 807    let _ = CicTypeChecker.type_of_aux' metasenv context term in
 808     let newmeta = new_meta () in
 809     let context_for_newmeta =
 810      (Some (C.Name "dummy_for_letin",C.Def term))::context in
 811     let irl =
 812      identity_relocation_list_for_metavariable context_for_newmeta in
 813      let newmetaty = CicSubstitution.lift 1 ty in
 814      let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in
 815       let _ = subst_meta_in_current_proof metano bo' [newmeta,context_for_newmeta,newmetaty] in
 816        goal := Some newmeta
 817 ;;
 818
 819 exception NotConvertible;;
 820
 821 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
 822 (*CSC: while [goal_input] can have a richer context (because of binders) *)
 823 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
 824 (*CSC: Is that evident? Is that right? Or should it be changed?          *)
 825 let change ~goal_input ~input =
 826  let curi,metasenv,pbo,pty =
 827   match !proof with
 828      None -> assert false
 829    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 830  in
 831  let metano,context,ty =
 832   match !goal with
 833      None -> assert false
 834    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 835  in
 836   (* are_convertible works only on well-typed terms *)
 837   ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
 838   if CicReduction.are_convertible context goal_input input then
 839    begin
 840     let replace =
 841      ProofEngineReduction.replace
 842       ~equality:(==) ~what:goal_input ~with_what:input
 843     in
 844     let ty' = replace ty in
 845     let context' =
 846      List.map
 847       (function
 848           Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
 849         | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
 850         | None -> None
 851       ) context
 852     in
 853      let metasenv' =
 854       List.map
 855        (function
 856            (n,_,_) when n = metano -> (metano,context',ty')
 857          | _ as t -> t
 858        ) metasenv
 859      in
 860       proof := Some (curi,metasenv',pbo,pty) ;
 861       goal := Some metano
 862    end
 863   else
 864    raise NotConvertible
 865 ;;