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