| _ -> 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 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
=
and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
let module C = Cic in
- (* let module R = CicMetaSubst in *)
let module R = CicReduction in
match R.whd ~subst context expectedtype with
C.MutInd (_,_,_) ->
| C.Appl (C.MutInd (_,_,_)::tl) ->
let (_,arguments) = split tl left_args_no in
(n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
- | C.Prod (name,so,de) ->
+ | C.Prod (_,so,de) ->
(* we expect that the actual type of the branch has the due
number of Prod *)
(match R.whd ~subst context actualtype with
(* we should also check that the name variable is anonymous in
the actual type de' ?? *)
check_branch (n+1)
- ((Some (name,(C.Decl so)))::context)
+ ((Some (name',(C.Decl so)))::context)
metasenv subst left_args_no de' term' de ugraph1
| _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
| _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
-and type_of_aux' ?(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
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 te',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv' context te ugraph1
in
+ let rec count_prods context ty =
+ match CicReduction.whd context ~subst:subst'' ty with
+ | Cic.Prod (n,s,t) ->
+ 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+ in
+ let exp_prods = count_prods context ty' in
+ let inf_prods = count_prods context inferredty in
+ let te', inferredty, metasenv'', subst'', ugraph2 =
+ let rec aux t m s ug it = function
+ | 0 -> t,it,m,s,ug
+ | n ->
+ 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
+ in
+ let s,m,ug =
+ fo_unif_subst s context m metaty src ug
+ in
+ let t =
+ match t with
+ | Cic.Appl l -> Cic.Appl (l @ [newmeta])
+ | _ -> Cic.Appl [t;newmeta]
+ in
+ aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1)
+ | _ -> t,it,m,s,ug
+ in
+ aux te' metasenv'' subst'' ugraph2 inferredty
+ (max 0 (inf_prods - exp_prods))
+ in
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
context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
+ CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
+ context))
in
let rec instantiate_prod t =
function
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
context)) exn
in
(p'::pl,j-1,
- outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+ outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
pl ([],List.length pl,[],subst,metasenv,ugraph3)
in
in
C.Appl (outtype'::args)
in
- CicReduction.whd ~subst context appl
+ CicReduction.head_beta_reduce ~delta:false
+ ~upto:(List.length args) appl
in
try
fo_unif_subst subst context metasenv instance instance'
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'
context ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst instance
context)))
- (subst,metasenv,ugraph5) pl' outtypeinstances
+ (subst,metasenv,ugraph5) pl' outtypeinstances
in
C.MutCase (uri, i, outtype, term', pl'),
CicReduction.head_beta_reduce
(CicMetaSubst.apply_subst subst
- (C.Appl(outtype::right_args@[term]))),
+ (C.Appl(outtype::right_args@[term']))),
subst,metasenv,ugraph6)
| C.Fix (i,fl) ->
let fl_ty',subst,metasenv,types,ugraph1,len =
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
context' ^ " but is here used with type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context))
+ context'))
in
fl @ [bo'] , subst',metasenv',ugraph'
) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
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
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_ge 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
| 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));
(* 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
- match CoercGraph.look_for_coercion' metasenv subst context src tgt with
+ (* instead of a dummy functional type we may create the real product
+ * using args_bo_and_ty, but since coercions lookup ignores the
+ * actual ariety we opt for the simple solution *)
+ let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
+ match CoercGraph.look_for_coercion metasenv subst context hetype fty with
| CoercGraph.NoCoercion -> []
- | CoercGraph.NotMetaClosed
- | CoercGraph.NotHandled _ ->
+ | CoercGraph.NotHandled ->
raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
| CoercGraph.SomeCoercionToTgt candidates
| CoercGraph.SomeCoercion candidates ->
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 _)
"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 error = ref None in
let possible_fixes =
fix_arity (List.length args) metasenv context subst he hetype
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: "^
with
| RefineFailure _ | Uncertain _
| HExtlib.Localized (_,RefineFailure _)
- | HExtlib.Localized (_,Uncertain _) -> None)
+ | HExtlib.Localized (_,Uncertain _) as exn ->
+ error := Some exn; None)
possible_fixes
with
| Some x -> x
| None ->
- raise
- (MoreArgsThanExpected
- (List.length args, RefineFailure (lazy "")))
+ match !error with
+ None ->
+ raise
+ (MoreArgsThanExpected
+ (List.length args, RefineFailure (lazy "")))
+ | Some exn -> raise exn
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 =
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) ^
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)
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)
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
(* substituted_t,substituted_ty,substituted_metasenv *)
(* ANDREA: spostare tutta questa robaccia da un altra parte *)
let cleaned_t =
- FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+ if clean_dummy_dependent_types then
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_t
+ else substituted_t in
let cleaned_ty =
- FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+ if clean_dummy_dependent_types then
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
+ else substituted_ty in
let cleaned_metasenv =
+ if clean_dummy_dependent_types then
List.map
(function (n,context,ty) ->
let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
in
(n,context',ty')
) substituted_metasenv
+ else
+ substituted_metasenv
+ in
+ (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
- (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
+ 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 *)
List.fold_right
(fun (name,b,ty,cl) (metasenv,ugraph,res) ->
let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph
+ (* clean_dummy_dependent_types: false to avoid cleaning the names
+ of the left products, that must be identical to those of the
+ constructors; however, non-left products should probably be
+ cleaned *)
+ type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
+ metasenv [] ty ugraph
in
metasenv,ugraph,(name,b,ty',cl)::res
) tys (metasenv,ugraph,[]) in
projects / helm.git / blobdiff