X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2FdoubleTypeInference.ml;h=69287243918419218848f810371f5c0c1843fa83;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=3163dfe09bf21804932f3a4cabefad32745e1752;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index 3163dfe09..692872439 100644
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -41,7 +41,7 @@ let double_work = ref 0;;
 
 let xxx_type_of_aux' m c t =
  let t1 = Sys.time () in
- let res = CicTypeChecker.type_of_aux' m c t in
+ let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
  let t2 = Sys.time () in
  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
  res
@@ -105,64 +105,64 @@ let rec does_not_occur n =
          ) fl true
 ;;
 
-(*CSC: potrebbe creare applicazioni di applicazioni *)
-(*CSC: ora non e' piu' head, ma completa!!! *)
-let rec head_beta_reduce =
+let rec beta_reduce =
  let module S = CicSubstitution in
  let module C = Cic in
   function
       C.Rel _ as t -> t
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.Var (uri,exp_named_subst)
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
-         (function None -> None | Some t -> Some (head_beta_reduce t)) l
+         (function None -> None | Some t -> Some (beta_reduce t)) l
        )
     | C.Sort _ as t -> t
     | C.Implicit _ -> assert false
     | C.Cast (te,ty) ->
-       C.Cast (head_beta_reduce te, head_beta_reduce ty)
+       C.Cast (beta_reduce te, beta_reduce ty)
     | C.Prod (n,s,t) ->
-       C.Prod (n, head_beta_reduce s, head_beta_reduce t)
+       C.Prod (n, beta_reduce s, beta_reduce t)
     | C.Lambda (n,s,t) ->
-       C.Lambda (n, head_beta_reduce s, head_beta_reduce t)
+       C.Lambda (n, beta_reduce s, beta_reduce t)
     | C.LetIn (n,s,t) ->
-       C.LetIn (n, head_beta_reduce s, head_beta_reduce t)
+       C.LetIn (n, beta_reduce s, beta_reduce t)
     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
        let he' = S.subst he t in
         if tl = [] then
-         head_beta_reduce he'
+         beta_reduce he'
         else
-         head_beta_reduce (C.Appl (he'::tl))
+         (match he' with
+             C.Appl l -> beta_reduce (C.Appl (l@tl))
+           | _ -> beta_reduce (C.Appl (he'::tl)))
     | C.Appl l ->
-       C.Appl (List.map head_beta_reduce l)
+       C.Appl (List.map beta_reduce l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri,i,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.MutInd (uri,i,exp_named_subst')
     | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
-        List.map (function (i,t) -> i, head_beta_reduce t) exp_named_subst
+        List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
        in
         C.MutConstruct (uri,i,j,exp_named_subst')
     | C.MutCase (sp,i,outt,t,pl) ->
-       C.MutCase (sp,i,head_beta_reduce outt,head_beta_reduce t,
-        List.map head_beta_reduce pl)
+       C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
+        List.map beta_reduce pl)
     | C.Fix (i,fl) ->
        let fl' =
         List.map
          (function (name,i,ty,bo) ->
-           name,i,head_beta_reduce ty,head_beta_reduce bo
+           name,i,beta_reduce ty,beta_reduce bo
          ) fl
        in
         C.Fix (i,fl')
@@ -170,7 +170,7 @@ let rec head_beta_reduce =
        let fl' =
         List.map
          (function (name,ty,bo) ->
-           name,head_beta_reduce ty,head_beta_reduce bo
+           name,beta_reduce ty,beta_reduce bo
          ) fl
        in
         C.CoFix (i,fl')
@@ -266,14 +266,14 @@ let type_of_constant uri =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constant")
   in
    match cobj with
-      C.Constant (_,_,ty,_) -> ty
-    | C.CurrentProof (_,_,_,ty,_) -> ty
+      C.Constant (_,_,ty,_,_) -> ty
+    | C.CurrentProof (_,_,_,ty,_,_) -> ty
     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 ;;
 
@@ -281,8 +281,8 @@ let type_of_variable uri =
  let module C = Cic in
  let module R = CicReduction in
  let module U = UriManager in
-  match CicEnvironment.is_type_checked uri with
-     CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
+  match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri 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))
@@ -293,13 +293,13 @@ let type_of_mutual_inductive_defs uri i =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
   in
    match cobj with
-      C.InductiveDefinition (dl,_,_) ->
+      C.InductiveDefinition (dl,_,_,_) ->
        let (_,_,arity,_) = List.nth dl i in
         arity
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -310,13 +310,13 @@ let type_of_mutual_inductive_constr uri i j =
  let module R = CicReduction in
  let module U = UriManager in
   let cobj =
-   match CicEnvironment.is_type_checked uri with
-      CicEnvironment.CheckedObj cobj -> cobj
+   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+      CicEnvironment.CheckedObj (cobj,_) -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constructor")
   in
    match cobj with
-      C.InductiveDefinition (dl,_,_) ->
+      C.InductiveDefinition (dl,_,_,_) ->
        let (_,_,_,cl) = List.nth dl i in
         let (_,ty) = List.nth cl (j-1) in
          ty
@@ -324,12 +324,17 @@ let type_of_mutual_inductive_constr uri i j =
 ;;
 
 module CicHash =
- Hashtbl.Make
-  (struct
-    type t = Cic.term
-    let equal = (==)
-    let hash = Hashtbl.hash
-   end)
+  struct
+    module Tmp = 
+     Hashtbl.Make
+      (struct
+        type t = Cic.term
+        let equal = (==)
+        let hash = Hashtbl.hash
+       end)
+    include Tmp
+    let empty () = Tmp.create 1
+  end
 ;;
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
@@ -361,17 +366,15 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
      | C.Meta (n,l) -> 
         (* Let's visit all the subterms that will not be visited later *)
-        let (_,canonical_context,_) =
-         List.find (function (m,_,_) -> n = m) metasenv
-        in
+        let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
          let lifted_canonical_context =
           let rec aux i =
            function
               [] -> []
             | (Some (n,C.Decl t))::tl ->
-               (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+               (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
             | (Some (n,C.Def (t,None)))::tl ->
-               (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::
+               (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
                 (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
             | (Some (_,C.Def (_,Some _)))::_ -> assert false
@@ -398,16 +401,16 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                | _,_ -> assert false (* the term is not well typed!!! *)
             ) l lifted_canonical_context
           in
-           let (_,canonical_context,ty) =
-            List.find (function (m,_,_) -> n = m) metasenv
-           in
+           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
             (* Checks suppressed *)
-            CicSubstitution.lift_meta l ty
-     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+            CicSubstitution.subst_meta l ty
+     | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
+         C.Sort (C.Type (CicUniv.fresh()))
+     | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
      | 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 (Some (head_beta_reduce ty)) in
+        let _ = type_of_aux context te (Some (beta_reduce ty)) in
         let _ = type_of_aux context ty None in
          (* Checks suppressed *)
          ty
@@ -425,7 +428,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               let ty =
                match R.whd context expectedty' with
                   C.Prod (_,_,expected_target_type) ->
-                   head_beta_reduce expected_target_type
+                   beta_reduce expected_target_type
                 | _ -> assert false
               in
                Some ty
@@ -455,7 +458,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         let expected_hetype =
          (* Inefficient, the head is computed twice. But I know *)
          (* of no other solution. *)                               
-         (head_beta_reduce
+         (beta_reduce
           (R.whd context (xxx_type_of_aux' metasenv context he)))
         in 
          let hetype = type_of_aux context he (Some expected_hetype) in 
@@ -464,7 +467,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            function
               _,[] -> []
             | C.Prod (n,s,t),he::tl ->
-               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+               (he, type_of_aux context he (Some (beta_reduce s)))::
                 (aux (R.whd context (S.subst he t), tl))
             | _ -> assert false
           in
@@ -475,7 +478,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
            function
               _,[] -> []
             | C.Prod (n,s,t),he::tl ->
-               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+               (he, type_of_aux context he (Some (beta_reduce s)))::
                 (aux (R.whd context (S.subst he t), tl))
             | _ -> assert false
           in
@@ -523,7 +526,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          in
           match
            R.whd context (type_of_aux context term
-            (Some (head_beta_reduce type_of_term)))
+            (Some (beta_reduce type_of_term)))
           with
              (*CSC manca il caso dei CAST *)
              C.MutInd (uri',i',exp_named_subst) ->
@@ -539,8 +542,13 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Checks suppressed *)
          (* Let's visit all the subterms that will not be visited later *)
          let (cl,parsno) =
-          match CicEnvironment.get_cooked_obj uri with
-             C.InductiveDefinition (tl,_,parsno) ->
+           let obj,_ =
+             try
+               CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+             with Not_found -> assert false
+           in
+          match obj with
+             C.InductiveDefinition (tl,_,parsno,_) ->
               let (_,_,_,cl) = List.nth tl i in (cl,parsno)
            | _ ->
              raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
@@ -559,7 +567,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                   (xxx_type_of_aux' metasenv context cons)
                in
                 ignore (type_of_aux context p
-                 (Some (head_beta_reduce expectedtype))) ;
+                 (Some (beta_reduce expectedtype))) ;
                 j+1
             ) 1 (List.combine pl cl)
           in
@@ -585,7 +593,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           List.iter
            (fun (_,_,ty,bo) ->
              let expectedty =
-              head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+              beta_reduce (CicSubstitution.lift (List.length fl) ty)
              in
               ignore (type_of_aux context' bo (Some expectedty))
            ) fl
@@ -609,7 +617,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           List.iter
            (fun (_,ty,bo) ->
              let expectedty =
-              head_beta_reduce (CicSubstitution.lift (List.length fl) ty)
+              beta_reduce (CicSubstitution.lift (List.length fl) ty)
              in
               ignore (type_of_aux context' bo (Some expectedty))
            ) fl
@@ -618,7 +626,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           let (_,ty,_) = List.nth fl i in
            ty
    in
-    let synthesized' = head_beta_reduce synthesized in
+    let synthesized' = beta_reduce synthesized in
      let types,res =
       match expectedty with
          None ->
@@ -632,22 +640,29 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
+      assert (not (CicHash.mem subterms_to_types t));
       CicHash.add subterms_to_types t types ;
       res
 
  and visit_exp_named_subst context uri exp_named_subst =
   let uris_and_types =
-   match CicEnvironment.get_cooked_obj uri with
-      Cic.Constant (_,_,_,params)
-    | Cic.CurrentProof (_,_,_,_,params)
-    | Cic.Variable (_,_,_,params)
-    | Cic.InductiveDefinition (_,params,_) ->
-       List.map
-        (function uri ->
-          match CicEnvironment.get_cooked_obj uri with
-             Cic.Variable (_,None,ty,_) -> uri,ty
-           | _ -> assert false (* the theorem is well-typed *)
-        ) params
+     let obj,_ =
+       try
+         CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+       with Not_found -> assert false
+     in
+    let params = CicUtil.params_of_obj obj in
+     List.map
+      (function uri ->
+         let obj,_ =
+           try
+             CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+           with Not_found -> assert false
+         in
+         match obj with
+           Cic.Variable (_,None,ty,_,_) -> uri,ty
+         | _ -> assert false (* the theorem is well-typed *)
+      ) params
   in
    let rec check uris_and_types subst =
     match uris_and_types,subst with
@@ -668,10 +683,19 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
    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 or s2 = C.CProp) -> (* different from Coq manual!!! *)
+      (C.Sort _, C.Sort s2)
+        when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
+	 (* different from Coq manual!!! *)
          C.Sort s2
-    | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+    | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
+	C.Sort (C.Type (CicUniv.fresh()))
+    | (C.Sort _,C.Sort (C.Type t1)) -> 
+        (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
+	C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+    | (C.Meta _, C.Sort _) -> t2'
+    | (C.Meta _, (C.Meta (_,_) as t))
+    | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
+        t2'
     | (_,_) ->
       raise
        (NotWellTyped