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 RefineFailure of string;;
  29 exception Uncertain of string;;
  30 exception AssertFailure of string;;
  31
  32 let debug_print = fun _ -> ()
  33
  34 let fo_unif_subst subst context metasenv t1 t2 ugraph =
  35   try
  36     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  37   with
  38       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  39     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  40 ;;
  41
  42 let rec split l n =
  43  match (l,n) with
  44     (l,0) -> ([], l)
  45   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  46   | (_,_) -> raise (AssertFailure "split: list too short")
  47 ;;
  48
  49 let rec type_of_constant uri ugraph =
  50  let module C = Cic in
  51  let module R = CicReduction in
  52  let module U = UriManager in
  53   let _ = CicTypeChecker.typecheck uri in
  54   let obj,u =
  55    try
  56     CicEnvironment.get_cooked_obj ugraph uri
  57    with Not_found -> assert false
  58   in
  59    match obj with
  60       C.Constant (_,_,ty,_,_) -> ty,u
  61     | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
  62     | _ ->
  63        raise
  64         (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
  65
  66 and type_of_variable uri ugraph =
  67   let module C = Cic in
  68   let module R = CicReduction in
  69   let module U = UriManager in
  70   let _ = CicTypeChecker.typecheck uri in
  71   let obj,u =
  72    try
  73     CicEnvironment.get_cooked_obj ugraph uri
  74     with Not_found -> assert false
  75   in
  76    match obj with
  77       C.Variable (_,_,ty,_,_) -> ty,u
  78     | _ ->
  79         raise
  80          (RefineFailure
  81           ("Unknown variable definition " ^ UriManager.string_of_uri uri))
  82
  83 and type_of_mutual_inductive_defs uri i ugraph =
  84   let module C = Cic in
  85   let module R = CicReduction in
  86   let module U = UriManager in
  87   let _ = CicTypeChecker.typecheck uri in
  88   let obj,u =
  89    try
  90     CicEnvironment.get_cooked_obj ugraph uri
  91    with Not_found -> assert false
  92   in
  93    match obj with
  94       C.InductiveDefinition (dl,_,_,_) ->
  95         let (_,_,arity,_) = List.nth dl i in
  96          arity,u
  97     | _ ->
  98        raise
  99         (RefineFailure
 100          ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 101
 102 and type_of_mutual_inductive_constr uri i j ugraph =
 103   let module C = Cic in
 104   let module R = CicReduction in
 105   let module U = UriManager in
 106   let _ = CicTypeChecker.typecheck uri in
 107    let obj,u =
 108     try
 109      CicEnvironment.get_cooked_obj ugraph uri
 110     with Not_found -> assert false
 111    in
 112     match obj with
 113         C.InductiveDefinition (dl,_,_,_) ->
 114           let (_,_,_,cl) = List.nth dl i in
 115           let (_,ty) = List.nth cl (j-1) in
 116             ty,u
 117       | _ ->
 118           raise
 119             (RefineFailure
 120                ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
 121
 122
 123 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 124
 125 (* the check_branch function checks if a branch of a case is refinable.
 126    It returns a pair (outype_instance,args), a subst and a metasenv.
 127    outype_instance is the expected result of applying the case outtype
 128    to args.
 129    The problem is that outype is in general unknown, and we should
 130    try to synthesize it from the above information, that is in general
 131    a second order unification problem. *)
 132
 133 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 134   let module C = Cic in
 135     (* let module R = CicMetaSubst in *)
 136   let module R = CicReduction in
 137     match R.whd ~subst context expectedtype with
 138         C.MutInd (_,_,_) ->
 139           (n,context,actualtype, [term]), subst, metasenv, ugraph
 140       | C.Appl (C.MutInd (_,_,_)::tl) ->
 141           let (_,arguments) = split tl left_args_no in
 142             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 143       | C.Prod (name,so,de) ->
 144           (* we expect that the actual type of the branch has the due
 145              number of Prod *)
 146           (match R.whd ~subst context actualtype with
 147                C.Prod (name',so',de') ->
 148                  let subst, metasenv, ugraph1 =
 149                    fo_unif_subst subst context metasenv so so' ugraph in
 150                  let term' =
 151                    (match CicSubstitution.lift 1 term with
 152                         C.Appl l -> C.Appl (l@[C.Rel 1])
 153                       | t -> C.Appl [t ; C.Rel 1]) in
 154                    (* we should also check that the name variable is anonymous in
 155                       the actual type de' ?? *)
 156                    check_branch (n+1)
 157                      ((Some (name,(C.Decl so)))::context)
 158                        metasenv subst left_args_no de' term' de ugraph1
 159              | _ -> raise (AssertFailure "Wrong number of arguments"))
 160       | _ -> raise (AssertFailure "Prod or MutInd expected")
 161
 162 and type_of_aux' metasenv context t ugraph =
 163   let rec type_of_aux subst metasenv context t ugraph =
 164     let module C = Cic in
 165     let module S = CicSubstitution in
 166     let module U = UriManager in
 167       match t with
 168           (*    function *)
 169           C.Rel n ->
 170             (try
 171                match List.nth context (n - 1) with
 172                    Some (_,C.Decl ty) ->
 173                      t,S.lift n ty,subst,metasenv, ugraph
 174                  | Some (_,C.Def (_,Some ty)) ->
 175                      t,S.lift n ty,subst,metasenv, ugraph
 176                  | Some (_,C.Def (bo,None)) ->
 177                      type_of_aux subst metasenv context (S.lift n bo) ugraph
 178                  | None -> raise (RefineFailure "Rel to hidden hypothesis")
 179              with
 180                  _ -> raise (RefineFailure "Not a close term")
 181             )
 182         | C.Var (uri,exp_named_subst) ->
 183             let exp_named_subst',subst',metasenv',ugraph1 =
 184               check_exp_named_subst
 185                 subst metasenv context exp_named_subst ugraph
 186             in
 187             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 188             let ty =
 189               CicSubstitution.subst_vars exp_named_subst' ty_uri
 190             in
 191               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 192         | C.Meta (n,l) ->
 193             (try
 194                let (canonical_context, term,ty) =
 195                  CicUtil.lookup_subst n subst
 196                in
 197                let l',subst',metasenv',ugraph1 =
 198                  check_metasenv_consistency n subst metasenv context
 199                    canonical_context l ugraph
 200                in
 201                  (* trust or check ??? *)
 202                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 203                    subst', metasenv', ugraph1
 204                    (* type_of_aux subst metasenv
 205                       context (CicSubstitution.subst_meta l term) *)
 206              with CicUtil.Subst_not_found _ ->
 207                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 208                let l',subst',metasenv', ugraph1 =
 209                  check_metasenv_consistency n subst metasenv context
 210                    canonical_context l ugraph
 211                in
 212                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 213                    subst', metasenv',ugraph1)
 214         | C.Sort (C.Type tno) ->
 215             let tno' = CicUniv.fresh() in
 216             let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 217               t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 218         | C.Sort _ ->
 219             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 220         | C.Implicit _ -> raise (AssertFailure "21")
 221         | C.Cast (te,ty) ->
 222             let ty',_,subst',metasenv',ugraph1 =
 223               type_of_aux subst metasenv context ty ugraph
 224             in
 225             let te',inferredty,subst'',metasenv'',ugraph2 =
 226               type_of_aux subst' metasenv' context te ugraph1
 227             in
 228               (try
 229                  let subst''',metasenv''',ugraph3 =
 230                    fo_unif_subst subst'' context metasenv''
 231                      inferredty ty ugraph2
 232                  in
 233                    C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 234                with
 235                    _ -> raise (RefineFailure "Cast"))
 236         | C.Prod (name,s,t) ->
 237             let s',sort1,subst',metasenv',ugraph1 =
 238               type_of_aux subst metasenv context s ugraph
 239             in
 240             let t',sort2,subst'',metasenv'',ugraph2 =
 241               type_of_aux subst' metasenv'
 242                 ((Some (name,(C.Decl s')))::context) t ugraph1
 243             in
 244             let sop,subst''',metasenv''',ugraph3 =
 245               sort_of_prod subst'' metasenv''
 246                 context (name,s') (sort1,sort2) ugraph2
 247             in
 248               C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 249         | C.Lambda (n,s,t) ->
 250             let s',sort1,subst',metasenv',ugraph1 =
 251               type_of_aux subst metasenv context s ugraph
 252             in
 253               (match CicReduction.whd ~subst:subst' context sort1 with
 254                    C.Meta _
 255                  | C.Sort _ -> ()
 256                  | _ ->
 257                      raise (RefineFailure (sprintf
 258                                              "Not well-typed lambda-abstraction: the source %s should be a type;
 259              instead it is a term of type %s" (CicPp.ppterm s)
 260                                              (CicPp.ppterm sort1)))
 261               ) ;
 262               let t',type2,subst'',metasenv'',ugraph2 =
 263                 type_of_aux subst' metasenv'
 264                   ((Some (n,(C.Decl s')))::context) t ugraph1
 265               in
 266                 C.Lambda (n,s',t'),C.Prod (n,s',type2),
 267                   subst'',metasenv'',ugraph2
 268         | C.LetIn (n,s,t) ->
 269             (* only to check if s is well-typed *)
 270             let s',ty,subst',metasenv',ugraph1 =
 271               type_of_aux subst metasenv context s ugraph
 272             in
 273             let t',inferredty,subst'',metasenv'',ugraph2 =
 274               type_of_aux subst' metasenv'
 275                 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
 276             in
 277               (* One-step LetIn reduction.
 278                * Even faster than the previous solution.
 279                * Moreover the inferred type is closer to the expected one.
 280                *)
 281               C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
 282                 subst'',metasenv'',ugraph2
 283         | C.Appl (he::((_::_) as tl)) ->
 284             let he',hetype,subst',metasenv',ugraph1 =
 285               type_of_aux subst metasenv context he ugraph
 286             in
 287             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 288               List.fold_right
 289                 (fun x (res,subst,metasenv,ugraph) ->
 290                    let x',ty,subst',metasenv',ugraph1 =
 291                      type_of_aux subst metasenv context x ugraph
 292                    in
 293                      (x', ty)::res,subst',metasenv',ugraph1
 294                 ) tl ([],subst',metasenv',ugraph1)
 295             in
 296             let tl',applty,subst''',metasenv''',ugraph3 =
 297               eat_prods subst'' metasenv'' context
 298                 hetype tlbody_and_type ugraph2
 299             in
 300               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
 301         | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
 302         | C.Const (uri,exp_named_subst) ->
 303             let exp_named_subst',subst',metasenv',ugraph1 =
 304               check_exp_named_subst subst metasenv context
 305                 exp_named_subst ugraph in
 306             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 307             let cty =
 308               CicSubstitution.subst_vars exp_named_subst' ty_uri
 309             in
 310               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 311         | C.MutInd (uri,i,exp_named_subst) ->
 312             let exp_named_subst',subst',metasenv',ugraph1 =
 313               check_exp_named_subst subst metasenv context
 314                 exp_named_subst ugraph
 315             in
 316             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 317             let cty =
 318               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 319               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 320         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 321             let exp_named_subst',subst',metasenv',ugraph1 =
 322               check_exp_named_subst subst metasenv context
 323                 exp_named_subst ugraph
 324             in
 325             let ty_uri,ugraph2 =
 326               type_of_mutual_inductive_constr uri i j ugraph1
 327             in
 328             let cty =
 329               CicSubstitution.subst_vars exp_named_subst' ty_uri
 330             in
 331               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 332                 metasenv',ugraph2
 333         | C.MutCase (uri, i, outtype, term, pl) ->
 334             (* first, get the inductive type (and noparams)
 335              * in the environment  *)
 336             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 337               let _ = CicTypeChecker.typecheck uri in
 338               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 339               match obj with
 340                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 341                     List.nth l i , expl_params, parsno, u
 342                 | _ ->
 343                     raise
 344                       (RefineFailure
 345                          ("Unkown mutual inductive definition " ^
 346                          U.string_of_uri uri))
 347            in
 348            let rec count_prod t =
 349              match CicReduction.whd ~subst context t with
 350                  C.Prod (_, _, t) -> 1 + (count_prod t)
 351                | _ -> 0
 352            in
 353            let no_args = count_prod arity in
 354              (* now, create a "generic" MutInd *)
 355            let metasenv,left_args =
 356              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 357            in
 358            let metasenv,right_args =
 359              let no_right_params = no_args - no_left_params in
 360                if no_right_params < 0 then assert false
 361                else CicMkImplicit.n_fresh_metas
 362                       metasenv subst context no_right_params
 363            in
 364            let metasenv,exp_named_subst =
 365              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 366            let expected_type =
 367              if no_args = 0 then
 368                C.MutInd (uri,i,exp_named_subst)
 369              else
 370                C.Appl
 371                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 372            in
 373              (* check consistency with the actual type of term *)
 374            let term',actual_type,subst,metasenv,ugraph1 =
 375              type_of_aux subst metasenv context term ugraph in
 376            let expected_type',_, subst, metasenv,ugraph2 =
 377              type_of_aux subst metasenv context expected_type ugraph1
 378            in
 379            let actual_type = CicReduction.whd ~subst context actual_type in
 380            let subst,metasenv,ugraph3 =
 381              fo_unif_subst subst context metasenv
 382                expected_type' actual_type ugraph2
 383            in
 384            let rec instantiate_prod t =
 385             function
 386                [] -> t
 387              | he::tl ->
 388                 match CicReduction.whd ~subst context t with
 389                    C.Prod (_,_,t') ->
 390                     instantiate_prod (CicSubstitution.subst he t') tl
 391                  | _ -> assert false
 392            in
 393            let arity_instantiated_with_left_args =
 394             instantiate_prod arity left_args in
 395              (* TODO: check if the sort elimination
 396               * is allowed: [(I q1 ... qr)|B] *)
 397            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 398              List.fold_left
 399                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
 400                   let constructor =
 401                     if left_args = [] then
 402                       (C.MutConstruct (uri,i,j,exp_named_subst))
 403                     else
 404                       (C.Appl
 405                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 406                   in
 407                   let p',actual_type,subst,metasenv,ugraph1 =
 408                     type_of_aux subst metasenv context p ugraph
 409                   in
 410                   let constructor',expected_type, subst, metasenv,ugraph2 =
 411                     type_of_aux subst metasenv context constructor ugraph1
 412                   in
 413                   let outtypeinstance,subst,metasenv,ugraph3 =
 414                     check_branch 0 context metasenv subst no_left_params
 415                       actual_type constructor' expected_type ugraph2
 416                   in
 417                     (pl @ [p'],j+1,
 418                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 419                ([],1,[],subst,metasenv,ugraph3) pl
 420            in
 421
 422              (* we are left to check that the outype matches his instances.
 423                 The easy case is when the outype is specified, that amount
 424                 to a trivial check. Otherwise, we should guess a type from
 425                 its instances
 426              *)
 427
 428            (match outtype with
 429            | C.Meta (n,l) ->
 430                (let candidate,ugraph5,metasenv,subst =
 431                  let exp_name_subst, metasenv =
 432                     let o,_ =
 433                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 434                     in
 435                     let uris = CicUtil.params_of_obj o in
 436                     List.fold_right (
 437                       fun uri (acc,metasenv) ->
 438                         let metasenv',new_meta =
 439                            CicMkImplicit.mk_implicit metasenv subst context
 440                         in
 441                         let irl =
 442                           CicMkImplicit.identity_relocation_list_for_metavariable
 443                             context
 444                         in
 445                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 446                     ) uris ([],metasenv)
 447                  in
 448                  let ty =
 449                   match left_args,right_args with
 450                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 451                    | _,_ ->
 452                       let rec mk_right_args =
 453                        function
 454                           0 -> []
 455                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 456                       in
 457                       let right_args_no = List.length right_args in
 458                       let lifted_left_args =
 459                        List.map (CicSubstitution.lift right_args_no) left_args
 460                       in
 461                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 462                         (lifted_left_args @ mk_right_args right_args_no))
 463                  in
 464                  let fresh_name =
 465                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 466                      context Cic.Anonymous ~typ:ty
 467                  in
 468                  match outtypeinstances with
 469                  | [] ->
 470                      let extended_context =
 471                       let rec add_right_args =
 472                        function
 473                           Cic.Prod (name,ty,t) ->
 474                            Some (name,Cic.Decl ty)::(add_right_args t)
 475                         | _ -> []
 476                       in
 477                        (Some (fresh_name,Cic.Decl ty))::
 478                        (List.rev
 479                         (add_right_args arity_instantiated_with_left_args))@
 480                        context
 481                      in
 482                      let metasenv,new_meta =
 483                        CicMkImplicit.mk_implicit metasenv subst extended_context
 484                      in
 485                      let irl =
 486                        CicMkImplicit.identity_relocation_list_for_metavariable
 487                          extended_context
 488                      in
 489                      let rec add_lambdas b =
 490                       function
 491                          Cic.Prod (name,ty,t) ->
 492                           Cic.Lambda (name,ty,(add_lambdas b t))
 493                        | _ -> Cic.Lambda (fresh_name, ty, b)
 494                      in
 495                      let candidate =
 496                       add_lambdas (Cic.Meta (new_meta,irl))
 497                        arity_instantiated_with_left_args
 498                      in
 499                      (Some candidate),ugraph4,metasenv,subst
 500                  | (constructor_args_no,_,instance,_)::tl ->
 501                      try
 502                        let instance',subst,metasenv =
 503                          CicMetaSubst.delift_rels subst metasenv
 504                           constructor_args_no instance
 505                        in
 506                        let candidate,ugraph,metasenv,subst =
 507                          List.fold_left (
 508                            fun (candidate_oty,ugraph,metasenv,subst)
 509                              (constructor_args_no,_,instance,_) ->
 510                                match candidate_oty with
 511                                | None -> None,ugraph,metasenv,subst
 512                                | Some ty ->
 513                                  try
 514                                    let instance',subst,metasenv =
 515                                      CicMetaSubst.delift_rels subst metasenv
 516                                       constructor_args_no instance
 517                                    in
 518                                    let subst,metasenv,ugraph =
 519                                     fo_unif_subst subst context metasenv
 520                                       instance' ty ugraph
 521                                    in
 522                                     candidate_oty,ugraph,metasenv,subst
 523                                  with
 524                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 525                                   | CicUnification.UnificationFailure _
 526                                   | CicUnification.Uncertain _ ->
 527                                      None,ugraph,metasenv,subst
 528                          ) (Some instance',ugraph4,metasenv,subst) tl
 529                        in
 530                        match candidate with
 531                        | None -> None, ugraph,metasenv,subst
 532                        | Some t ->
 533                           let rec add_lambdas n b =
 534                            function
 535                               Cic.Prod (name,ty,t) ->
 536                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 537                             | _ ->
 538                               Cic.Lambda (fresh_name, ty,
 539                                CicSubstitution.lift (n + 1) t)
 540                           in
 541                            Some
 542                             (add_lambdas 0 t arity_instantiated_with_left_args),
 543                            ugraph,metasenv,subst
 544                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 545                        None,ugraph4,metasenv,subst
 546                in
 547                match candidate with
 548                | None -> raise (Uncertain "can't solve an higher order unification problem")
 549                | Some candidate ->
 550                    let subst,metasenv,ugraph =
 551                      fo_unif_subst subst context metasenv
 552                        candidate outtype ugraph5
 553                    in
 554                      C.MutCase (uri, i, outtype, term', pl'),
 555                       CicReduction.head_beta_reduce
 556                        (CicMetaSubst.apply_subst subst
 557                         (Cic.Appl (outtype::right_args@[term']))),
 558                      subst,metasenv,ugraph)
 559            | _ ->    (* easy case *)
 560              let _,_, subst, metasenv,ugraph5 =
 561                type_of_aux subst metasenv context
 562                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 563              in
 564              let (subst,metasenv,ugraph6) =
 565                List.fold_left
 566                  (fun (subst,metasenv,ugraph)
 567                         (constructor_args_no,context,instance,args) ->
 568                     let instance' =
 569                       let appl =
 570                         let outtype' =
 571                           CicSubstitution.lift constructor_args_no outtype
 572                         in
 573                           C.Appl (outtype'::args)
 574                       in
 575                         CicReduction.whd ~subst context appl
 576                     in
 577                     fo_unif_subst subst context metasenv
 578                         instance instance' ugraph)
 579                  (subst,metasenv,ugraph5) outtypeinstances
 580              in
 581                C.MutCase (uri, i, outtype, term', pl'),
 582                  CicReduction.head_beta_reduce
 583                   (CicMetaSubst.apply_subst subst
 584                    (C.Appl(outtype::right_args@[term]))),
 585                  subst,metasenv,ugraph6)
 586         | C.Fix (i,fl) ->
 587             let fl_ty',subst,metasenv,types,ugraph1 =
 588               List.fold_left
 589                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 590                    let ty',_,subst',metasenv',ugraph1 =
 591                       type_of_aux subst metasenv context ty ugraph
 592                    in
 593                      fl @ [ty'],subst',metasenv',
 594                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 595                 ) ([],subst,metasenv,[],ugraph) fl
 596             in
 597             let len = List.length types in
 598             let context' = types@context in
 599             let fl_bo',subst,metasenv,ugraph2 =
 600               List.fold_left
 601                 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
 602                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 603                      type_of_aux subst metasenv context' bo ugraph
 604                    in
 605                    let subst',metasenv',ugraph' =
 606                      fo_unif_subst subst context' metasenv
 607                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 608                    in
 609                      fl @ [bo'] , subst',metasenv',ugraph'
 610                 ) ([],subst,metasenv,ugraph1) fl
 611             in
 612             let (_,_,ty,_) = List.nth fl i in
 613             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 614              * and we want the new fl with bo' and ty' injected in the right
 615              * place.
 616              *)
 617             let rec map3 f l1 l2 l3 =
 618               match l1,l2,l3 with
 619               | [],[],[] -> []
 620               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 621               | _ -> assert false
 622             in
 623             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 624               fl_ty' fl_bo' fl
 625             in
 626               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 627         | C.CoFix (i,fl) ->
 628             let fl_ty',subst,metasenv,types,ugraph1 =
 629               List.fold_left
 630                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 631                    let ty',_,subst',metasenv',ugraph1 =
 632                      type_of_aux subst metasenv context ty ugraph
 633                    in
 634                      fl @ [ty'],subst',metasenv',
 635                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 636                 ) ([],subst,metasenv,[],ugraph) fl
 637             in
 638             let len = List.length types in
 639             let context' = types@context in
 640             let fl_bo',subst,metasenv,ugraph2 =
 641               List.fold_left
 642                 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
 643                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 644                      type_of_aux subst metasenv context' bo ugraph
 645                    in
 646                    let subst',metasenv',ugraph' =
 647                      fo_unif_subst subst context' metasenv
 648                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 649                    in
 650                      fl @ [bo'],subst',metasenv',ugraph'
 651                 ) ([],subst,metasenv,ugraph1) fl
 652             in
 653             let (_,ty,_) = List.nth fl i in
 654             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 655              * and we want the new fl with bo' and ty' injected in the right
 656              * place.
 657              *)
 658             let rec map3 f l1 l2 l3 =
 659               match l1,l2,l3 with
 660               | [],[],[] -> []
 661               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 662               | _ -> assert false
 663             in
 664             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 665               fl_ty' fl_bo' fl
 666             in
 667               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 668
 669   (* check_metasenv_consistency checks that the "canonical" context of a
 670      metavariable is consitent - up to relocation via the relocation list l -
 671      with the actual context *)
 672   and check_metasenv_consistency
 673     metano subst metasenv context canonical_context l ugraph
 674     =
 675     let module C = Cic in
 676     let module R = CicReduction in
 677     let module S = CicSubstitution in
 678     let lifted_canonical_context =
 679       let rec aux i =
 680         function
 681             [] -> []
 682           | (Some (n,C.Decl t))::tl ->
 683               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 684           | (Some (n,C.Def (t,None)))::tl ->
 685               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 686           | None::tl -> None::(aux (i+1) tl)
 687           | (Some (n,C.Def (t,Some ty)))::tl ->
 688               (Some (n,
 689                      C.Def ((S.subst_meta l (S.lift i t)),
 690                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 691       in
 692         aux 1 canonical_context
 693     in
 694       try
 695         List.fold_left2
 696           (fun (l,subst,metasenv,ugraph) t ct ->
 697              match (t,ct) with
 698                  _,None ->
 699                    l @ [None],subst,metasenv,ugraph
 700                | Some t,Some (_,C.Def (ct,_)) ->
 701                    let subst',metasenv',ugraph' =
 702                    (try
 703                       fo_unif_subst subst context metasenv t ct ugraph
 704                     with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
 705                    in
 706                      l @ [Some t],subst',metasenv',ugraph'
 707                | Some t,Some (_,C.Decl ct) ->
 708                    let t',inferredty,subst',metasenv',ugraph1 =
 709                      type_of_aux subst metasenv context t ugraph
 710                    in
 711                    let subst'',metasenv'',ugraph2 =
 712                      (try
 713                         fo_unif_subst
 714                           subst' context metasenv' inferredty ct ugraph1
 715                       with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
 716                    in
 717                      l @ [Some t'], subst'',metasenv'',ugraph2
 718                | None, Some _  ->
 719                    raise (RefineFailure (sprintf
 720                                            "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
 721                                            (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 722                                            (CicMetaSubst.ppcontext subst canonical_context)))
 723           ) ([],subst,metasenv,ugraph) l lifted_canonical_context
 724       with
 725           Invalid_argument _ ->
 726             raise
 727             (RefineFailure
 728                (sprintf
 729                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 730                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 731                   (CicMetaSubst.ppcontext subst canonical_context)))
 732
 733   and check_exp_named_subst metasubst metasenv context tl ugraph =
 734     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 735       match tl with
 736           [] -> [],metasubst,metasenv,ugraph
 737         | ((uri,t) as subst)::tl ->
 738             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 739             let typeofvar =
 740               CicSubstitution.subst_vars substs ty_uri in
 741               (* CSC: why was this code here? it is wrong
 742                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 743                  Cic.Variable (_,Some bo,_,_) ->
 744                  raise
 745                  (RefineFailure
 746                  "A variable with a body can not be explicit substituted")
 747                  | Cic.Variable (_,None,_,_) -> ()
 748                  | _ ->
 749                  raise
 750                  (RefineFailure
 751                  ("Unkown variable definition " ^ UriManager.string_of_uri uri))
 752                  ) ;
 753               *)
 754             let t',typeoft,metasubst',metasenv',ugraph2 =
 755               type_of_aux metasubst metasenv context t ugraph1
 756             in
 757             let metasubst'',metasenv'',ugraph3 =
 758               try
 759                 fo_unif_subst
 760                   metasubst' context metasenv' typeoft typeofvar ugraph2
 761               with _ ->
 762                 raise (RefineFailure
 763                          ("Wrong Explicit Named Substitution: " ^
 764                            CicMetaSubst.ppterm metasubst' typeoft ^
 765                           " not unifiable with " ^
 766                           CicMetaSubst.ppterm metasubst' typeofvar))
 767             in
 768             (* FIXME: no mere tail recursive! *)
 769             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
 770               check_exp_named_subst_aux
 771                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
 772             in
 773               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
 774     in
 775       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 776
 777
 778   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
 779     let module C = Cic in
 780     let context_for_t2 = (Some (name,C.Decl s))::context in
 781     let t1'' = CicReduction.whd ~subst context t1 in
 782     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
 783       match (t1'', t2'') with
 784           (C.Sort s1, C.Sort s2)
 785             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 786               C.Sort s2,subst,metasenv,ugraph
 787         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 788             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 789             let t' = CicUniv.fresh() in
 790             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
 791             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
 792               C.Sort (C.Type t'),subst,metasenv,ugraph2
 793         | (C.Sort _,C.Sort (C.Type t1)) ->
 794             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 795             C.Sort (C.Type t1),subst,metasenv,ugraph
 796         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
 797         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 798             (* TODO how can we force the meta to become a sort? If we don't we
 799              * brake the invariant that refine produce only well typed terms *)
 800             (* TODO if we check the non meta term and if it is a sort then we are
 801              * likely to know the exact value of the result e.g. if the rhs is a
 802              * Sort (Prop | Set | CProp) then the result is the rhs *)
 803             let (metasenv,idx) =
 804               CicMkImplicit.mk_implicit_sort metasenv subst in
 805             let (subst, metasenv,ugraph1) =
 806               fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
 807             in
 808               t2'',subst,metasenv,ugraph1
 809         | (_,_) ->
 810             raise (RefineFailure (sprintf
 811                                     "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 812                                     (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 813                                     (CicPp.ppterm t2'')))
 814
 815   and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
 816     let rec mk_prod metasenv context =
 817       function
 818           [] ->
 819             let (metasenv, idx) =
 820               CicMkImplicit.mk_implicit_type metasenv subst context
 821             in
 822             let irl =
 823               CicMkImplicit.identity_relocation_list_for_metavariable context
 824             in
 825               metasenv,Cic.Meta (idx, irl)
 826         | (_,argty)::tl ->
 827             let (metasenv, idx) =
 828               CicMkImplicit.mk_implicit_type metasenv subst context
 829             in
 830             let irl =
 831               CicMkImplicit.identity_relocation_list_for_metavariable context
 832             in
 833             let meta = Cic.Meta (idx,irl) in
 834             let name =
 835               (* The name must be fresh for context.                 *)
 836               (* Nevertheless, argty is well-typed only in context.  *)
 837               (* Thus I generate a name (name_hint) in context and   *)
 838               (* then I generate a name --- using the hint name_hint *)
 839               (* --- that is fresh in (context'@context).            *)
 840               let name_hint =
 841                 (* Cic.Name "pippo" *)
 842                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
 843                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
 844                   (CicMetaSubst.apply_subst_context subst context)
 845                   Cic.Anonymous
 846                   ~typ:(CicMetaSubst.apply_subst subst argty)
 847               in
 848                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 849                 FreshNamesGenerator.mk_fresh_name ~subst
 850                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
 851             in
 852             let metasenv,target =
 853               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 854             in
 855               metasenv,Cic.Prod (name,meta,target)
 856     in
 857     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 858     let (subst, metasenv,ugraph1) =
 859       try
 860         fo_unif_subst subst context metasenv hetype hetype' ugraph
 861       with exn ->
 862         debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
 863                          (CicPp.ppterm hetype)
 864                          (CicPp.ppterm hetype')
 865                          (CicMetaSubst.ppmetasenv metasenv [])
 866                          (CicMetaSubst.ppsubst subst));
 867         raise exn
 868
 869     in
 870     let rec eat_prods metasenv subst context hetype ugraph =
 871       function
 872         | [] -> [],metasenv,subst,hetype,ugraph
 873         | (hete, hety)::tl ->
 874             (match hetype with
 875                  Cic.Prod (n,s,t) ->
 876                    let arg,subst,metasenv,ugraph1 =
 877                      try
 878                        let subst,metasenv,ugraph1 =
 879                          fo_unif_subst subst context metasenv hety s ugraph
 880                        in
 881                          hete,subst,metasenv,ugraph1
 882                      with exn ->
 883                        (* we search a coercion from hety to s *)
 884                        let coer = CoercGraph.look_for_coercion
 885                          (CicMetaSubst.apply_subst subst hety)
 886                          (CicMetaSubst.apply_subst subst s)
 887                        in
 888                        match coer with
 889                        | None -> raise exn
 890                        | Some c ->
 891                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
 892                    in
 893                    let coerced_args,metasenv',subst',t',ugraph2 =
 894                      eat_prods metasenv subst context
 895                        (* (CicMetaSubst.subst subst hete t) tl *)
 896                        (CicSubstitution.subst hete t) ugraph1 tl
 897                    in
 898                      arg::coerced_args,metasenv',subst',t',ugraph2
 899                | _ -> assert false
 900             )
 901     in
 902     let coerced_args,metasenv,subst,t,ugraph2 =
 903       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
 904     in
 905       coerced_args,t,subst,metasenv,ugraph2
 906   in
 907
 908   (* eat prods ends here! *)
 909
 910   let t',ty,subst',metasenv',ugraph1 =
 911    type_of_aux [] metasenv context t ugraph
 912   in
 913   let substituted_t = CicMetaSubst.apply_subst subst' t' in
 914   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 915     (* Andrea: ho rimesso qui l'applicazione della subst al
 916        metasenv dopo che ho droppato l'invariante che il metsaenv
 917        e' sempre istanziato *)
 918   let substituted_metasenv =
 919     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
 920     (* metasenv' *)
 921     (*  substituted_t,substituted_ty,substituted_metasenv *)
 922     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
 923   let cleaned_t =
 924     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 925   let cleaned_ty =
 926     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 927   let cleaned_metasenv =
 928     List.map
 929       (function (n,context,ty) ->
 930          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 931          let context' =
 932            List.map
 933              (function
 934                   None -> None
 935                 | Some (n, Cic.Decl t) ->
 936                     Some (n,
 937                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 938                 | Some (n, Cic.Def (bo,ty)) ->
 939                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 940                     let ty' =
 941                       match ty with
 942                           None -> None
 943                         | Some ty ->
 944                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 945                     in
 946                       Some (n, Cic.Def (bo',ty'))
 947              ) context
 948          in
 949            (n,context',ty')
 950       ) substituted_metasenv
 951   in
 952     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
 953 ;;
 954
 955 let type_of_aux' metasenv context term ugraph =
 956   try
 957     type_of_aux' metasenv context term ugraph
 958   with
 959     CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
 960
 961 (*CSC: this is a very very rough approximation; to be finished *)
 962 let are_all_occurrences_positive uri =
 963  let rec aux =
 964   (*CSC: here we should do a whd; but can we do that? *)
 965   function
 966      Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
 967    | Cic.MutInd (uri',_,_) when uri = uri' -> ()
 968    | Cic.Prod (_,_,t) -> aux t
 969    | _ -> raise (RefineFailure "not well formed constructor type")
 970  in
 971   aux
 972
 973 let typecheck metasenv uri obj =
 974  let ugraph = CicUniv.empty_ugraph in
 975  match obj with
 976     Cic.Constant (name,Some bo,ty,args,attrs) ->
 977      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
 978      let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
 979      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
 980      let bo' = CicMetaSubst.apply_subst subst bo' in
 981      let ty' = CicMetaSubst.apply_subst subst ty' in
 982      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 983       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
 984   | Cic.Constant (name,None,ty,args,attrs) ->
 985      let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
 986       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
 987   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
 988      assert (metasenv' = metasenv);
 989      (* Here we do not check the metasenv for correctness *)
 990      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
 991      let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
 992      begin
 993       match sort with
 994          Cic.Sort _
 995        (* instead of raising Uncertain, let's hope that the meta will become
 996           a sort *)
 997        | Cic.Meta _ -> ()
 998        | _ -> raise (RefineFailure "The term provided is not a type")
 999      end;
1000      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1001      let bo' = CicMetaSubst.apply_subst subst bo' in
1002      let ty' = CicMetaSubst.apply_subst subst ty' in
1003      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1004       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1005   | Cic.Variable _ -> assert false (* not implemented *)
1006   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1007      (*CSC: this code is greately simplified and many many checks are missing *)
1008      (*CSC: e.g. the constructors are not required to build their own types,  *)
1009      (*CSC: the arities are not required to have as type a sort, etc.         *)
1010      let uri = match uri with Some uri -> uri | None -> assert false in
1011      let typesno = List.length tys in
1012      (* first phase: we fix only the types *)
1013      let metasenv,ugraph,tys =
1014       List.fold_right
1015        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1016          let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1017           metasenv,ugraph,(name,b,ty',cl)::res
1018        ) tys (metasenv,ugraph,[]) in
1019      let con_context =
1020       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1021      (* second phase: we fix only the constructors *)
1022      let metasenv,ugraph,tys =
1023       List.fold_right
1024        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1025          let metasenv,ugraph,cl' =
1026           List.fold_right
1027            (fun (name,ty) (metasenv,ugraph,res) ->
1028              let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1029              let ty',_,metasenv,ugraph =
1030               type_of_aux' metasenv con_context ty ugraph in
1031              let undebrujin t =
1032               snd
1033                (List.fold_right
1034                  (fun (name,_,_,_) (i,t) ->
1035                    (* here the explicit_named_substituion is assumed to be *)
1036                    (* of length 0 *)
1037                    let t' = Cic.MutInd (uri,i,[])  in
1038                    let t = CicSubstitution.subst t' t in
1039                     i - 1,t
1040                  ) tys (typesno - 1,t)) in
1041              let ty' = undebrujin ty' in
1042               metasenv,ugraph,(name,ty')::res
1043            ) cl (metasenv,ugraph,[])
1044          in
1045           metasenv,ugraph,(name,b,ty,cl')::res
1046        ) tys (metasenv,ugraph,[]) in
1047      (* third phase: we check the positivity condition *)
1048      List.iter
1049       (fun (_,_,_,cl) ->
1050         List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
1051       ) tys ;
1052      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1053
1054 (* DEBUGGING ONLY
1055 let type_of_aux' metasenv context term =
1056  try
1057   let (t,ty,m) =
1058       type_of_aux' metasenv context term in
1059     debug_print
1060      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
1061    debug_print
1062     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
1063    (t,ty,m)
1064  with
1065  | RefineFailure msg as e ->
1066      debug_print ("@@@ REFINE FAILED: " ^ msg);
1067      raise e
1068  | Uncertain msg as e ->
1069      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
1070      raise e
1071 ;; *)