metasenv passed to get_relevance, Metas that stand for sorts have shift 0 and len 0

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index d37fdd441d3c689772e28fd9dd7e20712b6ac2d1..a7dfc50fad582819e0a62a2d97c076e8b51d9db9 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -180,12 +180,12 @@ let whd = R.whd
 
 let (===) x y = Pervasives.compare x y = 0 ;;
 
-let get_relevance = ref (fun ~subst:_ _ _ -> assert false);;
+let get_relevance = ref (fun ~metasenv:_ ~subst:_ _ _ -> assert false);;
 
 let set_get_relevance f = get_relevance := f;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible ?(subst=[]) =
+let are_convertible ~metasenv ~subst =
  let rec aux test_eq_only context t1 t2 =
    let alpha_eq test_eq_only t1 t2 =
      if t1 === t2 then
@@ -224,8 +224,8 @@ let are_convertible ?(subst=[]) =
           with Invalid_argument "List.for_all2" -> 
             prerr_endline ("Meta " ^ string_of_int n1 ^ 
               " occurrs with local contexts of different lenght\n"^
-              NCicPp.ppterm ~metasenv:[] ~subst ~context t1 ^ " === " ^
-              NCicPp.ppterm ~metasenv:[] ~subst ~context t2);
+              NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
+              NCicPp.ppterm ~metasenv ~subst ~context t2);
             assert false) -> true
 
        | C.Meta (n1,l1), _ ->
@@ -257,7 +257,8 @@ let are_convertible ?(subst=[]) =
               tl1 tl2 true relevance
             with Invalid_argument _ -> false
               | HExtlib.FailureAt fail ->
-                let relevance = !get_relevance ~subst context hd1 tl1 in
+                let relevance = 
+                   !get_relevance ~metasenv ~subst context hd1 tl1 in
                 let _,relevance = HExtlib.split_nth fail relevance in
                 let b,relevance = (match relevance with
                   | [] -> assert false
@@ -274,7 +275,7 @@ let are_convertible ?(subst=[]) =
 
        | (C.Appl (hd1::tl1),  C.Appl (hd2::tl2)) ->
            aux test_eq_only context hd1 hd2 &&
-          let relevance = !get_relevance ~subst context hd1 tl1 in
+          let relevance = !get_relevance ~metasenv ~subst context hd1 tl1 in
             (try
              HExtlib.list_forall_default3
               (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index c80da989d73c3bc53e29477de4df5e9b48e2e66d..696723bf6ad158b4bab916b2c5c9c72a4e7505c5 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -17,11 +17,11 @@ val whd :
     NCic.term
 
 val set_get_relevance : 
-  (subst:NCic.substitution ->
+  (metasenv:NCic.metasenv -> subst:NCic.substitution ->
    NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit
 
 val are_convertible :
-  ?subst:NCic.substitution ->
+  metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term -> bool
 
 

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index d9e6120d94d7cda03d172600d5699cc801cccbd1..da130c55574c07a501db14f6cd73ef0d676f0588 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -128,9 +128,10 @@ let sort_of_prod ~metasenv ~subst context (name,s) t (t1, t2) =
    | C.Sort _, C.Sort C.Prop -> t2
    | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
    | C.Sort C.Prop,C.Sort (C.Type _) -> t2
-   | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _
-   | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (_,(_,(C.Irl 0 | C.Ctx [])))
-   | C.Sort _, C.Meta  (_,(_,(C.Irl 0 | C.Ctx []))) -> t2
+   | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Sort _ -> t2
+   | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))), C.Meta (i,(_,(C.Irl 0 | C.Ctx [])))
+   | C.Sort _, C.Meta  (i,(_,(C.Irl 0 | C.Ctx []))) ->
+        NCic.Meta (i,(0, C.Irl 0))
    | x, (C.Sort _ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))))
    | _, x -> 
       let y, context = 
@@ -389,7 +390,9 @@ let rec typeof ~subst ~metasenv context term =
 (*          match ty with C.Implicit _ -> assert false | _ -> c,ty *)
         with U.Meta_not_found _ ->
          raise (AssertFailure (lazy (Printf.sprintf
-          "%s not found" (PP.ppterm ~subst ~metasenv ~context t))))
+          "%s not found in:\n%s" (PP.ppterm ~subst ~metasenv ~context t)
+           (PP.ppmetasenv ~subst metasenv)
+          )))
        in
         check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l;
         S.subst_meta l ty
@@ -414,7 +417,7 @@ let rec typeof ~subst ~metasenv context term =
     | C.LetIn (n,ty,t,bo) ->
        let ty_t = typeof_aux context t in
        let _ = typeof_aux context ty in
-       if not (R.are_convertible ~subst context ty_t ty) then
+       if not (R.are_convertible ~metasenv ~subst context ty_t ty) then
          raise 
           (TypeCheckerFailure 
             (lazy (Printf.sprintf
@@ -485,7 +488,7 @@ let rec typeof ~subst ~metasenv context term =
               let ty_branch = 
                 type_of_branch ~subst context leftno outtype cons ty_cons
               in
-              j+1, R.are_convertible ~subst context ty_p ty_branch,
+              j+1, R.are_convertible ~metasenv ~subst context ty_p ty_branch,
               ty_p, ty_branch
             else
               j,false,old_p_ty,old_exp_p_ty
@@ -519,7 +522,7 @@ let rec typeof ~subst ~metasenv context term =
          | 0,_,_::_
          | _,_,[] ->
             raise (AssertFailure (lazy (Printf.sprintf
-             "Local and canonical context %s have different lengths"
+             "(2) Local and canonical context %s have different lengths"
              (PP.ppterm ~subst ~context ~metasenv term))))
          | m,[],_::_ ->
             raise (TypeCheckerFailure (lazy (Printf.sprintf
@@ -530,7 +533,7 @@ let rec typeof ~subst ~metasenv context term =
                 (_,C.Decl t1), (_,C.Decl t2)
               | (_,C.Def (t1,_)), (_,C.Def (t2,_))
               | (_,C.Def (_,t1)), (_,C.Decl t2) ->
-                 if not (R.are_convertible ~subst tl t1 t2) then
+                 if not (R.are_convertible ~metasenv ~subst tl t1 t2) then
                   raise 
                       (TypeCheckerFailure 
                         (lazy (Printf.sprintf 
@@ -581,7 +584,7 @@ let rec typeof ~subst ~metasenv context term =
                     with Failure _ -> t)
               | _ -> t
              in
-             if not (R.are_convertible ~subst context optimized_t ct)
+             if not (R.are_convertible ~metasenv ~subst context optimized_t ct)
              then
                raise 
                  (TypeCheckerFailure 
@@ -592,7 +595,7 @@ let rec typeof ~subst ~metasenv context term =
                      (PP.ppterm ~subst ~metasenv ~context t))))
           | t, (_,C.Decl ct) ->
               let type_t = typeof_aux context t in
-              if not (R.are_convertible ~subst context type_t ct) then
+              if not (R.are_convertible ~metasenv ~subst context type_t ct) then
                 raise (TypeCheckerFailure 
                  (lazy (Printf.sprintf 
                   ("Not well typed metavariable local context: "^^
@@ -602,9 +605,9 @@ let rec typeof ~subst ~metasenv context term =
                   (PP.ppterm ~subst ~metasenv ~context type_t))))
         ) l lifted_canonical_context 
        with
-        Invalid_argument _ ->
+       | Invalid_argument "List.iter2" ->
           raise (AssertFailure (lazy (Printf.sprintf
-           "Local and canonical context %s have different lengths"
+           "(1) Local and canonical context %s have different lengths"
            (PP.ppterm ~subst ~metasenv ~context term))))
 
  in 
@@ -620,7 +623,7 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
    let arity2 = R.whd ~subst context arity2 in
      match arity1,arity2 with
       | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-         if not (R.are_convertible ~subst context so1 so2) then
+         if not (R.are_convertible ~metasenv ~subst context so1 so2) then
           raise (TypeCheckerFailure (lazy (Printf.sprintf
            "In outtype: expected %s, found %s"
            (PP.ppterm ~subst ~metasenv ~context so1)
@@ -629,7 +632,7 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
          aux ((name, C.Decl so1)::context)
           (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
       | C.Sort _, C.Prod (name,so,ta) ->
-         if not (R.are_convertible ~subst context so ind) then
+         if not (R.are_convertible ~metasenv ~subst context so ind) then
           raise (TypeCheckerFailure (lazy (Printf.sprintf
            "In outtype: expected %s, found %s"
            (PP.ppterm ~subst ~metasenv ~context ind)
@@ -651,8 +654,9 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
                  (cl_len = 0 ||
                   (itl_len = 1 && cl_len = 1 &&
                    let _,_,constrty = List.hd cl in
-                     is_non_recursive_singleton r itname ittype constrty &&
-                     is_non_informative leftno constrty))
+                     is_non_recursive_singleton 
+                       ~subst r itname ittype constrty &&
+                     is_non_informative ~metasenv ~subst leftno constrty))
                 then
                  raise (TypeCheckerFailure (lazy
                   ("Sort elimination not allowed")));
@@ -667,7 +671,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
   | (arg, ty_arg)::tl ->
       match R.whd ~subst context ty_he with 
       | C.Prod (_,s,t) ->
-          if R.are_convertible ~subst context ty_arg s then
+          if R.are_convertible ~metasenv ~subst context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
             raise 
@@ -694,28 +698,28 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
   in
     aux ty_he args_with_ty
 
-and is_non_recursive_singleton (Ref.Ref (uri,_)) iname ity cty =
+and is_non_recursive_singleton ~subst (Ref.Ref (uri,_)) iname ity cty =
      let ctx = [iname, C.Decl ity] in
      let cty = debruijn uri 1 [] cty in
      let len = List.length ctx in
      let rec aux ctx n nn t =
-       match R.whd ctx t with
+       match R.whd ~subst ctx t with
        | C.Prod (name, src, tgt) ->
-            does_not_occur ~subst:[] ctx n nn src &&
+            does_not_occur ~subst ctx n nn src &&
              aux ((name, C.Decl src) :: ctx) (n+1) (nn+1) tgt
        | C.Rel k | C.Appl (C.Rel k :: _) when k = nn -> true
        | _ -> assert false
      in
      aux ctx (len-1) len cty
 
-and is_non_informative paramsno c =
+and is_non_informative ~metasenv ~subst paramsno c =
  let rec aux context c =
    match R.whd context c with
     | C.Prod (n,so,de) ->
-       let s = typeof ~metasenv:[] ~subst:[] context so in
+       let s = typeof ~metasenv ~subst context so in
        s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
     | _ -> true in
- let context',dx = split_prods ~subst:[] [] paramsno c in
+ let context',dx = split_prods ~subst [] paramsno c in
   aux context' dx
 
 and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl = 
@@ -744,11 +748,12 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
                 let convertible =
                  match item1,item2 with
                    (n1,C.Decl ty1),(n2,C.Decl ty2) ->
-                     n1 = n2 && R.are_convertible ~subst context ty1 ty2
+                     n1 = n2 && 
+                     R.are_convertible ~metasenv ~subst context ty1 ty2
                  | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
                      n1 = n2
-                     && R.are_convertible ~subst context ty1 ty2
-                     && R.are_convertible ~subst context bo1 bo2
+                     && R.are_convertible ~metasenv ~subst context ty1 ty2
+                     && R.are_convertible ~metasenv ~subst context bo1 bo2
                  | _,_ -> false
                 in
                  if not convertible then
@@ -758,7 +763,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl =
                  else
                   item1::context
               ) [] sx_context_ty_rev sx_context_te_rev)
-            with Invalid_argument _ -> assert false);
+            with Invalid_argument "List.fold_left2" -> assert false);
            let con_sort = typeof ~subst ~metasenv context te in
            (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
                (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
@@ -1083,13 +1088,13 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) =
      ty
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
 
-and get_relevance ~subst context t args = 
-   let ty = typeof ~subst ~metasenv:[] context t in
+and get_relevance ~metasenv ~subst context t args = 
+   let ty = typeof ~subst ~metasenv context t in
    let rec aux context ty = function
      | [] -> [] 
      | arg::tl -> match R.whd ~subst context ty with
        | C.Prod (_,so,de) -> 
-           let sort = typeof ~subst ~metasenv:[] context so in
+           let sort = typeof ~subst ~metasenv context so in
            let new_ty = S.subst ~avoid_beta_redexes:true arg de in
            (*prerr_endline ("so: " ^ PP.ppterm ~subst ~metasenv:[]
             ~context so);
@@ -1102,14 +1107,14 @@ and get_relevance ~subst context t args =
              | C.Meta _ -> true::(aux context new_ty tl)
               | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
                "Prod: the type %s of the source of %s is not a sort" 
-                (PP.ppterm ~subst ~metasenv:[] ~context sort)
-                (PP.ppterm ~subst ~metasenv:[] ~context so)))))
+                (PP.ppterm ~subst ~metasenv ~context sort)
+                (PP.ppterm ~subst ~metasenv ~context so)))))
        | _ ->
           raise 
             (TypeCheckerFailure
               (lazy (Printf.sprintf
                 "Appl: %s is not a function, it cannot be applied"
-                (PP.ppterm ~subst ~metasenv:[] ~context
+                (PP.ppterm ~subst ~metasenv ~context
                  (let res = List.length tl in
                   let eaten = List.length args - res in
                    (C.Appl
@@ -1128,7 +1133,7 @@ let typecheck_context ~metasenv ~subst context =
        | name,C.Def (te,ty) ->
          ignore (typeof ~metasenv ~subst:[] context ty);
          let ty' = typeof ~metasenv ~subst:[] context te in
-          if not (R.are_convertible ~subst context ty' ty) then
+          if not (R.are_convertible ~metasenv ~subst context ty' ty) then
            raise (AssertFailure (lazy (Printf.sprintf (
             "the type of the definiens for %s in the context is not "^^
             "convertible with the declared one.\n"^^
@@ -1166,7 +1171,7 @@ let typecheck_subst ~metasenv subst =
       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 context ty' ty) then
+       if not (R.are_convertible ~metasenv ~subst context 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"^^
@@ -1187,7 +1192,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
    | C.Constant (relevance,_,Some te,ty,_) ->
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
-      if not (R.are_convertible ~subst [] ty_te ty) then
+      if not (R.are_convertible ~metasenv ~subst [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf (
         "the type of the body is not convertible with the declared one.\n"^^
         "inferred type:\n%s\nexpected type:\n%s")
@@ -1219,7 +1224,7 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) =
       in
       List.iter2 (fun (_,_,x,ty,_) bo ->
        let ty_bo = typeof ~subst ~metasenv types bo in
-       if not (R.are_convertible ~subst types ty_bo ty)
+       if not (R.are_convertible ~metasenv ~subst types ty_bo ty)
        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
        else
         if inductive then begin

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 3308633d6737c909b3329b5043fa1a65614a7912..c5ccff2a46a581eb6378878a5f9f2dc0a51790ef 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -34,7 +34,7 @@ val typeof:
     NCic.term
 
 val get_relevance : 
-  subst:NCic.substitution ->
+  metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term list -> bool list
 
 (* type_of_branch subst context leftno outtype