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