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
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'))
| _ -> 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
;;
-let mk_prod_of_metas metasenv context' subst args =
+let mk_prod_of_metas metasenv context subst args =
let rec mk_prod metasenv context' = function
| [] ->
let (metasenv, idx) =
(* then I generate a name --- using the hint name_hint *)
(* --- that is fresh in context'. *)
let name_hint =
- (* Cic.Name "pippo" *)
FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
- (CicMetaSubst.apply_subst_context subst context')
+ (CicMetaSubst.apply_subst_context subst context)
Cic.Anonymous
~typ:(CicMetaSubst.apply_subst subst argty)
in
- (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
FreshNamesGenerator.mk_fresh_name ~subst
[] context' name_hint ~typ:(Cic.Sort Cic.Prop)
in
in
metasenv,Cic.Prod (name,meta,target)
in
- mk_prod metasenv context' args
+ mk_prod metasenv context args
;;
let rec type_of_constant uri ugraph =
match List.nth context (n - 1) with
Some (_,C.Decl ty) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,Some ty)) ->
+ | Some (_,C.Def (_,ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (bo,None)) ->
- let ty,ugraph =
- (* if it is in the context it must be already well-typed*)
- CicTypeChecker.type_of_aux' ~subst metasenv context
- (S.lift n bo) ugraph
- in
- t,ty,subst,metasenv,ugraph
| None ->
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
in
C.Lambda (n,s',t'),C.Prod (n,s',type2),
subst'',metasenv'',ugraph2
- | C.LetIn (n,s,t) ->
- (* only to check if s is well-typed *)
- let s',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
+ | C.LetIn (n,s,ty,t) ->
+ (* only to check if s is well-typed *)
+ let s',ty',subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph in
+ let ty,_,subst',metasenv',ugraph1 =
+ type_of_aux subst' metasenv' context ty ugraph1 in
+ let subst',metasenv',ugraph1 =
+ try
+ fo_unif_subst subst' context metasenv'
+ ty ty' ugraph1
+ with
+ exn ->
+ enrich localization_tbl s' exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
+ context))
+ in
+ let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
let t',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),
+ C.LetIn (n,s',ty,t'),
CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
(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)
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("(10)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst term'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
exn ->
enrich localization_tbl constructor'
~f:(fun _ ->
- lazy ("(11)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context metasenv subst p'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context metasenv subst actual_type
exn ->
enrich localization_tbl p exn
~f:(function _ ->
- lazy ("(12)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst p
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance'
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("(13)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
exn ->
enrich localization_tbl bo exn
~f:(function _ ->
- lazy ("(14)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,
- C.Def ((S.subst_meta l (S.lift i t)),
- Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ | (Some (n,C.Def (t,ty)))::tl ->
+ (Some
+ (n,
+ C.Def
+ (S.subst_meta l (S.lift i t),
+ S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
_,None ->
l @ [None],subst,metasenv,ugraph
| Some t,Some (_,C.Def (ct,_)) ->
+ (*CSC: the following optimization is to avoid a possibly
+ expensive reduction that can be easily avoided and
+ that is quite frequent. However, this is better
+ handled using levels to control reduction *)
+ let optimized_t =
+ match t with
+ Cic.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ Some (_,C.Def (te,_)) -> S.lift n te
+ | _ -> t
+ with
+ Failure _ -> t)
+ | _ -> t
+ in
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.");
- 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))))))
+(*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 optimized_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 optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
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
(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)
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last he ugraph in
+ debug_print (lazy ("New head: "^ pp coerc));
+ 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 =
fo_unif_subst subst context metasenv infty expty ugraph
in
(t, expty), subst, metasenv, ugraph
- with Uncertain _ | RefineFailure _ as exn ->
- if not allow_coercions || not !insert_coercions then
- enrich localization_tbl t exn
- else
+ with (Uncertain _ | RefineFailure _ as exn)
+ when allow_coercions && !insert_coercions ->
let whd = CicReduction.whd ~delta:false in
let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
let infty = clean infty subst context in
Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
| Some (n, Cic.Def (bo,ty)) ->
let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' =
- match ty with
- None -> None
- | Some ty ->
- Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
in
Some (n, Cic.Def (bo',ty'))
) context
let ugraph = CicUniv.empty_ugraph in
match obj with
Cic.Constant (name,Some bo,ty,args,attrs) ->
+ (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
+ since type_of_aux' destroys localization information (which are
+ preserved by type_of_aux *)
+ let loc exn' =
+ try
+ Cic.CicHash.find localization_tbl bo
+ with Not_found ->
+ HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
+ raise exn' in
let bo',boty,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] bo ugraph in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+ let subst,metasenv,ugraph =
+ try
+ fo_unif_subst [] [] metasenv boty ty' ugraph
+ with
+ RefineFailure _
+ | Uncertain _ as exn ->
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
+ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
+ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
+ in
+ let exn' =
+ match exn with
+ RefineFailure _ -> RefineFailure msg
+ | Uncertain _ -> Uncertain msg
+ | _ -> assert false
+ in
+ raise (HExtlib.Localized (loc exn',exn'))
+ in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
| C.Lambda (name,so,dest) ->
let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.LetIn (name,so,dest) ->
- let _,ty,metasenv,ugraph =
- pack_coercions := false;
- type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
- pack_coercions := true;
- let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
- C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.LetIn (name,so,ty,dest) ->
+ let ctx' = Some (name,(C.Def (so,ty)))::ctx in
+ C.LetIn
+ (name, merge_coercions ctx so, merge_coercions ctx ty,
+ merge_coercions ctx' dest)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
projects / helm.git / blobdiff