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