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               CicSubstitution.subst_vars substs ty_uri in
 856               (* CSC: why was this code here? it is wrong
 857                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 858                  Cic.Variable (_,Some bo,_,_) ->
 859                  raise
 860                  (RefineFailure (lazy
 861                  "A variable with a body can not be explicit substituted"))
 862                  | Cic.Variable (_,None,_,_) -> ()
 863                  | _ ->
 864                  raise
 865                  (RefineFailure (lazy
 866                  ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
 867                  ) ;
 868               *)
 869             let t',typeoft,metasubst',metasenv',ugraph2 =
 870               type_of_aux metasubst metasenv context t ugraph1 in
 871             let subst = uri,t' in
 872             let metasubst'',metasenv'',ugraph3 =
 873               try
 874                 fo_unif_subst
 875                   metasubst' context metasenv' typeoft typeofvar ugraph2
 876               with _ ->
 877                 raise (RefineFailure (lazy
 878                          ("Wrong Explicit Named Substitution: " ^
 879                            CicMetaSubst.ppterm metasubst' typeoft ^
 880                           " not unifiable with " ^
 881                           CicMetaSubst.ppterm metasubst' typeofvar)))
 882             in
 883             (* FIXME: no mere tail recursive! *)
 884             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
 885               check_exp_named_subst_aux
 886                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
 887             in
 888               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
 889     in
 890       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 891
 892
 893   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
 894     let module C = Cic in
 895     let context_for_t2 = (Some (name,C.Decl s))::context in
 896     let t1'' = CicReduction.whd ~subst context t1 in
 897     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
 898       match (t1'', t2'') with
 899           (C.Sort s1, C.Sort s2)
 900             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
 901               (* different than Coq manual!!! *)
 902               C.Sort s2,subst,metasenv,ugraph
 903         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 904             let t' = CicUniv.fresh() in
 905             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
 906             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
 907               C.Sort (C.Type t'),subst,metasenv,ugraph2
 908         | (C.Sort _,C.Sort (C.Type t1)) ->
 909             C.Sort (C.Type t1),subst,metasenv,ugraph
 910         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
 911         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 912             (* TODO how can we force the meta to become a sort? If we don't we
 913              * brake the invariant that refine produce only well typed terms *)
 914             (* TODO if we check the non meta term and if it is a sort then we
 915              * are likely to know the exact value of the result e.g. if the rhs
 916              * is a Sort (Prop | Set | CProp) then the result is the rhs *)
 917             let (metasenv,idx) =
 918               CicMkImplicit.mk_implicit_sort metasenv subst in
 919             let (subst, metasenv,ugraph1) =
 920               fo_unif_subst subst context_for_t2 metasenv
 921                 (C.Meta (idx,[])) t2'' ugraph
 922             in
 923               t2'',subst,metasenv,ugraph1
 924         | _,_ ->
 925             raise
 926               (RefineFailure
 927                 (lazy
 928                   (sprintf
 929                     ("Two sorts were expected, found %s " ^^
 930                      "(that reduces to %s) and %s (that reduces to %s)")
 931                 (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 932                 (CicPp.ppterm t2''))))
 933
 934   and eat_prods
 935     allow_coercions subst metasenv context hetype tlbody_and_type ugraph
 936   =
 937     let rec mk_prod metasenv context =
 938       function
 939           [] ->
 940             let (metasenv, idx) =
 941               CicMkImplicit.mk_implicit_type metasenv subst context
 942             in
 943             let irl =
 944               CicMkImplicit.identity_relocation_list_for_metavariable context
 945             in
 946               metasenv,Cic.Meta (idx, irl)
 947         | (_,argty)::tl ->
 948             let (metasenv, idx) =
 949               CicMkImplicit.mk_implicit_type metasenv subst context
 950             in
 951             let irl =
 952               CicMkImplicit.identity_relocation_list_for_metavariable context
 953             in
 954             let meta = Cic.Meta (idx,irl) in
 955             let name =
 956               (* The name must be fresh for context.                 *)
 957               (* Nevertheless, argty is well-typed only in context.  *)
 958               (* Thus I generate a name (name_hint) in context and   *)
 959               (* then I generate a name --- using the hint name_hint *)
 960               (* --- that is fresh in (context'@context).            *)
 961               let name_hint =
 962                 (* Cic.Name "pippo" *)
 963                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
 964                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
 965                   (CicMetaSubst.apply_subst_context subst context)
 966                   Cic.Anonymous
 967                   ~typ:(CicMetaSubst.apply_subst subst argty)
 968               in
 969                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 970                 FreshNamesGenerator.mk_fresh_name ~subst
 971                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
 972             in
 973             let metasenv,target =
 974               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 975             in
 976               metasenv,Cic.Prod (name,meta,target)
 977     in
 978     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 979     let (subst, metasenv,ugraph1) =
 980       try
 981         fo_unif_subst subst context metasenv hetype hetype' ugraph
 982       with exn ->
 983         debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
 984                          (CicPp.ppterm hetype)
 985                          (CicPp.ppterm hetype')
 986                          (CicMetaSubst.ppmetasenv [] metasenv)
 987                          (CicMetaSubst.ppsubst subst)));
 988         raise exn
 989
 990     in
 991     let rec eat_prods metasenv subst context hetype ugraph =
 992       function
 993         | [] -> [],metasenv,subst,hetype,ugraph
 994         | (hete, hety)::tl ->
 995             (match hetype with
 996                  Cic.Prod (n,s,t) ->
 997                    let arg,subst,metasenv,ugraph1 =
 998                      try
 999                        let subst,metasenv,ugraph1 =
1000                          fo_unif_subst subst context metasenv hety s ugraph
1001                        in
1002                          hete,subst,metasenv,ugraph1
1003                      with exn when allow_coercions ->
1004                        (* we search a coercion from hety to s *)
1005                        let coer =
1006                          let carr t subst context =
1007                            CicMetaSubst.apply_subst subst t
1008                          in
1009                          let c_hety = carr hety subst context in
1010                          let c_s = carr s subst context in
1011                          CoercGraph.look_for_coercion c_hety c_s
1012                        in
1013                        match coer with
1014                        | CoercGraph.NoCoercion
1015                        | CoercGraph.NotHandled _ ->
1016                           let msg e =
1017                            lazy ("The term " ^
1018                             CicMetaSubst.ppterm_in_context subst hete
1019                              context ^ " has type " ^
1020                             CicMetaSubst.ppterm_in_context subst hety
1021                              context ^ " but is here used with type " ^
1022                             CicMetaSubst.ppterm_in_context subst s context
1023                              (* "\nReason: " ^ Lazy.force e*))
1024                           in
1025                            enrich
1026                             (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None)
1027                             msg exn
1028                        | CoercGraph.NotMetaClosed ->
1029                            raise (Uncertain (lazy "Coercions on meta"))
1030                        | CoercGraph.SomeCoercion c ->
1031                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
1032                    in
1033                    let coerced_args,metasenv',subst',t',ugraph2 =
1034                      eat_prods metasenv subst context
1035                        (CicSubstitution.subst arg t) ugraph1 tl
1036                    in
1037                      arg::coerced_args,metasenv',subst',t',ugraph2
1038                | _ -> assert false
1039             )
1040     in
1041     let coerced_args,metasenv,subst,t,ugraph2 =
1042       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
1043     in
1044       coerced_args,t,subst,metasenv,ugraph2
1045   in
1046
1047   (* eat prods ends here! *)
1048
1049   let t',ty,subst',metasenv',ugraph1 =
1050    type_of_aux [] metasenv context t ugraph
1051   in
1052   let substituted_t = CicMetaSubst.apply_subst subst' t' in
1053   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
1054     (* Andrea: ho rimesso qui l'applicazione della subst al
1055        metasenv dopo che ho droppato l'invariante che il metsaenv
1056        e' sempre istanziato *)
1057   let substituted_metasenv =
1058     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
1059     (* metasenv' *)
1060     (*  substituted_t,substituted_ty,substituted_metasenv *)
1061     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
1062   let cleaned_t =
1063     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
1064   let cleaned_ty =
1065     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
1066   let cleaned_metasenv =
1067     List.map
1068       (function (n,context,ty) ->
1069          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
1070          let context' =
1071            List.map
1072              (function
1073                   None -> None
1074                 | Some (n, Cic.Decl t) ->
1075                     Some (n,
1076                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
1077                 | Some (n, Cic.Def (bo,ty)) ->
1078                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
1079                     let ty' =
1080                       match ty with
1081                           None -> None
1082                         | Some ty ->
1083                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
1084                     in
1085                       Some (n, Cic.Def (bo',ty'))
1086              ) context
1087          in
1088            (n,context',ty')
1089       ) substituted_metasenv
1090   in
1091     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
1092 ;;
1093
1094 let type_of_aux' ?localization_tbl metasenv context term ugraph =
1095   try
1096     type_of_aux' ?localization_tbl metasenv context term ugraph
1097   with
1098     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
1099
1100 let undebrujin uri typesno tys t =
1101   snd
1102    (List.fold_right
1103      (fun (name,_,_,_) (i,t) ->
1104        (* here the explicit_named_substituion is assumed to be *)
1105        (* of length 0 *)
1106        let t' = Cic.MutInd (uri,i,[])  in
1107        let t = CicSubstitution.subst t' t in
1108         i - 1,t
1109      ) tys (typesno - 1,t))
1110
1111 let map_first_n n start f g l =
1112   let rec aux acc k l =
1113     if k < n then
1114       match l with
1115       | [] -> raise (Invalid_argument "map_first_n")
1116       | hd :: tl -> f hd k (aux acc (k+1) tl)
1117     else
1118       g acc l
1119   in
1120   aux start 0 l
1121
1122 (*CSC: this is a very rough approximation; to be finished *)
1123 let are_all_occurrences_positive metasenv ugraph uri tys leftno =
1124   let number_of_types = List.length tys in
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