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