(CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
+
+let enrich f =
+ function
+ RefineFailure msg -> raise (RefineFailure (f msg))
+ | Uncertain msg -> raise (Uncertain (f msg))
+ | _ -> assert false
let rec split l n =
match (l,n) with
in
let funs' = combine (funs, types) in
metasenv', Cic.CoFix (i, funs')
- | term -> metasenv,term
and do_subst metasenv context subst =
List.fold_right
(fun (uri, term) (metasenv, substs) ->
let te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
- (try
let subst''',metasenv''',ugraph3 =
fo_unif_subst subst'' context metasenv''
- inferredty ty ugraph2
+ inferredty ty' ugraph2
in
C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- with
- | _ -> raise (RefineFailure (lazy "Cast")))
| C.Prod (name,s,t) ->
let carr t subst context = CicMetaSubst.apply_subst subst t in
let coerce_to_sort
let search = CoercGraph.look_for_coercion in
let boh = search coercion_src coercion_tgt in
(match boh with
- | CoercGraph.NoCoercion ->
- raise (RefineFailure (lazy "no coercion"))
+ | CoercGraph.NoCoercion
| CoercGraph.NotHandled _ ->
- raise (RefineFailure (lazy "not a sort in PI"))
+ raise
+ (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
| CoercGraph.NotMetaClosed ->
- raise (Uncertain (lazy "Coercions on metas 1"))
+ raise
+ (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort")))
| CoercGraph.SomeCoercion c ->
Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
in
| C.Lambda (n,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- (match CicReduction.whd ~subst:subst' context sort1 with
+ type_of_aux subst metasenv context s ugraph in
+ let s',sort1 =
+ match CicReduction.whd ~subst:subst' context sort1 with
C.Meta _
- | C.Sort _ -> ()
- | _ ->
- raise (RefineFailure (lazy (sprintf
- "Not well-typed lambda-abstraction: the source %s should be a type;
- instead it is a term of type %s" (CicPp.ppterm s)
- (CicPp.ppterm sort1))))
- ) ;
+ | C.Sort _ -> s',sort1
+ | coercion_src ->
+ let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ match boh with
+ | CoercGraph.SomeCoercion c ->
+ Cic.Appl [c;s'], coercion_tgt
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _
+ | CoercGraph.NotMetaClosed ->
+ raise (RefineFailure (lazy (sprintf
+ "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
+ in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let metasenv',t = exp_impl metasenv' subst' context_for_t t in
let t',type2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
+ type_of_aux subst' metasenv' context_for_t t ugraph1
in
C.Lambda (n,s',t'),C.Prod (n,s',type2),
subst'',metasenv'',ugraph2
) tl ([],subst',metasenv',ugraph1)
in
let tl',applty,subst''',metasenv''',ugraph3 =
- eat_prods subst'' metasenv'' context
+ try
+ eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
+ with
+ exn ->
+ enrich
+ (fun msg ->
+ lazy ("The application " ^
+ CicMetaSubst.ppterm_in_context subst'' t context ^
+ " is not well typed:\n" ^ Lazy.force msg)) exn
in
C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
| C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
(Cic.Appl (outtype::right_args@[term']))),
subst,metasenv,ugraph)
| _ -> (* easy case *)
+ let outtype,outtypety, subst, metasenv,ugraph4 =
+ type_of_aux subst metasenv context outtype ugraph4
+ in
+ let tlbody_and_type,subst,metasenv,ugraph4 =
+ List.fold_right
+ (fun x (res,subst,metasenv,ugraph) ->
+ let x',ty,subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context x ugraph
+ in
+ (x', ty)::res,subst',metasenv',ugraph1
+ ) (right_args @ [term']) ([],subst,metasenv,ugraph4)
+ in
+ let _,_,subst,metasenv,ugraph4 =
+ eat_prods false subst metasenv context
+ outtypety tlbody_and_type ugraph4
+ in
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
(C.Appl ((outtype :: right_args) @ [term'])) ugraph4
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2''))))
- and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
+ and eat_prods
+ allow_coercions subst metasenv context hetype tlbody_and_type ugraph
+ =
let rec mk_prod metasenv context =
function
[] ->
fo_unif_subst subst context metasenv hety s ugraph
in
hete,subst,metasenv,ugraph1
- with exn ->
+ with exn when allow_coercions ->
(* we search a coercion from hety to s *)
let coer =
let carr t subst context =
in
match coer with
| CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotHandled _ ->
+ let msg e =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst hete
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context subst hety
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context subst s context
+ (* "\nReason: " ^ Lazy.force e*))
+ in
+ enrich msg exn
| CoercGraph.NotMetaClosed ->
raise (Uncertain (lazy "Coercions on meta"))
| CoercGraph.SomeCoercion c ->
in
let coerced_args,metasenv',subst',t',ugraph2 =
eat_prods metasenv subst context
- (* (CicMetaSubst.subst subst hete t) tl *)
- (CicSubstitution.subst hete t) ugraph1 tl
+ (CicSubstitution.subst arg t) ugraph1 tl
in
arg::coerced_args,metasenv',subst',t',ugraph2
| _ -> assert false
projects / helm.git / blobdiff