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