X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FdoubleTypeInference.ml;h=4afe0e47549d0e959d44442d23c98e78564b4d4e;hb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;hp=b06619c4ddf74d98929420761a7d3a61e34119c5;hpb=2dc0733271cd251aaa3edaece8a883fe691775ab;p=helm.git

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index b06619c4d..4afe0e475 100644
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -39,8 +39,12 @@ let rec head_beta_reduce =
  let module S = CicSubstitution in
  let module C = Cic in
   function
-      C.Rel _
-    | C.Var _ as t -> t
+      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
+       in
+        C.Var (uri,exp_named_subst)
     | C.Meta (n,l) ->
        C.Meta (n,
         List.map
@@ -64,11 +68,23 @@ let rec head_beta_reduce =
          head_beta_reduce (C.Appl (he'::tl))
     | C.Appl l ->
        C.Appl (List.map head_beta_reduce l)
-    | C.Const _ as t -> t
-    | C.MutInd _
-    | C.MutConstruct _ as t -> t
-    | C.MutCase (sp,cno,i,outt,t,pl) ->
-       C.MutCase (sp,cno,i,head_beta_reduce outt,head_beta_reduce t,
+    | C.Const (uri,exp_named_subst) ->
+       let exp_named_subst' =
+        List.map (function (i,t) -> i, head_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
+       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
+       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.Fix (i,fl) ->
        let fl' =
@@ -99,11 +115,9 @@ let syntactic_equality t t' =
   if t = t' then true
   else
    match t, t' with
-      C.Rel _, C.Rel _
-    | C.Var _, C.Var _
-    | C.Meta _, C.Meta _
-    | C.Sort _, C.Sort _
-    | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+      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'
@@ -118,12 +132,17 @@ let syntactic_equality t t' =
         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,_), C.Const (uri',_) -> UriManager.eq uri uri'
-    | C.MutInd (uri,_,i), C.MutInd (uri',_,i') ->
-       UriManager.eq uri uri' && i = i'
-    | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
-       UriManager.eq uri uri' && i = i' && j = j'
-    | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+    | 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' &&
@@ -143,7 +162,11 @@ let syntactic_equality t t' =
            b &&
             syntactic_equality ty ty' &&
              syntactic_equality bo bo') true fl fl'
-    | _,_ -> false
+    | _, _ -> 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'
@@ -158,20 +181,19 @@ let rec split l n =
   | (_,_) -> raise ListTooShort
 ;;
 
-let cooked_type_of_constant uri cookingsno =
+let type_of_constant uri =
  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
+   match CicEnvironment.is_type_checked uri 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
+      C.Constant (_,_,ty,_) -> ty
+    | C.CurrentProof (_,_,_,ty,_) -> ty
     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 ;;
 
@@ -179,20 +201,19 @@ 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
+  match CicEnvironment.is_type_checked 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))
 ;;
 
-let cooked_type_of_mutual_inductive_defs uri cookingsno i =
+let type_of_mutual_inductive_defs uri 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
+   match CicEnvironment.is_type_checked uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked inductive type")
@@ -204,12 +225,12 @@ let cooked_type_of_mutual_inductive_defs uri cookingsno i =
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
 
-let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
+let type_of_mutual_inductive_constr uri 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
+   match CicEnvironment.is_type_checked uri with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
        raise (NotWellTyped "Reference to an unchecked constructor")
@@ -217,7 +238,7 @@ let cooked_type_of_mutual_inductive_constr uri cookingsno i j =
    match cobj with
       C.InductiveDefinition (dl,_,_) ->
        let (_,_,_,cl) = List.nth dl i in
-        let (_,ty,_) = List.nth cl (j-1) in
+        let (_,ty) = List.nth cl (j-1) in
          ty
     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 ;;
@@ -253,7 +274,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          with
           _ -> raise (NotWellTyped "Not a close term")
         )
-     | C.Var uri -> type_of_variable uri
+     | C.Var (uri,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        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,_) =
@@ -355,14 +378,18 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          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.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) ->
+     | C.Const (uri,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+     | C.MutInd (uri,i,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst
+         (type_of_mutual_inductive_defs uri i)
+     | C.MutConstruct (uri,i,j,exp_named_subst) ->
+        visit_exp_named_subst context uri exp_named_subst ;
+        CicSubstitution.subst_vars exp_named_subst
+         (type_of_mutual_inductive_constr uri i j)
+     | C.MutCase (uri,i,outtype,term,pl) ->
         let outsort = type_of_aux context outtype None in
         let (need_dummy, k) =
          let rec guess_args context t =
@@ -373,10 +400,9 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
                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 ->
+                   C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
                     (false, 1)
-                 | C.Appl ((C.MutInd (uri',_,i')) :: _)
+                 | C.Appl ((C.MutInd (uri',i',_)) :: _)
                     when U.eq uri' uri && i' = i -> (false, 1)
                  | _ -> (true, 1)
                else
@@ -386,7 +412,7 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           let (b, k) = guess_args context outsort in
            if not b then (b, k - 1) else (b, k)
         in
-        let (parameters, arguments) =
+        let (parameters, arguments,exp_named_subst) =
          let type_of_term =
           CicTypeChecker.type_of_aux' metasenv context term
          in
@@ -395,18 +421,20 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
             (Some (head_beta_reduce type_of_term)))
           with
              (*CSC manca il caso dei CAST *)
-             C.MutInd (uri',_,i') ->
+             C.MutInd (uri',i',exp_named_subst) ->
               (* Checks suppressed *)
-              [],[]
-           | C.Appl (C.MutInd (uri',_,i') :: tl) ->
+              [],[],exp_named_subst
+           | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
+             let params,args =
               split tl (List.length tl - k)
+             in params,args,exp_named_subst
            | _ ->
              raise (NotWellTyped "MutCase: the term is not an inductive one")
         in
          (* Checks suppressed *)
          (* Let's visit all the subterms that will not be visited later *)
          let (cl,parsno) =
-          match CicEnvironment.get_cooked_obj uri cookingsno with
+          match CicEnvironment.get_cooked_obj uri with
              C.InductiveDefinition (tl,_,parsno) ->
               let (_,_,_,cl) = List.nth tl i in (cl,parsno)
            | _ ->
@@ -414,12 +442,12 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          in
           let _ =
            List.fold_left
-            (fun j (p,(_,c,_)) ->
+            (fun j (p,(_,c)) ->
               let cons =
                if parameters = [] then
-                (C.MutConstruct (uri,cookingsno,i,j))
+                (C.MutConstruct (uri,i,j,exp_named_subst))
                else
-                (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
+                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
               in
                let expectedtype =
                 type_of_branch context parsno need_dummy outtype cons
@@ -502,6 +530,34 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
       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
+  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' =
+         List.map
+          (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
+        in
+         check tytl' substtl
+     | _,_ -> assert false (* the theorem is well-typed *)
+   in
+    check uris_and_types exp_named_subst
+
  and sort_of_prod context (name,s) (t1, t2) =
   let module C = Cic in
    let t1' = CicReduction.whd context t1 in
@@ -551,7 +607,7 @@ and type_of_branch context argsno need_dummy outtype term constype =
           C.Appl l -> C.Appl (l@[C.Rel 1])
         | t -> C.Appl [t ; C.Rel 1]
       in
-       C.Prod (C.Anonimous,so,type_of_branch
+       C.Prod (C.Anonymous,so,type_of_branch
         ((Some (name,(C.Decl so)))::context) argsno need_dummy
         (CicSubstitution.lift 1 outtype) term' de)
   | _ -> raise (Impossible 20)