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 true 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 outtype,outtypety, subst, metasenv,ugraph4 =
 747                type_of_aux subst metasenv context outtype ugraph4
 748              in
 749              let tlbody_and_type,subst,metasenv,ugraph4 =
 750                List.fold_right
 751                  (fun x (res,subst,metasenv,ugraph) ->
 752                     let x',ty,subst',metasenv',ugraph1 =
 753                       type_of_aux subst metasenv context x ugraph
 754                     in
 755                       (x', ty)::res,subst',metasenv',ugraph1
 756                  ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
 757              in
 758              let _,_,subst,metasenv,ugraph4 =
 759                eat_prods false subst metasenv context
 760                  outtypety tlbody_and_type ugraph4
 761              in
 762              let _,_, subst, metasenv,ugraph5 =
 763                type_of_aux subst metasenv context
 764                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 765              in
 766              let (subst,metasenv,ugraph6) =
 767                List.fold_left
 768                  (fun (subst,metasenv,ugraph)
 769                         (constructor_args_no,context,instance,args) ->
 770                     let instance' =
 771                       let appl =
 772                         let outtype' =
 773                           CicSubstitution.lift constructor_args_no outtype
 774                         in
 775                           C.Appl (outtype'::args)
 776                       in
 777                         CicReduction.whd ~subst context appl
 778                     in
 779                     fo_unif_subst subst context metasenv
 780                         instance instance' ugraph)
 781                  (subst,metasenv,ugraph5) outtypeinstances
 782              in
 783                C.MutCase (uri, i, outtype, term', pl'),
 784                  CicReduction.head_beta_reduce
 785                   (CicMetaSubst.apply_subst subst
 786                    (C.Appl(outtype::right_args@[term]))),
 787                  subst,metasenv,ugraph6)
 788         | C.Fix (i,fl) ->
 789             let fl_ty',subst,metasenv,types,ugraph1 =
 790               List.fold_left
 791                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 792                    let ty',_,subst',metasenv',ugraph1 =
 793                       type_of_aux subst metasenv context ty ugraph
 794                    in
 795                      fl @ [ty'],subst',metasenv',
 796                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 797                 ) ([],subst,metasenv,[],ugraph) fl
 798             in
 799             let len = List.length types in
 800             let context' = types@context in
 801             let fl_bo',subst,metasenv,ugraph2 =
 802               List.fold_left
 803                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 804                    let metasenv, bo = exp_impl metasenv subst context' bo in
 805                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 806                      type_of_aux subst metasenv context' bo ugraph
 807                    in
 808                    let subst',metasenv',ugraph' =
 809                      fo_unif_subst subst context' metasenv
 810                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 811                    in
 812                      fl @ [bo'] , subst',metasenv',ugraph'
 813                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 814             in
 815             let ty = List.nth fl_ty' i in
 816             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 817              * and we want the new fl with bo' and ty' injected in the right
 818              * place.
 819              *)
 820             let rec map3 f l1 l2 l3 =
 821               match l1,l2,l3 with
 822               | [],[],[] -> []
 823               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 824               | _ -> assert false
 825             in
 826             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 827               fl_ty' fl_bo' fl
 828             in
 829               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 830         | C.CoFix (i,fl) ->
 831             let fl_ty',subst,metasenv,types,ugraph1 =
 832               List.fold_left
 833                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 834                    let ty',_,subst',metasenv',ugraph1 =
 835                      type_of_aux subst metasenv context ty ugraph
 836                    in
 837                      fl @ [ty'],subst',metasenv',
 838                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 839                 ) ([],subst,metasenv,[],ugraph) fl
 840             in
 841             let len = List.length types in
 842             let context' = types@context in
 843             let fl_bo',subst,metasenv,ugraph2 =
 844               List.fold_left
 845                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 846                    let metasenv, bo = exp_impl metasenv subst context' bo in
 847                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 848                      type_of_aux subst metasenv context' bo ugraph
 849                    in
 850                    let subst',metasenv',ugraph' =
 851                      fo_unif_subst subst context' metasenv
 852                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 853                    in
 854                      fl @ [bo'],subst',metasenv',ugraph'
 855                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 856             in
 857             let ty = List.nth fl_ty' i in
 858             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 859              * and we want the new fl with bo' and ty' injected in the right
 860              * place.
 861              *)
 862             let rec map3 f l1 l2 l3 =
 863               match l1,l2,l3 with
 864               | [],[],[] -> []
 865               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 866               | _ -> assert false
 867             in
 868             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 869               fl_ty' fl_bo' fl
 870             in
 871               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 872
 873   (* check_metasenv_consistency checks that the "canonical" context of a
 874      metavariable is consitent - up to relocation via the relocation list l -
 875      with the actual context *)
 876   and check_metasenv_consistency
 877     metano subst metasenv context canonical_context l ugraph
 878     =
 879     let module C = Cic in
 880     let module R = CicReduction in
 881     let module S = CicSubstitution in
 882     let lifted_canonical_context =
 883       let rec aux i =
 884         function
 885             [] -> []
 886           | (Some (n,C.Decl t))::tl ->
 887               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 888           | (Some (n,C.Def (t,None)))::tl ->
 889               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 890           | None::tl -> None::(aux (i+1) tl)
 891           | (Some (n,C.Def (t,Some ty)))::tl ->
 892               (Some (n,
 893                      C.Def ((S.subst_meta l (S.lift i t)),
 894                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 895       in
 896         aux 1 canonical_context
 897     in
 898       try
 899         List.fold_left2
 900           (fun (l,subst,metasenv,ugraph) t ct ->
 901              match (t,ct) with
 902                  _,None ->
 903                    l @ [None],subst,metasenv,ugraph
 904                | Some t,Some (_,C.Def (ct,_)) ->
 905                    let subst',metasenv',ugraph' =
 906                    (try
 907                       fo_unif_subst subst context metasenv t ct ugraph
 908                     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))))))
 909                    in
 910                      l @ [Some t],subst',metasenv',ugraph'
 911                | Some t,Some (_,C.Decl ct) ->
 912                    let t',inferredty,subst',metasenv',ugraph1 =
 913                      type_of_aux subst metasenv context t ugraph
 914                    in
 915                    let subst'',metasenv'',ugraph2 =
 916                      (try
 917                         fo_unif_subst
 918                           subst' context metasenv' inferredty ct ugraph1
 919                       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))))))
 920                    in
 921                      l @ [Some t'], subst'',metasenv'',ugraph2
 922                | None, Some _  ->
 923                    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
 924       with
 925           Invalid_argument _ ->
 926             raise
 927             (RefineFailure
 928                (lazy (sprintf
 929                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 930                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 931                   (CicMetaSubst.ppcontext subst canonical_context))))
 932
 933   and check_exp_named_subst metasubst metasenv context tl ugraph =
 934     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 935       match tl with
 936           [] -> [],metasubst,metasenv,ugraph
 937         | ((uri,t) as subst)::tl ->
 938             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 939             let typeofvar =
 940               CicSubstitution.subst_vars substs ty_uri in
 941               (* CSC: why was this code here? it is wrong
 942                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 943                  Cic.Variable (_,Some bo,_,_) ->
 944                  raise
 945                  (RefineFailure (lazy
 946                  "A variable with a body can not be explicit substituted"))
 947                  | Cic.Variable (_,None,_,_) -> ()
 948                  | _ ->
 949                  raise
 950                  (RefineFailure (lazy
 951                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
 952                  ) ;
 953               *)
 954             let t',typeoft,metasubst',metasenv',ugraph2 =
 955               type_of_aux metasubst metasenv context t ugraph1
 956             in
 957             let metasubst'',metasenv'',ugraph3 =
 958               try
 959                 fo_unif_subst
 960                   metasubst' context metasenv' typeoft typeofvar ugraph2
 961               with _ ->
 962                 raise (RefineFailure (lazy
 963                          ("Wrong Explicit Named Substitution: " ^
 964                            CicMetaSubst.ppterm metasubst' typeoft ^
 965                           " not unifiable with " ^
 966                           CicMetaSubst.ppterm metasubst' typeofvar)))
 967             in
 968             (* FIXME: no mere tail recursive! *)
 969             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
 970               check_exp_named_subst_aux
 971                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
 972             in
 973               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
 974     in
 975       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 976
 977
 978   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
 979     let module C = Cic in
 980     let context_for_t2 = (Some (name,C.Decl s))::context in
 981     let t1'' = CicReduction.whd ~subst context t1 in
 982     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
 983       match (t1'', t2'') with
 984           (C.Sort s1, C.Sort s2)
 985             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
 986               (* different than Coq manual!!! *)
 987               C.Sort s2,subst,metasenv,ugraph
 988         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 989             let t' = CicUniv.fresh() in
 990             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
 991             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
 992               C.Sort (C.Type t'),subst,metasenv,ugraph2
 993         | (C.Sort _,C.Sort (C.Type t1)) ->
 994             C.Sort (C.Type t1),subst,metasenv,ugraph
 995         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
 996         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 997             (* TODO how can we force the meta to become a sort? If we don't we
 998              * brake the invariant that refine produce only well typed terms *)
 999             (* TODO if we check the non meta term and if it is a sort then we
1000              * are likely to know the exact value of the result e.g. if the rhs
1001              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
1002             let (metasenv,idx) =
1003               CicMkImplicit.mk_implicit_sort metasenv subst in
1004             let (subst, metasenv,ugraph1) =
1005               fo_unif_subst subst context_for_t2 metasenv
1006                 (C.Meta (idx,[])) t2'' ugraph
1007             in
1008               t2'',subst,metasenv,ugraph1
1009         | _,_ ->
1010             raise
1011               (RefineFailure
1012                 (lazy
1013                   (sprintf
1014                     ("Two sorts were expected, found %s " ^^
1015                      "(that reduces to %s) and %s (that reduces to %s)")
1016                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
1017                 (CicPp.ppterm t2''))))
1018
1019   and eat_prods
1020     allow_coercions subst metasenv context hetype tlbody_and_type ugraph
1021   =
1022     let rec mk_prod metasenv context =
1023       function
1024           [] ->
1025             let (metasenv, idx) =
1026               CicMkImplicit.mk_implicit_type metasenv subst context
1027             in
1028             let irl =
1029               CicMkImplicit.identity_relocation_list_for_metavariable context
1030             in
1031               metasenv,Cic.Meta (idx, irl)
1032         | (_,argty)::tl ->
1033             let (metasenv, idx) =
1034               CicMkImplicit.mk_implicit_type metasenv subst context
1035             in
1036             let irl =
1037               CicMkImplicit.identity_relocation_list_for_metavariable context
1038             in
1039             let meta = Cic.Meta (idx,irl) in
1040             let name =
1041               (* The name must be fresh for context.                 *)
1042               (* Nevertheless, argty is well-typed only in context.  *)
1043               (* Thus I generate a name (name_hint) in context and   *)
1044               (* then I generate a name --- using the hint name_hint *)
1045               (* --- that is fresh in (context'@context).            *)
1046               let name_hint =
1047                 (* Cic.Name "pippo" *)
1048                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
1049                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
1050                   (CicMetaSubst.apply_subst_context subst context)
1051                   Cic.Anonymous
1052                   ~typ:(CicMetaSubst.apply_subst subst argty)
1053               in
1054                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
1055                 FreshNamesGenerator.mk_fresh_name ~subst
1056                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
1057             in
1058             let metasenv,target =
1059               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
1060             in
1061               metasenv,Cic.Prod (name,meta,target)
1062     in
1063     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
1064     let (subst, metasenv,ugraph1) =
1065       try
1066         fo_unif_subst subst context metasenv hetype hetype' ugraph
1067       with exn ->
1068         debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
1069                          (CicPp.ppterm hetype)
1070                          (CicPp.ppterm hetype')
1071                          (CicMetaSubst.ppmetasenv [] metasenv)
1072                          (CicMetaSubst.ppsubst subst)));
1073         raise exn
1074
1075     in
1076     let rec eat_prods metasenv subst context hetype ugraph =
1077       function
1078         | [] -> [],metasenv,subst,hetype,ugraph
1079         | (hete, hety)::tl ->
1080             (match hetype with
1081                  Cic.Prod (n,s,t) ->
1082                    let arg,subst,metasenv,ugraph1 =
1083                      try
1084                        let subst,metasenv,ugraph1 =
1085                          fo_unif_subst subst context metasenv hety s ugraph
1086                        in
1087                          hete,subst,metasenv,ugraph1
1088                      with exn when allow_coercions ->
1089                        (* we search a coercion from hety to s *)
1090                        let coer =
1091                          let carr t subst context =
1092                            CicMetaSubst.apply_subst subst t
1093                          in
1094                          let c_hety = carr hety subst context in
1095                          let c_s = carr s subst context in
1096                          CoercGraph.look_for_coercion c_hety c_s
1097                        in
1098                        match coer with
1099                        | CoercGraph.NoCoercion
1100                        | CoercGraph.NotHandled _ -> raise exn
1101                        | CoercGraph.NotMetaClosed ->
1102                            raise (Uncertain (lazy "Coercions on meta"))
1103                        | CoercGraph.SomeCoercion c ->
1104                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
1105                    in
1106                    let coerced_args,metasenv',subst',t',ugraph2 =
1107                      eat_prods metasenv subst context
1108                        (* (CicMetaSubst.subst subst hete t) tl *)
1109                        (CicSubstitution.subst hete t) ugraph1 tl
1110                    in
1111                      arg::coerced_args,metasenv',subst',t',ugraph2
1112                | _ -> assert false
1113             )
1114     in
1115     let coerced_args,metasenv,subst,t,ugraph2 =
1116       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1117     in
1118       coerced_args,t,subst,metasenv,ugraph2
1119   in
1120
1121   (* eat prods ends here! *)
1122
1123   let t',ty,subst',metasenv',ugraph1 =
1124    type_of_aux [] metasenv context t ugraph
1125   in
1126   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1127   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1128     (* Andrea: ho rimesso qui l'applicazione della subst al
1129        metasenv dopo che ho droppato l'invariante che il metsaenv
1130        e' sempre istanziato *)
1131   let substituted_metasenv =
1132     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1133     (* metasenv' *)
1134     (*  substituted_t,substituted_ty,substituted_metasenv *)
1135     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1136   let cleaned_t =
1137     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1138   let cleaned_ty =
1139     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1140   let cleaned_metasenv =
1141     List.map
1142       (function (n,context,ty) ->
1143          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1144          let context' =
1145            List.map
1146              (function
1147                   None -> None
1148                 | Some (n, Cic.Decl t) ->
1149                     Some (n,
1150                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1151                 | Some (n, Cic.Def (bo,ty)) ->
1152                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1153                     let ty' =
1154                       match ty with
1155                           None -> None
1156                         | Some ty ->
1157                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1158                     in
1159                       Some (n, Cic.Def (bo',ty'))
1160              ) context
1161          in
1162            (n,context',ty')
1163       ) substituted_metasenv
1164   in
1165     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1166 ;;
1167
1168 let type_of_aux' metasenv context term ugraph =
1169   try
1170     type_of_aux' metasenv context term ugraph
1171   with
1172     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1173
1174 let undebrujin uri typesno tys t =
1175   snd
1176    (List.fold_right
1177      (fun (name,_,_,_) (i,t) ->
1178        (* here the explicit_named_substituion is assumed to be *)
1179        (* of length 0 *)
1180        let t' = Cic.MutInd (uri,i,[])  in
1181        let t = CicSubstitution.subst t' t in
1182         i - 1,t
1183      ) tys (typesno - 1,t))
1184
1185 let map_first_n n start f g l =
1186   let rec aux acc k l =
1187     if k < n then
1188       match l with
1189       | [] -> raise (Invalid_argument "map_first_n")
1190       | hd :: tl -> f hd k (aux acc (k+1) tl)
1191     else
1192       g acc l
1193   in
1194   aux start 0 l
1195
1196 (*CSC: this is a very rough approximation; to be finished *)
1197 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1198   let number_of_types = List.length tys in
1199   let subst,metasenv,ugraph,tys =
1200     List.fold_right
1201       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1202         let subst,metasenv,ugraph,cl =
1203           List.fold_right
1204             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1205                let rec aux ctx k subst = function
1206                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1207                      let subst,metasenv,ugraph,tl =
1208                        map_first_n leftno
1209                          (subst,metasenv,ugraph,[])
1210                          (fun t n (subst,metasenv,ugraph,acc) ->
1211                            let subst,metasenv,ugraph =
1212                              fo_unif_subst
1213                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1214                            in
1215                            subst,metasenv,ugraph,(t::acc))
1216                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1217                          tl
1218                      in
1219                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1220                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1221                      subst,metasenv,ugraph,t
1222                  | Cic.Prod (name,s,t) ->
1223                      let ctx = (Some (name,Cic.Decl s))::ctx in
1224                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1225                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1226                  | _ ->
1227                      raise
1228                       (RefineFailure
1229                         (lazy "not well formed constructor type"))
1230                in
1231                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1232                subst,metasenv,ugraph,(name,ty) :: acc)
1233           cl (subst,metasenv,ugraph,[])
1234         in
1235         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1236       tys ([],metasenv,ugraph,[])
1237   in
1238   let substituted_tys =
1239     List.map
1240       (fun (name,ind,arity,cl) ->
1241         let cl =
1242           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1243         in
1244         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1245       tys
1246   in
1247   metasenv,ugraph,substituted_tys
1248
1249 let typecheck metasenv uri obj =
1250  let ugraph = CicUniv.empty_ugraph in
1251  match obj with
1252     Cic.Constant (name,Some bo,ty,args,attrs) ->
1253      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1254      let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1255      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1256      let bo' = CicMetaSubst.apply_subst subst bo' in
1257      let ty' = CicMetaSubst.apply_subst subst ty' in
1258      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1259       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1260   | Cic.Constant (name,None,ty,args,attrs) ->
1261      let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1262       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1263   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1264      assert (metasenv' = metasenv);
1265      (* Here we do not check the metasenv for correctness *)
1266      let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
1267      let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1268      begin
1269       match sort with
1270          Cic.Sort _
1271        (* instead of raising Uncertain, let's hope that the meta will become
1272           a sort *)
1273        | Cic.Meta _ -> ()
1274        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1275      end;
1276      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1277      let bo' = CicMetaSubst.apply_subst subst bo' in
1278      let ty' = CicMetaSubst.apply_subst subst ty' in
1279      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1280       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1281   | Cic.Variable _ -> assert false (* not implemented *)
1282   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1283      (*CSC: this code is greately simplified and many many checks are missing *)
1284      (*CSC: e.g. the constructors are not required to build their own types,  *)
1285      (*CSC: the arities are not required to have as type a sort, etc.         *)
1286      let uri = match uri with Some uri -> uri | None -> assert false in
1287      let typesno = List.length tys in
1288      (* first phase: we fix only the types *)
1289      let metasenv,ugraph,tys =
1290       List.fold_right
1291        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1292          let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
1293           metasenv,ugraph,(name,b,ty',cl)::res
1294        ) tys (metasenv,ugraph,[]) in
1295      let con_context =
1296       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1297      (* second phase: we fix only the constructors *)
1298      let metasenv,ugraph,tys =
1299       List.fold_right
1300        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1301          let metasenv,ugraph,cl' =
1302           List.fold_right
1303            (fun (name,ty) (metasenv,ugraph,res) ->
1304              let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1305              let ty',_,metasenv,ugraph =
1306               type_of_aux' metasenv con_context ty ugraph in
1307              let ty' = undebrujin uri typesno tys ty' in
1308               metasenv,ugraph,(name,ty')::res
1309            ) cl (metasenv,ugraph,[])
1310          in
1311           metasenv,ugraph,(name,b,ty,cl')::res
1312        ) tys (metasenv,ugraph,[]) in
1313      (* third phase: we check the positivity condition *)
1314      let metasenv,ugraph,tys =
1315        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1316      in
1317      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1318
1319 (* DEBUGGING ONLY
1320 let type_of_aux' metasenv context term =
1321  try
1322   let (t,ty,m) =
1323       type_of_aux' metasenv context term in
1324     debug_print (lazy
1325      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1326    debug_print (lazy
1327     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1328    (t,ty,m)
1329  with
1330  | RefineFailure msg as e ->
1331      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1332      raise e
1333  | Uncertain msg as e ->
1334      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1335      raise e
1336 ;; *)
1337
1338 let profiler2 = HExtlib.profile "CicRefine"
1339
1340 let type_of_aux' metasenv context term ugraph =
1341  profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
1342
1343 let typecheck metasenv uri obj =
1344  profiler2.HExtlib.profile (typecheck metasenv uri) obj