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;;
  29 exception Uncertain of string;;
  30 exception AssertFailure of string;;
  31
  32 let debug_print = fun _ -> ()
  33
  34 let fo_unif_subst subst context metasenv t1 t2 ugraph =
  35   try
  36     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
  37   with
  38       (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  39     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  40 ;;
  41
  42 let rec split l n =
  43  match (l,n) with
  44     (l,0) -> ([], l)
  45   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  46   | (_,_) -> raise (AssertFailure "split: list too short")
  47 ;;
  48
  49 let rec type_of_constant uri ugraph =
  50   let module C = Cic in
  51   let module R = CicReduction in
  52   let module U = UriManager in
  53     (*
  54       let obj =
  55       try
  56       CicEnvironment.get_cooked_obj uri
  57       with Not_found -> assert false
  58       in
  59     *)
  60   let obj,u= CicEnvironment.get_obj ugraph uri in
  61     match obj with
  62         C.Constant (_,_,ty,_,_) -> ty,u
  63       | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
  64       | _ ->
  65           raise
  66             (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
  67
  68 and type_of_variable uri ugraph =
  69   let module C = Cic in
  70   let module R = CicReduction in
  71   let module U = UriManager in
  72     (*
  73       let obj =
  74       try
  75       CicEnvironment.get_cooked_obj uri
  76       with Not_found -> assert false
  77       in
  78     *)
  79   let obj,u = CicEnvironment.get_obj ugraph uri in
  80     match obj with
  81         C.Variable (_,_,ty,_,_) -> ty,u
  82       |  _ ->
  83            raise
  84             (RefineFailure
  85                ("Unknown variable definition " ^ UriManager.string_of_uri uri))
  86
  87 and type_of_mutual_inductive_defs uri i ugraph =
  88   let module C = Cic in
  89   let module R = CicReduction in
  90   let module U = UriManager in
  91     (*
  92       let obj =
  93       try
  94       CicEnvironment.get_cooked_obj uri
  95       with Not_found -> assert false
  96       in
  97     *)
  98   let obj,u = CicEnvironment.get_obj ugraph uri in
  99     match obj with
 100         C.InductiveDefinition (dl,_,_,_) ->
 101           let (_,_,arity,_) = List.nth dl i in
 102             arity,u
 103       | _ ->
 104           raise
 105             (RefineFailure
 106                ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 107
 108 and type_of_mutual_inductive_constr uri i j ugraph =
 109   let module C = Cic in
 110   let module R = CicReduction in
 111   let module U = UriManager in
 112     (*
 113       let obj =
 114       try
 115       CicEnvironment.get_cooked_obj uri
 116       with Not_found -> assert false
 117       in
 118     *)
 119   let obj,u = CicEnvironment.get_obj ugraph uri in
 120     match obj with
 121         C.InductiveDefinition (dl,_,_,_) ->
 122           let (_,_,_,cl) = List.nth dl i in
 123           let (_,ty) = List.nth cl (j-1) in
 124             ty,u
 125       | _ ->
 126           raise
 127             (RefineFailure
 128                ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
 129
 130
 131 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 132
 133 (* the check_branch function checks if a branch of a case is refinable.
 134    It returns a pair (outype_instance,args), a subst and a metasenv.
 135    outype_instance is the expected result of applying the case outtype
 136    to args.
 137    The problem is that outype is in general unknown, and we should
 138    try to synthesize it from the above information, that is in general
 139    a second order unification problem. *)
 140
 141 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
 142   let module C = Cic in
 143     (* let module R = CicMetaSubst in *)
 144   let module R = CicReduction in
 145     match R.whd ~subst context expectedtype with
 146         C.MutInd (_,_,_) ->
 147           (n,context,actualtype, [term]), subst, metasenv, ugraph
 148       | C.Appl (C.MutInd (_,_,_)::tl) ->
 149           let (_,arguments) = split tl left_args_no in
 150             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
 151       | C.Prod (name,so,de) ->
 152           (* we expect that the actual type of the branch has the due
 153              number of Prod *)
 154           (match R.whd ~subst context actualtype with
 155                C.Prod (name',so',de') ->
 156                  let subst, metasenv, ugraph1 =
 157                    fo_unif_subst subst context metasenv so so' ugraph in
 158                  let term' =
 159                    (match CicSubstitution.lift 1 term with
 160                         C.Appl l -> C.Appl (l@[C.Rel 1])
 161                       | t -> C.Appl [t ; C.Rel 1]) in
 162                    (* we should also check that the name variable is anonymous in
 163                       the actual type de' ?? *)
 164                    check_branch (n+1)
 165                      ((Some (name,(C.Decl so)))::context)
 166                        metasenv subst left_args_no de' term' de ugraph1
 167              | _ -> raise (AssertFailure "Wrong number of arguments"))
 168       | _ -> raise (AssertFailure "Prod or MutInd expected")
 169
 170 and type_of_aux' metasenv context t ugraph =
 171   let rec type_of_aux subst metasenv context t ugraph =
 172     let module C = Cic in
 173     let module S = CicSubstitution in
 174     let module U = UriManager in
 175       match t with
 176           (*    function *)
 177           C.Rel n ->
 178             (try
 179                match List.nth context (n - 1) with
 180                    Some (_,C.Decl ty) ->
 181                      t,S.lift n ty,subst,metasenv, ugraph
 182                  | Some (_,C.Def (_,Some ty)) ->
 183                      t,S.lift n ty,subst,metasenv, ugraph
 184                  | Some (_,C.Def (bo,None)) ->
 185                      type_of_aux subst metasenv context (S.lift n bo) ugraph
 186                  | None -> raise (RefineFailure "Rel to hidden hypothesis")
 187              with
 188                  _ -> raise (RefineFailure "Not a close term")
 189             )
 190         | C.Var (uri,exp_named_subst) ->
 191             let exp_named_subst',subst',metasenv',ugraph1 =
 192               check_exp_named_subst
 193                 subst metasenv context exp_named_subst ugraph
 194             in
 195             let ty_uri,ugraph1 = type_of_variable uri ugraph in
 196             let ty =
 197               CicSubstitution.subst_vars exp_named_subst' ty_uri
 198             in
 199               C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
 200         | C.Meta (n,l) ->
 201             (try
 202                let (canonical_context, term,ty) =
 203                  CicUtil.lookup_subst n subst
 204                in
 205                let l',subst',metasenv',ugraph1 =
 206                  check_metasenv_consistency n subst metasenv context
 207                    canonical_context l ugraph
 208                in
 209                  (* trust or check ??? *)
 210                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 211                    subst', metasenv', ugraph1
 212                    (* type_of_aux subst metasenv
 213                       context (CicSubstitution.subst_meta l term) *)
 214              with CicUtil.Subst_not_found _ ->
 215                let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 216                let l',subst',metasenv', ugraph1 =
 217                  check_metasenv_consistency n subst metasenv context
 218                    canonical_context l ugraph
 219                in
 220                  C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
 221                    subst', metasenv',ugraph1)
 222         | C.Sort (C.Type tno) ->
 223             let tno' = CicUniv.fresh() in
 224             let ugraph1 = CicUniv.add_gt tno' tno ugraph in
 225               t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
 226         | C.Sort _ ->
 227             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
 228         | C.Implicit _ -> raise (AssertFailure "21")
 229         | C.Cast (te,ty) ->
 230             let ty',_,subst',metasenv',ugraph1 =
 231               type_of_aux subst metasenv context ty ugraph
 232             in
 233             let te',inferredty,subst'',metasenv'',ugraph2 =
 234               type_of_aux subst' metasenv' context te ugraph1
 235             in
 236               (try
 237                  let subst''',metasenv''',ugraph3 =
 238                    fo_unif_subst subst'' context metasenv''
 239                      inferredty ty ugraph2
 240                  in
 241                    C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
 242                with
 243                    _ -> raise (RefineFailure "Cast"))
 244         | C.Prod (name,s,t) ->
 245             let s',sort1,subst',metasenv',ugraph1 =
 246               type_of_aux subst metasenv context s ugraph
 247             in
 248             let t',sort2,subst'',metasenv'',ugraph2 =
 249               type_of_aux subst' metasenv'
 250                 ((Some (name,(C.Decl s')))::context) t ugraph1
 251             in
 252             let sop,subst''',metasenv''',ugraph3 =
 253               sort_of_prod subst'' metasenv''
 254                 context (name,s') (sort1,sort2) ugraph2
 255             in
 256               C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
 257         | C.Lambda (n,s,t) ->
 258             let s',sort1,subst',metasenv',ugraph1 =
 259               type_of_aux subst metasenv context s ugraph
 260             in
 261               (match CicReduction.whd ~subst:subst' context sort1 with
 262                    C.Meta _
 263                  | C.Sort _ -> ()
 264                  | _ ->
 265                      raise (RefineFailure (sprintf
 266                                              "Not well-typed lambda-abstraction: the source %s should be a type;
 267              instead it is a term of type %s" (CicPp.ppterm s)
 268                                              (CicPp.ppterm sort1)))
 269               ) ;
 270               let t',type2,subst'',metasenv'',ugraph2 =
 271                 type_of_aux subst' metasenv'
 272                   ((Some (n,(C.Decl s')))::context) t ugraph1
 273               in
 274                 C.Lambda (n,s',t'),C.Prod (n,s',type2),
 275                   subst'',metasenv'',ugraph2
 276         | C.LetIn (n,s,t) ->
 277             (* only to check if s is well-typed *)
 278             let s',ty,subst',metasenv',ugraph1 =
 279               type_of_aux subst metasenv context s ugraph
 280             in
 281             let t',inferredty,subst'',metasenv'',ugraph2 =
 282               type_of_aux subst' metasenv'
 283                 ((Some (n,(C.Def (s',Some ty))))::context) t ugraph1
 284             in
 285               (* One-step LetIn reduction.
 286                * Even faster than the previous solution.
 287                * Moreover the inferred type is closer to the expected one.
 288                *)
 289               C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
 290                 subst',metasenv',ugraph2
 291         | C.Appl (he::((_::_) as tl)) ->
 292             let he',hetype,subst',metasenv',ugraph1 =
 293               type_of_aux subst metasenv context he ugraph
 294             in
 295             let tlbody_and_type,subst'',metasenv'',ugraph2 =
 296               List.fold_right
 297                 (fun x (res,subst,metasenv,ugraph) ->
 298                    let x',ty,subst',metasenv',ugraph1 =
 299                      type_of_aux subst metasenv context x ugraph
 300                    in
 301                      (x', ty)::res,subst',metasenv',ugraph1
 302                 ) tl ([],subst',metasenv',ugraph1)
 303             in
 304             let tl',applty,subst''',metasenv''',ugraph3 =
 305               eat_prods subst'' metasenv'' context
 306                 hetype tlbody_and_type ugraph2
 307             in
 308               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
 309         | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
 310         | C.Const (uri,exp_named_subst) ->
 311             let exp_named_subst',subst',metasenv',ugraph1 =
 312               check_exp_named_subst subst metasenv context
 313                 exp_named_subst ugraph in
 314             let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
 315             let cty =
 316               CicSubstitution.subst_vars exp_named_subst' ty_uri
 317             in
 318               C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
 319         | C.MutInd (uri,i,exp_named_subst) ->
 320             let exp_named_subst',subst',metasenv',ugraph1 =
 321               check_exp_named_subst subst metasenv context
 322                 exp_named_subst ugraph
 323             in
 324             let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
 325             let cty =
 326               CicSubstitution.subst_vars exp_named_subst' ty_uri in
 327               C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
 328         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 329             let exp_named_subst',subst',metasenv',ugraph1 =
 330               check_exp_named_subst subst metasenv context
 331                 exp_named_subst ugraph
 332             in
 333             let ty_uri,ugraph2 =
 334               type_of_mutual_inductive_constr uri i j ugraph1
 335             in
 336             let cty =
 337               CicSubstitution.subst_vars exp_named_subst' ty_uri
 338             in
 339               C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
 340                 metasenv',ugraph2
 341         | C.MutCase (uri, i, outtype, term, pl) ->
 342             (* first, get the inductive type (and noparams)
 343              * in the environment  *)
 344             let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
 345               let obj,u = CicEnvironment.get_obj ugraph uri in
 346               match obj with
 347                   C.InductiveDefinition (l,expl_params,parsno,_) ->
 348                     List.nth l i , expl_params, parsno, u
 349                 | _ ->
 350                     raise
 351                       (RefineFailure
 352                          ("Unkown mutual inductive definition " ^
 353                          U.string_of_uri uri))
 354            in
 355            let rec count_prod t =
 356              match CicReduction.whd ~subst context t with
 357                  C.Prod (_, _, t) -> 1 + (count_prod t)
 358                | _ -> 0
 359            in
 360            let no_args = count_prod arity in
 361              (* now, create a "generic" MutInd *)
 362            let metasenv,left_args =
 363              CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
 364            in
 365            let metasenv,right_args =
 366              let no_right_params = no_args - no_left_params in
 367                if no_right_params < 0 then assert false
 368                else CicMkImplicit.n_fresh_metas
 369                       metasenv subst context no_right_params
 370            in
 371            let metasenv,exp_named_subst =
 372              CicMkImplicit.fresh_subst metasenv subst context expl_params in
 373            let expected_type =
 374              if no_args = 0 then
 375                C.MutInd (uri,i,exp_named_subst)
 376              else
 377                C.Appl
 378                  (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 379            in
 380              (* check consistency with the actual type of term *)
 381            let term',actual_type,subst,metasenv,ugraph1 =
 382              type_of_aux subst metasenv context term ugraph in
 383            let expected_type',_, subst, metasenv,ugraph2 =
 384              type_of_aux subst metasenv context expected_type ugraph1
 385            in
 386            let actual_type = CicReduction.whd ~subst context actual_type in
 387            let subst,metasenv,ugraph3 =
 388              fo_unif_subst subst context metasenv
 389                expected_type' actual_type ugraph2
 390            in
 391              (* TODO: check if the sort elimination
 392               * is allowed: [(I q1 ... qr)|B] *)
 393            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
 394              List.fold_left
 395                (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
 396                   let constructor =
 397                     if left_args = [] then
 398                       (C.MutConstruct (uri,i,j,exp_named_subst))
 399                     else
 400                       (C.Appl
 401                         (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 402                   in
 403                   let p',actual_type,subst,metasenv,ugraph1 =
 404                     type_of_aux subst metasenv context p ugraph
 405                   in
 406                   let constructor',expected_type, subst, metasenv,ugraph2 =
 407                     type_of_aux subst metasenv context constructor ugraph1
 408                   in
 409                   let outtypeinstance,subst,metasenv,ugraph3 =
 410                     check_branch 0 context metasenv subst no_left_params
 411                       actual_type constructor' expected_type ugraph2
 412                   in
 413                     (pl @ [p'],j+1,
 414                      outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
 415                ([],1,[],subst,metasenv,ugraph3) pl
 416            in
 417
 418              (* we are left to check that the outype matches his instances.
 419                 The easy case is when the outype is specified, that amount
 420                 to a trivial check. Otherwise, we should guess a type from
 421                 its instances
 422              *)
 423
 424            (match outtype with
 425            | C.Meta (n,l) ->
 426                (let candidate,ugraph5,metasenv =
 427                  let exp_name_subst, metasenv =
 428                     let o,_ =
 429                       CicEnvironment.get_obj CicUniv.empty_ugraph uri
 430                     in
 431                     let uris = CicUtil.params_of_obj o in
 432                     List.fold_right (
 433                       fun uri (acc,metasenv) ->
 434                         let metasenv',new_meta =
 435                            CicMkImplicit.mk_implicit metasenv subst context
 436                         in
 437                         let irl =
 438                           CicMkImplicit.identity_relocation_list_for_metavariable
 439                             context
 440                         in
 441                         (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
 442                     ) uris ([],metasenv)
 443                  in
 444                  let ty = Cic.MutInd(uri, i, exp_name_subst) in
 445                  let fresh_name =
 446                    FreshNamesGenerator.mk_fresh_name ~subst metasenv
 447                      context Cic.Anonymous ~typ:ty
 448                  in
 449                  match outtypeinstances with
 450                  | [] ->
 451                      let extended_context =
 452                        Some (fresh_name,Cic.Decl ty)::context
 453                      in
 454                      let metasenv,new_meta =
 455                        CicMkImplicit.mk_implicit metasenv subst extended_context
 456                      in
 457                      let irl =
 458                        CicMkImplicit.identity_relocation_list_for_metavariable
 459                          extended_context
 460                      in
 461                      let candidate =
 462                        Cic.Lambda(fresh_name, ty, Cic.Meta (new_meta,irl))
 463                      in
 464                      (Some candidate),ugraph4,metasenv
 465                  | (constructor_args_no,_,instance,_)::tl ->
 466                      try
 467                        let instance' =
 468                          CicSubstitution.delift constructor_args_no
 469                            (CicMetaSubst.apply_subst subst instance)
 470                        in
 471                        let candidate,ugraph,metasenv =
 472                          List.fold_left (
 473                            fun (candidate_oty,ugraph,metasenv)
 474                              (constructor_args_no,_,instance,_) ->
 475                                match candidate_oty with
 476                                | None -> None,ugraph,metasenv
 477                                | Some ty ->
 478                                  try
 479                                    let instance' =
 480                                      CicSubstitution.delift
 481                                       constructor_args_no
 482                                        (CicMetaSubst.apply_subst subst instance)
 483                                    in
 484                                    let b,ugraph1 =
 485                                       CicReduction.are_convertible context
 486                                         instance' ty ugraph
 487                                    in
 488                                    if b then
 489                                      candidate_oty,ugraph1,metasenv
 490                                    else
 491                                      None,ugraph,metasenv
 492                                  with Failure s -> None,ugraph,metasenv
 493                          ) (Some instance',ugraph4,metasenv) tl
 494                        in
 495                        match candidate with
 496                        | None -> None, ugraph,metasenv
 497                        | Some t ->
 498                            Some (Cic.Lambda (fresh_name, ty,
 499                              CicSubstitution.lift 1 t)),ugraph,metasenv
 500                      with Failure s ->
 501                        None,ugraph4,metasenv
 502                in
 503                match candidate with
 504                | None -> raise (Uncertain "can't solve an higher order unification problem")
 505                | Some candidate ->
 506                    let s,m,u =
 507                      fo_unif_subst subst context metasenv
 508                        candidate outtype ugraph5
 509                    in
 510                      C.MutCase (uri, i, outtype, term', pl'),
 511                        (Cic.Appl [outtype; term']),s,m,u)
 512            | _ ->    (* easy case *)
 513              let _,_, subst, metasenv,ugraph5 =
 514                type_of_aux subst metasenv context
 515                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 516              in
 517              let (subst,metasenv,ugraph6) =
 518                List.fold_left
 519                  (fun (subst,metasenv,ugraph)
 520                         (constructor_args_no,context,instance,args) ->
 521                     let instance' =
 522                       let appl =
 523                         let outtype' =
 524                           CicSubstitution.lift constructor_args_no outtype
 525                         in
 526                           C.Appl (outtype'::args)
 527                       in
 528                         CicReduction.whd ~subst context appl
 529                     in
 530                     fo_unif_subst subst context metasenv
 531                         instance instance' ugraph)
 532                  (subst,metasenv,ugraph5) outtypeinstances
 533              in
 534                C.MutCase (uri, i, outtype, term', pl'),
 535                  CicReduction.whd ~subst        context
 536                    (C.Appl(outtype::right_args@[term])),
 537                  subst,metasenv,ugraph6)
 538         | C.Fix (i,fl) ->
 539             let fl_ty',subst,metasenv,types,ugraph1 =
 540               List.fold_left
 541                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 542                    let ty',_,subst',metasenv',ugraph1 =
 543                       type_of_aux subst metasenv context ty ugraph
 544                    in
 545                      fl @ [ty'],subst',metasenv',
 546                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 547                 ) ([],subst,metasenv,[],ugraph) fl
 548             in
 549             let len = List.length types in
 550             let context' = types@context in
 551             let fl_bo',subst,metasenv,ugraph2 =
 552               List.fold_left
 553                 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
 554                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 555                      type_of_aux subst metasenv context' bo ugraph
 556                    in
 557                    let subst',metasenv',ugraph' =
 558                      fo_unif_subst subst context' metasenv
 559                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 560                    in
 561                      fl @ [bo'] , subst',metasenv',ugraph'
 562                 ) ([],subst,metasenv,ugraph1) fl
 563             in
 564             let (_,_,ty,_) = List.nth fl i in
 565             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 566              * and we want the new fl with bo' and ty' injected in the right
 567              * place.
 568              *)
 569             let rec map3 f l1 l2 l3 =
 570               match l1,l2,l3 with
 571               | [],[],[] -> []
 572               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 573               | _ -> assert false
 574             in
 575             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 576               fl_ty' fl_bo' fl
 577             in
 578               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 579         | C.CoFix (i,fl) ->
 580             let fl_ty',subst,metasenv,types,ugraph1 =
 581               List.fold_left
 582                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 583                    let ty',_,subst',metasenv',ugraph1 =
 584                      type_of_aux subst metasenv context ty ugraph
 585                    in
 586                      fl @ [ty'],subst',metasenv',
 587                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 588                 ) ([],subst,metasenv,[],ugraph) fl
 589             in
 590             let len = List.length types in
 591             let context' = types@context in
 592             let fl_bo',subst,metasenv,ugraph2 =
 593               List.fold_left
 594                 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
 595                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 596                      type_of_aux subst metasenv context' bo ugraph
 597                    in
 598                    let subst',metasenv',ugraph' =
 599                      fo_unif_subst subst context' metasenv
 600                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 601                    in
 602                      fl @ [bo'],subst',metasenv',ugraph'
 603                 ) ([],subst,metasenv,ugraph1) fl
 604             in
 605             let (_,ty,_) = List.nth fl i in
 606             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 607              * and we want the new fl with bo' and ty' injected in the right
 608              * place.
 609              *)
 610             let rec map3 f l1 l2 l3 =
 611               match l1,l2,l3 with
 612               | [],[],[] -> []
 613               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 614               | _ -> assert false
 615             in
 616             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 617               fl_ty' fl_bo' fl
 618             in
 619               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 620
 621   (* check_metasenv_consistency checks that the "canonical" context of a
 622      metavariable is consitent - up to relocation via the relocation list l -
 623      with the actual context *)
 624   and check_metasenv_consistency
 625     metano subst metasenv context canonical_context l ugraph
 626     =
 627     let module C = Cic in
 628     let module R = CicReduction in
 629     let module S = CicSubstitution in
 630     let lifted_canonical_context =
 631       let rec aux i =
 632         function
 633             [] -> []
 634           | (Some (n,C.Decl t))::tl ->
 635               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 636           | (Some (n,C.Def (t,None)))::tl ->
 637               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 638           | None::tl -> None::(aux (i+1) tl)
 639           | (Some (n,C.Def (t,Some ty)))::tl ->
 640               (Some (n,
 641                      C.Def ((S.subst_meta l (S.lift i t)),
 642                             Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 643       in
 644         aux 1 canonical_context
 645     in
 646       try
 647         List.fold_left2
 648           (fun (l,subst,metasenv,ugraph) t ct ->
 649              match (t,ct) with
 650                  _,None ->
 651                    l @ [None],subst,metasenv,ugraph
 652                | Some t,Some (_,C.Def (ct,_)) ->
 653                    let subst',metasenv',ugraph' =
 654                    (try
 655                       fo_unif_subst subst context metasenv t ct ugraph
 656                     with e -> raise (RefineFailure (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 -> msg | _ -> (Printexc.to_string e)))))
 657                    in
 658                      l @ [Some t],subst',metasenv',ugraph'
 659                | Some t,Some (_,C.Decl ct) ->
 660                    let t',inferredty,subst',metasenv',ugraph1 =
 661                      type_of_aux subst metasenv context t ugraph
 662                    in
 663                    let subst'',metasenv'',ugraph2 =
 664                      (try
 665                         fo_unif_subst
 666                           subst' context metasenv' inferredty ct ugraph1
 667                       with e -> raise (RefineFailure (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 -> msg | _ -> (Printexc.to_string e)))))
 668                    in
 669                      l @ [Some t'], subst'',metasenv'',ugraph2
 670                | None, Some _  ->
 671                    raise (RefineFailure (sprintf
 672                                            "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"
 673                                            (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 674                                            (CicMetaSubst.ppcontext subst canonical_context)))
 675           ) ([],subst,metasenv,ugraph) l lifted_canonical_context
 676       with
 677           Invalid_argument _ ->
 678             raise
 679             (RefineFailure
 680                (sprintf
 681                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 682                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 683                   (CicMetaSubst.ppcontext subst canonical_context)))
 684
 685   and check_exp_named_subst metasubst metasenv context tl ugraph =
 686     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 687       match tl with
 688           [] -> [],metasubst,metasenv,ugraph
 689         | ((uri,t) as subst)::tl ->
 690             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 691             let typeofvar =
 692               CicSubstitution.subst_vars substs ty_uri in
 693               (* CSC: why was this code here? it is wrong
 694                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 695                  Cic.Variable (_,Some bo,_,_) ->
 696                  raise
 697                  (RefineFailure
 698                  "A variable with a body can not be explicit substituted")
 699                  | Cic.Variable (_,None,_,_) -> ()
 700                  | _ ->
 701                  raise
 702                  (RefineFailure
 703                  ("Unkown variable definition " ^ UriManager.string_of_uri uri))
 704                  ) ;
 705               *)
 706             let t',typeoft,metasubst',metasenv',ugraph2 =
 707               type_of_aux metasubst metasenv context t ugraph1
 708             in
 709             let metasubst'',metasenv'',ugraph3 =
 710               try
 711                 fo_unif_subst
 712                   metasubst' context metasenv' typeoft typeofvar ugraph2
 713               with _ ->
 714                 raise (RefineFailure
 715                          ("Wrong Explicit Named Substitution: " ^
 716                            CicMetaSubst.ppterm metasubst' typeoft ^
 717                           " not unifiable with " ^
 718                           CicMetaSubst.ppterm metasubst' typeofvar))
 719             in
 720             (* FIXME: no mere tail recursive! *)
 721             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
 722               check_exp_named_subst_aux
 723                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
 724             in
 725               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
 726     in
 727       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 728
 729
 730   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
 731     let module C = Cic in
 732     let context_for_t2 = (Some (name,C.Decl s))::context in
 733     let t1'' = CicReduction.whd ~subst context t1 in
 734     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
 735       match (t1'', t2'') with
 736           (C.Sort s1, C.Sort s2)
 737             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 738               C.Sort s2,subst,metasenv,ugraph
 739         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 740             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 741             let t' = CicUniv.fresh() in
 742             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
 743             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
 744               C.Sort (C.Type t'),subst,metasenv,ugraph2
 745         | (C.Sort _,C.Sort (C.Type t1)) ->
 746             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 747             C.Sort (C.Type t1),subst,metasenv,ugraph
 748         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
 749         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 750             (* TODO how can we force the meta to become a sort? If we don't we
 751              * brake the invariant that refine produce only well typed terms *)
 752             (* TODO if we check the non meta term and if it is a sort then we are
 753              * likely to know the exact value of the result e.g. if the rhs is a
 754              * Sort (Prop | Set | CProp) then the result is the rhs *)
 755             let (metasenv,idx) =
 756               CicMkImplicit.mk_implicit_sort metasenv subst in
 757             let (subst, metasenv,ugraph1) =
 758               fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
 759             in
 760               t2'',subst,metasenv,ugraph1
 761         | (_,_) ->
 762             raise (RefineFailure (sprintf
 763                                     "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 764                                     (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 765                                     (CicPp.ppterm t2'')))
 766
 767   and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
 768     let rec mk_prod metasenv context =
 769       function
 770           [] ->
 771             let (metasenv, idx) =
 772               CicMkImplicit.mk_implicit_type metasenv subst context
 773             in
 774             let irl =
 775               CicMkImplicit.identity_relocation_list_for_metavariable context
 776             in
 777               metasenv,Cic.Meta (idx, irl)
 778         | (_,argty)::tl ->
 779             let (metasenv, idx) =
 780               CicMkImplicit.mk_implicit_type metasenv subst context
 781             in
 782             let irl =
 783               CicMkImplicit.identity_relocation_list_for_metavariable context
 784             in
 785             let meta = Cic.Meta (idx,irl) in
 786             let name =
 787               (* The name must be fresh for context.                 *)
 788               (* Nevertheless, argty is well-typed only in context.  *)
 789               (* Thus I generate a name (name_hint) in context and   *)
 790               (* then I generate a name --- using the hint name_hint *)
 791               (* --- that is fresh in (context'@context).            *)
 792               let name_hint =
 793                 (* Cic.Name "pippo" *)
 794                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
 795                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
 796                   (CicMetaSubst.apply_subst_context subst context)
 797                   Cic.Anonymous
 798                   ~typ:(CicMetaSubst.apply_subst subst argty)
 799               in
 800                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 801                 FreshNamesGenerator.mk_fresh_name ~subst
 802                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
 803             in
 804             let metasenv,target =
 805               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 806             in
 807               metasenv,Cic.Prod (name,meta,target)
 808     in
 809     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 810     let (subst, metasenv,ugraph1) =
 811       try
 812         fo_unif_subst subst context metasenv hetype hetype' ugraph
 813       with exn ->
 814         debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
 815                          (CicPp.ppterm hetype)
 816                          (CicPp.ppterm hetype')
 817                          (CicMetaSubst.ppmetasenv metasenv [])
 818                          (CicMetaSubst.ppsubst subst));
 819         raise exn
 820
 821     in
 822     let rec eat_prods metasenv subst context hetype ugraph =
 823       function
 824         | [] -> [],metasenv,subst,hetype,ugraph
 825         | (hete, hety)::tl ->
 826             (match hetype with
 827                  Cic.Prod (n,s,t) ->
 828                    let arg,subst,metasenv,ugraph1 =
 829                      try
 830                        let subst,metasenv,ugraph1 =
 831                          fo_unif_subst subst context metasenv hety s ugraph
 832                        in
 833                          hete,subst,metasenv,ugraph1
 834                      with exn ->
 835                        (* we search a coercion from hety to s *)
 836                        let coer = CoercGraph.look_for_coercion
 837                          (CicMetaSubst.apply_subst subst hety)
 838                          (CicMetaSubst.apply_subst subst s)
 839                        in
 840                        match coer with
 841                        | None -> raise exn
 842                        | Some c ->
 843                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
 844                    in
 845                    let coerced_args,metasenv',subst',t',ugraph2 =
 846                      eat_prods metasenv subst context
 847                        (* (CicMetaSubst.subst subst hete t) tl *)
 848                        (CicSubstitution.subst hete t) ugraph1 tl
 849                    in
 850                      arg::coerced_args,metasenv',subst',t',ugraph2
 851                | _ -> assert false
 852             )
 853     in
 854     let coerced_args,metasenv,subst,t,ugraph2 =
 855       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
 856     in
 857       coerced_args,t,subst,metasenv,ugraph2
 858   in
 859
 860   (* eat prods ends here! *)
 861
 862   let t',ty,subst',metasenv',ugraph1 =
 863    type_of_aux [] metasenv context t ugraph
 864   in
 865   let substituted_t = CicMetaSubst.apply_subst subst' t' in
 866   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 867     (* Andrea: ho rimesso qui l'applicazione della subst al
 868        metasenv dopo che ho droppato l'invariante che il metsaenv
 869        e' sempre istanziato *)
 870   let substituted_metasenv =
 871     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
 872     (* metasenv' *)
 873     (*  substituted_t,substituted_ty,substituted_metasenv *)
 874     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
 875   let cleaned_t =
 876     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 877   let cleaned_ty =
 878     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 879   let cleaned_metasenv =
 880     List.map
 881       (function (n,context,ty) ->
 882          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 883          let context' =
 884            List.map
 885              (function
 886                   None -> None
 887                 | Some (n, Cic.Decl t) ->
 888                     Some (n,
 889                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 890                 | Some (n, Cic.Def (bo,ty)) ->
 891                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 892                     let ty' =
 893                       match ty with
 894                           None -> None
 895                         | Some ty ->
 896                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 897                     in
 898                       Some (n, Cic.Def (bo',ty'))
 899              ) context
 900          in
 901            (n,context',ty')
 902       ) substituted_metasenv
 903   in
 904     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
 905 ;;
 906
 907 let type_of_aux' metasenv context term ugraph =
 908   try
 909     type_of_aux' metasenv context term ugraph
 910   with
 911     CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
 912
 913
 914 (* DEBUGGING ONLY
 915 let type_of_aux' metasenv context term =
 916  try
 917   let (t,ty,m) =
 918       type_of_aux' metasenv context term in
 919     debug_print
 920      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 921    debug_print
 922     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
 923    (t,ty,m)
 924  with
 925  | RefineFailure msg as e ->
 926      debug_print ("@@@ REFINE FAILED: " ^ msg);
 927      raise e
 928  | Uncertain msg as e ->
 929      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
 930      raise e
 931 ;; *)