| _ -> assert false
;;
+let unvariant newt =
+ match newt with
+ | Cic.Appl (hd::args) ->
+ let uri = CicUtil.uri_of_term hd in
+ (match
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
+ with
+ | Cic.Constant (_,Some t,_,[],attrs),_
+ when List.exists ((=) (`Flavour `Variant)) attrs ->
+ Cic.Appl (t::args)
+ | _ -> newt)
+ | _ -> newt
+;;
+
let is_a_double_coercion t =
let rec subst_nth n x l =
match n,l with
| _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
| _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
- ugraph
+and type_of_aux' ?(clean_dummy_dependent_types=true)
+ ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
let module C = Cic in
type_of_aux subst' metasenv' context te ugraph1
in
let rec count_prods context ty =
- match CicReduction.whd context ty with
+ match CicReduction.whd context ~subst:subst'' ty with
| Cic.Prod (n,s,t) ->
1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
let rec aux t m s ug it = function
| 0 -> t,it,m,s,ug
| n ->
- match CicReduction.whd context it with
+ match CicReduction.whd context ~subst:s it with
| Cic.Prod (_,src,tgt) ->
let newmeta, metaty, s, m, ug =
type_of_aux s m context (Cic.Implicit None) ug
let s,m,ug =
fo_unif_subst s context m metaty src ug
in
-(* prerr_endline "saturo"; *)
let t =
match t with
| Cic.Appl l -> Cic.Appl (l @ [newmeta])
aux te' metasenv'' subst'' ugraph2 inferredty
(max 0 (inf_prods - exp_prods))
in
-(* prerr_endline ("ottengo: " ^ CicPp.ppterm te'); *)
let (te', ty'), subst''',metasenv''',ugraph3 =
coerce_to_something true localization_tbl te' inferredty ty'
subst'' metasenv'' context ugraph2
exn ->
enrich localization_tbl s' exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(2) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
context ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("The term " ^
+ lazy ("(3) 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 ("The term " ^
+ lazy ("(4) 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 ("The term " ^
+ lazy ("(5) 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 ("The term " ^
+ lazy ("(7) 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 ("The term " ^
+ lazy ("(8) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
| CoercGraph.SomeCoercion candidates ->
let selected =
HExtlib.list_findopt
- (function (metasenv,last,c) ->
- match c with
- | c when not (CoercGraph.is_composite c) ->
- debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
- None
- | c ->
+ (fun (metasenv,last,c) _ ->
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv last head ugraph in
debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
ugraph
in
debug_print (lazy (" has type: "^ pp tty));
- Some (coerc,tty,subst,metasenv,ugraph)
+
+ Some (unvariant coerc,tty,subst,metasenv,ugraph)
with
| Uncertain _ | RefineFailure _
| HExtlib.Localized (_,Uncertain _)
ugraph in
match
HExtlib.list_findopt
- (fun (he,hetype,subst,metasenv,ugraph) ->
+ (fun (he,hetype,subst,metasenv,ugraph) _ ->
(* {{{ *)debug_print (lazy ("Try fix: "^
CicMetaSubst.ppterm_in_context ~metasenv subst he context));
debug_print (lazy (" of type: "^
let newt,newhety,subst,metasenv,ugraph =
type_of_aux subst metasenv context c ugraph in
let newt, newty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph newt expty
+ avoid_double_coercion context subst metasenv ugraph newt
+ expty
in
let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv newhety expty ugraph in
- Some ((newt,newty), subst, metasenv, ugraph)
+ fo_unif_subst subst context metasenv newhety expty ugraph
+ in
+ let b, ugraph =
+ CicReduction.are_convertible
+ ~subst ~metasenv context infty expty ugraph
+ in
+ if b then
+ Some ((t,infty), subst, metasenv, ugraph)
+ else
+ let newt = unvariant newt in
+ Some ((newt,newty), subst, metasenv, ugraph)
with
| Uncertain _ -> uncertain := true; None
| RefineFailure _ -> None)
coerce_to_something_aux t infty expty subst metasenv context ugraph
with Uncertain _ | RefineFailure _ as exn ->
let f _ =
- lazy ("The term " ^
+ lazy ("(9) The term " ^
CicMetaSubst.ppterm_in_context metasenv subst t context ^
" has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
infty context ^ " but is here used with type " ^
(* eat prods ends here! *)
let t',ty,subst',metasenv',ugraph1 =
- type_of_aux [] metasenv context t ugraph
+ type_of_aux subst metasenv context t ugraph
in
let substituted_t = CicMetaSubst.apply_subst subst' t' in
let substituted_ty = CicMetaSubst.apply_subst subst' ty in
else
substituted_metasenv
in
- (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
+ (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1)
+;;
+
+let type_of metasenv subst context t ug =
+ type_of_aux' metasenv subst context t ug
+;;
+
+let type_of_aux'
+ ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug
+=
+ let t,ty,m,s,ug =
+ type_of_aux' ?clean_dummy_dependent_types ?localization_tbl
+ metasenv [] context t ug
+ in
+ t,ty,m,ug
;;
let undebrujin uri typesno tys t =
RefineFailure _
| Uncertain _ as exn ->
let msg =
- lazy ("The term " ^
+ lazy ("(1) The term " ^
CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
" has type " ^
CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
| Cic.Constant (name,None,ty,args,attrs) ->
- let ty',_,metasenv,ugraph =
+ let ty',sort,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph
in
- Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+ (match CicReduction.whd [] sort with
+ Cic.Sort _
+ | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+ | _ -> raise (RefineFailure (lazy "")))
| Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
assert (metasenv' = metasenv);
(* Here we do not check the metasenv for correctness *)
let ty',sort,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph in
begin
- match sort with
+ match CicReduction.whd ~delta:true [] sort with
Cic.Sort _
(* instead of raising Uncertain, let's hope that the meta will become
a sort *)
projects / helm.git / blobdiff