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
+and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
ugraph
=
let rec type_of_aux subst metasenv context t ugraph =
match List.nth context (n - 1) with
Some (_,C.Decl ty) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,Some ty)) ->
+ | Some (_,C.Def (_,ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (bo,None)) ->
- let ty,ugraph =
- (* if it is in the context it must be already well-typed*)
- CicTypeChecker.type_of_aux' ~subst metasenv context
- (S.lift n bo) ugraph
- in
- t,ty,subst,metasenv,ugraph
| None ->
enrich localization_tbl t
(RefineFailure (lazy "Rel to hidden hypothesis"))
in
C.Lambda (n,s',t'),C.Prod (n,s',type2),
subst'',metasenv'',ugraph2
- | C.LetIn (n,s,t) ->
- (* only to check if s is well-typed *)
- let s',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
+ | C.LetIn (n,s,ty,t) ->
+ (* only to check if s is well-typed *)
+ let s',ty',subst',metasenv',ugraph1 =
+ type_of_aux subst metasenv context s ugraph in
+ let ty,_,subst',metasenv',ugraph1 =
+ type_of_aux subst' metasenv' context ty ugraph1 in
+ let subst',metasenv',ugraph1 =
+ try
+ fo_unif_subst subst' context metasenv'
+ ty ty' ugraph1
+ with
+ exn ->
+ enrich localization_tbl s' exn
+ ~f:(function _ ->
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
+ context ^ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
+ context ^ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
+ context))
+ in
+ let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
let t',inferredty,subst'',metasenv'',ugraph2 =
type_of_aux subst' metasenv'
* Even faster than the previous solution.
* Moreover the inferred type is closer to the expected one.
*)
- C.LetIn (n,s',t'),
+ C.LetIn (n,s',ty,t'),
CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
exn ->
enrich localization_tbl term' exn
~f:(function _ ->
- lazy ("(10)The term " ^
+ lazy ("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 ("(11)The term " ^
+ lazy ("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
(let candidate,ugraph5,metasenv,subst =
let exp_name_subst, metasenv =
let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
in
let uris = CicUtil.params_of_obj o in
List.fold_right (
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 ("(12)The term " ^
+ lazy ("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 ("(13)The term " ^
+ lazy ("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 ("(14)The term " ^
+ lazy ("The term " ^
CicMetaSubst.ppterm_in_context ~metasenv subst bo
context' ^ " has type " ^
CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
[] -> []
| (Some (n,C.Decl t))::tl ->
(Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,
- C.Def ((S.subst_meta l (S.lift i t)),
- Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ | (Some (n,C.Def (t,ty)))::tl ->
+ (Some
+ (n,
+ C.Def
+ (S.subst_meta l (S.lift i t),
+ S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
_,None ->
l @ [None],subst,metasenv,ugraph
| Some t,Some (_,C.Def (ct,_)) ->
+ (*CSC: the following optimization is to avoid a possibly
+ expensive reduction that can be easily avoided and
+ that is quite frequent. However, this is better
+ handled using levels to control reduction *)
+ let optimized_t =
+ match t with
+ Cic.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ Some (_,C.Def (te,_)) -> S.lift n te
+ | _ -> t
+ with
+ Failure _ -> t)
+ | _ -> t
+ in
let subst',metasenv',ugraph' =
(try
(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
* il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
- fo_unif_subst subst context metasenv t ct ugraph
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
+ fo_unif_subst subst context metasenv optimized_t ct ugraph
+ with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
in
l @ [Some t],subst',metasenv',ugraph'
| Some t,Some (_,C.Decl ct) ->
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
(fun (metasenv,last,coerc) ->
let pp t =
CicMetaSubst.ppterm_in_context ~metasenv subst t context in
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last he ugraph in
- debug_print (lazy ("New head: "^ pp coerc));
try
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last he ugraph in
+ debug_print (lazy ("New head: "^ pp coerc));
let tty,ugraph =
- CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
- debug_print (lazy (" has type: "^ pp tty));
- Some (coerc,tty,subst,metasenv,ugraph)
+ CicTypeChecker.type_of_aux' ~subst metasenv context coerc
+ ugraph
+ in
+ debug_print (lazy (" has type: "^ pp tty));
+ Some (coerc,tty,subst,metasenv,ugraph)
with
| Uncertain _ | RefineFailure _
| HExtlib.Localized (_,Uncertain _)
fo_unif_subst subst context metasenv infty expty ugraph
in
(t, expty), subst, metasenv, ugraph
- with Uncertain _ | RefineFailure _ as exn ->
- if not allow_coercions || not !insert_coercions then
- enrich localization_tbl t exn
- else
+ with (Uncertain _ | RefineFailure _ as exn)
+ when allow_coercions && !insert_coercions ->
let whd = CicReduction.whd ~delta:false in
let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
let infty = clean infty subst context 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
Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
| Some (n, Cic.Def (bo,ty)) ->
let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' =
- match ty with
- None -> None
- | Some ty ->
- Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
in
Some (n, Cic.Def (bo',ty'))
) context
in
(n,context',ty')
) substituted_metasenv
+ else
+ substituted_metasenv
in
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
metasenv,ugraph,substituted_tys
let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
match obj with
Cic.Constant (name,Some bo,ty,args,attrs) ->
+ (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
+ since type_of_aux' destroys localization information (which are
+ preserved by type_of_aux *)
+ let loc exn' =
+ try
+ Cic.CicHash.find localization_tbl bo
+ with Not_found ->
+ HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
+ raise exn' in
let bo',boty,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] bo ugraph in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+ let subst,metasenv,ugraph =
+ try
+ fo_unif_subst [] [] metasenv boty ty' ugraph
+ with
+ RefineFailure _
+ | Uncertain _ as exn ->
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
+ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
+ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
+ in
+ let exn' =
+ match exn with
+ RefineFailure _ -> RefineFailure msg
+ | Uncertain _ -> Uncertain msg
+ | _ -> assert false
+ in
+ raise (HExtlib.Localized (loc exn',exn'))
+ in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
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
(fun (name,ty) (metasenv,ugraph,res) ->
let ty =
CicTypeChecker.debrujin_constructor
- ~cb:(relocalize localization_tbl) uri typesno ty in
+ ~cb:(relocalize localization_tbl) uri typesno [] ty in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
| C.Lambda (name,so,dest) ->
let ctx' = (Some (name,C.Decl so))::ctx in
C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.LetIn (name,so,dest) ->
- let _,ty,metasenv,ugraph =
- pack_coercions := false;
- type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in
- pack_coercions := true;
- let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
- C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
+ | C.LetIn (name,so,ty,dest) ->
+ let ctx' = Some (name,(C.Def (so,ty)))::ctx in
+ C.LetIn
+ (name, merge_coercions ctx so, merge_coercions ctx ty,
+ merge_coercions ctx' dest)
| C.Appl l ->
let l = List.map (merge_coercions ctx) l in
let t = C.Appl l in
projects / helm.git / blobdiff