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