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