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