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