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