X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2FdoubleTypeInference.ml;h=4910275ea48c291662f213bd72fdb3ddd5e462c1;hb=83a4859b0a6fec3953dae70cd6177eecd850d012;hp=fd96270467aa746901de0ff2ba7e9d175f186197;hpb=df0bf216c6bbebf452c1b107a5d995bd8dd16451;p=helm.git

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index fd9627046..4910275ea 100644
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -33,6 +33,8 @@ exception WrongUriToMutualInductiveDefinitions of string;;
 exception ListTooShort;;
 exception RelToHiddenHypothesis;;
 
+(*CSC: must alfa-conversion be considered or not? *)
+
 let xxx_type_of_aux' m c t =
  try 
    Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
@@ -49,6 +51,8 @@ let rec does_not_occur n =
   function
      C.Rel m when m = n -> false
    | C.Rel _
+(* FG/CSC: maybe we assume the meta is guarded so we do not recur on its *)
+(*         explicit subsitutions (copied from the kernel) ???            *)
    | C.Meta _
    | C.Sort _
    | C.Implicit _ -> true 
@@ -60,9 +64,10 @@ let rec does_not_occur n =
    | C.Lambda (name,so,dest) ->
       does_not_occur n so &&
        does_not_occur (n + 1) dest
-   | C.LetIn (name,so,dest) ->
+   | C.LetIn (name,so,ty,dest) ->
       does_not_occur n so &&
-       does_not_occur (n + 1) dest
+       does_not_occur n ty &&
+        does_not_occur (n + 1) dest
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur n x) l true
    | C.Var (_,exp_named_subst)
@@ -115,8 +120,8 @@ let rec beta_reduce =
        C.Prod (n, beta_reduce s, beta_reduce t)
     | C.Lambda (n,s,t) ->
        C.Lambda (n, beta_reduce s, beta_reduce t)
-    | C.LetIn (n,s,t) ->
-       C.LetIn (n, beta_reduce s, beta_reduce t)
+    | C.LetIn (n,s,ty,t) ->
+       C.LetIn (n, beta_reduce s, beta_reduce ty, beta_reduce t)
     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
        let he' = S.subst he t in
         if tl = [] then
@@ -163,75 +168,6 @@ let rec beta_reduce =
         C.CoFix (i,fl')
 ;;
 
-(* syntactic_equality up to the                 *)
-(* distinction between fake dependent products  *)
-(* and non-dependent products, alfa-conversion  *)
-(*CSC: must alfa-conversion be considered or not? *)
-let syntactic_equality t t' =
- let module C = Cic in
- let rec syntactic_equality t t' =
-  if t = t' then true
-  else
-   match t, t' with
-      C.Var (uri,exp_named_subst), C.Var (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.Cast (te,ty), C.Cast (te',ty') ->
-       syntactic_equality te te' &&
-        syntactic_equality ty ty'
-    | C.Prod (_,s,t), C.Prod (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Lambda (_,s,t), C.Lambda (_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.LetIn (_,s,t), C.LetIn(_,s',t') ->
-       syntactic_equality s s' &&
-        syntactic_equality t t'
-    | C.Appl l, C.Appl l' ->
-       List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l'
-    | C.Const (uri,exp_named_subst), C.Const (uri',exp_named_subst') ->
-       UriManager.eq uri uri' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutInd (uri,i,exp_named_subst), C.MutInd (uri',i',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutConstruct (uri,i,j,exp_named_subst),
-      C.MutConstruct (uri',i',j',exp_named_subst') ->
-       UriManager.eq uri uri' && i = i' && j = j' &&
-        syntactic_equality_exp_named_subst exp_named_subst exp_named_subst'
-    | C.MutCase (sp,i,outt,t,pl), C.MutCase (sp',i',outt',t',pl') ->
-       UriManager.eq sp sp' && i = i' &&
-        syntactic_equality outt outt' &&
-         syntactic_equality t t' &&
-          List.fold_left2
-           (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl'
-    | C.Fix (i,fl), C.Fix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,i,ty,bo) (_,i',ty',bo') ->
-           b && i = i' &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | C.CoFix (i,fl), C.CoFix (i',fl') ->
-       i = i' &&
-        List.fold_left2
-         (fun b (_,ty,bo) (_,ty',bo') ->
-           b &&
-            syntactic_equality ty ty' &&
-             syntactic_equality bo bo') true fl fl'
-    | _, _ -> false (* we already know that t != t' *)
- and syntactic_equality_exp_named_subst exp_named_subst1 exp_named_subst2 =
-  List.fold_left2
-   (fun b (_,t1) (_,t2) -> b && syntactic_equality t1 t2) true
-   exp_named_subst1 exp_named_subst2
- in
-  try
-   syntactic_equality t t'
-  with
-   _ -> false
-;;
-
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
@@ -303,6 +239,18 @@ let type_of_mutual_inductive_constr uri i j =
 
 let pack_coercion = ref (fun _ _ _ -> assert false);;
 
+let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
+
+let cic_CicHash_add a b c =  
+  profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
+;;
+
+let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
+
+let cic_CicHash_mem a b =  
+  profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
+;;
+
 (* 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 expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -324,10 +272,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
         (try
           match List.nth context (n - 1) with
              Some (_,C.Decl t) -> S.lift n t
-           | Some (_,C.Def (_,Some ty)) -> S.lift n ty
-           | Some (_,C.Def (bo,None)) ->
-              type_of_aux context (S.lift n bo) expectedty
-	         | None -> raise RelToHiddenHypothesis
+           | Some (_,C.Def (_,ty)) -> S.lift n ty
+	   | None -> raise RelToHiddenHypothesis
          with
           _ -> raise (NotWellTyped "Not a close term")
         )
@@ -343,11 +289,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
               [] -> []
             | (Some (n,C.Decl t))::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.subst_meta l (S.lift i t)),None)))::
-                (aux (i+1) tl)
+            | (Some (n,C.Def (t,ty)))::tl ->
+               (Some (n,
+                C.Def
+                 ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i t))))::
+                  (aux (i+1) tl)
             | None::tl -> None::(aux (i+1) tl)
-            | (Some (_,C.Def (_,Some _)))::_ -> assert false
           in
            aux 1 canonical_context
          in
@@ -409,21 +356,22 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           in
            (* Checks suppressed *)
            C.Prod (n,s,type2)
-     | C.LetIn (n,s,t) ->
+     | C.LetIn (n,s,ty,t) ->
 (*CSC: What are the right expected types for the source and *)
 (*CSC: target of a LetIn? None used.                        *)
         (* Let's visit all the subterms that will not be visited later *)
-        let ty = type_of_aux context s None in
+        let _ = type_of_aux context ty None in
+        let _ = type_of_aux context s (Some ty) in
          let t_typ =
           (* Checks suppressed *)
-          type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
+          type_of_aux ((Some (n,(C.Def (s,ty))))::context) t None
          in  (* CicSubstitution.subst s t_typ *)
           if does_not_occur 1 t_typ then
            (* since [Rel 1] does not occur in typ, substituting any term *)
            (* in place of [Rel 1] is equivalent to delifting once        *)
            CicSubstitution.subst (C.Implicit None) t_typ
           else
-           C.LetIn (n,s,t_typ)
+           C.LetIn (n,s,ty,t_typ)
      | C.Appl (he::tl) when List.length tl > 0 ->
         (* 
         let expected_hetype =
@@ -609,7 +557,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          None ->
           (* No expected type *)
           {synthesized = synthesized' ; expected = None}, synthesized
-       | Some ty when syntactic_equality synthesized' ty ->
+       | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
           (* The expected type is synthactically equal to *)
           (* the synthesized type. Let's forget it.       *)
           {synthesized = synthesized' ; expected = None}, synthesized
@@ -617,8 +565,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
-      assert (not (Cic.CicHash.mem subterms_to_types t));
-      Cic.CicHash.add subterms_to_types t types ;
+(*      assert (not (cic_CicHash_mem subterms_to_types t));*)
+      cic_CicHash_add subterms_to_types t types ;
       res
 
  and visit_exp_named_subst context uri exp_named_subst =
@@ -643,7 +591,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
   in
    let rec check uris_and_types subst =
     match uris_and_types,subst with
-       _,[] -> []
+       _,[] -> ()
      | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
         ignore (type_of_aux context t (Some ty)) ;
         let tytl' =