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