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