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