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