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