;;
let is_a_double_coercion t =
- let last_of l =
- let rec aux acc = function
- | x::[] -> acc,x
- | x::tl -> aux (acc@[x]) tl
- | [] -> assert false
- in
- aux [] l
+ let rec subst_nth n x l =
+ match n,l with
+ | _, [] -> []
+ | 0, _::tl -> x :: tl
+ | n, hd::tl -> hd :: subst_nth (n-1) x tl
in
let imp = Cic.Implicit None in
let dummyres = false,imp, imp,imp,imp in
match t with
- | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 ->
- (match last_of tl with
- | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 ->
- let sib2,head = last_of tl2 in
- true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl
- (c2::sib2@[imp])])
+ | Cic.Appl l1 ->
+ (match CoercGraph.coerced_arg l1 with
+ | Some (Cic.Appl l2, pos1) ->
+ (match CoercGraph.coerced_arg l2 with
+ | Some (x, pos2) ->
+ true, List.hd l1, List.hd l2, x,
+ Cic.Appl (subst_nth (pos1 + 1)
+ (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
+ | _ -> dummyres)
| _ -> dummyres)
| _ -> dummyres
+;;
let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
=
t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
with
CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | C.Sort _ ->
+ | C.Sort (C.CProp tno) ->
+ let tno' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+ t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | C.Sort (C.Prop|C.Set) ->
t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
| C.Implicit infos ->
let metasenv',t' = exp_impl metasenv subst context infos in
let t1'' = CicReduction.whd ~subst context t1 in
let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
match (t1'', t2'') with
- (C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
+ | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
(* different than Coq manual!!! *)
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
C.Sort (C.Type t'),subst,metasenv,ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.Type t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) ->
C.Sort (C.Type t1),subst,metasenv,ugraph
+ | (C.Sort _,C.Sort (C.CProp t1)) ->
+ C.Sort (C.CProp t1),subst,metasenv,ugraph
| (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
| (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
(* given he:hety, gives beack all (c he) such that (c e):?->? *)
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
+ let src = CoercDb.coerc_carr_of_term hetype 0 in
+ let tgt = CoercDb.coerc_carr_of_term (Cic.Implicit None) 1 in
match CoercGraph.look_for_coercion' metasenv subst context src tgt with
| CoercGraph.NoCoercion -> []
- | CoercGraph.NotMetaClosed
- | CoercGraph.NotHandled _ ->
+ | CoercGraph.NotHandled ->
raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
| CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
CoercGraph.look_for_coercion metasenv subst context infty expty
in
match coer with
- | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy
- "coerce_atom_to_something fails since not meta closed"))
| CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _
- | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy
+ | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
+ "coerce_atom_to_something fails since no coercions found"))
+ | CoercGraph.NotHandled when
+ not (CicUtil.is_meta_closed infty) ||
+ not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
+ "coerce_atom_to_something fails since carriers have metas"))
+ | CoercGraph.NotHandled -> raise (RefineFailure (lazy
"coerce_atom_to_something fails since no coercions found"))
| CoercGraph.SomeCoercion candidates ->
debug_print (lazy (string_of_int (List.length candidates) ^
CicTypeChecker.type_of_aux' ~subst metasenv context m
CicUniv.oblivion_ugraph
with
- | Cic.MutInd _ as mty,_ -> [], mty
- | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+ | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
+ | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
snd (HExtlib.split_nth leftno args), mty
| _ -> assert false
- with CicTypeChecker.TypeCheckerFailure _ -> assert false
+ with CicTypeChecker.TypeCheckerFailure _ ->
+ raise (AssertFailure(lazy "already ill-typed matched term"))
in
let new_outty =
keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
projects / helm.git / blobdiff