helm/ocaml/cic_unification/cicRefine.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 open Printf
  27
  28 exception Impossible of int;;
  29 exception NotRefinable of string;;
  30 exception Uncertain of string;;
  31 exception WrongUriToConstant of string;;
  32 exception WrongUriToVariable of string;;
  33 exception ListTooShort;;
  34 exception WrongUriToMutualInductiveDefinitions of string;;
  35 exception RelToHiddenHypothesis;;
  36 exception MetasenvInconsistency;;
  37 exception MutCaseFixAndCofixRefineNotImplemented;;
  38 exception FreeMetaFound of int;;
  39 exception WrongArgumentNumber;;
  40
  41 let fdebug = ref 0;;
  42 let debug t context =
  43  let rec debug_aux t i =
  44   let module C = Cic in
  45   let module U = UriManager in
  46    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  47  in
  48   if !fdebug = 0 then
  49    raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
  50    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
  51 ;;
  52
  53 let debug_print = prerr_endline
  54
  55 let rec split l n =
  56  match (l,n) with
  57     (l,0) -> ([], l)
  58   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  59   | (_,_) -> raise ListTooShort
  60 ;;
  61
  62 let rec type_of_constant uri =
  63  let module C = Cic in
  64  let module R = CicReduction in
  65  let module U = UriManager in
  66   match CicEnvironment.get_cooked_obj uri with
  67      C.Constant (_,_,ty,_) -> ty
  68    | C.CurrentProof (_,_,_,ty,_) -> ty
  69    | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
  70
  71 and type_of_variable uri =
  72  let module C = Cic in
  73  let module R = CicReduction in
  74  let module U = UriManager in
  75   match CicEnvironment.get_cooked_obj uri with
  76      C.Variable (_,_,ty,_) -> ty
  77    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
  78
  79 and type_of_mutual_inductive_defs uri i =
  80  let module C = Cic in
  81  let module R = CicReduction in
  82  let module U = UriManager in
  83   match CicEnvironment.get_cooked_obj uri with
  84      C.InductiveDefinition (dl,_,_) ->
  85       let (_,_,arity,_) = List.nth dl i in
  86        arity
  87    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  88
  89 and type_of_mutual_inductive_constr uri i j =
  90  let module C = Cic in
  91  let module R = CicReduction in
  92  let module U = UriManager in
  93   match CicEnvironment.get_cooked_obj uri with
  94       C.InductiveDefinition (dl,_,_) ->
  95        let (_,_,_,cl) = List.nth dl i in
  96         let (_,ty) = List.nth cl (j-1) in
  97          ty
  98    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  99
 100 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 101
 102 (* the check_branch function checks if a branch of a case is refinable.
 103    It returns a pair (outype_instance,args), a subst and a metasenv.
 104    outype_instance is the expected result of applying the case outtype
 105    to args.
 106    The problem is that outype is in general unknown, and we should
 107    try to synthesize it from the above information, that is in general
 108    a second order unification problem. *)
 109
 110 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
 111   let module C = Cic in
 112   let module R = CicMetaSubst in
 113   let module Un = CicUnification in
 114   match R.whd subst context expectedtype with
 115      C.MutInd (_,_,_) ->
 116        (n,context,actualtype, [term]), subst, metasenv
 117    | C.Appl (C.MutInd (_,_,_)::tl) ->
 118        let (_,arguments) = split tl left_args_no in
 119        (n,context,actualtype, arguments@[term]), subst, metasenv
 120    | C.Prod (name,so,de) ->
 121       (* we expect that the actual type of the branch has the due
 122          number of Prod *)
 123       (match R.whd subst context actualtype with
 124            C.Prod (name',so',de') ->
 125              let subst, metasenv =
 126                 Un.fo_unif_subst subst context metasenv so so' in
 127              let term' =
 128                (match CicSubstitution.lift 1 term with
 129                    C.Appl l -> C.Appl (l@[C.Rel 1])
 130                  | t -> C.Appl [t ; C.Rel 1]) in
 131              (* we should also check that the name variable is anonymous in
 132              the actual type de' ?? *)
 133              check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
 134          | _ -> raise WrongArgumentNumber)
 135   | _ -> raise (NotRefinable "Prod or MutInd expected")
 136
 137 and type_of_aux' metasenv context t =
 138  let rec type_of_aux subst metasenv context =
 139   let module C = Cic in
 140   let module S = CicSubstitution in
 141   let module U = UriManager in
 142   let module Un = CicUnification in
 143    function
 144       C.Rel n ->
 145        (try
 146          match List.nth context (n - 1) with
 147             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
 148           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
 149           | Some (_,C.Def (bo,None)) ->
 150              type_of_aux subst metasenv context (S.lift n bo)
 151           | None -> raise RelToHiddenHypothesis
 152         with
 153          _ -> raise (NotRefinable "Not a close term")
 154        )
 155     | C.Var (uri,exp_named_subst) ->
 156       incr fdebug ;
 157       let subst',metasenv' =
 158        check_exp_named_subst subst metasenv context exp_named_subst in
 159       let ty =
 160        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
 161       in
 162        decr fdebug ;
 163        ty,subst',metasenv'
 164     | C.Meta (n,l) ->
 165        let (_,canonical_context,ty) =
 166         try
 167          List.find (function (m,_,_) -> n = m) metasenv
 168         with
 169          Not_found -> raise (FreeMetaFound n)
 170        in
 171         let subst',metasenv' =
 172          check_metasenv_consistency subst metasenv context canonical_context l
 173         in
 174          CicSubstitution.lift_meta l ty, subst', metasenv'
 175     | C.Sort s ->
 176        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
 177         subst,metasenv
 178     | C.Implicit -> raise (Impossible 21)
 179     | C.Cast (te,ty) ->
 180        let _,subst',metasenv' =
 181         type_of_aux subst metasenv context ty in
 182        let inferredty,subst'',metasenv'' =
 183         type_of_aux subst' metasenv' context ty
 184        in
 185         (try
 186           let subst''',metasenv''' =
 187            Un.fo_unif_subst subst'' context metasenv'' inferredty ty
 188           in
 189            ty,subst''',metasenv'''
 190          with
 191           _ -> raise (NotRefinable "Cast"))
 192     | C.Prod (name,s,t) ->
 193        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 194        let sort2,subst'',metasenv'' =
 195         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
 196        in
 197         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
 198    | C.Lambda (n,s,t) ->
 199        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 200        let type2,subst'',metasenv'' =
 201         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 202        in
 203         let sort2,subst''',metasenv''' =
 204          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
 205         in
 206          (* only to check if the product is well-typed *)
 207          let _,subst'''',metasenv'''' =
 208           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
 209          in
 210           C.Prod (n,s,type2),subst'''',metasenv''''
 211    | C.LetIn (n,s,t) ->
 212       (* only to check if s is well-typed *)
 213       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
 214       let inferredty,subst'',metasenv'' =
 215        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
 216       in
 217        (* One-step LetIn reduction. Even faster than the previous solution.
 218           Moreover the inferred type is closer to the expected one. *)
 219        CicSubstitution.subst s inferredty,subst',metasenv'
 220    | C.Appl (he::tl) when List.length tl > 0 ->
 221       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 222       let tlbody_and_type,subst'',metasenv'' =
 223        List.fold_right
 224         (fun x (res,subst,metasenv) ->
 225           let ty,subst',metasenv' =
 226            type_of_aux subst metasenv context x
 227           in
 228            (x, ty)::res,subst',metasenv'
 229         ) tl ([],subst',metasenv')
 230       in
 231        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 232    | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
 233    | C.Const (uri,exp_named_subst) ->
 234       incr fdebug ;
 235       let subst',metasenv' =
 236        check_exp_named_subst subst metasenv context exp_named_subst in
 237       let cty =
 238        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 239       in
 240        decr fdebug ;
 241        cty,subst',metasenv'
 242    | C.MutInd (uri,i,exp_named_subst) ->
 243       incr fdebug ;
 244       let subst',metasenv' =
 245        check_exp_named_subst subst metasenv context exp_named_subst in
 246       let cty =
 247        CicSubstitution.subst_vars exp_named_subst
 248         (type_of_mutual_inductive_defs uri i)
 249       in
 250        decr fdebug ;
 251        cty,subst',metasenv'
 252    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 253       let subst',metasenv' =
 254        check_exp_named_subst subst metasenv context exp_named_subst in
 255       let cty =
 256        CicSubstitution.subst_vars exp_named_subst
 257         (type_of_mutual_inductive_constr uri i j)
 258       in
 259        cty,subst',metasenv'
 260    | C.MutCase (uri, i, outtype, term, pl) ->
 261        (* first, get the inductive type (and noparams) in the environment  *)
 262        let (_,b,arity,constructors), expl_params, no_left_params =
 263          match CicEnvironment.get_cooked_obj ~trust:true uri with
 264             C.InductiveDefinition (l,expl_params,parsno) ->
 265               List.nth l i , expl_params, parsno
 266           | _ ->
 267             raise
 268              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
 269        let rec count_prod t =
 270          match CicMetaSubst.whd subst context t with
 271              C.Prod (_, _, t) -> 1 + (count_prod t)
 272            | _ -> 0 in
 273        let no_args = count_prod arity in
 274        (* now, create a "generic" MutInd *)
 275        let metasenv,left_args =
 276          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
 277        let metasenv,right_args =
 278          let no_right_params = no_args - no_left_params in
 279          if no_right_params < 0 then assert false
 280          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
 281        let metasenv,exp_named_subst =
 282          CicMkImplicit.fresh_subst metasenv context expl_params in
 283        let expected_type =
 284          if no_args = 0 then
 285            C.MutInd (uri,i,exp_named_subst)
 286          else
 287            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 288        in
 289        (* check consistency with the actual type of term *)
 290        let actual_type,subst,metasenv =
 291          type_of_aux subst metasenv context term in
 292        let _, subst, metasenv =
 293          type_of_aux subst metasenv context expected_type
 294        in
 295        let actual_type = CicMetaSubst.whd subst context actual_type in
 296        let subst,metasenv =
 297          Un.fo_unif_subst subst context metasenv expected_type actual_type
 298        in
 299        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 300        let (_,outtypeinstances,subst,metasenv) =
 301           List.fold_left
 302            (fun (j,outtypeinstances,subst,metasenv) p ->
 303              let constructor =
 304               if left_args = [] then
 305                (C.MutConstruct (uri,i,j,exp_named_subst))
 306               else
 307                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 308              in
 309              let actual_type,subst,metasenv =
 310                type_of_aux subst metasenv context p in
 311              let expected_type, subst, metasenv =
 312                type_of_aux subst metasenv context constructor in
 313              let outtypeinstance,subst,metasenv =
 314                check_branch
 315                 0 context metasenv subst
 316                 no_left_params actual_type constructor expected_type in
 317              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
 318             (1,[],subst,metasenv) pl in
 319         (* we are left to check that the outype matches his instances.
 320            The easy case is when the outype is specified, that amount
 321            to a trivial check. Otherwise, we should guess a type from
 322            its instances *)
 323         (* easy case *)
 324         let _, subst, metasenv =
 325           type_of_aux subst metasenv context
 326             (C.Appl ((outtype :: right_args) @ [term]))
 327         in
 328         let (subst,metasenv) =
 329           List.fold_left
 330             (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
 331               let instance' =
 332                 let appl =
 333                   let outtype' =
 334                     CicSubstitution.lift constructor_args_no outtype
 335                   in
 336                   C.Appl (outtype'::args)
 337                 in
 338 (*
 339                 (* if appl is not well typed then the type_of below solves the
 340                  * problem *)
 341                 let (_, subst, metasenv) =
 342                   type_of_aux subst metasenv context appl
 343                 in
 344 *)
 345                 CicMetaSubst.whd subst context appl
 346               in
 347                Un.fo_unif_subst subst context metasenv instance instance')
 348              (subst,metasenv) outtypeinstances in
 349         CicMetaSubst.whd subst
 350           context (C.Appl(outtype::right_args@[term])),subst,metasenv
 351    | C.Fix _
 352    | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
 353
 354  (* check_metasenv_consistency checks that the "canonical" context of a
 355  metavariable is consitent - up to relocation via the relocation list l -
 356  with the actual context *)
 357  and check_metasenv_consistency subst metasenv context canonical_context l =
 358    let module C = Cic in
 359    let module R = CicReduction in
 360    let module S = CicSubstitution in
 361     let lifted_canonical_context =
 362      let rec aux i =
 363       function
 364          [] -> []
 365        | (Some (n,C.Decl t))::tl ->
 366           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 367        | (Some (n,C.Def (t,None)))::tl ->
 368           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 369        | None::tl -> None::(aux (i+1) tl)
 370        | (Some (_,C.Def (_,Some _)))::_ -> assert false
 371      in
 372       aux 1 canonical_context
 373     in
 374      List.fold_left2
 375       (fun (subst,metasenv) t ct ->
 376         match (t,ct) with
 377            _,None ->
 378              subst,metasenv
 379          | Some t,Some (_,C.Def (ct,_)) ->
 380             (try
 381               CicUnification.fo_unif_subst subst context metasenv t ct
 382              with _ -> raise MetasenvInconsistency)
 383          | Some t,Some (_,C.Decl ct) ->
 384             let inferredty,subst',metasenv' =
 385              type_of_aux subst metasenv context t
 386             in
 387              (try
 388                CicUnification.fo_unif_subst
 389                 subst' context metasenv' inferredty ct
 390              with _ -> raise MetasenvInconsistency)
 391          | _, _  ->
 392              raise MetasenvInconsistency
 393       ) (subst,metasenv) l lifted_canonical_context
 394
 395  and check_exp_named_subst metasubst metasenv context =
 396   let rec check_exp_named_subst_aux metasubst metasenv substs =
 397    function
 398       [] -> metasubst,metasenv
 399     | ((uri,t) as subst)::tl ->
 400        let typeofvar =
 401         CicSubstitution.subst_vars substs (type_of_variable uri) in
 402        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 403            Cic.Variable (_,Some bo,_,_) ->
 404             raise
 405              (NotRefinable
 406                "A variable with a body can not be explicit substituted")
 407          | Cic.Variable (_,None,_,_) -> ()
 408          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 409        ) ;
 410        let typeoft,metasubst',metasenv' =
 411         type_of_aux metasubst metasenv context t
 412        in
 413         try
 414          let metasubst'',metasenv'' =
 415           CicUnification.fo_unif_subst
 416            metasubst' context metasenv' typeoft typeofvar
 417          in
 418           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 419         with _ ->
 420          raise (NotRefinable "Wrong Explicit Named Substitution")
 421   in
 422    check_exp_named_subst_aux metasubst metasenv []
 423
 424  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 425   let module C = Cic in
 426    (* ti could be a metavariable in the domain of the substitution *)
 427    let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
 428    let t1' = CicMetaSubst.apply_subst subst' t1 in
 429    let t2' = CicMetaSubst.apply_subst subst' t2 in
 430     let t1'' = CicMetaSubst.whd subst' context t1' in
 431     let t2'' = CicMetaSubst.whd subst' ((Some (name,C.Decl s))::context) t2' in
 432     match (t1'', t2'') with
 433        (C.Sort s1, C.Sort s2)
 434          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
 435           C.Sort s2,subst',metasenv'
 436      | (C.Sort s1, C.Sort s2) ->
 437          (*CSC manca la gestione degli universi!!! *)
 438          C.Sort C.Type,subst',metasenv'
 439      | (C.Meta _,_) | (_,C.Meta _) ->
 440          let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
 441          let irl =
 442            CicMkImplicit.identity_relocation_list_for_metavariable context
 443          in
 444          C.Meta (idx, irl), subst, metasenv'
 445      | (_,_) ->
 446          raise (NotRefinable (sprintf
 447           "Two types were expected, found %s of type %s and %s of type %s"
 448           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 449           (CicPp.ppterm t2'')))
 450
 451  and eat_prods subst metasenv context hetype =
 452   function
 453      [] -> hetype,subst,metasenv
 454    | (hete, hety)::tl ->
 455     (match (CicMetaSubst.whd subst context hetype) with
 456         Cic.Prod (n,s,t) ->
 457          let subst',metasenv' =
 458            CicUnification.fo_unif_subst subst context metasenv s hety
 459          in
 460           CicReduction.fdebug := -1 ;
 461           eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
 462       | Cic.Meta _ as t ->
 463          raise
 464           (Uncertain
 465             ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
 466       | _ -> raise (NotRefinable "Appl: wrong Prod-type")
 467     )
 468  in
 469   let ty,subst',metasenv' =
 470    type_of_aux [] metasenv context t
 471   in
 472    let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in
 473    (* we get rid of the metavariables that have been instantiated *)
 474    let metasenv''' =
 475     List.filter
 476      (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
 477      metasenv''
 478    in
 479     CicMetaSubst.apply_subst subst'' t,
 480      CicMetaSubst.apply_subst subst'' ty,
 481       subst'', metasenv'''
 482 ;;
 483
 484 (* DEBUGGING ONLY *)
 485 let type_of_aux' metasenv context term =
 486  try
 487   let (t,ty,s,m) = type_of_aux' metasenv context term in
 488 (*
 489    List.iter
 490     (function (i,t) ->
 491       debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
 492    List.iter
 493     (function (i,_,t) ->
 494       debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
 495 *)
 496    debug_print
 497     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
 498    (t,ty,s,m)
 499  with
 500  | CicUnification.AssertFailure msg as e ->
 501      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
 502      debug_print msg;
 503      raise e
 504  | CicUnification.UnificationFailure msg as e ->
 505      debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
 506      debug_print msg;
 507      raise e
 508  | e ->
 509 (*
 510    List.iter
 511     (function (i,_,t) ->
 512       debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
 513     metasenv ;
 514 *)
 515    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
 516    raise e
 517 ;;
 518