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