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.MutInd _
 137     | C.MutConstruct _ -> []
 138     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 139        (aux outt) @ (aux t) @
 140         (List.fold_left (fun i t -> i @ (aux t)) [] pl)
 141     | C.Fix (i,fl) ->
 142         List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 143     | C.CoFix (i,fl) ->
 144         List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
 145   in
 146    let metas = aux term in
 147     let rec elim_duplicates =
 148      function
 149         [] -> []
 150       | he::tl ->
 151          he::(elim_duplicates (List.filter (function el -> he <> el) tl))
 152     in
 153      elim_duplicates metas
 154 ;;
 155
 156 (* identity_relocation_list_for_metavariable i canonical_context         *)
 157 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 158 (* where n = List.length [canonical_context]                             *)
 159 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
 160 let identity_relocation_list_for_metavariable canonical_context =
 161  let canonical_context_length = List.length canonical_context in
 162   let rec aux =
 163    function
 164       (_,[]) -> []
 165     | (n,None::tl) -> None::(aux ((n+1),tl))
 166     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
 167   in
 168    aux (1,canonical_context)
 169 ;;
 170
 171 (* perforate context term ty                                                 *)
 172 (* replaces the term [term] in the proof with a new metavariable whose type  *)
 173 (* is [ty]. [context] must be the context of [term] in the whole proof. This *)
 174 (* could be easily computed; so the only reasons to have it as an argument   *)
 175 (* are efficiency reasons.                                                   *)
 176 let perforate context term ty =
 177  let module C = Cic in
 178   let newmeta = new_meta () in
 179    match !proof with
 180       None -> assert false
 181     | Some (uri,metasenv,bo,gty) ->
 182        (* We push the new meta at the end of the list for pretty-printing *)
 183        (* purposes: in this way metas are ordered.                        *)
 184        let metasenv' = metasenv@[newmeta,context,ty] in
 185         let irl = identity_relocation_list_for_metavariable context in
 186 (*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
 187         let bo' =
 188          ProofEngineReduction.replace (==) term (C.Meta (newmeta,irl)) bo
 189         in
 190         (* It may be possible that some metavariables occurred only in *)
 191         (* the term we are perforating and they now occurs no more. We *)
 192         (* get rid of them, collecting the really useful metavariables *)
 193         (* in metasenv''.                                              *)
 194 (*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *)
 195 (*CSC: di una metavariabile che compare in bo'!!!!!!!                     *)
 196          let newmetas = metas_in_term bo' in
 197           let metasenv'' =
 198            List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
 199           in
 200            proof := Some (uri,metasenv'',bo',gty) ;
 201            goal := Some newmeta
 202 ;;
 203
 204 (************************************************************)
 205 (*                  Some easy tactics.                      *)
 206 (************************************************************)
 207
 208 exception Fail of string;;
 209
 210 (*CSC: generatore di nomi? Chiedere il nome? *)
 211 let fresh_name =
 212  let next_fresh_index = ref 0
 213 in
 214  function () ->
 215   incr next_fresh_index ;
 216   "fresh_name" ^ string_of_int !next_fresh_index
 217 ;;
 218
 219 (* lambda_abstract newmeta ty *)
 220 (* returns a triple [bo],[context],[ty'] where              *)
 221 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
 222 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
 223 (* So, lambda_abstract is the core of the implementation of *)
 224 (* the Intros tactic.                                       *)
 225 let lambda_abstract context newmeta ty =
 226  let module C = Cic in
 227   let rec collect_context context =
 228    function
 229       C.Cast (te,_)   -> collect_context context te
 230     | C.Prod (n,s,t)  ->
 231        let n' =
 232         match n with
 233            C.Name _ -> n
 234 (*CSC: generatore di nomi? Chiedere il nome? *)
 235          | C.Anonimous -> C.Name (fresh_name ())
 236        in
 237         let (context',ty,bo) =
 238          collect_context ((Some (n',(C.Decl s)))::context) t
 239         in
 240          (context',ty,C.Lambda(n',s,bo))
 241     | C.LetIn (n,s,t) ->
 242        let (context',ty,bo) =
 243         collect_context ((Some (n,(C.Def s)))::context) t
 244        in
 245         (context',ty,C.LetIn(n,s,bo))
 246     | _ as t ->
 247       let irl = identity_relocation_list_for_metavariable context in
 248        context, t, (C.Meta (newmeta,irl))
 249   in
 250    collect_context context ty
 251 ;;
 252
 253 let intros () =
 254  let module C = Cic in
 255  let module R = CicReduction in
 256   let metasenv =
 257    match !proof with
 258       None -> assert false
 259     | Some (_,metasenv,_,_) -> metasenv
 260   in
 261   let metano,context,ty =
 262    match !goal with
 263       None -> assert false
 264     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 265   in
 266    let newmeta = new_meta () in
 267     let (context',ty',bo') = lambda_abstract context newmeta ty in
 268      let _ = subst_meta_in_current_proof metano bo' [newmeta,context',ty'] in
 269       goal := Some newmeta
 270 ;;
 271
 272 (* The term bo must be closed in the current context *)
 273 let exact bo =
 274  let module T = CicTypeChecker in
 275  let module R = CicReduction in
 276   let metasenv =
 277    match !proof with
 278       None -> assert false
 279     | Some (_,metasenv,_,_) -> metasenv
 280   in
 281   let metano,context,ty =
 282    match !goal with
 283       None -> assert false
 284     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 285   in
 286    if R.are_convertible context (T.type_of_aux' metasenv context bo) ty then
 287     begin
 288      let metasenv' = subst_meta_in_current_proof metano bo [] in
 289       goal :=
 290        match metasenv' with
 291           [] -> None
 292         | (n,_,_)::_ -> Some n
 293     end
 294    else
 295     raise (Fail "The type of the provided term is not the one expected.")
 296 ;;
 297
 298 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
 299 (*CSC: Elim tactic. Do we already need tacticals?                       *)
 300 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 301 (* head, a META environment in which there is new a META for each hypothesis,*)
 302 (* a list of arguments for the new applications and the indexes of the first *)
 303 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 304 (* is the nth new META lambda-abstracted as much as possible. Hence, this    *)
 305 (* functions already provides the behaviour of Intros on the new goals.      *)
 306 let new_metasenv_for_apply_intros context ty =
 307  let module C = Cic in
 308  let module S = CicSubstitution in
 309   let rec aux newmeta =
 310    function
 311       C.Cast (he,_) -> aux newmeta he
 312     | C.Prod (name,s,t) ->
 313        let newcontext,ty',newargument = lambda_abstract context newmeta s in
 314         let (res,newmetasenv,arguments,lastmeta) =
 315          aux (newmeta + 1) (S.subst newargument t)
 316         in
 317          res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta
 318     | t -> t,[],[],newmeta
 319   in
 320    let newmeta = new_meta () in
 321     (* WARNING: here we are using the invariant that above the most *)
 322     (* recente new_meta() there are no used metas.                  *)
 323     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 324      res,newmetasenv,arguments,newmeta,lastmeta
 325 ;;
 326
 327 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 328 (* head, a META environment in which there is new a META for each hypothesis,*)
 329 (* a list of arguments for the new applications and the indexes of the first *)
 330 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 331 (* is just the nth new META.                                                 *)
 332 let new_metasenv_for_apply context ty =
 333  let module C = Cic in
 334  let module S = CicSubstitution in
 335   let rec aux newmeta =
 336    function
 337       C.Cast (he,_) -> aux newmeta he
 338     | C.Prod (name,s,t) ->
 339        let irl = identity_relocation_list_for_metavariable context in
 340         let newargument = C.Meta (newmeta,irl) in
 341          let (res,newmetasenv,arguments,lastmeta) =
 342           aux (newmeta + 1) (S.subst newargument t)
 343          in
 344           res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
 345     | t -> t,[],[],newmeta
 346   in
 347    let newmeta = new_meta () in
 348     (* WARNING: here we are using the invariant that above the most *)
 349     (* recente new_meta() there are no used metas.                  *)
 350     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 351      res,newmetasenv,arguments,newmeta,lastmeta
 352 ;;
 353
 354
 355 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 356 let classify_metas newmeta in_subst_domain subst_in metasenv =
 357  List.fold_right
 358   (fun (i,canonical_context,ty) (old_uninst,new_uninst) ->
 359     if in_subst_domain i then
 360      old_uninst,new_uninst
 361     else
 362      let ty' = subst_in canonical_context ty in
 363       let canonical_context' =
 364        List.fold_right
 365         (fun entry canonical_context' ->
 366           let entry' =
 367            match entry with
 368               Some (n,Cic.Decl s) ->
 369                Some (n,Cic.Decl (subst_in canonical_context' s))
 370             | Some (n,Cic.Def s) ->
 371                Some (n,Cic.Def (subst_in canonical_context' s))
 372             | None -> None
 373           in
 374            entry'::canonical_context'
 375         ) canonical_context []
 376      in
 377       if i < newmeta then
 378        ((i,canonical_context',ty')::old_uninst),new_uninst
 379       else
 380        old_uninst,((i,canonical_context',ty')::new_uninst)
 381   ) metasenv ([],[])
 382 ;;
 383
 384 (* The term bo must be closed in the current context *)
 385 let apply term =
 386  let module T = CicTypeChecker in
 387  let module R = CicReduction in
 388  let module C = Cic in
 389   let metasenv =
 390    match !proof with
 391       None -> assert false
 392     | Some (_,metasenv,_,_) -> metasenv
 393   in
 394   let metano,context,ty =
 395    match !goal with
 396       None -> assert false
 397     | Some metano ->
 398        List.find (function (m,_,_) -> m=metano) metasenv
 399   in
 400    let termty = CicTypeChecker.type_of_aux' metasenv context term in
 401     (* newmeta is the lowest index of the new metas introduced *)
 402     let (consthead,newmetas,arguments,newmeta,_) =
 403      new_metasenv_for_apply context termty
 404     in
 405      let newmetasenv = newmetas@metasenv in
 406       let subst,newmetasenv' =
 407        CicUnification.fo_unif newmetasenv context consthead ty
 408       in
 409        let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
 410        let apply_subst = CicUnification.apply_subst subst in
 411         let old_uninstantiatedmetas,new_uninstantiatedmetas =
 412          (* subst_in doesn't need the context. Hence the underscore. *)
 413          let subst_in _ = CicUnification.apply_subst subst in
 414           classify_metas newmeta in_subst_domain subst_in newmetasenv'
 415         in
 416          let bo' =
 417           if List.length newmetas = 0 then
 418            term
 419           else
 420            let arguments' = List.map apply_subst arguments in
 421             Cic.Appl (term::arguments')
 422          in
 423           let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
 424           let newmetasenv''' =
 425            let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in
 426             subst_meta_and_metasenv_in_current_proof metano subst_in
 427              newmetasenv''
 428           in
 429            match newmetasenv''' with
 430               [] -> goal := None
 431             | (i,_,_)::_ -> goal := Some i
 432 ;;
 433
 434 let eta_expand metasenv context t arg =
 435  let module T = CicTypeChecker in
 436  let module S = CicSubstitution in
 437  let module C = Cic in
 438   let rec aux n =
 439    function
 440       t' when t' = S.lift n arg -> C.Rel (1 + n)
 441     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
 442     | C.Var _
 443     | C.Meta _
 444     | C.Sort _
 445     | C.Implicit as t -> t
 446     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
 447     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
 448     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
 449     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
 450     | C.Appl l -> C.Appl (List.map (aux n) l)
 451     | C.Const _ as t -> t
 452     | C.MutInd _
 453     | C.MutConstruct _ as t -> t
 454     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
 455        C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
 456         List.map (aux n) pl)
 457     | C.Fix (i,fl) ->
 458        let tylen = List.length fl in
 459         let substitutedfl =
 460          List.map
 461           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 462            fl
 463         in
 464          C.Fix (i, substitutedfl)
 465     | C.CoFix (i,fl) ->
 466        let tylen = List.length fl in
 467         let substitutedfl =
 468          List.map
 469           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 470            fl
 471         in
 472          C.CoFix (i, substitutedfl)
 473   in
 474    let argty =
 475     T.type_of_aux' metasenv context arg
 476    in
 477     (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
 478 ;;
 479
 480 exception NotAnInductiveTypeToEliminate;;
 481 exception NotTheRightEliminatorShape;;
 482 exception NoHypothesesFound;;
 483
 484 let elim_intros_simpl term =
 485  let module T = CicTypeChecker in
 486  let module U = UriManager in
 487  let module R = CicReduction in
 488  let module C = Cic in
 489   let curi,metasenv =
 490    match !proof with
 491       None -> assert false
 492     | Some (curi,metasenv,_,_) -> curi,metasenv
 493   in
 494   let metano,context,ty =
 495    match !goal with
 496       None -> assert false
 497     | Some metano ->
 498        List.find (function (m,_,_) -> m=metano) metasenv
 499   in
 500    let termty = T.type_of_aux' metasenv context term in
 501    let uri,cookingno,typeno,args =
 502     match termty with
 503        C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
 504      | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
 505          (uri,cookingno,typeno,args)
 506      | _ -> raise NotAnInductiveTypeToEliminate
 507    in
 508     let eliminator_uri =
 509      let buri = U.buri_of_uri uri in
 510      let name =
 511       match CicEnvironment.get_cooked_obj uri cookingno with
 512          C.InductiveDefinition (tys,_,_) ->
 513           let (name,_,_,_) = List.nth tys typeno in
 514            name
 515        | _ -> assert false
 516      in
 517      let ext =
 518       match T.type_of_aux' metasenv context ty with
 519          C.Sort C.Prop -> "_ind"
 520        | C.Sort C.Set  -> "_rec"
 521        | C.Sort C.Type -> "_rect"
 522        | _ -> assert false
 523      in
 524       U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
 525     in
 526      let eliminator_cookingno =
 527       UriManager.relative_depth curi eliminator_uri 0
 528      in
 529      let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
 530       let ety =
 531        T.type_of_aux' [] [] eliminator_ref
 532       in
 533        let (econclusion,newmetas,arguments,newmeta,lastmeta) =
 534 (*
 535         new_metasenv_for_apply context ety
 536 *)
 537         new_metasenv_for_apply_intros context ety
 538        in
 539         (* Here we assume that we have only one inductive hypothesis to *)
 540         (* eliminate and that it is the last hypothesis of the theorem. *)
 541         (* A better approach would be fingering the hypotheses in some  *)
 542         (* way.                                                         *)
 543         let meta_of_corpse =
 544          let (_,canonical_context,_) =
 545           List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas
 546          in
 547           let irl =
 548            identity_relocation_list_for_metavariable canonical_context
 549           in
 550            Cic.Meta (lastmeta - 1, irl)
 551         in
 552         let newmetasenv = newmetas @ metasenv in
 553         let subst1,newmetasenv' =
 554          CicUnification.fo_unif newmetasenv context term meta_of_corpse
 555         in
 556          let ueconclusion = CicUnification.apply_subst subst1 econclusion in
 557           (* The conclusion of our elimination principle is *)
 558           (*  (?i farg1 ... fargn)                         *)
 559           (* The conclusion of our goal is ty. So, we can   *)
 560           (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
 561           (* a new ty equal to (P farg1 ... fargn). Now     *)
 562           (* ?i can be instantiated with P and we are ready *)
 563           (* to refine the term.                            *)
 564           let emeta, fargs =
 565            match ueconclusion with
 566 (*CSC: Code to be used for Apply
 567               C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
 568             | C.Meta (emeta,_) -> emeta,[]
 569 *)
 570 (*CSC: Code to be used for ApplyIntros *)
 571               C.Appl (he::fargs) ->
 572                let rec find_head =
 573                 function
 574                    C.Meta (emeta,_) -> emeta
 575                  | C.Lambda (_,_,t) -> find_head t
 576                  | C.LetIn (_,_,t) -> find_head t
 577                  | _ ->raise NotTheRightEliminatorShape
 578                in
 579                 find_head he,fargs
 580             | C.Meta (emeta,_) -> emeta,[]
 581 (* *)
 582             | _ -> raise NotTheRightEliminatorShape
 583           in
 584            let ty' = CicUnification.apply_subst subst1 ty in
 585            let eta_expanded_ty =
 586 (*CSC: newmetasenv' era metasenv ??????????? *)
 587             List.fold_left (eta_expand newmetasenv' context) ty' fargs
 588            in
 589             let subst2,newmetasenv'' =
 590 (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
 591 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
 592              CicUnification.fo_unif
 593               newmetasenv' context ueconclusion eta_expanded_ty
 594             in
 595              let in_subst_domain i =
 596               let eq_to_i = function (j,_) -> i=j in
 597                List.exists eq_to_i subst1 ||
 598                List.exists eq_to_i subst2
 599              in
 600 (*CSC: codice per l'elim
 601               (* When unwinding the META that corresponds to the elimination *)
 602               (* predicate (which is emeta), we must also perform one-step   *)
 603               (* beta-reduction. apply_subst doesn't need the context. Hence *)
 604               (* the underscore.                                             *)
 605               let apply_subst _ t =
 606                let t' = CicUnification.apply_subst subst1 t in
 607                 CicUnification.apply_subst_reducing
 608                  subst2 (Some (emeta,List.length fargs)) t'
 609               in
 610 *)
 611 (*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *)
 612               let apply_subst context t =
 613                let t' = CicUnification.apply_subst (subst1@subst2) t in
 614                 ProofEngineReduction.simpl context t'
 615               in
 616 (* *)
 617                 let old_uninstantiatedmetas,new_uninstantiatedmetas =
 618                  classify_metas newmeta in_subst_domain apply_subst
 619                   newmetasenv''
 620                 in
 621                  let arguments' = List.map (apply_subst context) arguments in
 622                   let bo' = Cic.Appl (eliminator_ref::arguments') in
 623                    let newmetasenv''' =
 624                     new_uninstantiatedmetas@old_uninstantiatedmetas
 625                    in
 626                     let newmetasenv'''' =
 627                      (* When unwinding the META that corresponds to the *)
 628                      (* elimination predicate (which is emeta), we must *)
 629                      (* also perform one-step beta-reduction.           *)
 630                      (* The only difference w.r.t. apply_subst is that  *)
 631                      (* we also substitute metano with bo'.             *)
 632                      (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
 633                      (*CSC: no?                                              *)
 634 (*CSC: codice per l'elim
 635                      let apply_subst' t =
 636                       let t' = CicUnification.apply_subst subst1 t in
 637                        CicUnification.apply_subst_reducing
 638                         ((metano,bo')::subst2)
 639                         (Some (emeta,List.length fargs)) t'
 640                      in
 641 *)
 642 (*CSC: codice per l'elim_intros_simpl *)
 643                      let apply_subst' t =
 644                       CicUnification.apply_subst
 645                        ((metano,bo')::(subst1@subst2)) t
 646                      in
 647 (* *)
 648                       subst_meta_and_metasenv_in_current_proof metano
 649                        apply_subst' newmetasenv'''
 650                     in
 651                      match newmetasenv'''' with
 652                         [] -> goal := None
 653                       | (i,_,_)::_ -> goal := Some i
 654 ;;
 655
 656 let reduction_tactic reduction_function term =
 657  let curi,metasenv,pbo,pty =
 658   match !proof with
 659      None -> assert false
 660    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 661  in
 662  let metano,context,ty =
 663   match !goal with
 664      None -> assert false
 665    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 666  in
 667   (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 668   (* the type of one metavariable. So we replace it everywhere.   *)
 669   (*CSC: Il vero problema e' che non sapendo dove sia il term non *)
 670   (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma,  *)
 671   (*CSC: e' meglio prima cercare il termine e scoprirne il        *)
 672   (*CSC: contesto, poi ridurre e infine rimpiazzare.              *)
 673    let replace context where=
 674 (*CSC: Per il momento se la riduzione fallisce significa solamente che *)
 675 (*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!!      *)
 676 (*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *)
 677    try
 678     let term' = reduction_function context term in
 679      ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term'
 680       ~where:where
 681    with
 682     _ -> where
 683    in
 684     let ty' = replace context ty in
 685     let context' =
 686      List.fold_right
 687       (fun entry context ->
 688         match entry with
 689            Some (name,Cic.Def  t) ->
 690             (Some (name,Cic.Def  (replace context t)))::context
 691          | Some (name,Cic.Decl t) ->
 692             (Some (name,Cic.Decl (replace context t)))::context
 693          | None -> None::context
 694       ) context []
 695     in
 696      let metasenv' =
 697       List.map
 698        (function
 699            (n,_,_) when n = metano -> (metano,context',ty')
 700          | _ as t -> t
 701        ) metasenv
 702      in
 703       proof := Some (curi,metasenv',pbo,pty) ;
 704       goal := Some metano
 705 ;;
 706
 707 (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
 708 let reduction_tactic_in_scratch reduction_function term ty =
 709  let metasenv =
 710   match !proof with
 711      None -> []
 712    | Some (_,metasenv,_,_) -> metasenv
 713  in
 714  let metano,context,_ =
 715   match !goal with
 716      None -> assert false
 717    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 718  in
 719   let term' = reduction_function context term in
 720    ProofEngineReduction.replace
 721     ~equality:(==) ~what:term ~with_what:term' ~where:ty
 722 ;;
 723
 724 let whd    = reduction_tactic CicReduction.whd;;
 725 let reduce = reduction_tactic ProofEngineReduction.reduce;;
 726 let simpl  = reduction_tactic ProofEngineReduction.simpl;;
 727
 728 let whd_in_scratch    = reduction_tactic_in_scratch CicReduction.whd;;
 729 let reduce_in_scratch =
 730  reduction_tactic_in_scratch ProofEngineReduction.reduce;;
 731 let simpl_in_scratch  =
 732  reduction_tactic_in_scratch ProofEngineReduction.simpl;;
 733
 734 (* It is just the opposite of whd. The code should probably be merged. *)
 735 let fold term =
 736  let curi,metasenv,pbo,pty =
 737   match !proof with
 738      None -> assert false
 739    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 740  in
 741  let metano,context,ty =
 742   match !goal with
 743      None -> assert false
 744    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 745  in
 746   let term' = CicReduction.whd context term in
 747    (* We don't know if [term] is a subterm of [ty] or a subterm of *)
 748    (* the type of one metavariable. So we replace it everywhere.   *)
 749    (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
 750    (*CSC: che si guadagni nulla in fatto di efficienza.    *)
 751    let replace =
 752     ProofEngineReduction.replace
 753      ~equality:(ProofEngineReduction.syntactic_equality)
 754      ~what:term' ~with_what:term
 755    in
 756     let ty' = replace ty in
 757     let context' =
 758      List.map
 759       (function
 760           Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
 761         | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
 762         | None -> None
 763       ) context
 764     in
 765      let metasenv' =
 766       List.map
 767        (function
 768            (n,_,_) when n = metano -> (metano,context',ty')
 769          | _ as t -> t
 770        ) metasenv
 771      in
 772       proof := Some (curi,metasenv',pbo,pty) ;
 773       goal := Some metano
 774 ;;
 775
 776 let cut term =
 777  let module C = Cic in
 778   let curi,metasenv,pbo,pty =
 779    match !proof with
 780       None -> assert false
 781     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 782   in
 783   let metano,context,ty =
 784    match !goal with
 785       None -> assert false
 786     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 787   in
 788    let newmeta1 = new_meta () in
 789    let newmeta2 = newmeta1 + 1 in
 790    let context_for_newmeta1 =
 791     (Some (C.Name "dummy_for_cut",C.Decl term))::context in
 792    let irl1 =
 793     identity_relocation_list_for_metavariable context_for_newmeta1 in
 794    let irl2 = identity_relocation_list_for_metavariable context in
 795     let newmeta1ty = CicSubstitution.lift 1 ty in
 796     let bo' =
 797      C.Appl
 798       [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ;
 799        C.Meta (newmeta2,irl2)]
 800     in
 801      let _ =
 802       subst_meta_in_current_proof metano bo'
 803        [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
 804      in
 805       goal := Some newmeta1
 806 ;;
 807
 808 let letin term =
 809  let module C = Cic in
 810   let curi,metasenv,pbo,pty =
 811    match !proof with
 812       None -> assert false
 813     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 814   in
 815   let metano,context,ty =
 816    match !goal with
 817       None -> assert false
 818     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 819   in
 820    let _ = CicTypeChecker.type_of_aux' metasenv context term in
 821     let newmeta = new_meta () in
 822     let context_for_newmeta =
 823      (Some (C.Name "dummy_for_letin",C.Def term))::context in
 824     let irl =
 825      identity_relocation_list_for_metavariable context_for_newmeta in
 826      let newmetaty = CicSubstitution.lift 1 ty in
 827      let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in
 828       let _ = subst_meta_in_current_proof metano bo' [newmeta,context_for_newmeta,newmetaty] in
 829        goal := Some newmeta
 830 ;;
 831
 832 exception NotConvertible;;
 833
 834 (*CSC: Bug (or feature?). [input] is parsed in the context of the goal,  *)
 835 (*CSC: while [goal_input] can have a richer context (because of binders) *)
 836 (*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
 837 (*CSC: Is that evident? Is that right? Or should it be changed?          *)
 838 let change ~goal_input ~input =
 839  let curi,metasenv,pbo,pty =
 840   match !proof with
 841      None -> assert false
 842    | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 843  in
 844  let metano,context,ty =
 845   match !goal with
 846      None -> assert false
 847    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 848  in
 849   (* are_convertible works only on well-typed terms *)
 850   ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
 851   if CicReduction.are_convertible context goal_input input then
 852    begin
 853     let replace =
 854      ProofEngineReduction.replace
 855       ~equality:(==) ~what:goal_input ~with_what:input
 856     in
 857     let ty' = replace ty in
 858     let context' =
 859      List.map
 860       (function
 861           Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
 862         | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
 863         | None -> None
 864       ) context
 865     in
 866      let metasenv' =
 867       List.map
 868        (function
 869            (n,_,_) when n = metano -> (metano,context',ty')
 870          | _ as t -> t
 871        ) metasenv
 872      in
 873       proof := Some (curi,metasenv',pbo,pty) ;
 874       goal := Some metano
 875    end
 876   else
 877    raise NotConvertible
 878 ;;
 879
 880 let clearbody =
 881  let module C = Cic in
 882   function
 883      None -> assert false
 884    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
 885    | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
 886       let curi,metasenv,pbo,pty =
 887        match !proof with
 888           None -> assert false
 889         | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 890       in
 891        let metano,_,_ =
 892         match !goal with
 893            None -> assert false
 894          | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 895        in
 896         let string_of_name =
 897          function
 898             C.Name n -> n
 899           | C.Anonimous -> "_"
 900         in
 901         let metasenv' =
 902          List.map
 903           (function
 904               (m,canonical_context,ty) when m = metano ->
 905                 let canonical_context' =
 906                  List.fold_right
 907                   (fun entry context ->
 908                     match entry with
 909                        t when t == hyp_to_clear_body ->
 910                         let cleared_entry =
 911                          let ty =
 912                           CicTypeChecker.type_of_aux' metasenv context term
 913                          in
 914                           Some (n_to_clear_body, Cic.Decl ty)
 915                         in
 916                          cleared_entry::context
 917                      | None -> None::context
 918                      | Some (n,C.Decl t)
 919                      | Some (n,C.Def t) ->
 920                         let _ =
 921                          try
 922                           CicTypeChecker.type_of_aux' metasenv context t
 923                          with
 924                           _ ->
 925                             raise
 926                              (Fail
 927                                ("The correctness of hypothesis " ^
 928                                 string_of_name n ^
 929                                 " relies on the body of " ^
 930                                 string_of_name n_to_clear_body)
 931                              )
 932                         in
 933                          entry::context
 934                   ) canonical_context []
 935                 in
 936                  let _ =
 937                   try
 938                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
 939                   with
 940                    _ ->
 941                     raise
 942                      (Fail
 943                       ("The correctness of the goal relies on the body of " ^
 944                        string_of_name n_to_clear_body))
 945                  in
 946                   m,canonical_context',ty
 947             | t -> t
 948           ) metasenv
 949         in
 950          proof := Some (curi,metasenv',pbo,pty)
 951 ;;
 952
 953 let clear hyp_to_clear =
 954  let module C = Cic in
 955   match hyp_to_clear with
 956      None -> assert false
 957    | Some (n_to_clear, _) ->
 958       let curi,metasenv,pbo,pty =
 959        match !proof with
 960           None -> assert false
 961         | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 962       in
 963        let metano,context,ty =
 964         match !goal with
 965            None -> assert false
 966          | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 967        in
 968         let string_of_name =
 969          function
 970             C.Name n -> n
 971           | C.Anonimous -> "_"
 972         in
 973         let metasenv' =
 974          List.map
 975           (function
 976               (m,canonical_context,ty) when m = metano ->
 977                 let canonical_context' =
 978                  List.fold_right
 979                   (fun entry context ->
 980                     match entry with
 981                        t when t == hyp_to_clear -> None::context
 982                      | None -> None::context
 983                      | Some (n,C.Decl t)
 984                      | Some (n,C.Def t) ->
 985                         let _ =
 986                          try
 987                           CicTypeChecker.type_of_aux' metasenv context t
 988                          with
 989                           _ ->
 990                             raise
 991                              (Fail
 992                                ("Hypothesis " ^
 993                                 string_of_name n ^
 994                                 " uses hypothesis " ^
 995                                 string_of_name n_to_clear)
 996                              )
 997                         in
 998                          entry::context
 999                   ) canonical_context []
1000                 in
1001                  let _ =
1002                   try
1003                    CicTypeChecker.type_of_aux' metasenv canonical_context' ty
1004                   with
1005                    _ ->
1006                     raise
1007                      (Fail
1008                       ("Hypothesis " ^ string_of_name n_to_clear ^
1009                        " occurs in the goal"))
1010                  in
1011                   m,canonical_context',ty
1012             | t -> t
1013           ) metasenv
1014         in
1015          proof := Some (curi,metasenv',pbo,pty)
1016 ;;