helm/gTopLevel/doubleTypeInference.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 NotWellTyped of string;;
  28 exception WrongUriToConstant of string;;
  29 exception WrongUriToVariable of string;;
  30 exception WrongUriToMutualInductiveDefinitions of string;;
  31 exception ListTooShort;;
  32 exception RelToHiddenHypothesis;;
  33
  34 type types = {synthesized : Cic.term ; expected : Cic.term};;
  35
  36 let rec split l n =
  37  match (l,n) with
  38     (l,0) -> ([], l)
  39   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  40   | (_,_) -> raise ListTooShort
  41 ;;
  42
  43 let cooked_type_of_constant uri cookingsno =
  44  let module C = Cic in
  45  let module R = CicReduction in
  46  let module U = UriManager in
  47   let cobj =
  48    match CicEnvironment.is_type_checked uri cookingsno with
  49       CicEnvironment.CheckedObj cobj -> cobj
  50     | CicEnvironment.UncheckedObj uobj ->
  51        raise (NotWellTyped "Reference to an unchecked constant")
  52   in
  53    match cobj with
  54       C.Definition (_,_,ty,_) -> ty
  55     | C.Axiom (_,ty,_) -> ty
  56     | C.CurrentProof (_,_,_,ty) -> ty
  57     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
  58 ;;
  59
  60 let type_of_variable uri =
  61  let module C = Cic in
  62  let module R = CicReduction in
  63  let module U = UriManager in
  64   (* 0 because a variable is never cooked => no partial cooking at one level *)
  65   match CicEnvironment.is_type_checked uri 0 with
  66      CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
  67    | CicEnvironment.UncheckedObj (C.Variable _) ->
  68       raise (NotWellTyped "Reference to an unchecked variable")
  69    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
  70 ;;
  71
  72 let cooked_type_of_mutual_inductive_defs uri cookingsno i =
  73  let module C = Cic in
  74  let module R = CicReduction in
  75  let module U = UriManager in
  76   let cobj =
  77    match CicEnvironment.is_type_checked uri cookingsno with
  78       CicEnvironment.CheckedObj cobj -> cobj
  79     | CicEnvironment.UncheckedObj uobj ->
  80        raise (NotWellTyped "Reference to an unchecked inductive type")
  81   in
  82    match cobj with
  83       C.InductiveDefinition (dl,_,_) ->
  84        let (_,_,arity,_) = List.nth dl i in
  85         arity
  86     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  87 ;;
  88
  89 let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
  90  let module C = Cic in
  91  let module R = CicReduction in
  92  let module U = UriManager in
  93   let cobj =
  94    match CicEnvironment.is_type_checked uri cookingsno with
  95       CicEnvironment.CheckedObj cobj -> cobj
  96     | CicEnvironment.UncheckedObj uobj ->
  97        raise (NotWellTyped "Reference to an unchecked constructor")
  98   in
  99    match cobj with
 100       C.InductiveDefinition (dl,_,_) ->
 101        let (_,_,_,cl) = List.nth dl i in
 102         let (_,ty,_) = List.nth cl (j-1) in
 103          ty
 104     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 105 ;;
 106
 107 module CicHash =
 108  Hashtbl.Make
 109   (struct
 110     type t = Cic.term
 111     let equal = (==)
 112     let hash = Hashtbl.hash
 113    end)
 114 ;;
 115
 116 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 117 let rec type_of_aux' subterms_to_types metasenv context t =
 118  (* Coscoy's double type-inference algorithm             *)
 119  (* It computes the inner-types of every subterm of [t], *)
 120  (* even when they are not needed to compute the types   *)
 121  (* of other terms.                                      *)
 122  let rec type_of_aux context t =
 123   let module C = Cic in
 124   let module R = CicReduction in
 125   let module S = CicSubstitution in
 126   let module U = UriManager in
 127    let synthesized =
 128     match t with
 129        C.Rel n ->
 130         (try
 131           match List.nth context (n - 1) with
 132              Some (_,C.Decl t) -> S.lift n t
 133            | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
 134            | None -> raise RelToHiddenHypothesis
 135          with
 136           _ -> raise (NotWellTyped "Not a close term")
 137         )
 138      | C.Var uri -> type_of_variable uri
 139      | C.Meta (n,l) ->
 140         (* Let's visit all the subterms that will not be visited later *)
 141         let _ =
 142          List.iter
 143           (function None -> () | Some t -> ignore (type_of_aux context t)) l
 144         in
 145          let (_,canonical_context,ty) =
 146           List.find (function (m,_,_) -> n = m) metasenv
 147          in
 148           (* Checks suppressed *)
 149           CicSubstitution.lift_meta l ty
 150      | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
 151      | C.Implicit -> raise (Impossible 21)
 152      | C.Cast (te,ty) ->
 153         (* Let's visit all the subterms that will not be visited later *)
 154         let _ = type_of_aux context te in
 155         let _ = type_of_aux context ty in
 156          (* Checks suppressed *)
 157          ty
 158      | C.Prod (name,s,t) ->
 159         let sort1 = type_of_aux context s
 160         and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
 161          sort_of_prod context (name,s) (sort1,sort2)
 162      | C.Lambda (n,s,t) ->
 163         (* Let's visit all the subterms that will not be visited later *)
 164         let _ = type_of_aux context s in
 165          let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
 166           (* Checks suppressed *)
 167           C.Prod (n,s,type2)
 168      | C.LetIn (n,s,t) ->
 169         (* Let's visit all the subterms that will not be visited later *)
 170         let _ = type_of_aux context s in
 171          (* Checks suppressed *)
 172          C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
 173      | C.Appl (he::tl) when List.length tl > 0 ->
 174         let hetype = type_of_aux context he
 175         and tlbody_and_type =
 176          List.map (fun x -> (x, type_of_aux context x)) tl
 177         in
 178          eat_prods context hetype tlbody_and_type
 179      | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
 180      | C.Const (uri,cookingsno) ->
 181         cooked_type_of_constant uri cookingsno
 182      | C.Abst _ -> raise (Impossible 22)
 183      | C.MutInd (uri,cookingsno,i) ->
 184         cooked_type_of_mutual_inductive_defs uri cookingsno i
 185      | C.MutConstruct (uri,cookingsno,i,j) ->
 186         let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
 187          cty
 188      | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
 189         (* Let's visit all the subterms that will not be visited later *)
 190         let _ = List.map (type_of_aux context) pl in
 191          let outsort = type_of_aux context outtype in
 192          let (need_dummy, k) =
 193           let rec guess_args context t =
 194            match CicReduction.whd context t with
 195               C.Sort _ -> (true, 0)
 196             | C.Prod (name, s, t) ->
 197                let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
 198                 if n = 0 then
 199                  (* last prod before sort *)
 200                  match CicReduction.whd context s with
 201                     (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
 202                     C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
 203                      (false, 1)
 204                   | C.Appl ((C.MutInd (uri',_,i')) :: _)
 205                      when U.eq uri' uri && i' = i -> (false, 1)
 206                   | _ -> (true, 1)
 207                 else
 208                  (b, n + 1)
 209             | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
 210           in
 211            (*CSC whd non serve dopo type_of_aux ? *)
 212            let (b, k) = guess_args context outsort in
 213             if not b then (b, k - 1) else (b, k)
 214          in
 215          let (_, arguments) =
 216            match R.whd context (type_of_aux context term) with
 217               (*CSC manca il caso dei CAST *)
 218               C.MutInd (uri',_,i') ->
 219                (* Checks suppressed *)
 220                [],[]
 221             | C.Appl (C.MutInd (uri',_,i') :: tl) ->
 222                split tl (List.length tl - k)
 223             | _ ->
 224               raise (NotWellTyped "MutCase: the term is not an inductive one")
 225          in
 226           (* Checks suppressed *)
 227           if not need_dummy then
 228            C.Appl ((outtype::arguments)@[term])
 229           else if arguments = [] then
 230            outtype
 231           else
 232            C.Appl (outtype::arguments)
 233      | C.Fix (i,fl) ->
 234         (* Let's visit all the subterms that will not be visited later *)
 235         let context' =
 236          List.rev
 237           (List.map
 238             (fun (n,_,ty,_) ->
 239               let _ = type_of_aux context ty in
 240                (Some (C.Name n,(C.Decl ty)))
 241             ) fl
 242           ) @
 243           context
 244         in
 245          let _ =
 246           List.iter
 247            (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
 248          in
 249           (* Checks suppressed *)
 250           let (_,_,ty,_) = List.nth fl i in
 251            ty
 252      | C.CoFix (i,fl) ->
 253         (* Let's visit all the subterms that will not be visited later *)
 254         let context' =
 255          List.rev
 256           (List.map
 257             (fun (n,ty,_) ->
 258               let _ = type_of_aux context ty in
 259                (Some (C.Name n,(C.Decl ty)))
 260             ) fl
 261           ) @
 262           context
 263         in
 264          let _ =
 265           List.iter
 266            (fun (_,_,bo) -> ignore (type_of_aux context' bo))
 267          in
 268           (* Checks suppressed *)
 269           let (_,ty,_) = List.nth fl i in
 270            ty
 271    in
 272     (*CSC: Is whd the right thing to do? Or should full beta *)
 273     (*CSC: reduction be more appropriate?                    *)
 274 (*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
 275 (*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
 276     let synthesized' = CicReduction.whd context synthesized in
 277      CicHash.add subterms_to_types t
 278       {synthesized = synthesized' ; expected = Cic.Implicit} ;
 279      synthesized'
 280
 281  and sort_of_prod context (name,s) (t1, t2) =
 282   let module C = Cic in
 283    let t1' = CicReduction.whd context t1 in
 284    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
 285    match (t1', t2') with
 286       (C.Sort s1, C.Sort s2)
 287         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
 288          C.Sort s2
 289     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
 290     | (_,_) ->
 291       raise
 292        (NotWellTyped
 293         ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
 294
 295  and eat_prods context hetype =
 296   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
 297   (*CSC: cucinati                                                         *)
 298   function
 299      [] -> hetype
 300    | (hete, hety)::tl ->
 301     (match (CicReduction.whd context hetype) with
 302         Cic.Prod (n,s,t) ->
 303          (* Checks suppressed *)
 304          eat_prods context (CicSubstitution.subst hete t) tl
 305       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
 306     )
 307
 308  in
 309   type_of_aux context t
 310 ;;
 311
 312 let double_type_of metasenv context t =
 313  let subterms_to_types = CicHash.create 503 in
 314   ignore (type_of_aux' subterms_to_types metasenv context t) ;
 315   subterms_to_types
 316 ;;