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                       raise (RefineFailure (lazy "no coercion"))
 397                   | CoercGraph.NotHandled _ ->
 398                       raise (RefineFailure (lazy "not a sort in PI"))
 399                   | CoercGraph.NotMetaClosed ->
 400                       raise (Uncertain (lazy "Coercions on metas 1"))
 401                   | CoercGraph.SomeCoercion c ->
 402                       Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
 403             in
 404             let s',sort1,subst',metasenv',ugraph1 =
 405               type_of_aux subst metasenv context s ugraph
 406             in
 407             let s',sort1,subst', metasenv',ugraph1 =
 408               coerce_to_sort true (Cic.Type(CicUniv.fresh()))
 409               s' sort1 subst' context metasenv' ugraph1
 410             in
 411             let context_for_t = ((Some (name,(C.Decl s')))::context) in
 412             let metasenv',t = exp_impl metasenv' subst' context_for_t t in
 413             let t',sort2,subst'',metasenv'',ugraph2 =
 414               type_of_aux subst' metasenv'
 415                 context_for_t t ugraph1
 416             in
 417             let t',sort2,subst'',metasenv'',ugraph2 =
 418               coerce_to_sort false (Cic.Type(CicUniv.fresh()))
 419               t' sort2 subst'' context_for_t metasenv'' ugraph2
 420             in
 421               let sop,subst''',metasenv''',ugraph3 =
 422                 sort_of_prod subst'' metasenv''
 423                   context (name,s') (sort1,sort2) ugraph2
 424               in
 425                 C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 426         | C.Lambda (n,s,t) ->
 427
 428             let s',sort1,subst',metasenv',ugraph1 =
 429               type_of_aux subst metasenv context s ugraph
 430             in
 431             (match CicReduction.whd ~subst:subst' context sort1 with
 432                  C.Meta _
 433                | C.Sort _ -> ()
 434                | _ ->
 435                    raise (RefineFailure (lazy (sprintf
 436                                            "Not well-typed lambda-abstraction: the source %s should be a type;
 437            instead it is a term of type %s" (CicPp.ppterm s)
 438                                            (CicPp.ppterm sort1))))
 439             ) ;
 440             let context_for_t = ((Some (n,(C.Decl s')))::context) in
 441             let metasenv',t = exp_impl metasenv' subst' context_for_t t in
 442             let t',type2,subst'',metasenv'',ugraph2 =
 443               type_of_aux subst' metasenv'
 444                 context_for_t t ugraph1
 445             in
 446               C.Lambda (n,s',t'),C.Prod (n,s',type2),
 447                 subst'',metasenv'',ugraph2
 448         | C.LetIn (n,s,t) ->
 449             (* only to check if s is well-typed *)
 450             let s',ty,subst',metasenv',ugraph1 =
 451               type_of_aux subst metasenv context s ugraph
 452             in
 453            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
 454             let metasenv',t = exp_impl metasenv' subst' context_for_t t in
 455
 456             let t',inferredty,subst'',metasenv'',ugraph2 =
 457               type_of_aux subst' metasenv'
 458                 context_for_t t ugraph1
 459             in
 460               (* One-step LetIn reduction.
 461                * Even faster than the previous solution.
 462                * Moreover the inferred type is closer to the expected one.
 463                *)
 464               C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
 465                 subst'',metasenv'',ugraph2
 466         | C.Appl (he::((_::_) as tl)) ->
 467             let he',hetype,subst',metasenv',ugraph1 =
 468               type_of_aux subst metasenv context he ugraph
 469             in
 470             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 471               List.fold_right
 472                 (fun x (res,subst,metasenv,ugraph) ->
 473                    let x',ty,subst',metasenv',ugraph1 =
 474                      type_of_aux subst metasenv context x ugraph
 475                    in
 476                      (x', ty)::res,subst',metasenv',ugraph1
 477                 ) tl ([],subst',metasenv',ugraph1)
 478             in
 479             let tl',applty,subst''',metasenv''',ugraph3 =
 480               eat_prods true subst'' metasenv'' context
 481                 hetype tlbody_and_type ugraph2
 482             in
 483               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
 484         | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
 485         | C.Const (uri,exp_named_subst) ->
 486             let exp_named_subst',subst',metasenv',ugraph1 =
 487               check_exp_named_subst subst metasenv context
 488                 exp_named_subst ugraph in
 489             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 490             let cty =
 491               CicSubstitution.subst_vars exp_named_subst' ty_uri
 492             in
 493               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 494         | C.MutInd (uri,i,exp_named_subst) ->
 495             let exp_named_subst',subst',metasenv',ugraph1 =
 496               check_exp_named_subst subst metasenv context
 497                 exp_named_subst ugraph
 498             in
 499             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 500             let cty =
 501               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 502               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 503         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 504             let exp_named_subst',subst',metasenv',ugraph1 =
 505               check_exp_named_subst subst metasenv context
 506                 exp_named_subst ugraph
 507             in
 508             let ty_uri,ugraph2 =
 509               type_of_mutual_inductive_constr uri i j ugraph1
 510             in
 511             let cty =
 512               CicSubstitution.subst_vars exp_named_subst' ty_uri
 513             in
 514               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 515                 metasenv',ugraph2
 516         | C.MutCase (uri, i, outtype, term, pl) ->
 517             (* first, get the inductive type (and noparams)
 518              * in the environment  *)
 519             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 520               let _ = CicTypeChecker.typecheck uri in
 521               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 522               match obj with
 523                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 524                     List.nth l i , expl_params, parsno, u
 525                 | _ ->
 526                     raise
 527                       (RefineFailure
 528                          (lazy ("Unkown mutual inductive definition " ^
 529                          U.string_of_uri uri)))
 530            in
 531            let rec count_prod t =
 532              match CicReduction.whd ~subst context t with
 533                  C.Prod (_, _, t) -> 1 + (count_prod t)
 534                | _ -> 0
 535            in
 536            let no_args = count_prod arity in
 537              (* now, create a "generic" MutInd *)
 538            let metasenv,left_args =
 539              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 540            in
 541            let metasenv,right_args =
 542              let no_right_params = no_args - no_left_params in
 543                if no_right_params < 0 then assert false
 544                else CicMkImplicit.n_fresh_metas
 545                       metasenv subst context no_right_params
 546            in
 547            let metasenv,exp_named_subst =
 548              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 549            let expected_type =
 550              if no_args = 0 then
 551                C.MutInd (uri,i,exp_named_subst)
 552              else
 553                C.Appl
 554                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 555            in
 556              (* check consistency with the actual type of term *)
 557            let term',actual_type,subst,metasenv,ugraph1 =
 558              type_of_aux subst metasenv context term ugraph in
 559            let expected_type',_, subst, metasenv,ugraph2 =
 560              type_of_aux subst metasenv context expected_type ugraph1
 561            in
 562            let actual_type = CicReduction.whd ~subst context actual_type in
 563            let subst,metasenv,ugraph3 =
 564              fo_unif_subst subst context metasenv
 565                expected_type' actual_type ugraph2
 566            in
 567            let rec instantiate_prod t =
 568             function
 569                [] -> t
 570              | he::tl ->
 571                 match CicReduction.whd ~subst context t with
 572                    C.Prod (_,_,t') ->
 573                     instantiate_prod (CicSubstitution.subst he t') tl
 574                  | _ -> assert false
 575            in
 576            let arity_instantiated_with_left_args =
 577             instantiate_prod arity left_args in
 578              (* TODO: check if the sort elimination
 579               * is allowed: [(I q1 ... qr)|B] *)
 580            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 581              List.fold_left
 582                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
 583                   let constructor =
 584                     if left_args = [] then
 585                       (C.MutConstruct (uri,i,j,exp_named_subst))
 586                     else
 587                       (C.Appl
 588                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 589                   in
 590                   let p',actual_type,subst,metasenv,ugraph1 =
 591                     type_of_aux subst metasenv context p ugraph
 592                   in
 593                   let constructor',expected_type, subst, metasenv,ugraph2 =
 594                     type_of_aux subst metasenv context constructor ugraph1
 595                   in
 596                   let outtypeinstance,subst,metasenv,ugraph3 =
 597                     check_branch 0 context metasenv subst no_left_params
 598                       actual_type constructor' expected_type ugraph2
 599                   in
 600                     (pl @ [p'],j+1,
 601                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 602                ([],1,[],subst,metasenv,ugraph3) pl
 603            in
 604
 605              (* we are left to check that the outype matches his instances.
 606                 The easy case is when the outype is specified, that amount
 607                 to a trivial check. Otherwise, we should guess a type from
 608                 its instances
 609              *)
 610
 611            (match outtype with
 612            | C.Meta (n,l) ->
 613                (let candidate,ugraph5,metasenv,subst =
 614                  let exp_name_subst, metasenv =
 615                     let o,_ =
 616                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 617                     in
 618                     let uris = CicUtil.params_of_obj o in
 619                     List.fold_right (
 620                       fun uri (acc,metasenv) ->
 621                         let metasenv',new_meta =
 622                            CicMkImplicit.mk_implicit metasenv subst context
 623                         in
 624                         let irl =
 625                           CicMkImplicit.identity_relocation_list_for_metavariable
 626                             context
 627                         in
 628                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 629                     ) uris ([],metasenv)
 630                  in
 631                  let ty =
 632                   match left_args,right_args with
 633                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 634                    | _,_ ->
 635                       let rec mk_right_args =
 636                        function
 637                           0 -> []
 638                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 639                       in
 640                       let right_args_no = List.length right_args in
 641                       let lifted_left_args =
 642                        List.map (CicSubstitution.lift right_args_no) left_args
 643                       in
 644                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 645                         (lifted_left_args @ mk_right_args right_args_no))
 646                  in
 647                  let fresh_name =
 648                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 649                      context Cic.Anonymous ~typ:ty
 650                  in
 651                  match outtypeinstances with
 652                  | [] ->
 653                      let extended_context =
 654                       let rec add_right_args =
 655                        function
 656                           Cic.Prod (name,ty,t) ->
 657                            Some (name,Cic.Decl ty)::(add_right_args t)
 658                         | _ -> []
 659                       in
 660                        (Some (fresh_name,Cic.Decl ty))::
 661                        (List.rev
 662                         (add_right_args arity_instantiated_with_left_args))@
 663                        context
 664                      in
 665                      let metasenv,new_meta =
 666                        CicMkImplicit.mk_implicit metasenv subst extended_context
 667                      in
 668                        let irl =
 669                        CicMkImplicit.identity_relocation_list_for_metavariable
 670                          extended_context
 671                      in
 672                      let rec add_lambdas b =
 673                       function
 674                          Cic.Prod (name,ty,t) ->
 675                           Cic.Lambda (name,ty,(add_lambdas b t))
 676                        | _ -> Cic.Lambda (fresh_name, ty, b)
 677                      in
 678                      let candidate =
 679                       add_lambdas (Cic.Meta (new_meta,irl))
 680                        arity_instantiated_with_left_args
 681                      in
 682                      (Some candidate),ugraph4,metasenv,subst
 683                  | (constructor_args_no,_,instance,_)::tl ->
 684                      try
 685                        let instance',subst,metasenv =
 686                          CicMetaSubst.delift_rels subst metasenv
 687                           constructor_args_no instance
 688                        in
 689                        let candidate,ugraph,metasenv,subst =
 690                          List.fold_left (
 691                            fun (candidate_oty,ugraph,metasenv,subst)
 692                              (constructor_args_no,_,instance,_) ->
 693                                match candidate_oty with
 694                                | None -> None,ugraph,metasenv,subst
 695                                | Some ty ->
 696                                  try
 697                                    let instance',subst,metasenv =
 698                                      CicMetaSubst.delift_rels subst metasenv
 699                                       constructor_args_no instance
 700                                    in
 701                                    let subst,metasenv,ugraph =
 702                                     fo_unif_subst subst context metasenv
 703                                       instance' ty ugraph
 704                                    in
 705                                     candidate_oty,ugraph,metasenv,subst
 706                                  with
 707                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 708                                   | CicUnification.UnificationFailure _
 709                                   | CicUnification.Uncertain _ ->
 710                                      None,ugraph,metasenv,subst
 711                          ) (Some instance',ugraph4,metasenv,subst) tl
 712                        in
 713                        match candidate with
 714                        | None -> None, ugraph,metasenv,subst
 715                        | Some t ->
 716                           let rec add_lambdas n b =
 717                            function
 718                               Cic.Prod (name,ty,t) ->
 719                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 720                             | _ ->
 721                               Cic.Lambda (fresh_name, ty,
 722                                CicSubstitution.lift (n + 1) t)
 723                           in
 724                            Some
 725                             (add_lambdas 0 t arity_instantiated_with_left_args),
 726                            ugraph,metasenv,subst
 727                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 728                        None,ugraph4,metasenv,subst
 729                in
 730                match candidate with
 731                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 732                | Some candidate ->
 733                    let subst,metasenv,ugraph =
 734                      fo_unif_subst subst context metasenv
 735                        candidate outtype ugraph5
 736                    in
 737                      C.MutCase (uri, i, outtype, term', pl'),
 738                       CicReduction.head_beta_reduce
 739                        (CicMetaSubst.apply_subst subst
 740                         (Cic.Appl (outtype::right_args@[term']))),
 741                      subst,metasenv,ugraph)
 742            | _ ->    (* easy case *)
 743              let outtype,outtypety, subst, metasenv,ugraph4 =
 744                type_of_aux subst metasenv context outtype ugraph4
 745              in
 746              let tlbody_and_type,subst,metasenv,ugraph4 =
 747                List.fold_right
 748                  (fun x (res,subst,metasenv,ugraph) ->
 749                     let x',ty,subst',metasenv',ugraph1 =
 750                       type_of_aux subst metasenv context x ugraph
 751                     in
 752                       (x', ty)::res,subst',metasenv',ugraph1
 753                  ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
 754              in
 755              let _,_,subst,metasenv,ugraph4 =
 756                eat_prods false subst metasenv context
 757                  outtypety tlbody_and_type ugraph4
 758              in
 759              let _,_, subst, metasenv,ugraph5 =
 760                type_of_aux subst metasenv context
 761                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 762              in
 763              let (subst,metasenv,ugraph6) =
 764                List.fold_left
 765                  (fun (subst,metasenv,ugraph)
 766                         (constructor_args_no,context,instance,args) ->
 767                     let instance' =
 768                       let appl =
 769                         let outtype' =
 770                           CicSubstitution.lift constructor_args_no outtype
 771                         in
 772                           C.Appl (outtype'::args)
 773                       in
 774                         CicReduction.whd ~subst context appl
 775                     in
 776                     fo_unif_subst subst context metasenv
 777                         instance instance' ugraph)
 778                  (subst,metasenv,ugraph5) outtypeinstances
 779              in
 780                C.MutCase (uri, i, outtype, term', pl'),
 781                  CicReduction.head_beta_reduce
 782                   (CicMetaSubst.apply_subst subst
 783                    (C.Appl(outtype::right_args@[term]))),
 784                  subst,metasenv,ugraph6)
 785         | C.Fix (i,fl) ->
 786             let fl_ty',subst,metasenv,types,ugraph1 =
 787               List.fold_left
 788                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 789                    let ty',_,subst',metasenv',ugraph1 =
 790                       type_of_aux subst metasenv context ty ugraph
 791                    in
 792                      fl @ [ty'],subst',metasenv',
 793                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 794                 ) ([],subst,metasenv,[],ugraph) fl
 795             in
 796             let len = List.length types in
 797             let context' = types@context in
 798             let fl_bo',subst,metasenv,ugraph2 =
 799               List.fold_left
 800                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 801                    let metasenv, bo = exp_impl metasenv subst context' bo in
 802                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 803                      type_of_aux subst metasenv context' bo ugraph
 804                    in
 805                    let subst',metasenv',ugraph' =
 806                      fo_unif_subst subst context' metasenv
 807                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 808                    in
 809                      fl @ [bo'] , subst',metasenv',ugraph'
 810                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 811             in
 812             let ty = List.nth fl_ty' i in
 813             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 814              * and we want the new fl with bo' and ty' injected in the right
 815              * place.
 816              *)
 817             let rec map3 f l1 l2 l3 =
 818               match l1,l2,l3 with
 819               | [],[],[] -> []
 820               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 821               | _ -> assert false
 822             in
 823             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 824               fl_ty' fl_bo' fl
 825             in
 826               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 827         | C.CoFix (i,fl) ->
 828             let fl_ty',subst,metasenv,types,ugraph1 =
 829               List.fold_left
 830                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 831                    let ty',_,subst',metasenv',ugraph1 =
 832                      type_of_aux subst metasenv context ty ugraph
 833                    in
 834                      fl @ [ty'],subst',metasenv',
 835                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 836                 ) ([],subst,metasenv,[],ugraph) fl
 837             in
 838             let len = List.length types in
 839             let context' = types@context in
 840             let fl_bo',subst,metasenv,ugraph2 =
 841               List.fold_left
 842                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 843                    let metasenv, bo = exp_impl metasenv subst context' bo in
 844                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 845                      type_of_aux subst metasenv context' bo ugraph
 846                    in
 847                    let subst',metasenv',ugraph' =
 848                      fo_unif_subst subst context' metasenv
 849                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 850                    in
 851                      fl @ [bo'],subst',metasenv',ugraph'
 852                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 853             in
 854             let ty = List.nth fl_ty' i in
 855             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 856              * and we want the new fl with bo' and ty' injected in the right
 857              * place.
 858              *)
 859             let rec map3 f l1 l2 l3 =
 860               match l1,l2,l3 with
 861               | [],[],[] -> []
 862               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 863               | _ -> assert false
 864             in
 865             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 866               fl_ty' fl_bo' fl
 867             in
 868               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 869
 870   (* check_metasenv_consistency checks that the "canonical" context of a
 871      metavariable is consitent - up to relocation via the relocation list l -
 872      with the actual context *)
 873   and check_metasenv_consistency
 874     metano subst metasenv context canonical_context l ugraph
 875     =
 876     let module C = Cic in
 877     let module R = CicReduction in
 878     let module S = CicSubstitution in
 879     let lifted_canonical_context =
 880       let rec aux i =
 881         function
 882             [] -> []
 883           | (Some (n,C.Decl t))::tl ->
 884               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 885           | (Some (n,C.Def (t,None)))::tl ->
 886               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 887           | None::tl -> None::(aux (i+1) tl)
 888           | (Some (n,C.Def (t,Some ty)))::tl ->
 889               (Some (n,
 890                      C.Def ((S.subst_meta l (S.lift i t)),
 891                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 892       in
 893         aux 1 canonical_context
 894     in
 895       try
 896         List.fold_left2
 897           (fun (l,subst,metasenv,ugraph) t ct ->
 898              match (t,ct) with
 899                  _,None ->
 900                    l @ [None],subst,metasenv,ugraph
 901                | Some t,Some (_,C.Def (ct,_)) ->
 902                    let subst',metasenv',ugraph' =
 903                    (try
 904                       fo_unif_subst subst context metasenv t ct ugraph
 905                     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))))))
 906                    in
 907                      l @ [Some t],subst',metasenv',ugraph'
 908                | Some t,Some (_,C.Decl ct) ->
 909                    let t',inferredty,subst',metasenv',ugraph1 =
 910                      type_of_aux subst metasenv context t ugraph
 911                    in
 912                    let subst'',metasenv'',ugraph2 =
 913                      (try
 914                         fo_unif_subst
 915                           subst' context metasenv' inferredty ct ugraph1
 916                       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))))))
 917                    in
 918                      l @ [Some t'], subst'',metasenv'',ugraph2
 919                | None, Some _  ->
 920                    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
 921       with
 922           Invalid_argument _ ->
 923             raise
 924             (RefineFailure
 925                (lazy (sprintf
 926                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 927                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 928                   (CicMetaSubst.ppcontext subst canonical_context))))
 929
 930   and check_exp_named_subst metasubst metasenv context tl ugraph =
 931     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 932       match tl with
 933           [] -> [],metasubst,metasenv,ugraph
 934         | ((uri,t) as subst)::tl ->
 935             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 936             let typeofvar =
 937               CicSubstitution.subst_vars substs ty_uri in
 938               (* CSC: why was this code here? it is wrong
 939                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 940                  Cic.Variable (_,Some bo,_,_) ->
 941                  raise
 942                  (RefineFailure (lazy
 943                  "A variable with a body can not be explicit substituted"))
 944                  | Cic.Variable (_,None,_,_) -> ()
 945                  | _ ->
 946                  raise
 947                  (RefineFailure (lazy
 948                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
 949                  ) ;
 950               *)
 951             let t',typeoft,metasubst',metasenv',ugraph2 =
 952               type_of_aux metasubst metasenv context t ugraph1
 953             in
 954             let metasubst'',metasenv'',ugraph3 =
 955               try
 956                 fo_unif_subst
 957                   metasubst' context metasenv' typeoft typeofvar ugraph2
 958               with _ ->
 959                 raise (RefineFailure (lazy
 960                          ("Wrong Explicit Named Substitution: " ^
 961                            CicMetaSubst.ppterm metasubst' typeoft ^
 962                           " not unifiable with " ^
 963                           CicMetaSubst.ppterm metasubst' typeofvar)))
 964             in
 965             (* FIXME: no mere tail recursive! *)
 966             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
 967               check_exp_named_subst_aux
 968                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
 969             in
 970               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
 971     in
 972       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 973
 974
 975   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
 976     let module C = Cic in
 977     let context_for_t2 = (Some (name,C.Decl s))::context in
 978     let t1'' = CicReduction.whd ~subst context t1 in
 979     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
 980       match (t1'', t2'') with
 981           (C.Sort s1, C.Sort s2)
 982             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
 983               (* different than Coq manual!!! *)
 984               C.Sort s2,subst,metasenv,ugraph
 985         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 986             let t' = CicUniv.fresh() in
 987             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
 988             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
 989               C.Sort (C.Type t'),subst,metasenv,ugraph2
 990         | (C.Sort _,C.Sort (C.Type t1)) ->
 991             C.Sort (C.Type t1),subst,metasenv,ugraph
 992         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
 993         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 994             (* TODO how can we force the meta to become a sort? If we don't we
 995              * brake the invariant that refine produce only well typed terms *)
 996             (* TODO if we check the non meta term and if it is a sort then we
 997              * are likely to know the exact value of the result e.g. if the rhs
 998              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
 999             let (metasenv,idx) =
1000               CicMkImplicit.mk_implicit_sort metasenv subst in
1001             let (subst, metasenv,ugraph1) =
1002               fo_unif_subst subst context_for_t2 metasenv
1003                 (C.Meta (idx,[])) t2'' ugraph
1004             in
1005               t2'',subst,metasenv,ugraph1
1006         | _,_ ->
1007             raise
1008               (RefineFailure
1009                 (lazy
1010                   (sprintf
1011                     ("Two sorts were expected, found %s " ^^
1012                      "(that reduces to %s) and %s (that reduces to %s)")
1013                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1014                 (CicPp.ppterm t2''))))
1015
1016   and eat_prods
1017     allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1018   =
1019     let rec mk_prod metasenv context =
1020       function
1021           [] ->
1022             let (metasenv, idx) =
1023               CicMkImplicit.mk_implicit_type metasenv subst context
1024             in
1025             let irl =
1026               CicMkImplicit.identity_relocation_list_for_metavariable context
1027             in
1028               metasenv,Cic.Meta (idx, irl)
1029         | (_,argty)::tl ->
1030             let (metasenv, idx) =
1031               CicMkImplicit.mk_implicit_type metasenv subst context
1032             in
1033             let irl =
1034               CicMkImplicit.identity_relocation_list_for_metavariable context
1035             in
1036             let meta = Cic.Meta (idx,irl) in
1037             let name =
1038               (* The name must be fresh for context.                 *)
1039               (* Nevertheless, argty is well-typed only in context.  *)
1040               (* Thus I generate a name (name_hint) in context and   *)
1041               (* then I generate a name --- using the hint name_hint *)
1042               (* --- that is fresh in (context'@context).            *)
1043               let name_hint =
1044                 (* Cic.Name "pippo" *)
1045                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1046                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1047                   (CicMetaSubst.apply_subst_context subst context)
1048                   Cic.Anonymous
1049                   ~typ:(CicMetaSubst.apply_subst subst argty)
1050               in
1051                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1052                 FreshNamesGenerator.mk_fresh_name ~subst
1053                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
1054             in
1055             let metasenv,target =
1056               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
1057             in
1058               metasenv,Cic.Prod (name,meta,target)
1059     in
1060     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1061     let (subst, metasenv,ugraph1) =
1062       try
1063         fo_unif_subst subst context metasenv hetype hetype' ugraph
1064       with exn ->
1065         debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1066                          (CicPp.ppterm hetype)
1067                          (CicPp.ppterm hetype')
1068                          (CicMetaSubst.ppmetasenv [] metasenv)
1069                          (CicMetaSubst.ppsubst subst)));
1070         raise exn
1071
1072     in
1073     let rec eat_prods metasenv subst context hetype ugraph =
1074       function
1075         | [] -> [],metasenv,subst,hetype,ugraph
1076         | (hete, hety)::tl ->
1077             (match hetype with
1078                  Cic.Prod (n,s,t) ->
1079                    let arg,subst,metasenv,ugraph1 =
1080                      try
1081                        let subst,metasenv,ugraph1 =
1082                          fo_unif_subst subst context metasenv hety s ugraph
1083                        in
1084                          hete,subst,metasenv,ugraph1
1085                      with exn when allow_coercions ->
1086                        (* we search a coercion from hety to s *)
1087                        let coer =
1088                          let carr t subst context =
1089                            CicMetaSubst.apply_subst subst t
1090                          in
1091                          let c_hety = carr hety subst context in
1092                          let c_s = carr s subst context in
1093                          CoercGraph.look_for_coercion c_hety c_s
1094                        in
1095                        match coer with
1096                        | CoercGraph.NoCoercion
1097                        | CoercGraph.NotHandled _ -> raise exn
1098                        | CoercGraph.NotMetaClosed ->
1099                            raise (Uncertain (lazy "Coercions on meta"))
1100                        | CoercGraph.SomeCoercion c ->
1101                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
1102                    in
1103                    let coerced_args,metasenv',subst',t',ugraph2 =
1104                      eat_prods metasenv subst context
1105                        (CicSubstitution.subst arg t) ugraph1 tl
1106                    in
1107                      arg::coerced_args,metasenv',subst',t',ugraph2
1108                | _ -> assert false
1109             )
1110     in
1111     let coerced_args,metasenv,subst,t,ugraph2 =
1112       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1113     in
1114       coerced_args,t,subst,metasenv,ugraph2
1115   in
1116
1117   (* eat prods ends here! *)
1118
1119   let t',ty,subst',metasenv',ugraph1 =
1120    type_of_aux [] metasenv context t ugraph
1121   in
1122   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1123   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1124     (* Andrea: ho rimesso qui l'applicazione della subst al
1125        metasenv dopo che ho droppato l'invariante che il metsaenv
1126        e' sempre istanziato *)
1127   let substituted_metasenv =
1128     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1129     (* metasenv' *)
1130     (*  substituted_t,substituted_ty,substituted_metasenv *)
1131     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1132   let cleaned_t =
1133     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1134   let cleaned_ty =
1135     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1136   let cleaned_metasenv =
1137     List.map
1138       (function (n,context,ty) ->
1139          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1140          let context' =
1141            List.map
1142              (function
1143                   None -> None
1144                 | Some (n, Cic.Decl t) ->
1145                     Some (n,
1146                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1147                 | Some (n, Cic.Def (bo,ty)) ->
1148                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1149                     let ty' =
1150                       match ty with
1151                           None -> None
1152                         | Some ty ->
1153                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1154                     in
1155                       Some (n, Cic.Def (bo',ty'))
1156              ) context
1157          in
1158            (n,context',ty')
1159       ) substituted_metasenv
1160   in
1161     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1162 ;;
1163
1164 let type_of_aux' metasenv context term ugraph =
1165   try
1166     type_of_aux' metasenv context term ugraph
1167   with
1168     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1169
1170 let undebrujin uri typesno tys t =
1171   snd
1172    (List.fold_right
1173      (fun (name,_,_,_) (i,t) ->
1174        (* here the explicit_named_substituion is assumed to be *)
1175        (* of length 0 *)
1176        let t' = Cic.MutInd (uri,i,[])  in
1177        let t = CicSubstitution.subst t' t in
1178         i - 1,t
1179      ) tys (typesno - 1,t))
1180
1181 let map_first_n n start f g l =
1182   let rec aux acc k l =
1183     if k < n then
1184       match l with
1185       | [] -> raise (Invalid_argument "map_first_n")
1186       | hd :: tl -> f hd k (aux acc (k+1) tl)
1187     else
1188       g acc l
1189   in
1190   aux start 0 l
1191
1192 (*CSC: this is a very rough approximation; to be finished *)
1193 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1194   let number_of_types = List.length tys in
1195   let subst,metasenv,ugraph,tys =
1196     List.fold_right
1197       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1198         let subst,metasenv,ugraph,cl =
1199           List.fold_right
1200             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1201                let rec aux ctx k subst = function
1202                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1203                      let subst,metasenv,ugraph,tl =
1204                        map_first_n leftno
1205                          (subst,metasenv,ugraph,[])
1206                          (fun t n (subst,metasenv,ugraph,acc) ->
1207                            let subst,metasenv,ugraph =
1208                              fo_unif_subst
1209                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1210                            in
1211                            subst,metasenv,ugraph,(t::acc))
1212                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1213                          tl
1214                      in
1215                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1216                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1217                      subst,metasenv,ugraph,t
1218                  | Cic.Prod (name,s,t) ->
1219                      let ctx = (Some (name,Cic.Decl s))::ctx in
1220                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1221                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1222                  | _ ->
1223                      raise
1224                       (RefineFailure
1225                         (lazy "not well formed constructor type"))
1226                in
1227                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1228                subst,metasenv,ugraph,(name,ty) :: acc)
1229           cl (subst,metasenv,ugraph,[])
1230         in
1231         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1232       tys ([],metasenv,ugraph,[])
1233   in
1234   let substituted_tys =
1235     List.map
1236       (fun (name,ind,arity,cl) ->
1237         let cl =
1238           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1239         in
1240         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1241       tys
1242   in
1243   metasenv,ugraph,substituted_tys
1244
1245 let typecheck metasenv uri obj =
1246  let ugraph = CicUniv.empty_ugraph in
1247  match obj with
1248     Cic.Constant (name,Some bo,ty,args,attrs) ->
1249      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1250      let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1251      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1252      let bo' = CicMetaSubst.apply_subst subst bo' in
1253      let ty' = CicMetaSubst.apply_subst subst ty' in
1254      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1255       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1256   | Cic.Constant (name,None,ty,args,attrs) ->
1257      let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1258       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1259   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1260      assert (metasenv' = metasenv);
1261      (* Here we do not check the metasenv for correctness *)
1262      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1263      let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1264      begin
1265       match sort with
1266          Cic.Sort _
1267        (* instead of raising Uncertain, let's hope that the meta will become
1268           a sort *)
1269        | Cic.Meta _ -> ()
1270        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1271      end;
1272      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1273      let bo' = CicMetaSubst.apply_subst subst bo' in
1274      let ty' = CicMetaSubst.apply_subst subst ty' in
1275      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1276       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1277   | Cic.Variable _ -> assert false (* not implemented *)
1278   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1279      (*CSC: this code is greately simplified and many many checks are missing *)
1280      (*CSC: e.g. the constructors are not required to build their own types,  *)
1281      (*CSC: the arities are not required to have as type a sort, etc.         *)
1282      let uri = match uri with Some uri -> uri | None -> assert false in
1283      let typesno = List.length tys in
1284      (* first phase: we fix only the types *)
1285      let metasenv,ugraph,tys =
1286       List.fold_right
1287        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1288          let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1289           metasenv,ugraph,(name,b,ty',cl)::res
1290        ) tys (metasenv,ugraph,[]) in
1291      let con_context =
1292       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1293      (* second phase: we fix only the constructors *)
1294      let metasenv,ugraph,tys =
1295       List.fold_right
1296        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1297          let metasenv,ugraph,cl' =
1298           List.fold_right
1299            (fun (name,ty) (metasenv,ugraph,res) ->
1300              let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1301              let ty',_,metasenv,ugraph =
1302               type_of_aux' metasenv con_context ty ugraph in
1303              let ty' = undebrujin uri typesno tys ty' in
1304               metasenv,ugraph,(name,ty')::res
1305            ) cl (metasenv,ugraph,[])
1306          in
1307           metasenv,ugraph,(name,b,ty,cl')::res
1308        ) tys (metasenv,ugraph,[]) in
1309      (* third phase: we check the positivity condition *)
1310      let metasenv,ugraph,tys =
1311        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1312      in
1313      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1314
1315 (* DEBUGGING ONLY
1316 let type_of_aux' metasenv context term =
1317  try
1318   let (t,ty,m) =
1319       type_of_aux' metasenv context term in
1320     debug_print (lazy
1321      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1322    debug_print (lazy
1323     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1324    (t,ty,m)
1325  with
1326  | RefineFailure msg as e ->
1327      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1328      raise e
1329  | Uncertain msg as e ->
1330      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1331      raise e
1332 ;; *)
1333
1334 let profiler2 = HExtlib.profile "CicRefine"
1335
1336 let type_of_aux' metasenv context term ugraph =
1337  profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
1338
1339 let typecheck metasenv uri obj =
1340  profiler2.HExtlib.profile (typecheck metasenv uri) obj