X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;h=e4f4ef8e0c002a600f791d37ec2f9524730dbefb;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=b50667bb5546a745ac53420827f0cdbd1d300dc6;hpb=bff82b0ee42229e87bad101341fc5789d8199153;p=helm.git diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index b50667bb5..e4f4ef8e0 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -31,6 +31,9 @@ exception RefineFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +(* for internal use only; the integer is the number of surplus arguments *) +exception MoreArgsThanExpected of int * exn;; + let insert_coercions = ref true let pack_coercions = ref true @@ -88,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = try Cic.CicHash.find localization_tbl t with Not_found -> - prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); raise exn' in raise (HExtlib.Localized (loc,exn')) @@ -149,15 +152,16 @@ let is_a_double_coercion t = | _ -> dummyres) | _ -> dummyres -let more_args_than_expected - localization_tbl metasenv subst he context hetype' tlbody_and_type exn +let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn = + let len = List.length tlbody_and_type in let msg = lazy ("The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ - " (that has type "^CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ - ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected") + " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ + ") is here applied to " ^ string_of_int len ^ + " arguments but here it can handle only up to " ^ + string_of_int (len - residuals) ^ " arguments") in enrich localization_tbl he ~f:(fun _-> msg) exn ;; @@ -523,6 +527,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) in + if List.length constructors <> List.length pl then + enrich localization_tbl t + (RefineFailure + (lazy "Wrong number of cases")) ; let rec count_prod t = match CicReduction.whd ~subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) @@ -953,7 +961,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | Some t,Some (_,C.Def (ct,_)) -> let subst',metasenv',ugraph' = (try -prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Rel corrispondente. Si puo' ottimizzare il caso t = rel."); +(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' + * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*) fo_unif_subst subst context metasenv t ct ugraph with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in @@ -1179,18 +1188,19 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in tlbody_and_type,subst,metasenv,ugraph - and eat_prods + and eat_prods allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph = (* given he:hety, gives beack all (c he) such that (c e):?->? *) - let fix_arity exn metasenv context subst he hetype ugraph = + let fix_arity n 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.NoCoercion -> [] | CoercGraph.NotMetaClosed - | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotHandled _ -> + raise (MoreArgsThanExpected (n,Uncertain (lazy ""))) | CoercGraph.SomeCoercionToTgt candidates | CoercGraph.SomeCoercion candidates -> HExtlib.filter_map @@ -1201,11 +1211,10 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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) + let tty,ugraph = + CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in + debug_print (lazy (" has type: "^ pp tty)); + Some (coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) @@ -1239,9 +1248,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il "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 + fix_arity (List.length args) metasenv context subst he hetype + ugraph in match HExtlib.list_findopt (fun (he,hetype,subst,metasenv,ugraph) -> @@ -1253,13 +1262,17 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il try Some (eat_prods_and_args metasenv subst context he hetype ugraph [] args) - with RefineFailure _ | Uncertain _ -> None) + with + | RefineFailure _ | Uncertain _ + | HExtlib.Localized (_,RefineFailure _) + | HExtlib.Localized (_,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 + raise + (MoreArgsThanExpected + (List.length args, RefineFailure (lazy ""))) 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 = @@ -1281,8 +1294,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty in let coerced_args,subst,metasenv,he,t,ugraph = + try eat_prods_and_args metasenv subst context he hetype' ugraph1 [] args_bo_and_ty + with + MoreArgsThanExpected (residuals,exn) -> + more_args_than_expected localization_tbl metasenv + subst he context hetype' residuals args_bo_and_ty exn in he,(List.map fst coerced_args),t,subst,metasenv,ugraph @@ -1316,7 +1334,9 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ " <==> " ^ - CicMetaSubst.ppterm_in_context ~metasenv subst t context)); + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ + "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c + context)); debug_print (lazy ("FO_UNIF_SUBST: " ^ CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *) let subst,metasenv,ugraph =