huge commit regarding coercions to funclass and eat_prods. before there was a

so broken behaviour that is impossible to describe the changes.

now:
  eat_prods he hety args

  starts checking if hety is metaclosed, if it is does nothing, if not
  unifies it with ?->?-> ... ->? s.t. there is a Pi for every args.
  if this unification fails, does nothing (all coercions are in the
  second phase.

  continues eating prods in hety and args in parallel, if there is an arg
  and no more prods, tries to fix the arity of (he already_processed_args).
  fix_arity gives a range of possible coercions to funclass s.t.
  (c (he ..)) : FunType. The eat prods and args continues, eting the remaining
  args toghether with FunType. If it fails, it continues with another c to
  another FunType. This recursively (yes, it backtracks. no strong opinion
  here, but there is no sane heuristinc to chose one FunType).

  the code is reduced to 1/3, but Localization of errors probably need fixing.

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index bb978a4cce3b2eef43b4a389ff0243e31d8ffbac..1242a1cded879cb24a21c7d3be344f34a8228d1b 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1197,148 +1197,84 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
   and eat_prods 
     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 eaten args_bo_and_ty ugraph =
-      (* {{{ body *)
-      let pristinemenv = metasenv in
-      let metasenv,hetype' = 
-        mk_prod_of_metas metasenv context subst args_bo_and_ty 
-      in
-      try
-        let subst,metasenv,ugraph = 
-          fo_unif_subst_eat_prods 
-            subst context metasenv hetype hetype' ugraph
-        in
-        subst,metasenv,ugraph,hetype',he,args_bo_and_ty
-      with RefineFailure s | Uncertain s as exn 
-      when allow_coercions && !insert_coercions ->
-        (* {{{ we search a coercion of the head (saturated) to funclass *)
-        let metasenv = pristinemenv in
-        debug_print (lazy 
-          ("Fixing arity of: "^CicMetaSubst.ppterm ~metasenv subst hetype ^
-           " since unif failed with: " ^ CicMetaSubst.ppterm ~metasenv subst hetype' 
-           (* ^ " cause: " ^ Lazy.force s *)));
-        let how_many_args_are_needed = 
-          let rec aux n = function
-            | Cic.Prod(_,_,t) -> aux (n+1) t
-            | _ -> n
-          in
-          aux 0 (CicMetaSubst.apply_subst subst hetype)
-        in
-        let args, remainder = 
-          HExtlib.split_nth how_many_args_are_needed args_bo_and_ty
-        in
-        let args = List.map fst (eaten@args) in
-        let x = 
-          if args <> [] then 
-            match he with
-            | Cic.Appl l -> Cic.Appl (l@args)
-            | _ -> Cic.Appl (he::args) 
-          else
-            he
-        in
-        let x,xty,subst,metasenv,ugraph =
-         (*CSC: here unsharing is necessary to avoid an unwanted
-           relocalization. However, this also shows a great source of
-           inefficiency: "x" is refined twice (once now and once in the
-           subsequent eat_prods_and_args). Morevoer, how is divergence avoided?
-         *)
-         type_of_aux subst metasenv context (Unshare.unshare x) ugraph
-        in
-        let carr_src = 
-          CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) 
-        in
-        let carr_tgt = CoercDb.Fun 0 in
-        match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with
-        | CoercGraph.NoCoercion 
-        | CoercGraph.NotMetaClosed 
-        | CoercGraph.NotHandled _ -> raise exn
-        | CoercGraph.SomeCoercionToTgt candidates
-        | CoercGraph.SomeCoercion candidates ->
-            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
-                try
-                  (* we want this to be available in the error handler fo the
-                   * following (so it has its own try. *)
-                  let t,tty,subst,metasenv,ugraph =
-                    type_of_aux subst metasenv context coerc ugraph
-                  in 
-                  try
-                    let metasenv, hetype' = 
-                      mk_prod_of_metas metasenv context subst remainder 
-                    in
-                    debug_print (lazy 
-                      ("  unif: " ^ CicMetaSubst.ppterm ~metasenv subst tty ^ " = " ^ 
-                       CicMetaSubst.ppterm ~metasenv subst hetype'));
-                    let subst,metasenv,ugraph = 
-                      fo_unif_subst_eat_prods 
-                        subst context metasenv tty hetype' ugraph
-                    in
-                    debug_print (lazy " success!");
-                    Some (subst,metasenv,ugraph,tty,t,remainder) 
-                  with 
-                  | Uncertain _ | RefineFailure _ ->
-                      try 
-                        let subst,metasenv,ugraph,hetype',he,args_bo_and_ty =
-                          fix_arity
-                            metasenv context subst t tty [] remainder ugraph
-                        in
-                        Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty)
-                      with Uncertain _ | RefineFailure _ -> None
-                with
-                   Uncertain _
-                 | RefineFailure _
-                 | HExtlib.Localized (_,Uncertain _)
-                 | HExtlib.Localized (_,RefineFailure _) -> None 
-                 | exn -> assert false) (* ritornare None, e' un localized *)
-              candidates
-           with
-           | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)->
-               subst,metasenv,ugraph,hetype',he,args_bo_and_ty
-           | None -> 
-               more_args_than_expected localization_tbl metasenv
-                 subst he context hetype args_bo_and_ty exn
-      (* }}} end coercion to funclass stuff *)           
-      (* }}} end fix_arity *)           
+    (* given he:hety, gives beack all (c he) such that (c e):?->? *)
+    let fix_arity exn metasenv context subst he hetype ugraph =
+      let hetype = CicMetaSubst.apply_subst subst hetype in
+      let src = CoercDb.coerc_carr_of_term hetype in 
+      let tgt = CoercDb.Fun 0 in
+      match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+      | CoercGraph.NoCoercion 
+      | CoercGraph.NotMetaClosed 
+      | CoercGraph.NotHandled _ -> raise exn
+      | CoercGraph.SomeCoercionToTgt candidates
+      | CoercGraph.SomeCoercion candidates ->
+          HExtlib.filter_map
+            (fun (metasenv,last,coerc) -> 
+              let pp t = 
+                CicMetaSubst.ppterm_in_context ~metasenv subst t context in
+              let subst,metasenv,ugraph =
+               fo_unif_subst subst context metasenv last he ugraph in
+              debug_print (lazy ("New head: "^ pp coerc));
+              try
+                let t,tty,subst,metasenv,ugraph =
+                  type_of_aux subst metasenv context coerc ugraph in 
+                (*{{{*)debug_print (lazy (" refined: "^ pp t));
+                debug_print (lazy (" has type: "^ pp tty));(*}}}*)
+                Some (t,tty,subst,metasenv,ugraph)
+              with
+              | Uncertain _ | RefineFailure _
+              | HExtlib.Localized (_,Uncertain _)
+              | HExtlib.Localized (_,RefineFailure _) -> None 
+              | exn -> assert false) 
+            candidates
     in
     (* aux function to process the type of the head and the args in parallel *)
-    let rec eat_prods_and_args 
-      pristinemenv metasenv subst context pristinehe he hetype ugraph newargs 
-    =
-      (* {{{ body *)
+    let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
       function
-        | [] -> newargs,subst,metasenv,he,hetype,ugraph
-        | (hete, hety)::tl as rest ->
-            match (CicReduction.whd ~subst context hetype) with 
-            | Cic.Prod (n,s,t) ->
-                let arg,subst,metasenv,ugraph =
-                  coerce_to_something allow_coercions localization_tbl 
-                    hete hety s subst metasenv context ugraph in
-                eat_prods_and_args 
-                  pristinemenv metasenv subst context pristinehe he
-                  (CicSubstitution.subst (fst arg) t) 
-                  ugraph (newargs@[arg]) tl
-            | _ -> 
-                try
-                  let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
-                    fix_arity 
-                      pristinemenv context subst he hetype 
-                       newargs rest ugraph
-                  in
-                  eat_prods_and_args metasenv
-                    metasenv subst context pristinehe he hetype' 
-                    ugraph [] args_bo_and_ty
-                with RefineFailure _ | Uncertain _ as exn ->
-                  (* unable to fix arity *)
-                   more_args_than_expected localization_tbl metasenv
-                     subst he context hetype args_bo_and_ty exn
-      (* }}} *)
+      | [] -> newargs,subst,metasenv,he,hetype,ugraph
+      | (hete, hety)::tl as args ->
+          match (CicReduction.whd ~subst context hetype) with 
+          | Cic.Prod (n,s,t) ->
+              let arg,subst,metasenv,ugraph =
+                coerce_to_something allow_coercions localization_tbl 
+                  hete hety s subst metasenv context ugraph in
+              eat_prods_and_args 
+                metasenv subst context he (CicSubstitution.subst (fst arg) t) 
+                ugraph (newargs@[arg]) tl
+          | _ -> 
+              let he = 
+                match he, newargs with
+                | _, [] -> he
+                | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
+                | _ -> Cic.Appl (he::List.map fst newargs)
+              in
+              (*{{{*) debug_print (lazy 
+               let pp x = 
+                CicMetaSubst.ppterm_in_context ~metasenv subst x context in
+               "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
+               "\n but is applyed to: " ^ String.concat ";" 
+               (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
+              let exn = RefineFailure (lazy ("more args than expected")) in
+              let possible_fixes = 
+               fix_arity exn metasenv context subst he hetype ugraph in
+              match
+                HExtlib.list_findopt
+                 (fun (he,hetype,subst,metasenv,ugraph) ->
+                   (* {{{ *)debug_print (lazy ("Try fix: "^
+                    CicMetaSubst.ppterm_in_context ~metasenv subst he context));
+                   debug_print (lazy (" of type: "^
+                    CicMetaSubst.ppterm_in_context 
+                    ~metasenv subst hetype context)); (* }}} *)
+                   try      
+                    Some (eat_prods_and_args 
+                      metasenv subst context he hetype ugraph [] args)
+                   with RefineFailure _ | Uncertain _ -> None)
+                possible_fixes
+              with
+              | Some x -> x
+              | None ->
+                 more_args_than_expected localization_tbl metasenv
+                   subst he context hetype args_bo_and_ty exn
     in
     (* first we check if we are in the simple case of a meta closed term *)
     let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
@@ -1347,16 +1283,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
       subst,metasenv,ugraph,hetype,he,args_bo_and_ty
      else
        (* this (says CSC) is also useful to infer dependent types *)
-       try
-         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
-            subst he context hetype args_bo_and_ty exn
+        let pristinemenv = metasenv in
+        let metasenv,hetype' = 
+          mk_prod_of_metas metasenv context subst args_bo_and_ty 
+        in
+        try
+          let subst,metasenv,ugraph = 
+           fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
+          in
+          subst,metasenv,ugraph,hetype',he,args_bo_and_ty
+        with RefineFailure _ | Uncertain _ ->
+          subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
     in
     let coerced_args,subst,metasenv,he,t,ugraph =
       eat_prods_and_args 
-        metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty
+        metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
     in
     he,(List.map fst coerced_args),t,subst,metasenv,ugraph
 
@@ -1382,17 +1323,16 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
           candidates found"));
           let uncertain = ref false in
           let selected = 
-(*             HExtlib.list_findopt *)
             let posibilities =
               HExtlib.filter_map
               (fun (metasenv,last,c) -> 
                try
-                debug_print (lazy ("FO_UNIF_SUBST: " ^
+                (* {{{ *) 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));
+                CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
                 let subst,metasenv,ugraph =
                  fo_unif_subst subst context metasenv last t ugraph
                 in
@@ -1440,10 +1380,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: " ^
+          (*{{{*) 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));
+          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");