helm/ocaml/cic_unification/cicRefine.ml

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