1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty

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

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index e3e92d098f0f4ed34935543f7a666ec5bb246475..bb978a4cce3b2eef43b4a389ff0243e31d8ffbac 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -1198,7 +1198,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
     allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph 
   =
     (* aux function to add coercions to funclass *)
-    let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph =
+    let rec fix_arity metasenv context subst he hetype eaten args_bo_and_ty ugraph =
       (* {{{ body *)
       let pristinemenv = metasenv in
       let metasenv,hetype' = 
@@ -1228,7 +1228,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
         let args, remainder = 
           HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
         in
-        let args = List.map fst args in
+        let args = List.map fst (eaten@args) in
         let x = 
           if args <> [] then 
             match he with
@@ -1258,9 +1258,11 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
             match  
             HExtlib.list_findopt 
               (fun (metasenv,last,coerc) -> 
+                debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
+                debug_print (lazy ("Last " ^ CicMetaSubst.ppterm ~metasenv subst last));
+                debug_print (lazy ("x " ^ CicMetaSubst.ppterm ~metasenv subst x));
                 let subst,metasenv,ugraph =
                  fo_unif_subst subst context metasenv last x ugraph in
-                debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc));
                 try
                   (* we want this to be available in the error handler fo the
                    * following (so it has its own try. *)
@@ -1285,7 +1287,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                       try 
                         let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
                           fix_arity
-                            metasenv context subst t tty remainder ugraph
+                            metasenv context subst t tty [] remainder ugraph
                         in
                         Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
                       with Uncertain _ | RefineFailure _ -> None
@@ -1312,7 +1314,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       (* {{{ body *)
       function
         | [] -> newargs,subst,metasenv,he,hetype,ugraph
-        | (hete, hety)::tl ->
+        | (hete, hety)::tl as rest ->
             match (CicReduction.whd ~subst context hetype) with 
             | Cic.Prod (n,s,t) ->
                 let arg,subst,metasenv,ugraph =
@@ -1327,7 +1329,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                   let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
                     fix_arity 
                       pristinemenv context subst he hetype 
-                       (newargs@[hete,hety]@tl) ugraph
+                       newargs rest ugraph
                   in
                   eat_prods_and_args metasenv
                     metasenv subst context pristinehe he hetype' 
@@ -1346,7 +1348,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
      else
        (* this (says CSC) is also useful to infer dependent types *)
        try
-        fix_arity metasenv context subst he hetype args_bo_and_ty ugraph
+         fix_arity metasenv context subst he hetype [] args_bo_and_ty ugraph
        with RefineFailure _ | Uncertain _ as exn ->
          (* unable to fix arity *)
           more_args_than_expected localization_tbl metasenv
@@ -1376,6 +1378,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
           "coerce_atom_to_something fails since no coercions found"))
       | CoercGraph.SomeCoercion candidates -> 
+          debug_print (lazy (string_of_int (List.length candidates) ^ "
+          candidates found"));
           let uncertain = ref false in
           let selected = 
 (*             HExtlib.list_findopt *)
@@ -1383,8 +1387,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               HExtlib.filter_map
               (fun (metasenv,last,c) -> 
                try
+                debug_print (lazy ("FO_UNIF_SUBST: " ^
+                CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
+                " <==> " ^
+                CicMetaSubst.ppterm_in_context ~metasenv subst t context));
+                debug_print (lazy ("FO_UNIF_SUBST: " ^
+                CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t));
                 let subst,metasenv,ugraph =
-                 fo_unif_subst subst context metasenv last t ugraph in
+                 fo_unif_subst subst context metasenv last t ugraph
+                in
+
                 let newt,newhety,subst,metasenv,ugraph = 
                  type_of_aux subst metasenv context c ugraph in
                 let newt, newty, subst, metasenv, ugraph = 
@@ -1428,6 +1440,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
           let infty = clean infty subst context in
           let expty = clean expty subst context in
           let t = clean t subst context in
+          debug_print (lazy ("COERCE_TO_SOMETHING: " ^
+          CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
+          CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^ " ==> " ^
+          CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
           match infty, expty, t with
           | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2), Cic.Fix (n,fl) ->
               debug_print (lazy "FIX");
@@ -1698,7 +1714,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
                 ~metasenv subst coerced context));
               (coerced, expty), subst, metasenv, ugraph
           | _ -> 
-              debug_print (lazy "ATOM");
+              debug_print (lazy ("ATOM: " ^ CicMetaSubst.ppterm_in_context
+              ~metasenv subst infty context ^ " ==> " ^
+              CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
             coerce_atom_to_something t infty expty subst metasenv context ugraph
     in
     try