X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=a77b293c1ae42d67ef8bdc0bdf09471441d431ef;hb=18d8d7128c16b5d4dd589d75a2e7c026ac7d405d;hp=f1a99408ab80764685a0486deb696eb070f98ec9;hpb=90a9ceff7dc614e7be0b600fc6c820abd980595a;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f1a99408a..a77b293c1 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -28,217 +28,9 @@ let shift_k e (c,rf,x,safes) =
 
 (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *)
 
-(*
-exception CicEnvironmentError;;
 
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
-(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
-(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
-(*CSC strictly_positive                                                  *)
-(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
-and weakly_positive context n nn uri te =
- let module C = Cic in
-(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
-  let dummy_mutind =
-   C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
-  in
-  (*CSC: mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_mutind =
-   function
-      C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
-       dummy_mutind
-    | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
-    | C.Prod (name,so,ta) ->
-       C.Prod (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
-    | C.Lambda (name,so,ta) ->
-       C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
-        subst_inductive_type_with_dummy_mutind ta)
-    | C.Appl tl ->
-       C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
-    | C.MutCase (uri,i,outtype,term,pl) ->
-       C.MutCase (uri,i,
-        subst_inductive_type_with_dummy_mutind outtype,
-        subst_inductive_type_with_dummy_mutind term,
-        List.map subst_inductive_type_with_dummy_mutind pl)
-    | C.Fix (i,fl) ->
-       C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
-    | C.CoFix (i,fl) ->
-       C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
-        subst_inductive_type_with_dummy_mutind ty,
-        subst_inductive_type_with_dummy_mutind bo)) fl)
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.Const (uri,exp_named_subst')
-    | C.MutInd (uri,typeno,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.MutInd (uri,typeno,exp_named_subst')
-    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-        List.map
-         (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
-         exp_named_subst
-       in
-        C.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | t -> t
-  in
-  match CicReduction.whd context te with
-(*
-     C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
-*)
-     C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
-   | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
-   | C.Prod (C.Anonymous,source,dest) ->
-      strictly_positive context n nn
-       (subst_inductive_type_with_dummy_mutind source) &&
-       weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
-        (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
-       (* dummy abstraction, so we behave as in the anonimous case *)
-       strictly_positive context n nn
-        (subst_inductive_type_with_dummy_mutind source) &&
-         weakly_positive ((Some (name,(C.Decl source)))::context)
-         (n + 1) (nn + 1) uri dest
-   | C.Prod (name,source,dest) ->
-       does_not_occur context n nn
-         (subst_inductive_type_with_dummy_mutind source)&&
-         weakly_positive ((Some (name,(C.Decl source)))::context)
-         (n + 1) (nn + 1) uri dest
-   | _ ->
-     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
-
-(* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
-(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
-and instantiate_parameters params c =
- let module C = Cic in
-  match (c,params) with
-     (c,[]) -> c
-   | (C.Prod (_,_,ta), he::tl) ->
-       instantiate_parameters tl
-        (CicSubstitution.subst he ta)
-   | (C.Cast (te,_), _) -> instantiate_parameters params te
-   | (t,l) -> raise (AssertFailure (lazy "1"))
-
-and strictly_positive context n nn te =
- let module C = Cic in
- let module U = UriManager in
-  match CicReduction.whd context te with
-   | t when does_not_occur context n nn t -> true
-   | C.Rel _ -> true
-   | C.Cast (te,ty) ->
-      (*CSC: bisogna controllare ty????*)
-      strictly_positive context n nn te
-   | C.Prod (name,so,ta) ->
-      does_not_occur context n nn so &&
-       strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
-   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-   | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> 
-      let (ok,paramsno,ity,cl,name) =
-        let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-          match o with
-              C.InductiveDefinition (tl,_,paramsno,_) ->
-                let (name,_,ity,cl) = List.nth tl i in
-                (List.length tl = 1, paramsno, ity, cl, name) 
-                (* (true, paramsno, ity, cl, name) *)
-            | _ ->
-                raise 
-                  (TypeCheckerFailure
-                     (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
-      in 
-      let (params,arguments) = split tl paramsno in
-      let lifted_params = List.map (CicSubstitution.lift 1) params in
-      let cl' =
-        List.map
-          (fun (_,te) ->
-             instantiate_parameters lifted_params
-               (CicSubstitution.subst_vars exp_named_subst te)
-          ) cl
-      in
-        ok &&
-          List.fold_right
-          (fun x i -> i && does_not_occur context n nn x)
-          arguments true &&
-         (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
-          List.fold_right
-          (fun x i ->
-             i &&
-               weakly_positive
-               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
-               x
-          ) cl' true
-   | t -> false
-       
-(* the inductive type indexes are s.t. n < x <= nn *)
-and are_all_occurrences_positive context uri indparamsno i n nn te =
- let module C = Cic in
-  match CicReduction.whd context te with
-     C.Appl ((C.Rel m)::tl) when m = i ->
-      (*CSC: riscrivere fermandosi a 0 *)
-      (* let's check if the inductive type is applied at least to *)
-      (* indparamsno parameters                                   *)
-      let last =
-       List.fold_left
-        (fun k x ->
-          if k = 0 then 0
-          else
-           match CicReduction.whd context x with
-              C.Rel m when m = n - (indparamsno - k) -> k - 1
-            | _ ->
-              raise (TypeCheckerFailure
-               (lazy 
-               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
-                UriManager.string_of_uri uri)))
-        ) indparamsno tl
-      in
-       if last = 0 then
-        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
-       else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
-          UriManager.string_of_uri uri)))
-   | C.Rel m when m = i ->
-      if indparamsno = 0 then
-       true
-      else
-        raise (TypeCheckerFailure
-         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
-          UriManager.string_of_uri uri)))
-   | C.Prod (C.Anonymous,source,dest) ->
-       let b = strictly_positive context n nn source in
-       b &&
-       are_all_occurrences_positive
-        ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
-   | C.Prod (name,source,dest) when
-      does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
-      (* dummy abstraction, so we behave as in the anonimous case *)
-      strictly_positive context n nn source &&
-       are_all_occurrences_positive
-        ((Some (name,(C.Decl source)))::context) uri indparamsno
-        (i+1) (n + 1) (nn + 1) dest
-   | C.Prod (name,source,dest) ->
-      does_not_occur context n nn source &&
-       are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
-        uri indparamsno (i+1) (n + 1) (nn + 1) dest
-   | _ ->
-     raise
-      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
-        (UriManager.string_of_uri uri))))
 
+(*
 (* the boolean h means already protected *)
 (* args is the list of arguments the type of the constructor that may be *)
 (* found in head position must be applied to.                            *)
@@ -557,9 +349,12 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected\n%s\nfound\n%s")
-                  (NCicPp.ppterm ~subst ~metasenv ~context s)
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut it should have type \n%s\n")
+                  (NCicPp.ppterm ~subst ~metasenv ~context he)
+                  (NCicPp.ppterm ~subst ~metasenv ~context arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
        | _ ->
           raise 
             (TypeCheckerFailure
@@ -615,6 +410,116 @@ let does_not_occur ~subst context n nn t =
    with DoesOccur -> false
 ;;
 
+(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
+(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
+(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
+(*CSC strictly_positive                                                  *)
+(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
+let rec weakly_positive ~subst context n nn uri te =
+(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
+  let dummy_mutind = C.Implicit `Hole in
+  (*CSC: mettere in cicSubstitution *)
+  let rec subst_inductive_type_with_dummy_mutind _ = function
+    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri ->
+       dummy_mutind
+    | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind t
+  in
+  match R.whd context te with
+   | C.Const (Ref.Ref (_,uri',Ref.Ind _))
+   | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true
+   | C.Prod (name,source,dest) when
+      does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest ->
+       (* dummy abstraction, so we behave as in the anonimous case *)
+       strictly_positive ~subst context n nn
+        (subst_inductive_type_with_dummy_mutind () source) &&
+         weakly_positive ~subst ((name,C.Decl source)::context)
+         (n + 1) (nn + 1) uri dest
+   | C.Prod (name,source,dest) ->
+       does_not_occur ~subst context n nn
+         (subst_inductive_type_with_dummy_mutind () source)&&
+         weakly_positive ~subst ((name,C.Decl source)::context)
+         (n + 1) (nn + 1) uri dest
+   | _ ->
+     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
+
+(* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
+(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
+and instantiate_parameters params c =
+  match c, params with
+  | c,[] -> c
+  | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta)
+  | t,l -> raise (AssertFailure (lazy "1"))
+
+and strictly_positive ~subst context n nn te =
+  match R.whd context te with
+   | t when does_not_occur ~subst context n nn t -> true
+   | C.Rel _ -> true
+   | C.Prod (name,so,ta) ->
+      does_not_occur ~subst context n nn so &&
+       strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
+   | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
+      List.for_all (does_not_occur ~subst context n nn) tl
+   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> 
+      let _,paramsno,tyl,_,i = E.get_checked_indtys r in
+      let _,name,ity,cl = List.nth tyl i in
+      let ok = List.length tyl = 1 in
+      let params, arguments = HExtlib.split_nth paramsno tl in
+      let lifted_params = List.map (S.lift 1) params in
+      let cl =
+        List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl 
+      in
+      ok &&
+      List.for_all (does_not_occur ~subst context n nn) arguments &&
+      List.for_all 
+        (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl
+   | _ -> false
+       
+(* the inductive type indexes are s.t. n < x <= nn *)
+and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
+  match R.whd context te with
+  |  C.Appl ((C.Rel m)::tl) when m = i ->
+      let last =
+       List.fold_left
+        (fun k x ->
+          if k = 0 then 0
+          else
+           match R.whd context x with
+           |  C.Rel m when m = n - (indparamsno - k) -> k - 1
+           | _ -> raise (TypeCheckerFailure (lazy 
+              ("Non-positive occurence in mutual inductive definition(s) [1]" ^
+              NUri.string_of_uri uri))))
+        indparamsno tl
+      in
+       if last = 0 then
+        List.for_all (does_not_occur ~subst context n nn) tl
+       else
+        raise (TypeCheckerFailure
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+          NUri.string_of_uri uri)))
+  | C.Rel m when m = i ->
+      if indparamsno = 0 then
+       true
+      else
+        raise (TypeCheckerFailure
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
+          NUri.string_of_uri uri)))
+  | C.Prod (name,source,dest) when
+      does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest ->
+      strictly_positive ~subst context n nn source &&
+       are_all_occurrences_positive ~subst 
+        ((name,C.Decl source)::context) uri indparamsno
+        (i+1) (n + 1) (nn + 1) dest
+   | C.Prod (name,source,dest) ->
+      does_not_occur ~subst context n nn source &&
+       are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
+        uri indparamsno (i+1) (n + 1) (nn + 1) dest
+   | _ ->
+     raise
+      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
+        (NUri.string_of_uri uri))))
+;;
+
 exception NotGuarded of string Lazy.t;;
 
 let rec typeof ~subst ~metasenv context term =
@@ -678,17 +583,20 @@ let rec typeof ~subst ~metasenv context term =
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
 (*
-       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map snd args_with_ty)));
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map fst args_with_ty)));
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
-      let leftno = E.get_indty_leftno r in
+      let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
+      let constructorsno =
+        let _,_,_,cl = List.nth itl tyno in List.length cl
+      in
       let parameters, arguments =
         let ty = R.whd ~subst context (typeof_aux context term) in
         let r',tl =
@@ -722,12 +630,6 @@ let rec typeof ~subst ~metasenv context term =
       check_allowed_sort_elimination ~subst ~metasenv r context
        sort_of_ind_type type_of_sort_of_ind_ty outsort;
       (* let's check if the type of branches are right *)
-      let leftno,constructorsno =
-        let inductive,leftno,itl,_,i = E.get_checked_indtys r in
-        let _,name,ty,cl = List.nth itl i in
-        let cl_len = List.length cl in
-        leftno, cl_len
-      in
       if List.length pl <> constructorsno then
        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
       let j,branches_ok,p_ty, exp_p_ty =
@@ -922,6 +824,8 @@ let rec typeof ~subst ~metasenv context term =
             | (C.Sort (C.CProp | C.Type _), C.Sort _)
             | (C.Sort C.Prop, C.Sort C.Prop) -> ()
             | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
+        (* TODO: we should pass all these parameters since we
+         * have them already *)
                 let inductive,leftno,itl,_,i = E.get_checked_indtys r in
                 let itl_len = List.length itl in
                 let _,name,ty,cl = List.nth itl i in
@@ -949,7 +853,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
   (* let's check if the types of the inductive constructors are well formed. *)
   let len = List.length tyl in
-  let tys = List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
+  let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
   ignore
    (List.fold_right
     (fun (_,_,_,cl) i ->
@@ -958,10 +862,10 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
            let debruijnedte = debruijn uri len te in
            ignore (typeof ~subst ~metasenv tys debruijnedte);
            (* let's check also the positivity conditions *)
-           if false (*
+           if 
              not
-               (are_all_occurrences_positive tys uri indparamsno i 0 len
-                  debruijnedte) *)
+               (are_all_occurrences_positive ~subst tys uri leftno i 0 len
+                  debruijnedte) 
            then
              raise
                (TypeCheckerFailure
@@ -1064,7 +968,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with
@@ -1165,8 +1069,6 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
        check_obj_well_typed uobj;
        E.add_obj uobj;
        !logger (`Type_checking_completed uri);
-       if not (fst (E.get_obj uri)) then
-         raise (AssertFailure (lazy "environment error"));
        uobj
   in
   match cobj, ref with