From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 May 2008 16:06:45 +0000 (+0000)
Subject: New checks for well-formedness of metasenvs and substs.
X-Git-Tag: make_still_working~5211
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f93b83e4e8af580bc627ea0e8e601f0333c63df2;p=helm.git

New checks for well-formedness of metasenvs and substs.
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index a62238cfb..598512373 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -975,9 +975,62 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
 ;;
 
+let typecheck_context ~metasenv ~subst context =
+ ignore
+  (List.fold_right
+   (fun d context  ->
+     begin
+      match snd d with
+         C.Decl t -> ignore (typeof ~metasenv ~subst:[] context t)
+       | C.Def (te,ty) ->
+          ignore (typeof ~metasenv ~subst:[] context te);
+         ignore (typeof ~metasenv ~subst:[] context ty);
+     end;
+     d::context
+   ) context [])
+;;
+
+let typecheck_metasenv metasenv =
+ ignore
+  (List.fold_left
+    (fun metasenv (i,(_,context,ty) as conj) ->
+      if List.mem_assoc i metasenv then
+       raise (TypeCheckerFailure (lazy ("duplicate meta " ^ string_of_int i ^
+        " in metasenv")));
+      typecheck_context ~metasenv ~subst:[] context;
+      ignore (typeof ~metasenv ~subst:[] context ty);
+      metasenv @ [conj]
+    ) [] metasenv)
+;;
+
+let typecheck_subst ~metasenv subst =
+ ignore
+  (List.fold_left
+    (fun subst (i,(_,context,ty,bo) as conj) ->
+      if List.mem_assoc i subst then
+       raise (AssertFailure (lazy ("duplicate meta " ^ string_of_int i ^
+        " in substitution")));
+      if List.mem_assoc i metasenv then
+       raise (AssertFailure (lazy ("meta " ^ string_of_int i ^
+        " is both in the metasenv and in the substitution")));
+      typecheck_context ~metasenv ~subst context;
+      ignore (typeof ~metasenv ~subst context ty);
+      let ty' = typeof ~metasenv ~subst context bo in
+       if not (R.are_convertible ~subst [] ty' ty) then
+        raise (AssertFailure (lazy (Printf.sprintf (
+         "the type of the definiens for %d in the substitution is not "^^
+         "convertible with the declared one.\n"^^
+         "inferred type:\n%s\nexpected type:\n%s")
+         i
+         (PP.ppterm ~subst ~metasenv ~context:[] ty') 
+         (PP.ppterm ~subst ~metasenv ~context:[] ty))));
+      subst @ [conj]
+    ) [] subst)
+;;
+
 let typecheck_obj (uri,height,metasenv,subst,kind) =
- (* CSC: here we should typecheck the metasenv and the subst *)
- assert (metasenv = [] && subst = []);
+ typecheck_metasenv metasenv;
+ typecheck_subst ~metasenv subst;
  match kind with
    | C.Constant (_,_,Some te,ty,_) ->
       let _ = typeof ~subst ~metasenv [] ty in