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