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