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