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                    let s,m,u =
 481                      fo_unif_subst subst context metasenv
 482                        candidate outtype ugraph5
 483                    in
 484                      C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
 485            | _ ->    (* easy case *)
 486              let _,_, subst, metasenv,ugraph5 =
 487                type_of_aux subst metasenv context
 488                  (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
 489              in
 490              let (subst,metasenv,ugraph6) =
 491                List.fold_left
 492                  (fun (subst,metasenv,ugraph)
 493                         (constructor_args_no,context,instance,args) ->
 494                     let instance' =
 495                       let appl =
 496                         let outtype' =
 497                           CicSubstitution.lift constructor_args_no outtype
 498                         in
 499                           C.Appl (outtype'::args)
 500                       in
 501                         CicReduction.whd ~subst context appl
 502                     in
 503                     fo_unif_subst subst context metasenv
 504                         instance instance' ugraph)
 505                  (subst,metasenv,ugraph5) outtypeinstances
 506              in
 507                C.MutCase (uri, i, outtype, term', pl'),
 508                  CicReduction.whd ~subst        context
 509                    (C.Appl(outtype::right_args@[term])),
 510                  subst,metasenv,ugraph6)
 511         | C.Fix (i,fl) ->
 512             let fl_ty',subst,metasenv,types,ugraph1 =
 513               List.fold_left
 514                 (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) ->
 515                    let ty',_,subst',metasenv',ugraph1 =
 516                       type_of_aux subst metasenv context ty ugraph
 517                    in
 518                      fl @ [ty'],subst',metasenv',
 519                        Some (C.Name n,(C.Decl ty')) :: types, ugraph
 520                 ) ([],subst,metasenv,[],ugraph) fl
 521             in
 522             let len = List.length types in
 523             let context' = types@context in
 524             let fl_bo',subst,metasenv,ugraph2 =
 525               List.fold_left
 526                 (fun (fl,subst,metasenv,ugraph) (name,x,ty,bo) ->
 527                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 528                      type_of_aux subst metasenv context' bo ugraph
 529                    in
 530                    let subst',metasenv',ugraph' =
 531                      fo_unif_subst subst context' metasenv
 532                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 533                    in
 534                      fl @ [bo'] , subst',metasenv',ugraph'
 535                 ) ([],subst,metasenv,ugraph1) fl
 536             in
 537             let (_,_,ty,_) = List.nth fl i in
 538             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 539              * and we want the new fl with bo' and ty' injected in the right
 540              * place.
 541              *)
 542             let rec map3 f l1 l2 l3 =
 543               match l1,l2,l3 with
 544               | [],[],[] -> []
 545               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 546               | _ -> assert false
 547             in
 548             let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
 549               fl_ty' fl_bo' fl
 550             in
 551               C.Fix (i,fl''),ty,subst,metasenv,ugraph2
 552         | C.CoFix (i,fl) ->
 553             let fl_ty',subst,metasenv,types,ugraph1 =
 554               List.fold_left
 555                 (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) ->
 556                    let ty',_,subst',metasenv',ugraph1 =
 557                      type_of_aux subst metasenv context ty ugraph
 558                    in
 559                      fl @ [ty'],subst',metasenv',
 560                        Some (C.Name n,(C.Decl ty')) :: types, ugraph1
 561                 ) ([],subst,metasenv,[],ugraph) fl
 562             in
 563             let len = List.length types in
 564             let context' = types@context in
 565             let fl_bo',subst,metasenv,ugraph2 =
 566               List.fold_left
 567                 (fun (fl,subst,metasenv,ugraph) (name,ty,bo) ->
 568                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
 569                      type_of_aux subst metasenv context' bo ugraph
 570                    in
 571                    let subst',metasenv',ugraph' =
 572                      fo_unif_subst subst context' metasenv
 573                        ty_of_bo (CicSubstitution.lift len ty) ugraph1
 574                    in
 575                      fl @ [bo'],subst',metasenv',ugraph'
 576                 ) ([],subst,metasenv,ugraph1) fl
 577             in
 578             let (_,ty,_) = List.nth fl i in
 579             (* now we have the new ty in fl_ty', the new bo in fl_bo',
 580              * and we want the new fl with bo' and ty' injected in the right
 581              * place.
 582              *)
 583             let rec map3 f l1 l2 l3 =
 584               match l1,l2,l3 with
 585               | [],[],[] -> []
 586               | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
 587               | _ -> assert false
 588             in
 589             let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
 590               fl_ty' fl_bo' fl
 591             in
 592               C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
 593
 594   (* check_metasenv_consistency checks that the "canonical" context of a
 595      metavariable is consitent - up to relocation via the relocation list l -
 596      with the actual context *)
 597   and check_metasenv_consistency
 598     metano subst metasenv context canonical_context l ugraph
 599     =
 600     let module C = Cic in
 601     let module R = CicReduction in
 602     let module S = CicSubstitution in
 603     let lifted_canonical_context =
 604       let rec aux i =
 605         function
 606             [] -> []
 607           | (Some (n,C.Decl t))::tl ->
 608               (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 609           | (Some (n,C.Def (t,None)))::tl ->
 610               (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 611           | None::tl -> None::(aux (i+1) tl)
 612           | (Some (n,C.Def (t,Some ty)))::tl ->
 613               (Some (n,
 614                      C.Def ((S.lift_meta l (S.lift i t)),
 615                             Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 616       in
 617         aux 1 canonical_context
 618     in
 619       try
 620         List.fold_left2
 621           (fun (l,subst,metasenv,ugraph) t ct ->
 622              match (t,ct) with
 623                  _,None ->
 624                    l @ [None],subst,metasenv,ugraph
 625                | Some t,Some (_,C.Def (ct,_)) ->
 626                    let subst',metasenv',ugraph' =
 627                    (try
 628                       fo_unif_subst subst context metasenv t ct ugraph
 629                     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)))))
 630                    in
 631                      l @ [Some t],subst',metasenv',ugraph'
 632                | Some t,Some (_,C.Decl ct) ->
 633                    let t',inferredty,subst',metasenv',ugraph1 =
 634                      type_of_aux subst metasenv context t ugraph
 635                    in
 636                    let subst'',metasenv'',ugraph2 =
 637                      (try
 638                         fo_unif_subst
 639                           subst' context metasenv' inferredty ct ugraph1
 640                       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)))))
 641                    in
 642                      l @ [Some t'], subst'',metasenv'',ugraph2
 643                | None, Some _  ->
 644                    raise (RefineFailure (sprintf
 645                                            "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"
 646                                            (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 647                                            (CicMetaSubst.ppcontext subst canonical_context)))
 648           ) ([],subst,metasenv,ugraph) l lifted_canonical_context
 649       with
 650           Invalid_argument _ ->
 651             raise
 652             (RefineFailure
 653                (sprintf
 654                   "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 655                   (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 656                   (CicMetaSubst.ppcontext subst canonical_context)))
 657
 658   and check_exp_named_subst metasubst metasenv context tl ugraph =
 659     let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph  =
 660       match tl with
 661           [] -> [],metasubst,metasenv,ugraph
 662         | ((uri,t) as subst)::tl ->
 663             let ty_uri,ugraph1 =  type_of_variable uri ugraph in
 664             let typeofvar =
 665               CicSubstitution.subst_vars substs ty_uri in
 666               (* CSC: why was this code here? it is wrong
 667                  (match CicEnvironment.get_cooked_obj ~trust:false uri with
 668                  Cic.Variable (_,Some bo,_,_) ->
 669                  raise
 670                  (RefineFailure
 671                  "A variable with a body can not be explicit substituted")
 672                  | Cic.Variable (_,None,_,_) -> ()
 673                  | _ ->
 674                  raise
 675                  (RefineFailure
 676                  ("Unkown variable definition " ^ UriManager.string_of_uri uri))
 677                  ) ;
 678               *)
 679             let t',typeoft,metasubst',metasenv',ugraph2 =
 680               type_of_aux metasubst metasenv context t ugraph1
 681             in
 682             let metasubst'',metasenv'',ugraph3 =
 683               try
 684                 fo_unif_subst
 685                   metasubst' context metasenv' typeoft typeofvar ugraph2
 686               with _ ->
 687                 raise (RefineFailure
 688                          ("Wrong Explicit Named Substitution: " ^
 689                            CicMetaSubst.ppterm metasubst' typeoft ^
 690                           " not unifiable with " ^
 691                           CicMetaSubst.ppterm metasubst' typeofvar))
 692             in
 693             (* FIXME: no mere tail recursive! *)
 694             let exp_name_subst, metasubst''', metasenv''', ugraph4 =
 695               check_exp_named_subst_aux
 696                 metasubst'' metasenv'' (substs@[subst]) tl ugraph3
 697             in
 698               ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
 699     in
 700       check_exp_named_subst_aux metasubst metasenv [] tl ugraph
 701
 702
 703   and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph =
 704     let module C = Cic in
 705     let context_for_t2 = (Some (name,C.Decl s))::context in
 706     let t1'' = CicReduction.whd ~subst context t1 in
 707     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
 708       match (t1'', t2'') with
 709           (C.Sort s1, C.Sort s2)
 710             when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 711               C.Sort s2,subst,metasenv,ugraph
 712         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 713             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 714             let t' = CicUniv.fresh() in
 715             let ugraph1 = CicUniv.add_ge t' t1 ugraph in
 716             let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
 717               C.Sort (C.Type t'),subst,metasenv,ugraph2
 718         | (C.Sort _,C.Sort (C.Type t1)) ->
 719             (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 720             C.Sort (C.Type t1),subst,metasenv,ugraph
 721         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
 722         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 723             (* TODO how can we force the meta to become a sort? If we don't we
 724              * brake the invariant that refine produce only well typed terms *)
 725             (* TODO if we check the non meta term and if it is a sort then we are
 726              * likely to know the exact value of the result e.g. if the rhs is a
 727              * Sort (Prop | Set | CProp) then the result is the rhs *)
 728             let (metasenv,idx) =
 729               CicMkImplicit.mk_implicit_sort metasenv subst in
 730             let (subst, metasenv,ugraph1) =
 731               fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
 732             in
 733               t2'',subst,metasenv,ugraph1
 734         | (_,_) ->
 735             raise (RefineFailure (sprintf
 736                                     "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 737                                     (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 738                                     (CicPp.ppterm t2'')))
 739
 740   and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
 741     let rec mk_prod metasenv context =
 742       function
 743           [] ->
 744             let (metasenv, idx) =
 745               CicMkImplicit.mk_implicit_type metasenv subst context
 746             in
 747             let irl =
 748               CicMkImplicit.identity_relocation_list_for_metavariable context
 749             in
 750               metasenv,Cic.Meta (idx, irl)
 751         | (_,argty)::tl ->
 752             let (metasenv, idx) =
 753               CicMkImplicit.mk_implicit_type metasenv subst context
 754             in
 755             let irl =
 756               CicMkImplicit.identity_relocation_list_for_metavariable context
 757             in
 758             let meta = Cic.Meta (idx,irl) in
 759             let name =
 760               (* The name must be fresh for context.                 *)
 761               (* Nevertheless, argty is well-typed only in context.  *)
 762               (* Thus I generate a name (name_hint) in context and   *)
 763               (* then I generate a name --- using the hint name_hint *)
 764               (* --- that is fresh in (context'@context).            *)
 765               let name_hint =
 766                 (* Cic.Name "pippo" *)
 767                 FreshNamesGenerator.mk_fresh_name ~subst metasenv
 768                   (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
 769                   (CicMetaSubst.apply_subst_context subst context)
 770                   Cic.Anonymous
 771                   ~typ:(CicMetaSubst.apply_subst subst argty)
 772               in
 773                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 774                 FreshNamesGenerator.mk_fresh_name ~subst
 775                   [] context name_hint ~typ:(Cic.Sort Cic.Prop)
 776             in
 777             let metasenv,target =
 778               mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 779             in
 780               metasenv,Cic.Prod (name,meta,target)
 781     in
 782     let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 783     let (subst, metasenv,ugraph1) =
 784       try
 785         fo_unif_subst subst context metasenv hetype hetype' ugraph
 786       with exn ->
 787         prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
 788                          (CicPp.ppterm hetype)
 789                          (CicPp.ppterm hetype')
 790                          (CicMetaSubst.ppmetasenv metasenv [])
 791                          (CicMetaSubst.ppsubst subst));
 792         raise exn
 793
 794     in
 795     let rec eat_prods metasenv subst context hetype ugraph =
 796       function
 797         | [] -> [],metasenv,subst,hetype,ugraph
 798         | (hete, hety)::tl ->
 799             (match hetype with
 800                  Cic.Prod (n,s,t) ->
 801                    let arg,subst,metasenv,ugraph1 =
 802                      try
 803                        let subst,metasenv,ugraph1 =
 804                          fo_unif_subst subst context metasenv hety s ugraph
 805                        in
 806                          hete,subst,metasenv,ugraph1
 807                      with exn ->
 808                        (* we search a coercion from hety to s *)
 809                        let coer = look_for_coercion
 810                          (CicMetaSubst.apply_subst subst hety)
 811                          (CicMetaSubst.apply_subst subst s)
 812                        in
 813                        match coer with
 814                        | None -> raise exn
 815                        | Some c ->
 816                            (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
 817                    in
 818                    let coerced_args,metasenv',subst',t',ugraph2 =
 819                      eat_prods metasenv subst context
 820                        (* (CicMetaSubst.subst subst hete t) tl *)
 821                        (CicSubstitution.subst hete t) ugraph1 tl
 822                    in
 823                      arg::coerced_args,metasenv',subst',t',ugraph2
 824                | _ -> assert false
 825             )
 826     in
 827     let coerced_args,metasenv,subst,t,ugraph2 =
 828       eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type
 829     in
 830       coerced_args,t,subst,metasenv,ugraph2
 831   in
 832
 833   (* eat prods ends here! *)
 834
 835   let t',ty,subst',metasenv',ugraph1 =
 836    type_of_aux [] metasenv context t ugraph
 837   in
 838   let substituted_t = CicMetaSubst.apply_subst subst' t' in
 839   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 840     (* Andrea: ho rimesso qui l'applicazione della subst al
 841        metasenv dopo che ho droppato l'invariante che il metsaenv
 842        e' sempre istanziato *)
 843   let substituted_metasenv =
 844     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
 845     (* metasenv' *)
 846     (*  substituted_t,substituted_ty,substituted_metasenv *)
 847     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
 848   let cleaned_t =
 849     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 850   let cleaned_ty =
 851     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 852   let cleaned_metasenv =
 853     List.map
 854       (function (n,context,ty) ->
 855          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 856          let context' =
 857            List.map
 858              (function
 859                   None -> None
 860                 | Some (n, Cic.Decl t) ->
 861                     Some (n,
 862                           Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 863                 | Some (n, Cic.Def (bo,ty)) ->
 864                     let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 865                     let ty' =
 866                       match ty with
 867                           None -> None
 868                         | Some ty ->
 869                             Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 870                     in
 871                       Some (n, Cic.Def (bo',ty'))
 872              ) context
 873          in
 874            (n,context',ty')
 875       ) substituted_metasenv
 876   in
 877     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
 878 ;;
 879
 880 (* DEBUGGING ONLY
 881 let type_of_aux' metasenv context term =
 882  try
 883   let (t,ty,m) =
 884       type_of_aux' metasenv context term in
 885     debug_print
 886      ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 887    debug_print
 888     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
 889    (t,ty,m)
 890  with
 891  | RefineFailure msg as e ->
 892      debug_print ("@@@ REFINE FAILED: " ^ msg);
 893      raise e
 894  | Uncertain msg as e ->
 895      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
 896      raise e
 897 ;; *)