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