helm/ocaml/cic_unification/cicRefine.ml

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