removed no longer used METAs

[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 20be9363bbbc385ad82d972ad51b1769635bc4b1..620f66f1831a4ec598178645201dd7686c47c7d7 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Printf
 
 exception RefineFailure of string Lazy.t;;
@@ -851,7 +853,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
 
   and  avoid_double_coercion subst metasenv ugraph t ty = 
     match t with
-    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when 
+    | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) when 
       CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
           let source_carr = CoercGraph.source_of c2 in
           let tgt_carr = CicMetaSubst.apply_subst subst ty in
@@ -1011,22 +1013,22 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
   and eat_prods 
     allow_coercions subst metasenv context hetype tlbody_and_type ugraph 
   =
-    let rec mk_prod metasenv context =
+    let rec mk_prod metasenv context' =
       function
           [] ->
             let (metasenv, idx) = 
-              CicMkImplicit.mk_implicit_type metasenv subst context 
+              CicMkImplicit.mk_implicit_type metasenv subst context'
             in
             let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context
+              CicMkImplicit.identity_relocation_list_for_metavariable context'
             in
               metasenv,Cic.Meta (idx, irl)
         | (_,argty)::tl ->
             let (metasenv, idx) = 
-              CicMkImplicit.mk_implicit_type metasenv subst context 
+              CicMkImplicit.mk_implicit_type metasenv subst context' 
             in
             let irl =
-              CicMkImplicit.identity_relocation_list_for_metavariable context
+              CicMkImplicit.identity_relocation_list_for_metavariable context'
             in
             let meta = Cic.Meta (idx,irl) in
             let name =
@@ -1034,7 +1036,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               (* Nevertheless, argty is well-typed only in context.  *)
               (* Thus I generate a name (name_hint) in context and   *)
               (* then I generate a name --- using the hint name_hint *)
-              (* --- that is fresh in (context'@context).            *)
+              (* --- that is fresh in context'.                      *)
               let name_hint = 
                 (* Cic.Name "pippo" *)
                 FreshNamesGenerator.mk_fresh_name ~subst metasenv 
@@ -1045,10 +1047,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
               in
                 (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
                 FreshNamesGenerator.mk_fresh_name ~subst
-                  [] context name_hint ~typ:(Cic.Sort Cic.Prop)
+                  [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
             in
             let metasenv,target =
-              mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+              mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
             in
               metasenv,Cic.Prod (name,meta,target)
     in
@@ -1113,9 +1115,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                            let newt, _, subst, metasenv, ugraph = 
                              avoid_double_coercion 
                               subst metasenv ugraph 
-                                (Cic.Appl[c;hete]) tgt_carr
-                           in
-                            newt, subst, metasenv, ugraph)
+                                (Cic.Appl[c;hete]) tgt_carr in
+                           try
+                            let newty,newhety,subst,metasenv,ugraph = 
+                              type_of_aux subst metasenv context newt ugraph in
+                            let subst,metasenv,ugraph1 = 
+                             fo_unif_subst subst context metasenv 
+                                newhety s ugraph
+                            in
+                             newt, subst, metasenv, ugraph
+                           with exn ->
+                            enrich localization_tbl hete
+                             ~f:(fun _ ->
+                               (lazy ("The term " ^
+                                 CicMetaSubst.ppterm_in_context subst hete
+                                  context ^ " has type " ^
+                                 CicMetaSubst.ppterm_in_context subst hety
+                                  context ^ " but is here used with type " ^
+                                 CicMetaSubst.ppterm_in_context subst s context
+                                  (* "\nReason: " ^ Lazy.force e*)))) exn)
                      | exn ->
                         enrich localization_tbl hete
                          ~f:(fun _ ->
@@ -1331,7 +1349,9 @@ let typecheck metasenv uri obj ~localization_tbl =
          let metasenv,ugraph,cl' =
           List.fold_right
            (fun (name,ty) (metasenv,ugraph,res) ->
-             let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+             let ty =
+              CicTypeChecker.debrujin_constructor
+               ~cb:(relocalize localization_tbl) uri typesno ty in
              let ty',_,metasenv,ugraph =
               type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in