;;
let rec type_of_constant uri ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u= CicEnvironment.get_obj ugraph uri in
- match obj with
- C.Constant (_,_,ty,_,_) -> ty,u
- | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.Constant (_,_,ty,_,_) -> ty,u
+ | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
+ | _ ->
+ raise
+ (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
and type_of_variable uri ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u = CicEnvironment.get_obj ugraph uri in
- match obj with
- C.Variable (_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure
- ("Unknown variable definition " ^ UriManager.string_of_uri uri))
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.Variable (_,_,ty,_,_) -> ty,u
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown variable definition " ^ UriManager.string_of_uri uri))
and type_of_mutual_inductive_defs uri i ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u = CicEnvironment.get_obj ugraph uri in
- match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,arity,_) = List.nth dl i in
- arity,u
- | _ ->
- raise
- (RefineFailure
- ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
+ match obj with
+ C.InductiveDefinition (dl,_,_,_) ->
+ let (_,_,arity,_) = List.nth dl i in
+ arity,u
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
and type_of_mutual_inductive_constr uri i j ugraph =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj uri
- with Not_found -> assert false
- in
- *)
- let obj,u = CicEnvironment.get_obj ugraph uri in
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u =
+ try
+ CicEnvironment.get_cooked_obj ugraph uri
+ with Not_found -> assert false
+ in
match obj with
C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cl) = List.nth dl i in
| Some (_,C.Def (_,Some ty)) ->
t,S.lift n ty,subst,metasenv, ugraph
| Some (_,C.Def (bo,None)) ->
- type_of_aux subst metasenv context (S.lift n bo) ugraph
+ 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 -> raise (RefineFailure "Rel to hidden hypothesis")
with
_ -> raise (RefineFailure "Not a close term")
* Moreover the inferred type is closer to the expected one.
*)
C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
- subst',metasenv',ugraph2
+ subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
let he',hetype,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context he ugraph
(* first, get the inductive type (and noparams)
* in the environment *)
let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
- let obj,u = CicEnvironment.get_obj ugraph uri in
+ let _ = CicTypeChecker.typecheck uri in
+ let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
match obj with
C.InductiveDefinition (l,expl_params,parsno,_) ->
List.nth l i , expl_params, parsno, u
(let candidate,ugraph5,metasenv,subst =
let exp_name_subst, metasenv =
let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
in
let uris = CicUtil.params_of_obj o in
List.fold_right (
(Some candidate),ugraph4,metasenv,subst
| (constructor_args_no,_,instance,_)::tl ->
try
- let instance' =
- CicMetaSubst.delift_rels constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
let candidate,ugraph,metasenv,subst =
List.fold_left (
| None -> None,ugraph,metasenv,subst
| Some ty ->
try
- let instance' =
- CicMetaSubst.delift_rels
- constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv
candidate outtype ugraph5
in
C.MutCase (uri, i, outtype, term', pl'),
- (Cic.Appl (outtype::right_args@[term'])),
+ CicReduction.head_beta_reduce
+ (CicMetaSubst.apply_subst subst
+ (Cic.Appl (outtype::right_args@[term']))),
subst,metasenv,ugraph)
| _ -> (* easy case *)
let _,_, subst, metasenv,ugraph5 =
(subst,metasenv,ugraph5) outtypeinstances
in
C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.whd ~subst context
- (C.Appl(outtype::right_args@[term])),
+ CicReduction.head_beta_reduce
+ (CicMetaSubst.apply_subst subst
+ (C.Appl(outtype::right_args@[term]))),
subst,metasenv,ugraph6)
| C.Fix (i,fl) ->
let fl_ty',subst,metasenv,types,ugraph1 =
type_of_aux' metasenv context term ugraph
with
CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+
+(*CSC: this is a very very rough approximation; to be finished *)
+let are_all_occurrences_positive uri =
+ let rec aux =
+ (*CSC: here we should do a whd; but can we do that? *)
+ function
+ Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> ()
+ | Cic.MutInd (uri',_,_) when uri = uri' -> ()
+ | Cic.Prod (_,_,t) -> aux t
+ | _ -> raise (RefineFailure "not well formed constructor type")
+ in
+ aux
+let typecheck metasenv uri obj =
+ let ugraph = CicUniv.empty_ugraph in
+ match obj with
+ Cic.Constant (name,Some bo,ty,args,attrs) ->
+ let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
+ let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph 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
+ Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
+ | Cic.Constant (name,None,ty,args,attrs) ->
+ let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
+ | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
+ assert (metasenv' = metasenv);
+ (* Here we do not check the metasenv for correctness *)
+ let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
+ let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ begin
+ match sort with
+ Cic.Sort _
+ (* instead of raising Uncertain, let's hope that the meta will become
+ a sort *)
+ | Cic.Meta _ -> ()
+ | _ -> raise (RefineFailure "The term provided is not a type")
+ end;
+ let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph 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
+ Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
+ | Cic.Variable _ -> assert false (* not implemented *)
+ | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
+ (*CSC: this code is greately simplified and many many checks are missing *)
+ (*CSC: e.g. the constructors are not required to build their own types, *)
+ (*CSC: the arities are not required to have as type a sort, etc. *)
+ let uri = match uri with Some uri -> uri | None -> assert false in
+ let typesno = List.length tys in
+ (* first phase: we fix only the types *)
+ let metasenv,ugraph,tys =
+ List.fold_right
+ (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+ let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ metasenv,ugraph,(name,b,ty',cl)::res
+ ) tys (metasenv,ugraph,[]) in
+ let con_context =
+ List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
+ (* second phase: we fix only the constructors *)
+ let metasenv,ugraph,tys =
+ List.fold_right
+ (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
+ let metasenv,ugraph,cl' =
+ List.fold_right
+ (fun (name,ty) (metasenv,ugraph,res) ->
+ let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+ let ty',_,metasenv,ugraph =
+ type_of_aux' metasenv con_context ty ugraph in
+ let undebrujin t =
+ snd
+ (List.fold_right
+ (fun (name,_,_,_) (i,t) ->
+ (* here the explicit_named_substituion is assumed to be *)
+ (* of length 0 *)
+ let t' = Cic.MutInd (uri,i,[]) in
+ let t = CicSubstitution.subst t' t in
+ i - 1,t
+ ) tys (typesno - 1,t)) in
+ let ty' = undebrujin ty' in
+ metasenv,ugraph,(name,ty')::res
+ ) cl (metasenv,ugraph,[])
+ in
+ metasenv,ugraph,(name,b,ty,cl')::res
+ ) tys (metasenv,ugraph,[]) in
+ (* third phase: we check the positivity condition *)
+ List.iter
+ (fun (_,_,_,cl) ->
+ List.iter (fun (_,ty) -> are_all_occurrences_positive uri ty) cl
+ ) tys ;
+ Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
projects / helm.git / blobdiff