helm/ocaml/cic_unification/cicRefine.ml

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