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