]> matita.cs.unibo.it Git - helm.git/commitdiff
* doubleTypeInference.ml* added. For now, it just computes the synthesized type.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Jun 2002 17:39:19 +0000 (17:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Jun 2002 17:39:19 +0000 (17:39 +0000)
  The expected type is expected soon ;-)
* great performance improvement. For example, the rendering of limit_plus
  is now "only" 30s (was 50s)

helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/cic2acic.ml
helm/gTopLevel/cic2acic.mli
helm/gTopLevel/doubleTypeInference.ml [new file with mode: 0644]
helm/gTopLevel/doubleTypeInference.mli [new file with mode: 0644]

index 5a677d73a1cd89b817ba5900e7fa0eb43215f342..7d0186948c275aa14320080bbad92dc9142ea4d3 100644 (file)
@@ -1,7 +1,9 @@
 proofEngine.cmo: proofEngineReduction.cmo 
 proofEngine.cmx: proofEngineReduction.cmx 
-cic2acic.cmo: cic2acic.cmi 
-cic2acic.cmx: cic2acic.cmi 
+doubleTypeInference.cmo: doubleTypeInference.cmi 
+doubleTypeInference.cmx: doubleTypeInference.cmi 
+cic2acic.cmo: doubleTypeInference.cmi cic2acic.cmi 
+cic2acic.cmx: doubleTypeInference.cmx cic2acic.cmi 
 logicalOperations.cmo: proofEngine.cmo 
 logicalOperations.cmx: proofEngine.cmx 
 sequentPp.cmo: cic2Xml.cmo cic2acic.cmi proofEngine.cmo 
index 44c9887f77da93bef40a146ef523bb8a09203f9a..8a9c5e535792782c06f68609b80692f447ca2a06 100644 (file)
@@ -15,12 +15,13 @@ all: gTopLevel
 opt: gTopLevel.opt
 
 DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \
-          cic2acic.ml cic2acic.mli logicalOperations.ml sequentPp.ml \
-          mquery.mli mquery.ml gTopLevel.ml
+          doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
+          cic2acic.mli logicalOperations.ml sequentPp.ml mquery.mli \
+          mquery.ml gTopLevel.ml
 
 TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \
-               cic2Xml.cmo cic2acic.cmo logicalOperations.cmo sequentPp.cmo \
-               mquery.cmo gTopLevel.cmo
+               cic2Xml.cmo doubleTypeInference.cmo cic2acic.cmo \
+               logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo
 
 depend:
        $(OCAMLDEP) $(DEPOBJS) > .depend
index ffe9dbd4db98f0e1abe90fc2851b84484c3680c8..7b9511da11d1653d9db106c626235dc17b986d67 100644 (file)
@@ -53,9 +53,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
  let module T = CicTypeChecker in
  let module C = Cic in
   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
+   let terms_to_types = DoubleTypeInference.double_type_of metasenv context t in
    let rec aux computeinnertypes father context tt =
     let fresh_id'' = fresh_id' father tt in
-    let aux' = aux true (Some fresh_id'') in
+    (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
+    let aux' = aux computeinnertypes (Some fresh_id'') in
      (* First of all we compute the inner type and the inner sort *)
      (* of the term. They may be useful in what follows.          *)
      (*CSC: This is a very inefficient way of computing inner types *)
@@ -71,11 +73,19 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       let ainnertype,innertype,innersort =
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
 (*CSC: (expected type + inferred type). Just for now we use the usual *)
-(*CSC: type-inference, but the result is very poort. As a very weak   *)
+(*CSC: type-inference, but the result is very poor. As a very weak    *)
 (*CSC: patch, I apply whd to the computed type. Full beta             *)
 (*CSC: reduction would be a much better option.                       *)
         let innertype =
-         CicReduction.whd context (T.type_of_aux' metasenv context tt)
+         if computeinnertypes then
+          let {DoubleTypeInference.synthesized = synthesized} =
+           DoubleTypeInference.CicHash.find terms_to_types tt
+          in
+           synthesized
+         else
+          (* We are already in an inner-type and Coscoy's double *)
+          (* type inference algorithm has not been applied.      *)
+          CicReduction.whd context (T.type_of_aux' metasenv context tt)
         in
          let innersort = T.type_of_aux' metasenv context innertype in
           let ainnertype =
@@ -203,8 +213,6 @@ let acic_of_cic_context metasenv context t =
    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
 
-exception Found of (Cic.name * Cic.context_entry) list;;
-
 let acic_object_of_cic_object obj =
  let module C = Cic in
   let ids_to_terms = Hashtbl.create 503 in
index 479a5760c63f9fadb0906fdc498efeed31f8baf5..a2c0497f1e3658aebaa8dfa270ccae89b65de7bf 100644 (file)
@@ -26,8 +26,6 @@
 exception NotImplemented
 exception NotEnoughElements
 exception NameExpected
-exception Found of (Cic.name * Cic.context_entry) list
-exception NotImplemented
 
 val acic_of_cic_context' :
   int ref ->                              (* seed *)
diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
new file mode 100644 (file)
index 0000000..50a81c5
--- /dev/null
@@ -0,0 +1,316 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+exception Impossible of int;;
+exception NotWellTyped of string;;
+exception WrongUriToConstant of string;;
+exception WrongUriToVariable of string;;
+exception WrongUriToMutualInductiveDefinitions of string;;
+exception ListTooShort;;
+exception RelToHiddenHypothesis;;
+
+type types = {synthesized : Cic.term ; expected : Cic.term};;
+
+let rec split l n =
+ match (l,n) with
+    (l,0) -> ([], l)
+  | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
+  | (_,_) -> raise ListTooShort
+;;
+
+let cooked_type_of_constant uri cookingsno =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  let cobj =
+   match CicEnvironment.is_type_checked uri cookingsno with
+      CicEnvironment.CheckedObj cobj -> cobj
+    | CicEnvironment.UncheckedObj uobj ->
+       raise (NotWellTyped "Reference to an unchecked constant")
+  in
+   match cobj with
+      C.Definition (_,_,ty,_) -> ty
+    | C.Axiom (_,ty,_) -> ty
+    | C.CurrentProof (_,_,_,ty) -> ty
+    | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+;;
+
+let type_of_variable uri =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  (* 0 because a variable is never cooked => no partial cooking at one level *)
+  match CicEnvironment.is_type_checked uri 0 with
+     CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
+   | CicEnvironment.UncheckedObj (C.Variable _) ->
+      raise (NotWellTyped "Reference to an unchecked variable")
+   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+;;
+
+let cooked_type_of_mutual_inductive_defs uri cookingsno i =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  let cobj =
+   match CicEnvironment.is_type_checked uri cookingsno with
+      CicEnvironment.CheckedObj cobj -> cobj
+    | CicEnvironment.UncheckedObj uobj ->
+       raise (NotWellTyped "Reference to an unchecked inductive type")
+  in
+   match cobj with
+      C.InductiveDefinition (dl,_,_) ->
+       let (_,_,arity,_) = List.nth dl i in
+        arity
+    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+;;
+
+let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  let cobj =
+   match CicEnvironment.is_type_checked uri cookingsno with
+      CicEnvironment.CheckedObj cobj -> cobj
+    | CicEnvironment.UncheckedObj uobj ->
+       raise (NotWellTyped "Reference to an unchecked constructor")
+  in
+   match cobj with
+      C.InductiveDefinition (dl,_,_) ->
+       let (_,_,_,cl) = List.nth dl i in
+        let (_,ty,_) = List.nth cl (j-1) in
+         ty
+    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+;;
+
+module CicHash =
+ Hashtbl.Make
+  (struct
+    type t = Cic.term
+    let equal = (==)
+    let hash = Hashtbl.hash
+   end)
+;;
+
+(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
+let rec type_of_aux' subterms_to_types metasenv context t =
+ (* Coscoy's double type-inference algorithm             *)
+ (* It computes the inner-types of every subterm of [t], *)
+ (* even when they are not needed to compute the types   *)
+ (* of other terms.                                      *)
+ let rec type_of_aux context t =
+  let module C = Cic in
+  let module R = CicReduction in
+  let module S = CicSubstitution in
+  let module U = UriManager in
+   let synthesized =
+    match t with
+       C.Rel n ->
+        (try
+          match List.nth context (n - 1) with
+             Some (_,C.Decl t) -> S.lift n t
+           | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
+          | None -> raise RelToHiddenHypothesis
+         with
+          _ -> raise (NotWellTyped "Not a close term")
+        )
+     | C.Var uri -> type_of_variable uri
+     | C.Meta (n,l) -> 
+        (* Let's visit all the subterms that will not be visited later *)
+        let _ =
+         List.iter
+          (function None -> () | Some t -> ignore (type_of_aux context t)) l
+        in
+         let (_,canonical_context,ty) =
+          List.find (function (m,_,_) -> n = m) metasenv
+         in
+          (* Checks suppressed *)
+          CicSubstitution.lift_meta l ty
+     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+     | C.Implicit -> raise (Impossible 21)
+     | C.Cast (te,ty) ->
+        (* Let's visit all the subterms that will not be visited later *)
+        let _ = type_of_aux context te in
+        let _ = type_of_aux context ty in
+         (* Checks suppressed *)
+         ty
+     | C.Prod (name,s,t) ->
+        let sort1 = type_of_aux context s
+        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
+         sort_of_prod context (name,s) (sort1,sort2)
+     | C.Lambda (n,s,t) ->
+        (* Let's visit all the subterms that will not be visited later *)
+        let _ = type_of_aux context s in
+         let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
+          (* Checks suppressed *)
+          C.Prod (n,s,type2)
+     | C.LetIn (n,s,t) ->
+        (* Let's visit all the subterms that will not be visited later *)
+        let _ = type_of_aux context s in
+         (* Checks suppressed *)
+         C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)
+     | C.Appl (he::tl) when List.length tl > 0 ->
+        let hetype = type_of_aux context he
+        and tlbody_and_type =
+         List.map (fun x -> (x, type_of_aux context x)) tl
+        in
+         eat_prods context hetype tlbody_and_type
+     | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
+     | C.Const (uri,cookingsno) ->
+        cooked_type_of_constant uri cookingsno
+     | C.Abst _ -> raise (Impossible 22)
+     | C.MutInd (uri,cookingsno,i) ->
+        cooked_type_of_mutual_inductive_defs uri cookingsno i
+     | C.MutConstruct (uri,cookingsno,i,j) ->
+        let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j in
+         cty
+     | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
+        (* Let's visit all the subterms that will not be visited later *)
+        let _ = List.map (type_of_aux context) pl in
+         let outsort = type_of_aux context outtype in
+         let (need_dummy, k) =
+          let rec guess_args context t =
+           match CicReduction.whd context t with
+              C.Sort _ -> (true, 0)
+            | C.Prod (name, s, t) ->
+               let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
+                if n = 0 then
+                 (* last prod before sort *)
+                 match CicReduction.whd context s with
+                    (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
+                    C.MutInd (uri',_,i') when U.eq uri' uri && i' = i ->
+                     (false, 1)
+                  | C.Appl ((C.MutInd (uri',_,i')) :: _)
+                     when U.eq uri' uri && i' = i -> (false, 1)
+                  | _ -> (true, 1)
+                else
+                 (b, n + 1)
+            | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
+          in
+           (*CSC whd non serve dopo type_of_aux ? *)
+           let (b, k) = guess_args context outsort in
+            if not b then (b, k - 1) else (b, k)
+         in
+         let (_, arguments) =
+           match R.whd context (type_of_aux context term) with
+              (*CSC manca il caso dei CAST *)
+              C.MutInd (uri',_,i') ->
+               (* Checks suppressed *)
+               [],[]
+            | C.Appl (C.MutInd (uri',_,i') :: tl) ->
+               split tl (List.length tl - k)
+            | _ ->
+              raise (NotWellTyped "MutCase: the term is not an inductive one")
+         in
+          (* Checks suppressed *)
+          if not need_dummy then
+           C.Appl ((outtype::arguments)@[term])
+          else if arguments = [] then
+           outtype
+          else
+           C.Appl (outtype::arguments)
+     | C.Fix (i,fl) ->
+        (* Let's visit all the subterms that will not be visited later *)
+        let context' =
+         List.rev
+          (List.map
+            (fun (n,_,ty,_) ->
+              let _ = type_of_aux context ty in
+               (Some (C.Name n,(C.Decl ty)))
+            ) fl
+          ) @
+          context
+        in
+         let _ =
+          List.iter
+           (fun (_,_,_,bo) -> ignore (type_of_aux context' bo))
+         in
+          (* Checks suppressed *)
+          let (_,_,ty,_) = List.nth fl i in
+           ty
+     | C.CoFix (i,fl) ->
+        (* Let's visit all the subterms that will not be visited later *)
+        let context' =
+         List.rev
+          (List.map
+            (fun (n,ty,_) ->
+              let _ = type_of_aux context ty in
+               (Some (C.Name n,(C.Decl ty)))
+            ) fl
+          ) @
+          context
+        in
+         let _ =
+          List.iter
+           (fun (_,_,bo) -> ignore (type_of_aux context' bo))
+         in
+          (* Checks suppressed *)
+          let (_,ty,_) = List.nth fl i in
+           ty
+   in
+    (*CSC: Is whd the right thing to do? Or should full beta *)
+    (*CSC: reduction be more appropriate?                    *)
+(*CSC: Nota: whd fa troppo (esempio: fa anche iota) e full beta sembra molto *)
+(*CSC: costosa quando fatta ogni passo. Fare solo un passo? *)
+    let synthesized' = CicReduction.whd context synthesized in
+     CicHash.add subterms_to_types t
+      {synthesized = synthesized' ; expected = Cic.Implicit} ;
+     synthesized'
+
+ and sort_of_prod context (name,s) (t1, t2) =
+  let module C = Cic in
+   let t1' = CicReduction.whd context t1 in
+   let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
+   match (t1', t2') with
+      (C.Sort s1, C.Sort s2)
+        when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+         C.Sort s2
+    | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+    | (_,_) ->
+      raise
+       (NotWellTyped
+        ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
+
+ and eat_prods context hetype =
+  (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
+  (*CSC: cucinati                                                         *)
+  function
+     [] -> hetype
+   | (hete, hety)::tl ->
+    (match (CicReduction.whd context hetype) with
+        Cic.Prod (n,s,t) ->
+         (* Checks suppressed *)
+         eat_prods context (CicSubstitution.subst hete t) tl
+      | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
+    )
+
+ in
+  type_of_aux context t
+;;
+
+let double_type_of metasenv context t =
+ let subterms_to_types = CicHash.create 503 in
+  ignore (type_of_aux' subterms_to_types metasenv context t) ;
+  subterms_to_types
+;;
diff --git a/helm/gTopLevel/doubleTypeInference.mli b/helm/gTopLevel/doubleTypeInference.mli
new file mode 100644 (file)
index 0000000..4de5bc0
--- /dev/null
@@ -0,0 +1,19 @@
+exception Impossible of int
+exception NotWellTyped of string
+exception WrongUriToConstant of string
+exception WrongUriToVariable of string
+exception WrongUriToMutualInductiveDefinitions of string
+exception ListTooShort
+exception RelToHiddenHypothesis
+
+type types = {synthesized : Cic.term ; expected : Cic.term};;
+
+module CicHash :
+  sig
+    type key = Cic.term
+    and 'a t
+    val find : 'a t -> key -> 'a
+  end
+
+val double_type_of :
+ Cic.metasenv -> Cic.context -> Cic.term -> types CicHash.t