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 WrongUriToMutualInductiveDefinitions of string;;
  32 exception RelToHiddenHypothesis;;
  33 exception MetasenvInconsistency;;
  34 exception MutCaseFixAndCofixRefineNotImplemented;;
  35 exception FreeMetaFound of int;;
  36
  37 let fdebug = ref 0;;
  38 let debug t context =
  39  let rec debug_aux t i =
  40   let module C = Cic in
  41   let module U = UriManager in
  42    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  43  in
  44   if !fdebug = 0 then
  45    raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
  46    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
  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   match CicEnvironment.get_cooked_obj uri with
  54      C.Constant (_,_,ty,_) -> ty
  55    | C.CurrentProof (_,_,_,ty,_) -> ty
  56    | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
  57
  58 and type_of_variable 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.Variable (_,_,ty,_) -> ty
  64    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
  65
  66 and type_of_mutual_inductive_defs uri i =
  67  let module C = Cic in
  68  let module R = CicReduction in
  69  let module U = UriManager in
  70   match CicEnvironment.get_cooked_obj uri with
  71      C.InductiveDefinition (dl,_,_) ->
  72       let (_,_,arity,_) = List.nth dl i in
  73        arity
  74    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  75
  76 and type_of_mutual_inductive_constr uri i j =
  77  let module C = Cic in
  78  let module R = CicReduction in
  79  let module U = UriManager in
  80   match CicEnvironment.get_cooked_obj uri with
  81       C.InductiveDefinition (dl,_,_) ->
  82        let (_,_,_,cl) = List.nth dl i in
  83         let (_,ty) = List.nth cl (j-1) in
  84          ty
  85    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  86
  87 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
  88 and type_of_aux' metasenv context t =
  89  let rec type_of_aux subst metasenv context =
  90   let module C = Cic in
  91   let module S = CicSubstitution in
  92   let module U = UriManager in
  93   let module Un = CicUnification in
  94    function
  95       C.Rel n ->
  96        (try
  97          match List.nth context (n - 1) with
  98             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
  99           | Some (_,C.Def bo) ->
 100              type_of_aux subst metasenv context (S.lift n bo)
 101           | None -> raise RelToHiddenHypothesis
 102         with
 103          _ -> raise (NotRefinable "Not a close term")
 104        )
 105     | C.Var (uri,exp_named_subst) ->
 106       incr fdebug ;
 107       let subst',metasenv' =
 108        check_exp_named_subst subst metasenv context exp_named_subst in
 109       let ty =
 110        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
 111       in
 112        decr fdebug ;
 113        ty,subst',metasenv'
 114     | C.Meta (n,l) ->
 115        let (_,canonical_context,ty) =
 116         try
 117          List.find (function (m,_,_) -> n = m) metasenv
 118         with
 119          Not_found -> raise (FreeMetaFound n)
 120        in
 121         let subst',metasenv' =
 122          check_metasenv_consistency subst metasenv context canonical_context l
 123         in
 124          CicSubstitution.lift_meta l ty, subst', metasenv'
 125     | C.Sort s ->
 126        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
 127         subst,metasenv
 128     | C.Implicit -> raise (Impossible 21)
 129     | C.Cast (te,ty) ->
 130        let _,subst',metasenv' =
 131         type_of_aux subst metasenv context ty in
 132        let inferredty,subst'',metasenv'' =
 133         type_of_aux subst' metasenv' context ty
 134        in
 135         (try
 136           let subst''',metasenv''' =
 137            Un.fo_unif_subst subst'' context metasenv'' inferredty ty
 138           in
 139            ty,subst''',metasenv'''
 140          with
 141           _ -> raise (NotRefinable "Cast"))
 142     | C.Prod (name,s,t) ->
 143        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 144        let sort2,subst'',metasenv'' =
 145         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
 146        in
 147         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
 148    | C.Lambda (n,s,t) ->
 149        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 150        let type2,subst'',metasenv'' =
 151         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 152        in
 153         let sort2,subst''',metasenv''' =
 154          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
 155         in
 156          (* only to check if the product is well-typed *)
 157          let _,subst'''',metasenv'''' =
 158           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
 159          in
 160           C.Prod (n,s,type2),subst'''',metasenv''''
 161    | C.LetIn (n,s,t) ->
 162       (* only to check if s is well-typed *)
 163       let _,subst',metasenv' = type_of_aux subst metasenv context s in
 164       let inferredty,subst'',metasenv'' =
 165        type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
 166       in
 167        (* One-step LetIn reduction. Even faster than the previous solution.
 168           Moreover the inferred type is closer to the expected one. *)
 169        CicSubstitution.subst s inferredty,subst',metasenv'
 170    | C.Appl (he::tl) when List.length tl > 0 ->
 171       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 172       let tlbody_and_type,subst'',metasenv'' =
 173        List.fold_right
 174         (fun x (res,subst,metasenv) ->
 175           let ty,subst',metasenv' =
 176            type_of_aux subst metasenv context x
 177           in
 178            (x, ty)::res,subst',metasenv'
 179         ) tl ([],subst',metasenv')
 180       in
 181        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 182    | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
 183    | C.Const (uri,exp_named_subst) ->
 184       incr fdebug ;
 185       let subst',metasenv' =
 186        check_exp_named_subst subst metasenv context exp_named_subst in
 187       let cty =
 188        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 189       in
 190        decr fdebug ;
 191        cty,subst',metasenv'
 192    | C.MutInd (uri,i,exp_named_subst) ->
 193       incr fdebug ;
 194       let subst',metasenv' =
 195        check_exp_named_subst subst metasenv context exp_named_subst in
 196       let cty =
 197        CicSubstitution.subst_vars exp_named_subst
 198         (type_of_mutual_inductive_defs uri i)
 199       in
 200        decr fdebug ;
 201        cty,subst',metasenv'
 202    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 203       let subst',metasenv' =
 204        check_exp_named_subst subst metasenv context exp_named_subst in
 205       let cty =
 206        CicSubstitution.subst_vars exp_named_subst
 207         (type_of_mutual_inductive_constr uri i j)
 208       in
 209        cty,subst',metasenv'
 210    | C.MutCase _
 211    | C.Fix _
 212    | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
 213
 214  (* check_metasenv_consistency checks that the "canonical" context of a
 215  metavariable is consitent - up to relocation via the relocation list l -
 216  with the actual context *)
 217  and check_metasenv_consistency subst metasenv context canonical_context l =
 218    let module C = Cic in
 219    let module R = CicReduction in
 220    let module S = CicSubstitution in
 221     let lifted_canonical_context =
 222      let rec aux i =
 223       function
 224          [] -> []
 225        | (Some (n,C.Decl t))::tl ->
 226           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 227        | (Some (n,C.Def t))::tl ->
 228           (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 229        | None::tl -> None::(aux (i+1) tl)
 230      in
 231       aux 1 canonical_context
 232     in
 233      List.fold_left2
 234       (fun (subst,metasenv) t ct ->
 235         match (t,ct) with
 236            _,None -> subst,metasenv
 237          | Some t,Some (_,C.Def ct) ->
 238             (try
 239               CicUnification.fo_unif_subst subst context metasenv t ct
 240              with _ -> raise MetasenvInconsistency)
 241          | Some t,Some (_,C.Decl ct) ->
 242             let inferredty,subst',metasenv' =
 243              type_of_aux subst metasenv context t
 244             in
 245              (try
 246                CicUnification.fo_unif_subst subst context metasenv inferredty ct
 247              with _ -> raise MetasenvInconsistency)
 248          | _, _  -> raise MetasenvInconsistency
 249       ) (subst,metasenv) l lifted_canonical_context
 250
 251  and check_exp_named_subst metasubst metasenv context =
 252   let rec check_exp_named_subst_aux metasubst metasenv substs =
 253    function
 254       [] -> metasubst,metasenv
 255     | ((uri,t) as subst)::tl ->
 256        let typeofvar =
 257         CicSubstitution.subst_vars substs (type_of_variable uri) in
 258        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 259            Cic.Variable (_,Some bo,_,_) ->
 260             raise
 261              (NotRefinable
 262                "A variable with a body can not be explicit substituted")
 263          | Cic.Variable (_,None,_,_) -> ()
 264          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 265        ) ;
 266        let typeoft,metasubst',metasenv' =
 267         type_of_aux metasubst metasenv context t
 268        in
 269         try
 270          let metasubst'',metasenv'' =
 271           CicUnification.fo_unif_subst
 272            metasubst' context metasenv' typeoft typeofvar
 273          in
 274           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 275         with _ ->
 276          raise (NotRefinable "Wrong Explicit Named Substitution")
 277   in
 278    check_exp_named_subst_aux metasubst metasenv []
 279
 280  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 281   let module C = Cic in
 282    (* ti could be a metavariable in the domain of the substitution *)
 283    let subst',metasenv' = CicUnification.unwind_subst metasenv subst in
 284    let t1' = CicUnification.apply_subst subst' t1 in
 285    let t2' = CicUnification.apply_subst subst' t2 in
 286     let t1'' = CicReduction.whd context t1' in
 287     let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' in
 288     match (t1'', t2'') with
 289        (C.Sort s1, C.Sort s2)
 290          when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
 291           C.Sort s2,subst',metasenv'
 292      | (C.Sort s1, C.Sort s2) ->
 293          (*CSC manca la gestione degli universi!!! *)
 294          C.Sort C.Type,subst',metasenv'
 295      | (C.Meta _,_)
 296      | (_,C.Meta _) ->
 297        raise
 298         (Uncertain
 299           ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
 300            CicPp.ppterm t2''))
 301      | (_,_) ->
 302        raise
 303         (NotRefinable
 304          ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
 305
 306  and eat_prods subst metasenv context hetype =
 307   function
 308      [] -> hetype,subst,metasenv
 309    | (hete, hety)::tl ->
 310     (match (CicReduction.whd context hetype) with
 311         Cic.Prod (n,s,t) ->
 312          let subst',metasenv' =
 313           try
 314            CicUnification.fo_unif_subst subst context metasenv s hety
 315           with _ ->
 316            raise (NotRefinable "Appl: wrong parameter-type")
 317          in
 318           CicReduction.fdebug := -1 ;
 319           eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
 320       | Cic.Meta _ as t ->
 321          raise
 322           (Uncertain
 323             ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
 324       | _ -> raise (NotRefinable "Appl: wrong Prod-type")
 325     )
 326  in
 327   let ty,subst',metasenv' =
 328    type_of_aux [] metasenv context t
 329   in
 330    let subst'',metasenv'' = CicUnification.unwind_subst metasenv' subst' in
 331    (* we get rid of the metavariables that have been instantiated *)
 332    let metasenv''' =
 333     List.filter
 334      (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
 335      metasenv''
 336    in
 337     CicUnification.apply_subst subst'' t,
 338      CicUnification.apply_subst subst'' ty,
 339      subst'', metasenv'''
 340 ;;
 341
 342 (* DEBUGGING ONLY *)
 343 let type_of_aux' metasenv context term =
 344  try
 345   let (t,ty,s,m) =
 346    type_of_aux' metasenv context term
 347   in
 348    List.iter
 349     (function (i,t) ->
 350       prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
 351    List.iter
 352     (function (i,_,t) ->
 353       prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
 354    prerr_endline
 355     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
 356    (t,ty,s,m)
 357  with
 358   e ->
 359    List.iter
 360     (function (i,_,t) ->
 361       prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
 362     metasenv ;
 363    prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
 364    raise e
 365 ;;