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