some minor fixes

[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 a263a2eb4dc4fcece602edd7dfc1916f062ca9d6..eb350d2e5165500501cea3efb33154a31fad6f4b 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -131,6 +131,20 @@ let exp_impl metasenv subst context =
   | _ -> assert false
 ;;
 
+let unvariant newt =
+ match newt with
+ | Cic.Appl (hd::args) ->
+    let uri = CicUtil.uri_of_term hd in
+    (match 
+      CicEnvironment.get_obj CicUniv.oblivion_ugraph uri 
+    with
+    | Cic.Constant (_,Some t,_,[],attrs),_ 
+      when List.exists ((=) (`Flavour `Variant)) attrs -> 
+       Cic.Appl (t::args)
+    | _ -> newt)
+ | _ -> newt
+;;
+
 let is_a_double_coercion t =
   let rec subst_nth n x l =
     match n,l with
@@ -1191,12 +1205,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) ->
-               match c with 
-               | c when not (CoercGraph.is_composite c) -> 
-                   debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
-                   None
-               | c ->
+             (fun (metasenv,last,c) _ ->
                let subst,metasenv,ugraph =
                 fo_unif_subst subst context metasenv last head ugraph in
                debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
@@ -1305,7 +1314,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                   ugraph
                 in 
                  debug_print (lazy (" has type: "^ pp tty));
-                 Some (coerc,tty,subst,metasenv,ugraph)
+
+                 Some (unvariant coerc,tty,subst,metasenv,ugraph)
               with
               | Uncertain _ | RefineFailure _
               | HExtlib.Localized (_,Uncertain _)
@@ -1345,7 +1355,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: "^
@@ -1444,11 +1454,21 @@ 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 
+                 let newt =  unvariant newt in
+                  Some ((newt,newty), subst, metasenv, ugraph)
                with 
                | Uncertain _ -> uncertain := true; None
                | RefineFailure _ -> None)
@@ -1973,10 +1993,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 *)
@@ -1985,7 +2008,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 *)