Effects of fixing bugs for other regression tests ;-)

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 60b6129b1c2db4ca806e4460872e95db635f525d..060d2bd1f767c9767fdd1c6cb99b65d22f8bca9e 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -163,7 +163,7 @@ and type_of_aux' metasenv context t =
     | C.Meta (n,l) -> 
        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         let subst',metasenv' =
-         check_metasenv_consistency subst metasenv context canonical_context l
+         check_metasenv_consistency n subst metasenv context canonical_context l
         in
         CicSubstitution.lift_meta l ty, subst', metasenv'
     | C.Sort s ->
@@ -188,7 +188,8 @@ and type_of_aux' metasenv context t =
        let sort2,subst'',metasenv'' =
         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
        in
-        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
+        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
+         subst'',metasenv''
    | C.Lambda (n,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
        let type2,subst'',metasenv'' =
@@ -198,10 +199,10 @@ and type_of_aux' metasenv context t =
          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
         in
          (* only to check if the product is well-typed *)
-         let _,subst'''',metasenv'''' =
+         let _ =
           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
          in
-          C.Prod (n,s,type2),subst'''',metasenv''''
+          C.Prod (n,s,type2),subst''',metasenv'''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
@@ -389,7 +390,9 @@ and type_of_aux' metasenv context t =
  (* check_metasenv_consistency checks that the "canonical" context of a
  metavariable is consitent - up to relocation via the relocation list l -
  with the actual context *)
- and check_metasenv_consistency subst metasenv context canonical_context l =
+ and check_metasenv_consistency
+  metano subst metasenv context canonical_context l
+ =
    let module C = Cic in
    let module R = CicReduction in
    let module S = CicSubstitution in
@@ -427,7 +430,10 @@ and type_of_aux' metasenv context t =
                 subst' context metasenv' inferredty ct
              with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
          | None, Some _  ->
-             raise (NotRefinable "The local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context")
+             raise (NotRefinable (sprintf
+              "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
+              (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+              (CicMetaSubst.ppcontext subst canonical_context)))
       ) (subst,metasenv) l lifted_canonical_context 
 
  and check_exp_named_subst metasubst metasenv context =
@@ -466,24 +472,21 @@ and type_of_aux' metasenv context t =
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
-          C.Sort s2,subst,metasenv
+          C.Sort s2
      | (C.Sort s1, C.Sort s2) ->
          (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst,metasenv
+         C.Sort C.Type
      | (C.Meta _,_) | (_,C.Meta _) ->
          (* TODO how can we force the meta to become a sort? If we don't we
           * brake the invariant that refine produce only well typed terms *)
          (* TODO if we check the non meta term and if it is a sort then we are
           * likely to know the exact value of the result e.g. if the rhs is a
           * Sort (Prop | Set | CProp) then the result is the rhs *)
-         let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in
-         let irl =
-           CicMkImplicit.identity_relocation_list_for_metavariable context
-         in
-         C.Meta (idx, irl), subst, metasenv
+         (C.Sort C.Type)
+(*           t2'' *)
      | (_,_) ->
          raise (NotRefinable (sprintf
-          "Two types were expected, found %s (that reduces to %s) and %s (that reducecs to %s)"
+          "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
           (CicPp.ppterm t2'')))
 
@@ -503,7 +506,9 @@ and type_of_aux' metasenv context t =
        let (metasenv, idx) =
         CicMkImplicit.mk_implicit metasenv (context'' @ context) in
        let irl =
-         (Some (Cic.Rel 1))::args'@(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2 context)
+         (Some (Cic.Rel 1))::args' @
+          (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
+            context)
        in
        let newmeta = Cic.Meta (idx, irl) in
        let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in