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      let (t',_,_,_,_) as res =
 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                     (x', ty)::res,subst',metasenv',ugraph1
 396                 ) tl ([],subst',metasenv',ugraph1)
 397             in
 398             let tl',applty,subst''',metasenv''',ugraph3 =
 399               eat_prods true subst'' metasenv'' context
 400                 hetype tlbody_and_type ugraph2
 401             in
 402               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
 403         | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
 404         | C.Const (uri,exp_named_subst) ->
 405             let exp_named_subst',subst',metasenv',ugraph1 =
 406               check_exp_named_subst subst metasenv context
 407                 exp_named_subst ugraph in
 408             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 409             let cty =
 410               CicSubstitution.subst_vars exp_named_subst' ty_uri
 411             in
 412               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 413         | C.MutInd (uri,i,exp_named_subst) ->
 414             let exp_named_subst',subst',metasenv',ugraph1 =
 415               check_exp_named_subst subst metasenv context
 416                 exp_named_subst ugraph
 417             in
 418             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 419             let cty =
 420               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 421               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 422         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 423             let exp_named_subst',subst',metasenv',ugraph1 =
 424               check_exp_named_subst subst metasenv context
 425                 exp_named_subst ugraph
 426             in
 427             let ty_uri,ugraph2 =
 428               type_of_mutual_inductive_constr uri i j ugraph1
 429             in
 430             let cty =
 431               CicSubstitution.subst_vars exp_named_subst' ty_uri
 432             in
 433               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 434                 metasenv',ugraph2
 435         | C.MutCase (uri, i, outtype, term, pl) ->
 436             (* first, get the inductive type (and noparams)
 437              * in the environment  *)
 438             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 439               let _ = CicTypeChecker.typecheck uri in
 440               let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
 441               match obj with
 442                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 443                     List.nth l i , expl_params, parsno, u
 444                 | _ ->
 445                     raise
 446                       (RefineFailure
 447                          (lazy ("Unkown mutual inductive definition " ^
 448                          U.string_of_uri uri)))
 449            in
 450            let rec count_prod t =
 451              match CicReduction.whd ~subst context t with
 452                  C.Prod (_, _, t) -> 1 + (count_prod t)
 453                | _ -> 0
 454            in
 455            let no_args = count_prod arity in
 456              (* now, create a "generic" MutInd *)
 457            let metasenv,left_args =
 458              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 459            in
 460            let metasenv,right_args =
 461              let no_right_params = no_args - no_left_params in
 462                if no_right_params < 0 then assert false
 463                else CicMkImplicit.n_fresh_metas
 464                       metasenv subst context no_right_params
 465            in
 466            let metasenv,exp_named_subst =
 467              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 468            let expected_type =
 469              if no_args = 0 then
 470                C.MutInd (uri,i,exp_named_subst)
 471              else
 472                C.Appl
 473                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 474            in
 475              (* check consistency with the actual type of term *)
 476            let term',actual_type,subst,metasenv,ugraph1 =
 477              type_of_aux subst metasenv context term ugraph in
 478            let expected_type',_, subst, metasenv,ugraph2 =
 479              type_of_aux subst metasenv context expected_type ugraph1
 480            in
 481            let actual_type = CicReduction.whd ~subst context actual_type in
 482            let subst,metasenv,ugraph3 =
 483              fo_unif_subst subst context metasenv
 484                expected_type' actual_type ugraph2
 485            in
 486            let rec instantiate_prod t =
 487             function
 488                [] -> t
 489              | he::tl ->
 490                 match CicReduction.whd ~subst context t with
 491                    C.Prod (_,_,t') ->
 492                     instantiate_prod (CicSubstitution.subst he t') tl
 493                  | _ -> assert false
 494            in
 495            let arity_instantiated_with_left_args =
 496             instantiate_prod arity left_args in
 497              (* TODO: check if the sort elimination
 498               * is allowed: [(I q1 ... qr)|B] *)
 499            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 500              List.fold_left
 501                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
 502                   let constructor =
 503                     if left_args = [] then
 504                       (C.MutConstruct (uri,i,j,exp_named_subst))
 505                     else
 506                       (C.Appl
 507                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 508                   in
 509                   let p',actual_type,subst,metasenv,ugraph1 =
 510                     type_of_aux subst metasenv context p ugraph
 511                   in
 512                   let constructor',expected_type, subst, metasenv,ugraph2 =
 513                     type_of_aux subst metasenv context constructor ugraph1
 514                   in
 515                   let outtypeinstance,subst,metasenv,ugraph3 =
 516                     check_branch 0 context metasenv subst no_left_params
 517                       actual_type constructor' expected_type ugraph2
 518                   in
 519                     (pl @ [p'],j+1,
 520                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 521                ([],1,[],subst,metasenv,ugraph3) pl
 522            in
 523
 524              (* we are left to check that the outype matches his instances.
 525                 The easy case is when the outype is specified, that amount
 526                 to a trivial check. Otherwise, we should guess a type from
 527                 its instances
 528              *)
 529
 530            let outtype,outtypety, subst, metasenv,ugraph4 =
 531              type_of_aux subst metasenv context outtype ugraph4 in
 532            (match outtype with
 533            | C.Meta (n,l) ->
 534                (let candidate,ugraph5,metasenv,subst =
 535                  let exp_name_subst, metasenv =
 536                     let o,_ =
 537                       CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 538                     in
 539                     let uris = CicUtil.params_of_obj o in
 540                     List.fold_right (
 541                       fun uri (acc,metasenv) ->
 542                         let metasenv',new_meta =
 543                            CicMkImplicit.mk_implicit metasenv subst context
 544                         in
 545                         let irl =
 546                           CicMkImplicit.identity_relocation_list_for_metavariable
 547                             context
 548                         in
 549                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 550                     ) uris ([],metasenv)
 551                  in
 552                  let ty =
 553                   match left_args,right_args with
 554                      [],[] -> Cic.MutInd(uri, i, exp_name_subst)
 555                    | _,_ ->
 556                       let rec mk_right_args =
 557                        function
 558                           0 -> []
 559                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
 560                       in
 561                       let right_args_no = List.length right_args in
 562                       let lifted_left_args =
 563                        List.map (CicSubstitution.lift right_args_no) left_args
 564                       in
 565                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
 566                         (lifted_left_args @ mk_right_args right_args_no))
 567                  in
 568                  let fresh_name =
 569                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 570                      context Cic.Anonymous ~typ:ty
 571                  in
 572                  match outtypeinstances with
 573                  | [] ->
 574                      let extended_context =
 575                       let rec add_right_args =
 576                        function
 577                           Cic.Prod (name,ty,t) ->
 578                            Some (name,Cic.Decl ty)::(add_right_args t)
 579                         | _ -> []
 580                       in
 581                        (Some (fresh_name,Cic.Decl ty))::
 582                        (List.rev
 583                         (add_right_args arity_instantiated_with_left_args))@
 584                        context
 585                      in
 586                      let metasenv,new_meta =
 587                        CicMkImplicit.mk_implicit metasenv subst extended_context
 588                      in
 589                        let irl =
 590                        CicMkImplicit.identity_relocation_list_for_metavariable
 591                          extended_context
 592                      in
 593                      let rec add_lambdas b =
 594                       function
 595                          Cic.Prod (name,ty,t) ->
 596                           Cic.Lambda (name,ty,(add_lambdas b t))
 597                        | _ -> Cic.Lambda (fresh_name, ty, b)
 598                      in
 599                      let candidate =
 600                       add_lambdas (Cic.Meta (new_meta,irl))
 601                        arity_instantiated_with_left_args
 602                      in
 603                      (Some candidate),ugraph4,metasenv,subst
 604                  | (constructor_args_no,_,instance,_)::tl ->
 605                      try
 606                        let instance',subst,metasenv =
 607                          CicMetaSubst.delift_rels subst metasenv
 608                           constructor_args_no instance
 609                        in
 610                        let candidate,ugraph,metasenv,subst =
 611                          List.fold_left (
 612                            fun (candidate_oty,ugraph,metasenv,subst)
 613                              (constructor_args_no,_,instance,_) ->
 614                                match candidate_oty with
 615                                | None -> None,ugraph,metasenv,subst
 616                                | Some ty ->
 617                                  try
 618                                    let instance',subst,metasenv =
 619                                      CicMetaSubst.delift_rels subst metasenv
 620                                       constructor_args_no instance
 621                                    in
 622                                    let subst,metasenv,ugraph =
 623                                     fo_unif_subst subst context metasenv
 624                                       instance' ty ugraph
 625                                    in
 626                                     candidate_oty,ugraph,metasenv,subst
 627                                  with
 628                                     CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
 629                                   | CicUnification.UnificationFailure _
 630                                   | CicUnification.Uncertain _ ->
 631                                      None,ugraph,metasenv,subst
 632                          ) (Some instance',ugraph4,metasenv,subst) tl
 633                        in
 634                        match candidate with
 635                        | None -> None, ugraph,metasenv,subst
 636                        | Some t ->
 637                           let rec add_lambdas n b =
 638                            function
 639                               Cic.Prod (name,ty,t) ->
 640                                Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
 641                             | _ ->
 642                               Cic.Lambda (fresh_name, ty,
 643                                CicSubstitution.lift (n + 1) t)
 644                           in
 645                            Some
 646                             (add_lambdas 0 t arity_instantiated_with_left_args),
 647                            ugraph,metasenv,subst
 648                      with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
 649                        None,ugraph4,metasenv,subst
 650                in
 651                match candidate with
 652                | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
 653                | Some candidate ->
 654                    let subst,metasenv,ugraph =
 655                      fo_unif_subst subst context metasenv
 656                        candidate outtype ugraph5
 657                    in
 658                      C.MutCase (uri, i, outtype, term', pl'),
 659                       CicReduction.head_beta_reduce
 660                        (CicMetaSubst.apply_subst subst
 661                         (Cic.Appl (outtype::right_args@[term']))),
 662                      subst,metasenv,ugraph)
 663            | _ ->    (* easy case *)
 664              let tlbody_and_type,subst,metasenv,ugraph4 =
 665                List.fold_right
 666                  (fun x (res,subst,metasenv,ugraph) ->
 667                     let x',ty,subst',metasenv',ugraph1 =
 668                       type_of_aux subst metasenv context x ugraph
 669                     in
 670                       (x', ty)::res,subst',metasenv',ugraph1
 671                  ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
 672              in
 673              let _,_,subst,metasenv,ugraph4 =
 674                eat_prods false subst metasenv context
 675                  outtypety tlbody_and_type ugraph4
 676              in
 677              let _,_, subst, metasenv,ugraph5 =
 678                type_of_aux subst metasenv context
 679                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 680              in
 681              let (subst,metasenv,ugraph6) =
 682                List.fold_left
 683                  (fun (subst,metasenv,ugraph)
 684                         (constructor_args_no,context,instance,args) ->
 685                     let instance' =
 686                       let appl =
 687                         let outtype' =
 688                           CicSubstitution.lift constructor_args_no outtype
 689                         in
 690                           C.Appl (outtype'::args)
 691                       in
 692                         CicReduction.whd ~subst context appl
 693                     in
 694                     fo_unif_subst subst context metasenv
 695                         instance instance' ugraph)
 696                  (subst,metasenv,ugraph5) outtypeinstances
 697              in
 698                C.MutCase (uri, i, outtype, term', pl'),
 699                  CicReduction.head_beta_reduce
 700                   (CicMetaSubst.apply_subst subst
 701                    (C.Appl(outtype::right_args@[term]))),
 702                  subst,metasenv,ugraph6)
 703         | C.Fix (i,fl) ->
 704             let fl_ty',subst,metasenv,types,ugraph1 =
 705               List.fold_left
 706                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 707                    let ty',_,subst',metasenv',ugraph1 =
 708                       type_of_aux subst metasenv context ty ugraph
 709                    in
 710                      fl @ [ty'],subst',metasenv',
 711                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 712                 ) ([],subst,metasenv,[],ugraph) fl
 713             in
 714             let len = List.length types in
 715             let context' = types@context in
 716             let fl_bo',subst,metasenv,ugraph2 =
 717               List.fold_left
 718                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
 719                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 720                      type_of_aux subst metasenv context' bo ugraph
 721                    in
 722                    let subst',metasenv',ugraph' =
 723                      fo_unif_subst subst context' metasenv
 724                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 725                    in
 726                      fl @ [bo'] , subst',metasenv',ugraph'
 727                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 728             in
 729             let ty = List.nth fl_ty' i in
 730             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 731              * and we want the new fl with bo' and ty' injected in the right
 732              * place.
 733              *)
 734             let rec map3 f l1 l2 l3 =
 735               match l1,l2,l3 with
 736               | [],[],[] -> []
 737               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 738               | _ -> assert false
 739             in
 740             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 741               fl_ty' fl_bo' fl
 742             in
 743               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 744         | C.CoFix (i,fl) ->
 745             let fl_ty',subst,metasenv,types,ugraph1 =
 746               List.fold_left
 747                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 748                    let ty',_,subst',metasenv',ugraph1 =
 749                      type_of_aux subst metasenv context ty ugraph
 750                    in
 751                      fl @ [ty'],subst',metasenv',
 752                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 753                 ) ([],subst,metasenv,[],ugraph) fl
 754             in
 755             let len = List.length types in
 756             let context' = types@context in
 757             let fl_bo',subst,metasenv,ugraph2 =
 758               List.fold_left
 759                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
 760                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 761                      type_of_aux subst metasenv context' bo ugraph
 762                    in
 763                    let subst',metasenv',ugraph' =
 764                      fo_unif_subst subst context' metasenv
 765                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 766                    in
 767                      fl @ [bo'],subst',metasenv',ugraph'
 768                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
 769             in
 770             let ty = List.nth fl_ty' i in
 771             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 772              * and we want the new fl with bo' and ty' injected in the right
 773              * place.
 774              *)
 775             let rec map3 f l1 l2 l3 =
 776               match l1,l2,l3 with
 777               | [],[],[] -> []
 778               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 779               | _ -> assert false
 780             in
 781             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 782               fl_ty' fl_bo' fl
 783             in
 784               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 785      in
 786       relocalize localization_tbl t t';
 787       res
 788
 789   (* check_metasenv_consistency checks that the "canonical" context of a
 790      metavariable is consitent - up to relocation via the relocation list l -
 791      with the actual context *)
 792   and check_metasenv_consistency
 793     metano subst metasenv context canonical_context l ugraph
 794     =
 795     let module C = Cic in
 796     let module R = CicReduction in
 797     let module S = CicSubstitution in
 798     let lifted_canonical_context =
 799       let rec aux i =
 800         function
 801             [] -> []
 802           | (Some (n,C.Decl t))::tl ->
 803               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 804           | (Some (n,C.Def (t,None)))::tl ->
 805               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 806           | None::tl -> None::(aux (i+1) tl)
 807           | (Some (n,C.Def (t,Some ty)))::tl ->
 808               (Some (n,
 809                      C.Def ((S.subst_meta l (S.lift i t)),
 810                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 811       in
 812         aux 1 canonical_context
 813     in
 814       try
 815         List.fold_left2
 816           (fun (l,subst,metasenv,ugraph) t ct ->
 817              match (t,ct) with
 818                  _,None ->
 819                    l @ [None],subst,metasenv,ugraph
 820                | Some t,Some (_,C.Def (ct,_)) ->
 821                    let subst',metasenv',ugraph' =
 822                    (try
 823                       fo_unif_subst subst context metasenv t ct ugraph
 824                     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))))))
 825                    in
 826                      l @ [Some t],subst',metasenv',ugraph'
 827                | Some t,Some (_,C.Decl ct) ->
 828                    let t',inferredty,subst',metasenv',ugraph1 =
 829                      type_of_aux subst metasenv context t ugraph
 830                    in
 831                    let subst'',metasenv'',ugraph2 =
 832                      (try
 833                         fo_unif_subst
 834                           subst' context metasenv' inferredty ct ugraph1
 835                       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))))))
 836                    in
 837                      l @ [Some t'], subst'',metasenv'',ugraph2
 838                | None, Some _  ->
 839                    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
 840       with
 841           Invalid_argument _ ->
 842             raise
 843             (RefineFailure
 844                (lazy (sprintf
 845                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 846                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 847                   (CicMetaSubst.ppcontext subst canonical_context))))
 848
 849   and check_exp_named_subst metasubst metasenv context tl ugraph =
 850     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 851       match tl with
 852           [] -> [],metasubst,metasenv,ugraph
 853         | (uri,t)::tl ->
 854             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 855             let typeofvar =
 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 subst,metasenv,ugraph,tys =
1126     List.fold_right
1127       (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
1128         let subst,metasenv,ugraph,cl =
1129           List.fold_right
1130             (fun (name,ty) (subst,metasenv,ugraph,acc) ->
1131                let rec aux ctx k subst = function
1132                  | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
1133                      let subst,metasenv,ugraph,tl =
1134                        map_first_n leftno
1135                          (subst,metasenv,ugraph,[])
1136                          (fun t n (subst,metasenv,ugraph,acc) ->
1137                            let subst,metasenv,ugraph =
1138                              fo_unif_subst
1139                                subst ctx metasenv t (Cic.Rel (k-n)) ugraph
1140                            in
1141                            subst,metasenv,ugraph,(t::acc))
1142                          (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
1143                          tl
1144                      in
1145                      subst,metasenv,ugraph,(Cic.Appl (hd::tl))
1146                  | Cic.MutInd(uri',_,_) as t when uri = uri'->
1147                      subst,metasenv,ugraph,t
1148                  | Cic.Prod (name,s,t) ->
1149                      let ctx = (Some (name,Cic.Decl s))::ctx in
1150                      let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
1151                      subst,metasenv,ugraph,Cic.Prod (name,s,t)
1152                  | _ ->
1153                      raise
1154                       (RefineFailure
1155                         (lazy "not well formed constructor type"))
1156                in
1157                let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
1158                subst,metasenv,ugraph,(name,ty) :: acc)
1159           cl (subst,metasenv,ugraph,[])
1160         in
1161         subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
1162       tys ([],metasenv,ugraph,[])
1163   in
1164   let substituted_tys =
1165     List.map
1166       (fun (name,ind,arity,cl) ->
1167         let cl =
1168           List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
1169         in
1170         name,ind,CicMetaSubst.apply_subst subst arity,cl)
1171       tys
1172   in
1173   metasenv,ugraph,substituted_tys
1174
1175 let typecheck metasenv uri obj ~localization_tbl =
1176  let ugraph = CicUniv.empty_ugraph in
1177  match obj with
1178     Cic.Constant (name,Some bo,ty,args,attrs) ->
1179      let bo',boty,metasenv,ugraph =
1180       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1181      let ty',_,metasenv,ugraph =
1182       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1183      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1184      let bo' = CicMetaSubst.apply_subst subst bo' in
1185      let ty' = CicMetaSubst.apply_subst subst ty' in
1186      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1187       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
1188   | Cic.Constant (name,None,ty,args,attrs) ->
1189      let ty',_,metasenv,ugraph =
1190       type_of_aux' ~localization_tbl metasenv [] ty ugraph
1191      in
1192       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
1193   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
1194      assert (metasenv' = metasenv);
1195      (* Here we do not check the metasenv for correctness *)
1196      let bo',boty,metasenv,ugraph =
1197       type_of_aux' ~localization_tbl metasenv [] bo ugraph in
1198      let ty',sort,metasenv,ugraph =
1199       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
1200      begin
1201       match sort with
1202          Cic.Sort _
1203        (* instead of raising Uncertain, let's hope that the meta will become
1204           a sort *)
1205        | Cic.Meta _ -> ()
1206        | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
1207      end;
1208      let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
1209      let bo' = CicMetaSubst.apply_subst subst bo' in
1210      let ty' = CicMetaSubst.apply_subst subst ty' in
1211      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
1212       Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
1213   | Cic.Variable _ -> assert false (* not implemented *)
1214   | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
1215      (*CSC: this code is greately simplified and many many checks are missing *)
1216      (*CSC: e.g. the constructors are not required to build their own types,  *)
1217      (*CSC: the arities are not required to have as type a sort, etc.         *)
1218      let uri = match uri with Some uri -> uri | None -> assert false in
1219      let typesno = List.length tys in
1220      (* first phase: we fix only the types *)
1221      let metasenv,ugraph,tys =
1222       List.fold_right
1223        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1224          let ty',_,metasenv,ugraph =
1225           type_of_aux' ~localization_tbl metasenv [] ty ugraph
1226          in
1227           metasenv,ugraph,(name,b,ty',cl)::res
1228        ) tys (metasenv,ugraph,[]) in
1229      let con_context =
1230       List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
1231      (* second phase: we fix only the constructors *)
1232      let metasenv,ugraph,tys =
1233       List.fold_right
1234        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
1235          let metasenv,ugraph,cl' =
1236           List.fold_right
1237            (fun (name,ty) (metasenv,ugraph,res) ->
1238              let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
1239              let ty',_,metasenv,ugraph =
1240               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
1241              let ty' = undebrujin uri typesno tys ty' in
1242               metasenv,ugraph,(name,ty')::res
1243            ) cl (metasenv,ugraph,[])
1244          in
1245           metasenv,ugraph,(name,b,ty,cl')::res
1246        ) tys (metasenv,ugraph,[]) in
1247      (* third phase: we check the positivity condition *)
1248      let metasenv,ugraph,tys =
1249        are_all_occurrences_positive metasenv ugraph uri tys paramsno
1250      in
1251      Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
1252
1253 (* DEBUGGING ONLY
1254 let type_of_aux' metasenv context term =
1255  try
1256   let (t,ty,m) =
1257       type_of_aux' metasenv context term in
1258     debug_print (lazy
1259      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
1260    debug_print (lazy
1261     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
1262    (t,ty,m)
1263  with
1264  | RefineFailure msg as e ->
1265      debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
1266      raise e
1267  | Uncertain msg as e ->
1268      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
1269      raise e
1270 ;; *)
1271
1272 let profiler2 = HExtlib.profile "CicRefine"
1273
1274 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1275  profiler2.HExtlib.profile
1276   (type_of_aux' ?localization_tbl metasenv context term) ugraph
1277
1278 let typecheck ~localization_tbl metasenv uri obj =
1279  profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj