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 option};;
  35
  36 (*CSC: potrebbe creare applicazioni di applicazioni *)
  37 (*CSC: ora non e' piu' head, ma completa!!! *)
  38 let rec head_beta_reduce =
  39  let module S = CicSubstitution in
  40  let module C = Cic in
  41   function
  42       C.Rel _
  43     | C.Var _ as t -> t
  44     | C.Meta (n,l) ->
  45        C.Meta (n,
  46         List.map
  47          (function None -> None | Some t -> Some (head_beta_reduce t)) l
  48        )
  49     | C.Sort _ as t -> t
  50     | C.Implicit -> assert false
  51     | C.Cast (te,ty) ->
  52        C.Cast (head_beta_reduce te, head_beta_reduce ty)
  53     | C.Prod (n,s,t) ->
  54        C.Prod (n, head_beta_reduce s, head_beta_reduce t)
  55     | C.Lambda (n,s,t) ->
  56        C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
  57     | C.LetIn (n,s,t) ->
  58        C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
  59     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
  60        let he' = S.subst he t in
  61         if tl = [] then
  62          head_beta_reduce he'
  63         else
  64          head_beta_reduce (C.Appl (he'::tl))
  65     | C.Appl l ->
  66        C.Appl (List.map head_beta_reduce l)
  67     | C.Const _ as t -> t
  68     | C.MutInd _
  69     | C.MutConstruct _ as t -> t
  70     | C.MutCase (sp,cno,i,outt,t,pl) ->
  71        C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
  72         List.map head_beta_reduce pl)
  73     | C.Fix (i,fl) ->
  74        let fl' =
  75         List.map
  76          (function (name,i,ty,bo) ->
  77            name,i,head_beta_reduce ty,head_beta_reduce bo
  78          ) fl
  79        in
  80         C.Fix (i,fl')
  81     | C.CoFix (i,fl) ->
  82        let fl' =
  83         List.map
  84          (function (name,ty,bo) ->
  85            name,head_beta_reduce ty,head_beta_reduce bo
  86          ) fl
  87        in
  88         C.CoFix (i,fl')
  89 ;;
  90
  91 (* syntactic_equality up to cookingsno for uris *)
  92 (* (which is often syntactically irrilevant),   *)
  93 (* distinction between fake dependent products  *)
  94 (* and non-dependent products, alfa-conversion  *)
  95 (*CSC: must alfa-conversion be considered or not? *)
  96 let syntactic_equality t t' =
  97  let module C = Cic in
  98  let rec syntactic_equality t t' =
  99   if t = t' then true
 100   else
 101    match t, t' with
 102       C.Rel _, C.Rel _
 103     | C.Var _, C.Var _
 104     | C.Meta _, C.Meta _
 105     | C.Sort _, C.Sort _
 106     | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
 107     | C.Cast (te,ty), C.Cast (te',ty') ->
 108        syntactic_equality te te' &&
 109         syntactic_equality ty ty'
 110     | C.Prod (_,s,t), C.Prod (_,s',t') ->
 111        syntactic_equality s s' &&
 112         syntactic_equality t t'
 113     | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
 114        syntactic_equality s s' &&
 115         syntactic_equality t t'
 116     | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
 117        syntactic_equality s s' &&
 118         syntactic_equality t t'
 119     | C.Appl l, C.Appl l' ->
 120        List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
 121     | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri'
 122     | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
 123        UriManager.eq uri uri' && i = i'
 124     | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
 125        UriManager.eq uri uri' && i = i' && j = j'
 126     | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
 127        UriManager.eq sp sp' && i = i' &&
 128         syntactic_equality outt outt' &&
 129          syntactic_equality t t' &&
 130           List.fold_left2
 131            (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
 132     | C.Fix (i,fl), C.Fix (i',fl') ->
 133        i = i' &&
 134         List.fold_left2
 135          (fun b (_,i,ty,bo) (_,i',ty',bo') ->
 136            b && i = i' &&
 137             syntactic_equality ty ty' &&
 138              syntactic_equality bo bo') true fl fl'
 139     | C.CoFix (i,fl), C.CoFix (i',fl') ->
 140        i = i' &&
 141         List.fold_left2
 142          (fun b (_,ty,bo) (_,ty',bo') ->
 143            b &&
 144             syntactic_equality ty ty' &&
 145              syntactic_equality bo bo') true fl fl'
 146     | _,_ -> false
 147  in
 148   try
 149    syntactic_equality t t'
 150   with
 151    _ -> false
 152 ;;
 153
 154 let rec split l n =
 155  match (l,n) with
 156     (l,0) -> ([], l)
 157   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
 158   | (_,_) -> raise ListTooShort
 159 ;;
 160
 161 let cooked_type_of_constant uri cookingsno =
 162  let module C = Cic in
 163  let module R = CicReduction in
 164  let module U = UriManager in
 165   let cobj =
 166    match CicEnvironment.is_type_checked uri cookingsno with
 167       CicEnvironment.CheckedObj cobj -> cobj
 168     | CicEnvironment.UncheckedObj uobj ->
 169        raise (NotWellTyped "Reference to an unchecked constant")
 170   in
 171    match cobj with
 172       C.Definition (_,_,ty,_) -> ty
 173     | C.Axiom (_,ty,_) -> ty
 174     | C.CurrentProof (_,_,_,ty) -> ty
 175     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 176 ;;
 177
 178 let type_of_variable uri =
 179  let module C = Cic in
 180  let module R = CicReduction in
 181  let module U = UriManager in
 182   (* 0 because a variable is never cooked => no partial cooking at one level *)
 183   match CicEnvironment.is_type_checked uri 0 with
 184      CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
 185    | CicEnvironment.UncheckedObj (C.Variable _) ->
 186       raise (NotWellTyped "Reference to an unchecked variable")
 187    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 188 ;;
 189
 190 let cooked_type_of_mutual_inductive_defs uri cookingsno i =
 191  let module C = Cic in
 192  let module R = CicReduction in
 193  let module U = UriManager in
 194   let cobj =
 195    match CicEnvironment.is_type_checked uri cookingsno with
 196       CicEnvironment.CheckedObj cobj -> cobj
 197     | CicEnvironment.UncheckedObj uobj ->
 198        raise (NotWellTyped "Reference to an unchecked inductive type")
 199   in
 200    match cobj with
 201       C.InductiveDefinition (dl,_,_) ->
 202        let (_,_,arity,_) = List.nth dl i in
 203         arity
 204     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 205 ;;
 206
 207 let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
 208  let module C = Cic in
 209  let module R = CicReduction in
 210  let module U = UriManager in
 211   let cobj =
 212    match CicEnvironment.is_type_checked uri cookingsno with
 213       CicEnvironment.CheckedObj cobj -> cobj
 214     | CicEnvironment.UncheckedObj uobj ->
 215        raise (NotWellTyped "Reference to an unchecked constructor")
 216   in
 217    match cobj with
 218       C.InductiveDefinition (dl,_,_) ->
 219        let (_,_,_,cl) = List.nth dl i in
 220         let (_,ty,_) = List.nth cl (j-1) in
 221          ty
 222     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 223 ;;
 224
 225 module CicHash =
 226  Hashtbl.Make
 227   (struct
 228     type t = Cic.term
 229     let equal = (==)
 230     let hash = Hashtbl.hash
 231    end)
 232 ;;
 233
 234 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 235 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
 236  (* Coscoy's double type-inference algorithm             *)
 237  (* It computes the inner-types of every subterm of [t], *)
 238  (* even when they are not needed to compute the types   *)
 239  (* of other terms.                                      *)
 240  let rec type_of_aux context t expectedty =
 241   let module C = Cic in
 242   let module R = CicReduction in
 243   let module S = CicSubstitution in
 244   let module U = UriManager in
 245    let synthesized =
 246     match t with
 247        C.Rel n ->
 248         (try
 249           match List.nth context (n - 1) with
 250              Some (_,C.Decl t) -> S.lift n t
 251            | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) expectedty
 252            | None -> raise RelToHiddenHypothesis
 253          with
 254           _ -> raise (NotWellTyped "Not a close term")
 255         )
 256      | C.Var uri -> type_of_variable uri
 257      | C.Meta (n,l) ->
 258         (* Let's visit all the subterms that will not be visited later *)
 259         let (_,canonical_context,_) =
 260          List.find (function (m,_,_) -> n = m) metasenv
 261         in
 262          let lifted_canonical_context =
 263           let rec aux i =
 264            function
 265               [] -> []
 266             | (Some (n,C.Decl t))::tl ->
 267                (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 268             | (Some (n,C.Def t))::tl ->
 269                (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 270             | None::tl -> None::(aux (i+1) tl)
 271           in
 272            aux 1 canonical_context
 273          in
 274           let _ =
 275            List.iter2
 276             (fun t ct ->
 277               match t,ct with
 278                  _,None -> ()
 279                | Some t,Some (_,C.Def ct) ->
 280                   let expected_type =
 281                    R.whd context
 282                     (CicTypeChecker.type_of_aux' metasenv context ct)
 283                   in
 284                    (* Maybe I am a bit too paranoid, because   *)
 285                    (* if the term is well-typed than t and ct  *)
 286                    (* are convertible. Nevertheless, I compute *)
 287                    (* the expected type.                       *)
 288                    ignore (type_of_aux context t (Some expected_type))
 289                | Some t,Some (_,C.Decl ct) ->
 290                   ignore (type_of_aux context t (Some ct))
 291                | _,_ -> assert false (* the term is not well typed!!! *)
 292             ) l lifted_canonical_context
 293           in
 294            let (_,canonical_context,ty) =
 295             List.find (function (m,_,_) -> n = m) metasenv
 296            in
 297             (* Checks suppressed *)
 298             CicSubstitution.lift_meta l ty
 299      | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
 300      | C.Implicit -> raise (Impossible 21)
 301      | C.Cast (te,ty) ->
 302         (* Let's visit all the subterms that will not be visited later *)
 303         let _ = type_of_aux context te (Some (head_beta_reduce ty)) in
 304         let _ = type_of_aux context ty None in
 305          (* Checks suppressed *)
 306          ty
 307      | C.Prod (name,s,t) ->
 308         let sort1 = type_of_aux context s None
 309         and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
 310          sort_of_prod context (name,s) (sort1,sort2)
 311      | C.Lambda (n,s,t) ->
 312         (* Let's visit all the subterms that will not be visited later *)
 313         let _ = type_of_aux context s None in
 314          let expected_target_type =
 315           match expectedty with
 316              None -> None
 317            | Some expectedty' ->
 318               let ty =
 319                match R.whd context expectedty' with
 320                   C.Prod (_,_,expected_target_type) ->
 321                    head_beta_reduce expected_target_type
 322                 | _ -> assert false
 323               in
 324                Some ty
 325          in
 326           let type2 =
 327            type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
 328           in
 329            (* Checks suppressed *)
 330            C.Prod (n,s,type2)
 331      | C.LetIn (n,s,t) ->
 332 (*CSC: What are the right expected types for the source and *)
 333 (*CSC: target of a LetIn? None used.                        *)
 334         (* Let's visit all the subterms that will not be visited later *)
 335         let _ = type_of_aux context s None in
 336          (* Checks suppressed *)
 337          C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
 338      | C.Appl (he::tl) when List.length tl > 0 ->
 339         let expected_hetype =
 340          (* Inefficient, the head is computed twice. But I know *)
 341          (* of no other solution.                               *)
 342          R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
 343         in
 344          let hetype = type_of_aux context he (Some expected_hetype) in
 345          let tlbody_and_type =
 346           let rec aux =
 347            function
 348               _,[] -> []
 349             | C.Prod (n,s,t),he::tl ->
 350                (he, type_of_aux context he (Some (head_beta_reduce s)))::
 351                 (aux (R.whd context (S.subst he t), tl))
 352             | _ -> assert false
 353           in
 354            aux (expected_hetype, tl)
 355          in
 356           eat_prods context hetype tlbody_and_type
 357      | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
 358      | C.Const (uri,cookingsno) ->
 359         cooked_type_of_constant uri cookingsno
 360      | C.MutInd (uri,cookingsno,i) ->
 361         cooked_type_of_mutual_inductive_defs uri cookingsno i
 362      | C.MutConstruct (uri,cookingsno,i,j) ->
 363         let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
 364          cty
 365      | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
 366         let outsort = type_of_aux context outtype None in
 367         let (need_dummy, k) =
 368          let rec guess_args context t =
 369           match CicReduction.whd context t with
 370              C.Sort _ -> (true, 0)
 371            | C.Prod (name, s, t) ->
 372               let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
 373                if n = 0 then
 374                 (* last prod before sort *)
 375                 match CicReduction.whd context s with
 376                    (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
 377                    C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
 378                     (false, 1)
 379                  | C.Appl ((C.MutInd (uri',_,i')) :: _)
 380                     when U.eq uri' uri && i' = i -> (false, 1)
 381                  | _ -> (true, 1)
 382                else
 383                 (b, n + 1)
 384            | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
 385          in
 386           let (b, k) = guess_args context outsort in
 387            if not b then (b, k - 1) else (b, k)
 388         in
 389         let (parameters, arguments) =
 390          let type_of_term =
 391           CicTypeChecker.type_of_aux' metasenv context term
 392          in
 393           match
 394            R.whd context (type_of_aux context term
 395             (Some (head_beta_reduce type_of_term)))
 396           with
 397              (*CSC manca il caso dei CAST *)
 398              C.MutInd (uri',_,i') ->
 399               (* Checks suppressed *)
 400               [],[]
 401            | C.Appl (C.MutInd (uri',_,i') :: tl) ->
 402               split tl (List.length tl - k)
 403            | _ ->
 404              raise (NotWellTyped "MutCase: the term is not an inductive one")
 405         in
 406          (* Checks suppressed *)
 407          (* Let's visit all the subterms that will not be visited later *)
 408          let (cl,parsno) =
 409           match CicEnvironment.get_cooked_obj uri cookingsno with
 410              C.InductiveDefinition (tl,_,parsno) ->
 411               let (_,_,_,cl) = List.nth tl i in (cl,parsno)
 412            | _ ->
 413              raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 414          in
 415           let _ =
 416            List.fold_left
 417             (fun j (p,(_,c,_)) ->
 418               let cons =
 419                if parameters = [] then
 420                 (C.MutConstruct (uri,cookingsno,i,j))
 421                else
 422                 (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
 423               in
 424                let expectedtype =
 425                 type_of_branch context parsno need_dummy outtype cons
 426                   (CicTypeChecker.type_of_aux' metasenv context cons)
 427                in
 428                 ignore (type_of_aux context p
 429                  (Some (head_beta_reduce expectedtype))) ;
 430                 j+1
 431             ) 1 (List.combine pl cl)
 432           in
 433            if not need_dummy then
 434             C.Appl ((outtype::arguments)@[term])
 435            else if arguments = [] then
 436             outtype
 437            else
 438             C.Appl (outtype::arguments)
 439      | C.Fix (i,fl) ->
 440         (* Let's visit all the subterms that will not be visited later *)
 441         let context' =
 442          List.rev
 443           (List.map
 444             (fun (n,_,ty,_) ->
 445               let _ = type_of_aux context ty None in
 446                (Some (C.Name n,(C.Decl ty)))
 447             ) fl
 448           ) @
 449           context
 450         in
 451          let _ =
 452           List.iter
 453            (fun (_,_,ty,bo) ->
 454              let expectedty =
 455               head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
 456              in
 457               ignore (type_of_aux context' bo (Some expectedty))
 458            ) fl
 459          in
 460           (* Checks suppressed *)
 461           let (_,_,ty,_) = List.nth fl i in
 462            ty
 463      | C.CoFix (i,fl) ->
 464         (* Let's visit all the subterms that will not be visited later *)
 465         let context' =
 466          List.rev
 467           (List.map
 468             (fun (n,ty,_) ->
 469               let _ = type_of_aux context ty None in
 470                (Some (C.Name n,(C.Decl ty)))
 471             ) fl
 472           ) @
 473           context
 474         in
 475          let _ =
 476           List.iter
 477            (fun (_,ty,bo) ->
 478              let expectedty =
 479               head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
 480              in
 481               ignore (type_of_aux context' bo (Some expectedty))
 482            ) fl
 483          in
 484           (* Checks suppressed *)
 485           let (_,ty,_) = List.nth fl i in
 486            ty
 487    in
 488     let synthesized' = head_beta_reduce synthesized in
 489      let types,res =
 490       match expectedty with
 491          None ->
 492           (* No expected type *)
 493           {synthesized = synthesized' ; expected = None}, synthesized
 494        | Some ty when syntactic_equality synthesized' ty ->
 495           (* The expected type is synthactically equal to *)
 496           (* the synthesized type. Let's forget it.       *)
 497           {synthesized = synthesized' ; expected = None}, synthesized
 498        | Some expectedty' ->
 499           {synthesized = synthesized' ; expected = Some expectedty'},
 500           expectedty'
 501      in
 502       CicHash.add subterms_to_types t types ;
 503       res
 504
 505  and sort_of_prod context (name,s) (t1, t2) =
 506   let module C = Cic in
 507    let t1' = CicReduction.whd context t1 in
 508    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
 509    match (t1', t2') with
 510       (C.Sort s1, C.Sort s2)
 511         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
 512          C.Sort s2
 513     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
 514     | (_,_) ->
 515       raise
 516        (NotWellTyped
 517         ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
 518
 519  and eat_prods context hetype =
 520   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
 521   (*CSC: cucinati                                                         *)
 522   function
 523      [] -> hetype
 524    | (hete, hety)::tl ->
 525     (match (CicReduction.whd context hetype) with
 526         Cic.Prod (n,s,t) ->
 527          (* Checks suppressed *)
 528          eat_prods context (CicSubstitution.subst hete t) tl
 529       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
 530     )
 531
 532 and type_of_branch context argsno need_dummy outtype term constype =
 533  let module C = Cic in
 534  let module R = CicReduction in
 535   match R.whd context constype with
 536      C.MutInd (_,_,_) ->
 537       if need_dummy then
 538        outtype
 539       else
 540        C.Appl [outtype ; term]
 541    | C.Appl (C.MutInd (_,_,_)::tl) ->
 542       let (_,arguments) = split tl argsno
 543       in
 544        if need_dummy && arguments = [] then
 545         outtype
 546        else
 547         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
 548    | C.Prod (name,so,de) ->
 549       let term' =
 550        match CicSubstitution.lift 1 term with
 551           C.Appl l -> C.Appl (l@[C.Rel 1])
 552         | t -> C.Appl [t ; C.Rel 1]
 553       in
 554        C.Prod (C.Anonimous,so,type_of_branch
 555         ((Some (name,(C.Decl so)))::context) argsno need_dummy
 556         (CicSubstitution.lift 1 outtype) term' de)
 557   | _ -> raise (Impossible 20)
 558
 559  in
 560   type_of_aux context t expectedty
 561 ;;
 562
 563 let double_type_of metasenv context t expectedty =
 564  let subterms_to_types = CicHash.create 503 in
 565   ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
 566   subterms_to_types
 567 ;;