bug fixed, all convertible was called without a metasenv

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index fe5ee7fe378942f14c08ebe923a7a689698af4b4..45b2bce8f79b97bdd29e02e795d37cd8e32a549c 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -406,7 +406,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
               type_of_aux subst' metasenv' context te ugraph1
             in
             let rec count_prods context ty =
-              match CicReduction.whd context ty with
+              match CicReduction.whd context ~subst:subst'' ty with
               | Cic.Prod (n,s,t) -> 
                  1 + count_prods (Some (n,Cic.Decl s)::context) t
               | _ -> 0
@@ -417,7 +417,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                let rec aux t m s ug it = function
                  | 0 -> t,it,m,s,ug
                  | n ->
-                      match CicReduction.whd context it with
+                      match CicReduction.whd context ~subst:s it with
                       | Cic.Prod (_,src,tgt) -> 
                           let newmeta, metaty, s, m, ug =
                             type_of_aux s m context (Cic.Implicit None) ug
@@ -425,7 +425,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                           let s,m,ug = 
                             fo_unif_subst s context m metaty src ug
                           in
-(*                           prerr_endline "saturo"; *)
                           let t =
                             match t with
                             | Cic.Appl l -> Cic.Appl (l @ [newmeta])
@@ -437,7 +436,6 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                  aux te' metasenv'' subst'' ugraph2 inferredty
                    (max 0 (inf_prods - exp_prods))
             in
-(*             prerr_endline ("ottengo: " ^ CicPp.ppterm te'); *)
             let (te', ty'), subst''',metasenv''',ugraph3 =
               coerce_to_something true localization_tbl te' inferredty ty'
                 subst'' metasenv'' context ugraph2
@@ -1193,7 +1191,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
       | CoercGraph.SomeCoercion candidates -> 
          let selected =
            HExtlib.list_findopt
-             (function (metasenv,last,c) ->
+             (fun (metasenv,last,c) _ ->
                match c with 
                | c when not (CoercGraph.is_composite c) -> 
                    debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
@@ -1347,7 +1345,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 ugraph in
               match
                 HExtlib.list_findopt
-                 (fun (he,hetype,subst,metasenv,ugraph) ->
+                 (fun (he,hetype,subst,metasenv,ugraph) _ ->
                    (* {{{ *)debug_print (lazy ("Try fix: "^
                     CicMetaSubst.ppterm_in_context ~metasenv subst he context));
                    debug_print (lazy (" of type: "^
@@ -1446,11 +1444,20 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                 let newt,newhety,subst,metasenv,ugraph = 
                  type_of_aux subst metasenv context c ugraph in
                 let newt, newty, subst, metasenv, ugraph = 
-                 avoid_double_coercion context subst metasenv ugraph newt expty 
+                  avoid_double_coercion context subst metasenv ugraph newt
+                    expty 
                 in
                 let subst,metasenv,ugraph = 
-                  fo_unif_subst subst context metasenv newhety expty ugraph in
-                 Some ((newt,newty), subst, metasenv, ugraph)
+                  fo_unif_subst subst context metasenv newhety expty ugraph
+                in
+                let b, ugraph =
+                  CicReduction.are_convertible 
+                    ~subst ~metasenv context infty expty ugraph
+                in
+                if b then 
+                  Some ((t,infty), subst, metasenv, ugraph)
+                else 
+                  Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None
                | RefineFailure _ -> None)
@@ -1975,10 +1982,13 @@ let typecheck metasenv uri obj ~localization_tbl =
      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
   | Cic.Constant (name,None,ty,args,attrs) ->
-     let ty',_,metasenv,ugraph =
+     let ty',sort,metasenv,ugraph =
       type_of_aux' ~localization_tbl metasenv [] ty ugraph
      in
-      Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+      (match CicReduction.whd [] sort with
+          Cic.Sort _
+        | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+        | _ -> raise (RefineFailure (lazy "")))
   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
      assert (metasenv' = metasenv);
      (* Here we do not check the metasenv for correctness *)
@@ -1987,7 +1997,7 @@ let typecheck metasenv uri obj ~localization_tbl =
      let ty',sort,metasenv,ugraph =
       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
      begin
-      match sort with
+       match CicReduction.whd ~delta:true [] sort with
          Cic.Sort _
        (* instead of raising Uncertain, let's hope that the meta will become
           a sort *)