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
| _ -> 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
;;
(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)
| 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
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
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 _)
"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) ->
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 =
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
(* {{{ *) 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 =
projects / helm.git / blobdiff