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 exception Impossible of int;;
  27 exception NotRefinable of string;;
  28 exception Uncertain of string;;
  29 exception WrongUriToConstant of string;;
  30 exception WrongUriToVariable of string;;
  31 exception ListTooShort;;
  32 exception WrongUriToMutualInductiveDefinitions of string;;
  33 exception RelToHiddenHypothesis;;
  34 exception MetasenvInconsistency;;
  35 exception MutCaseFixAndCofixRefineNotImplemented;;
  36 exception FreeMetaFound of int;;
  37 exception WrongArgumentNumber;;
  38
  39 let fdebug = ref 0;;
  40 let debug t context =
  41  let rec debug_aux t i =
  42   let module C = Cic in
  43   let module U = UriManager in
  44    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  45  in
  46   if !fdebug = 0 then
  47    raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
  48    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
  49 ;;
  50
  51 let rec split l n =
  52  match (l,n) with
  53     (l,0) -> ([], l)
  54   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  55   | (_,_) -> raise ListTooShort
  56 ;;
  57
  58 let rec type_of_constant uri =
  59  let module C = Cic in
  60  let module R = CicReduction in
  61  let module U = UriManager in
  62   match CicEnvironment.get_cooked_obj uri with
  63      C.Constant (_,_,ty,_) -> ty
  64    | C.CurrentProof (_,_,_,ty,_) -> ty
  65    | _ -> raise (WrongUriToConstant (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   match CicEnvironment.get_cooked_obj uri with
  72      C.Variable (_,_,ty,_) -> ty
  73    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
  74
  75 and type_of_mutual_inductive_defs uri i =
  76  let module C = Cic in
  77  let module R = CicReduction in
  78  let module U = UriManager in
  79   match CicEnvironment.get_cooked_obj uri with
  80      C.InductiveDefinition (dl,_,_) ->
  81       let (_,_,arity,_) = List.nth dl i in
  82        arity
  83    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  84
  85 and type_of_mutual_inductive_constr uri i j =
  86  let module C = Cic in
  87  let module R = CicReduction in
  88  let module U = UriManager in
  89   match CicEnvironment.get_cooked_obj uri with
  90       C.InductiveDefinition (dl,_,_) ->
  91        let (_,_,_,cl) = List.nth dl i in
  92         let (_,ty) = List.nth cl (j-1) in
  93          ty
  94    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  95
  96 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
  97
  98 (* the check_branch function checks if a branch of a case is refinable.
  99    It returns a pair (outype_instance,args), a subst and a metasenv.
 100    outype_instance is the expected result of applying the case outtype
 101    to args.
 102    The problem is that outype is in general unknown, and we should
 103    try to synthesize it from the above information, that is in general
 104    a second order unification problem. *)
 105
 106 and check_branch context metasenv subst left_args_no actualtype term expectedtype =
 107   let module C = Cic in
 108   let module R = CicReduction in
 109   let module Un = CicUnification in
 110   match R.whd context expectedtype with
 111      C.MutInd (_,_,_) ->
 112        (actualtype, [term]), subst, metasenv
 113    | C.Appl (C.MutInd (_,_,_)::tl) ->
 114        let (_,arguments) = split tl left_args_no in
 115        (actualtype, arguments@[term]), subst, metasenv
 116    | C.Prod (name,so,de) ->
 117       (* we expect that the actual type of the branch has the due
 118          number of Prod *)
 119       (match R.whd context actualtype with
 120            C.Prod (name',so',de') ->
 121              let subst,metsaenv =
 122                 Un.fo_unif_subst subst context metasenv so so' in
 123              let term' =
 124                (match CicSubstitution.lift 1 term with
 125                    C.Appl l -> C.Appl (l@[C.Rel 1])
 126                  | t -> C.Appl [t ; C.Rel 1]) in
 127              (* we should also check that the name variable is anonymous in
 128              the actual type de' ?? *)
 129              check_branch ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
 130          | _ -> raise WrongArgumentNumber)
 131   | _ -> raise (NotRefinable "Prod or MutInd expected")
 132
 133 and type_of_aux' metasenv context t =
 134  let rec type_of_aux subst metasenv context =
 135   let module C = Cic in
 136   let module S = CicSubstitution in
 137   let module U = UriManager in
 138   let module Un = CicUnification in
 139    function
 140       C.Rel n ->
 141        (try
 142          match List.nth context (n - 1) with
 143             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
 144           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
 145           | Some (_,C.Def (bo,None)) ->
 146              prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
 147              type_of_aux subst metasenv context (S.lift n bo)
 148           | None -> raise RelToHiddenHypothesis
 149         with
 150          _ -> raise (NotRefinable "Not a close term")
 151        )
 152     | C.Var (uri,exp_named_subst) ->
 153       incr fdebug ;
 154       let subst',metasenv' =
 155        check_exp_named_subst subst metasenv context exp_named_subst in
 156       let ty =
 157        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
 158       in
 159        decr fdebug ;
 160        ty,subst',metasenv'
 161     | C.Meta (n,l) ->
 162        let (_,canonical_context,ty) =
 163         try
 164          List.find (function (m,_,_) -> n = m) metasenv
 165         with
 166          Not_found -> raise (FreeMetaFound n)
 167        in
 168         let subst',metasenv' =
 169          check_metasenv_consistency subst metasenv context canonical_context l
 170         in
 171          CicSubstitution.lift_meta l ty, subst', metasenv'
 172     | C.Sort s ->
 173        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
 174         subst,metasenv
 175     | C.Implicit -> raise (Impossible 21)
 176     | C.Cast (te,ty) ->
 177        let _,subst',metasenv' =
 178         type_of_aux subst metasenv context ty in
 179        let inferredty,subst'',metasenv'' =
 180         type_of_aux subst' metasenv' context ty
 181        in
 182         (try
 183           let subst''',metasenv''' =
 184            Un.fo_unif_subst subst'' context metasenv'' inferredty ty
 185           in
 186            ty,subst''',metasenv'''
 187          with
 188           _ -> raise (NotRefinable "Cast"))
 189     | C.Prod (name,s,t) ->
 190        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 191        let sort2,subst'',metasenv'' =
 192         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
 193        in
 194         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
 195    | C.Lambda (n,s,t) ->
 196        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 197        let type2,subst'',metasenv'' =
 198         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 199        in
 200         let sort2,subst''',metasenv''' =
 201          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
 202         in
 203          (* only to check if the product is well-typed *)
 204          let _,subst'''',metasenv'''' =
 205           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
 206          in
 207           C.Prod (n,s,type2),subst'''',metasenv''''
 208    | C.LetIn (n,s,t) ->
 209       (* only to check if s is well-typed *)
 210       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
 211       let inferredty,subst'',metasenv'' =
 212        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
 213       in
 214        (* One-step LetIn reduction. Even faster than the previous solution.
 215           Moreover the inferred type is closer to the expected one. *)
 216        CicSubstitution.subst s inferredty,subst',metasenv'
 217    | C.Appl (he::tl) when List.length tl > 0 ->
 218       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 219       let tlbody_and_type,subst'',metasenv'' =
 220        List.fold_right
 221         (fun x (res,subst,metasenv) ->
 222           let ty,subst',metasenv' =
 223            type_of_aux subst metasenv context x
 224           in
 225            (x, ty)::res,subst',metasenv'
 226         ) tl ([],subst',metasenv')
 227       in
 228        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 229    | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
 230    | C.Const (uri,exp_named_subst) ->
 231       incr fdebug ;
 232       let subst',metasenv' =
 233        check_exp_named_subst subst metasenv context exp_named_subst in
 234       let cty =
 235        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 236       in
 237        decr fdebug ;
 238        cty,subst',metasenv'
 239    | C.MutInd (uri,i,exp_named_subst) ->
 240       incr fdebug ;
 241       let subst',metasenv' =
 242        check_exp_named_subst subst metasenv context exp_named_subst in
 243       let cty =
 244        CicSubstitution.subst_vars exp_named_subst
 245         (type_of_mutual_inductive_defs uri i)
 246       in
 247        decr fdebug ;
 248        cty,subst',metasenv'
 249    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 250       let subst',metasenv' =
 251        check_exp_named_subst subst metasenv context exp_named_subst in
 252       let cty =
 253        CicSubstitution.subst_vars exp_named_subst
 254         (type_of_mutual_inductive_constr uri i j)
 255       in
 256        cty,subst',metasenv'
 257    | C.MutCase (uri, i, outtype, term, pl) ->
 258        (* first, get the inductive type (and noparams) in the environment  *)
 259        let (_,b,arity,constructors), expl_params, no_left_params =
 260          match CicEnvironment.get_cooked_obj ~trust:true uri with
 261             C.InductiveDefinition (l,expl_params,parsno) ->
 262               List.nth l i , expl_params, parsno
 263           | _ ->
 264             raise
 265              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
 266        let rec count_prod t =
 267          match CicReduction.whd context t with
 268              C.Prod (_, _, t) -> 1 + (count_prod t)
 269            | _ -> 0 in
 270        let no_args = count_prod arity in
 271        (* now, create a "generic" MutInd *)
 272        let metasenv,left_args =
 273          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
 274        let metasenv,right_args =
 275          let no_right_params = no_args - no_left_params in
 276          if no_right_params < 0 then assert false
 277          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
 278        let metasenv,exp_named_subst =
 279          CicMkImplicit.fresh_subst metasenv context expl_params in
 280        let expected_type =
 281          if no_args = 0 then
 282            C.MutInd (uri,i,exp_named_subst)
 283          else
 284            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 285        in
 286        (* check consistency with the actual type of term *)
 287        let actual_type,subst,metasenv =
 288          type_of_aux subst metasenv context term in
 289        let subst,metasenv =
 290          Un.fo_unif_subst
 291            subst
 292            context
 293            metasenv expected_type (CicReduction.whd context actual_type) in
 294        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 295        let (_,outtypeinstances,subst,metasenv) =
 296           List.fold_left
 297            (fun (j,outtypeinstances,subst,metasenv) p ->
 298              let constructor =
 299               if left_args = [] then
 300                (C.MutConstruct (uri,i,j,exp_named_subst))
 301               else
 302                (C.Appl
 303                  (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 304              in
 305              let actual_type,subst,metasenv =
 306                type_of_aux subst metasenv context p in
 307              let expected_type, subst, metasenv =
 308                type_of_aux subst metasenv context constructor in
 309              let outtypeinstance,subst,metasenv =
 310                check_branch
 311                 context metasenv subst
 312                 no_left_params actual_type constructor expected_type in
 313              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
 314             (1,[],subst,metasenv) pl in
 315         (* we are left to check that the outype matches his instances.
 316            The easy case is when the outype is specified, that amount
 317            to a trivial check. Otherwise, we should guess a type from
 318            its instances *)
 319         (* easy case *)
 320         let (subst,metasenv) =
 321           List.fold_left
 322             (fun (subst,metasenv) (instance,args) ->
 323                let instance' =
 324                  CicReduction.whd context (C.Appl(outtype::args)) in
 325                Un.fo_unif_subst subst context metasenv instance instance')
 326              (subst,metasenv) outtypeinstances in
 327         CicReduction.whd
 328           context (C.Appl(outtype::right_args@[term])),subst,metasenv
 329    | C.Fix _
 330    | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
 331
 332  (* check_metasenv_consistency checks that the "canonical" context of a
 333  metavariable is consitent - up to relocation via the relocation list l -
 334  with the actual context *)
 335  and check_metasenv_consistency subst metasenv context canonical_context l =
 336    let module C = Cic in
 337    let module R = CicReduction in
 338    let module S = CicSubstitution in
 339     let lifted_canonical_context =
 340      let rec aux i =
 341       function
 342          [] -> []
 343        | (Some (n,C.Decl t))::tl ->
 344           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 345        | (Some (n,C.Def (t,None)))::tl ->
 346           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 347        | None::tl -> None::(aux (i+1) tl)
 348        | (Some (_,C.Def (_,Some _)))::_ -> assert false
 349      in
 350       aux 1 canonical_context
 351     in
 352      List.fold_left2
 353       (fun (subst,metasenv) t ct ->
 354         match (t,ct) with
 355            _,None -> subst,metasenv
 356          | Some t,Some (_,C.Def (ct,_)) ->
 357             (try
 358               CicUnification.fo_unif_subst subst context metasenv t ct
 359              with _ -> raise MetasenvInconsistency)
 360          | Some t,Some (_,C.Decl ct) ->
 361             let inferredty,subst',metasenv' =
 362              type_of_aux subst metasenv context t
 363             in
 364              (try
 365                CicUnification.fo_unif_subst subst context metasenv inferredty ct
 366              with _ -> raise MetasenvInconsistency)
 367          | _, _  -> raise MetasenvInconsistency
 368       ) (subst,metasenv) l lifted_canonical_context
 369
 370  and check_exp_named_subst metasubst metasenv context =
 371   let rec check_exp_named_subst_aux metasubst metasenv substs =
 372    function
 373       [] -> metasubst,metasenv
 374     | ((uri,t) as subst)::tl ->
 375        let typeofvar =
 376         CicSubstitution.subst_vars substs (type_of_variable uri) in
 377        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 378            Cic.Variable (_,Some bo,_,_) ->
 379             raise
 380              (NotRefinable
 381                "A variable with a body can not be explicit substituted")
 382          | Cic.Variable (_,None,_,_) -> ()
 383          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 384        ) ;
 385        let typeoft,metasubst',metasenv' =
 386         type_of_aux metasubst metasenv context t
 387        in
 388         try
 389          let metasubst'',metasenv'' =
 390           CicUnification.fo_unif_subst
 391            metasubst' context metasenv' typeoft typeofvar
 392          in
 393           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 394         with _ ->
 395          raise (NotRefinable "Wrong Explicit Named Substitution")
 396   in
 397    check_exp_named_subst_aux metasubst metasenv []
 398
 399  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 400   let module C = Cic in
 401    (* ti could be a metavariable in the domain of the substitution *)
 402    let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
 403    let t1' = CicUnification.apply_subst subst' t1 in
 404    let t2' = CicUnification.apply_subst subst' t2 in
 405     let t1'' = CicReduction.whd context t1' in
 406     let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
 407     match (t1'', t2'') with
 408        (C.Sort s1, C.Sort s2)
 409          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
 410           C.Sort s2,subst',metasenv'
 411      | (C.Sort s1, C.Sort s2) ->
 412          (*CSC manca la gestione degli universi!!! *)
 413          C.Sort C.Type,subst',metasenv'
 414      | (C.Meta _,_)
 415      | (_,C.Meta _) ->
 416        raise
 417         (Uncertain
 418           ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
 419            CicPp.ppterm t2''))
 420      | (_,_) ->
 421        raise
 422         (NotRefinable
 423          ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
 424
 425  and eat_prods subst metasenv context hetype =
 426   function
 427      [] -> hetype,subst,metasenv
 428    | (hete, hety)::tl ->
 429     (match (CicReduction.whd context hetype) with
 430         Cic.Prod (n,s,t) ->
 431          let subst',metasenv' =
 432           try
 433            CicUnification.fo_unif_subst subst context metasenv s hety
 434           with _ ->
 435            raise (NotRefinable "Appl: wrong parameter-type")
 436          in
 437           CicReduction.fdebug := -1 ;
 438           eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
 439       | Cic.Meta _ as t ->
 440          raise
 441           (Uncertain
 442             ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
 443       | _ -> raise (NotRefinable "Appl: wrong Prod-type")
 444     )
 445  in
 446   let ty,subst',metasenv' =
 447    type_of_aux [] metasenv context t
 448   in
 449    let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
 450    (* we get rid of the metavariables that have been instantiated *)
 451    let metasenv''' =
 452     List.filter
 453      (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
 454      metasenv''
 455    in
 456     CicUnification.apply_subst subst'' t,
 457      CicUnification.apply_subst subst'' ty,
 458      subst'', metasenv'''
 459 ;;
 460
 461 (* DEBUGGING ONLY *)
 462 let type_of_aux' metasenv context term =
 463  try
 464   let (t,ty,s,m) =
 465    type_of_aux' metasenv context term
 466   in
 467    List.iter
 468     (function (i,t) ->
 469       prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
 470    List.iter
 471     (function (i,_,t) ->
 472       prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
 473    prerr_endline
 474     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
 475    (t,ty,s,m)
 476  with
 477   e ->
 478    List.iter
 479     (function (i,_,t) ->
 480       prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
 481     metasenv ;
 482    prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
 483    raise e
 484 ;;
 485
 486
 487
 488
 489
 490
 491
 492
 493
 494