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