(CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
| (CicUnification.Uncertain msg) -> raise (Uncertain msg)
;;
-
+
let rec split l n =
match (l,n) with
(l,0) -> ([], l)
type_of_aux subst' metasenv'
((Some (name,(C.Decl s')))::context) t ugraph1
in
- let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod subst'' metasenv''
- context (name,s') (sort1,sort2) ugraph2
- in
- C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
+ (try
+ let sop,subst''',metasenv''',ugraph3 =
+ sort_of_prod subst'' metasenv''
+ context (name,s') (sort1,sort2) ugraph2
+ in
+ C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
+ with
+ | RefineFailure _ as exn ->
+ (* given [t] of type [type_to_coerce] returns
+ * a term that has type [tgt_sort] eventually
+ * derived from (coercion [t]) *)
+ let refined_target = t' in
+ let sort_of_refined_target = sort2 in
+ let carr t subst context = CicMetaSubst.apply_subst subst t in
+ let coerce_to_sort tgt_sort t type_to_coerce subst ctx =
+ match type_to_coerce with
+ | Cic.Sort _ -> t
+ | term ->
+ let coercion_src = carr type_to_coerce subst ctx in
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in
+ let search = CoercGraph.look_for_coercion in
+ (match search coercion_src coercion_tgt with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotMetaClosed ->
+ raise (Uncertain "Coercions on metas")
+ | CoercGraph.SomeCoercion c -> Cic.Appl [c;t])
+ in
+ (* this is probably not the best... *)
+ let tgt_sort_for_pi_source = Cic.Type(CicUniv.fresh()) in
+ let tgt_sort_for_pi_target = Cic.Type(CicUniv.fresh()) in
+ let new_src =
+ coerce_to_sort tgt_sort_for_pi_source s sort1 subst context
+ in
+ let context_with_new_src =
+ ((Some (name,(C.Decl new_src)))::context)
+ in
+ let new_tgt =
+ coerce_to_sort
+ tgt_sort_for_pi_target
+ refined_target sort_of_refined_target
+ subst context_with_new_src
+ in
+ let newprod = C.Prod (name,new_src,new_tgt) in
+ let _,sort_of_refined_prod,subst,metasenv,ugraph3 =
+ type_of_aux subst metasenv context newprod ugraph2
+ in
+ (* this if for a coercion on the tail of the arrow *)
+ let new_target =
+ match sort_of_refined_target with
+ | Cic.Sort _ -> refined_target
+ | _ -> new_tgt
+ in
+ C.Prod(name,new_src,new_target),
+ sort_of_refined_prod,subst,metasenv,ugraph3)
| C.Lambda (n,s,t) ->
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
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) -> (* different than Coq manual!!! *)
+ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
+ (* different than Coq manual!!! *)
C.Sort s2,subst,metasenv,ugraph
| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
let t' = CicUniv.fresh() in
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
C.Sort (C.Type t'),subst,metasenv,ugraph2
| (C.Sort _,C.Sort (C.Type t1)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
C.Sort (C.Type 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
* brake the invariant that refine produce only well typed terms *)
- (* TODO if we check the non meta term and if it is a sort then we are
- * likely to know the exact value of the result e.g. if the rhs is a
- * Sort (Prop | Set | CProp) then the result is the rhs *)
+ (* TODO if we check the non meta term and if it is a sort then we
+ * are likely to know the exact value of the result e.g. if the rhs
+ * is a Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
CicMkImplicit.mk_implicit_sort metasenv subst in
let (subst, metasenv,ugraph1) =
- fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' ugraph
+ fo_unif_subst subst context_for_t2 metasenv
+ (C.Meta (idx,[])) t2'' ugraph
in
t2'',subst,metasenv,ugraph1
- | (_,_) ->
- raise (RefineFailure (Reason (sprintf
- "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
- (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
- (CicPp.ppterm t2''))))
+ | _,_ ->
+ raise
+ (RefineFailure
+ (Reason
+ (sprintf
+ ("Two sorts were expected, found %s " ^^
+ "(that reduces to %s) and %s (that reduces to %s)")
+ (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
+ (CicPp.ppterm t2''))))
and eat_prods subst metasenv context hetype tlbody_and_type ugraph =
let rec mk_prod metasenv context =
hete,subst,metasenv,ugraph1
with exn ->
(* we search a coercion from hety to s *)
- let coer = CoercGraph.look_for_coercion
- (CicMetaSubst.apply_subst subst hety)
- (CicMetaSubst.apply_subst subst s)
+ let coer =
+ let carr t subst context =
+ CicMetaSubst.apply_subst subst t
+ in
+ let c_hety = carr hety subst context in
+ let c_s = carr s subst context in
+ CoercGraph.look_for_coercion c_hety c_s
in
match coer with
- | None -> raise exn
- | Some c ->
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ -> raise exn
+ | CoercGraph.NotMetaClosed ->
+ raise (Uncertain "Coercions on meta")
+ | CoercGraph.SomeCoercion c ->
(Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
in
let coerced_args,metasenv',subst',t',ugraph2 =
projects / helm.git / blobdiff