exception Uncertain of string;;
exception AssertFailure of string;;
-let debug_print = prerr_endline
+let debug_print = fun _ -> ()
let fo_unif_subst subst context metasenv t1 t2 ugraph =
try
| (_,_) -> raise (AssertFailure "split: list too short")
;;
-let look_for_coercion src tgt =
- if (src = (CicUtil.term_of_uri "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)")) &&
- (tgt = (CicUtil.term_of_uri "cic:/Coq/Reals/Rdefinitions/R.con"))
- then
- begin
- prerr_endline "TROVATA coercion";
- Some (CicUtil.term_of_uri "cic:/Coq/Reals/Raxioms/INR.con")
- end
- else
- begin
- prerr_endline (sprintf "NON TROVATA la coercion %s %s" (CicPp.ppterm src)
- (CicPp.ppterm tgt));
- None
- end
-;;
-
-
let rec type_of_constant uri ugraph =
let module C = Cic in
let module R = CicReduction in
canonical_context l ugraph
in
(* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv', ugraph1
(* type_of_aux subst metasenv
- context (CicSubstitution.lift_meta l term) *)
+ context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let l',subst',metasenv', ugraph1 =
check_metasenv_consistency n subst metasenv context
canonical_context l ugraph
in
- C.Meta (n,l'),CicSubstitution.lift_meta l' ty,
+ C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
subst', metasenv',ugraph1)
| C.Sort (C.Type tno) ->
let tno' = CicUniv.fresh() in
(try
let subst''',metasenv''',ugraph3 =
fo_unif_subst subst'' context metasenv''
- inferredty ty' ugraph2
+ inferredty ty ugraph2
in
C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
with
* 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
fo_unif_subst subst context metasenv
expected_type' actual_type ugraph2
in
+ let rec instantiate_prod t =
+ function
+ [] -> t
+ | he::tl ->
+ match CicReduction.whd ~subst context t with
+ C.Prod (_,_,t') ->
+ instantiate_prod (CicSubstitution.subst he t') tl
+ | _ -> assert false
+ in
+ let arity_instantiated_with_left_args =
+ instantiate_prod arity left_args in
(* TODO: check if the sort elimination
* is allowed: [(I q1 ... qr)|B] *)
let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
(match outtype with
| C.Meta (n,l) ->
- (let candidate,ugraph5 =
+ (let candidate,ugraph5,metasenv,subst =
+ let exp_name_subst, metasenv =
+ let o,_ =
+ CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ in
+ let uris = CicUtil.params_of_obj o in
+ List.fold_right (
+ fun uri (acc,metasenv) ->
+ let metasenv',new_meta =
+ CicMkImplicit.mk_implicit metasenv subst context
+ in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable
+ context
+ in
+ (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
+ ) uris ([],metasenv)
+ in
+ let ty =
+ match left_args,right_args with
+ [],[] -> Cic.MutInd(uri, i, exp_name_subst)
+ | _,_ ->
+ let rec mk_right_args =
+ function
+ 0 -> []
+ | n -> (Cic.Rel n)::(mk_right_args (n - 1))
+ in
+ let right_args_no = List.length right_args in
+ let lifted_left_args =
+ List.map (CicSubstitution.lift right_args_no) left_args
+ in
+ Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
+ (lifted_left_args @ mk_right_args right_args_no))
+ in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name ~subst metasenv
+ context Cic.Anonymous ~typ:ty
+ in
match outtypeinstances with
- | [] -> raise (Uncertain "Inference of annotation for empty inductive types not implemented")
+ | [] ->
+ let extended_context =
+ let rec add_right_args =
+ function
+ Cic.Prod (name,ty,t) ->
+ Some (name,Cic.Decl ty)::(add_right_args t)
+ | _ -> []
+ in
+ (Some (fresh_name,Cic.Decl ty))::
+ (List.rev
+ (add_right_args arity_instantiated_with_left_args))@
+ context
+ in
+ let metasenv,new_meta =
+ CicMkImplicit.mk_implicit metasenv subst extended_context
+ in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable
+ extended_context
+ in
+ let rec add_lambdas b =
+ function
+ Cic.Prod (name,ty,t) ->
+ Cic.Lambda (name,ty,(add_lambdas b t))
+ | _ -> Cic.Lambda (fresh_name, ty, b)
+ in
+ let candidate =
+ add_lambdas (Cic.Meta (new_meta,irl))
+ arity_instantiated_with_left_args
+ in
+ (Some candidate),ugraph4,metasenv,subst
| (constructor_args_no,_,instance,_)::tl ->
try
- let instance' =
- CicSubstitution.delift 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 (
- fun (candidate_oty,ugraph)
+ fun (candidate_oty,ugraph,metasenv,subst)
(constructor_args_no,_,instance,_) ->
match candidate_oty with
- | None -> None,ugraph
+ | None -> None,ugraph,metasenv,subst
| Some ty ->
try
- let instance' =
- CicSubstitution.delift
- constructor_args_no
- (CicMetaSubst.apply_subst subst instance)
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
in
- let b,ugraph1 =
- CicReduction.are_convertible context
- instance' ty ugraph
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv
+ instance' ty ugraph
in
- if b then
- candidate_oty,ugraph1
- else
- None,ugraph
- with Failure s -> None,ugraph
- ) (Some instance',ugraph4) tl
- with Failure s ->
- None,ugraph4
+ candidate_oty,ugraph,metasenv,subst
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ None,ugraph,metasenv,subst
+ ) (Some instance',ugraph4,metasenv,subst) tl
+ in
+ match candidate with
+ | None -> None, ugraph,metasenv,subst
+ | Some t ->
+ let rec add_lambdas n b =
+ function
+ Cic.Prod (name,ty,t) ->
+ Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
+ | _ ->
+ Cic.Lambda (fresh_name, ty,
+ CicSubstitution.lift (n + 1) t)
+ in
+ Some
+ (add_lambdas 0 t arity_instantiated_with_left_args),
+ ugraph,metasenv,subst
+ with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ None,ugraph4,metasenv,subst
in
match candidate with
| None -> raise (Uncertain "can't solve an higher order unification problem")
| Some candidate ->
- prerr_endline ("CANDIDATE=" ^ (CicPp.ppterm candidate));
- let s,m,u =
+ let subst,metasenv,ugraph =
fo_unif_subst subst context metasenv
candidate outtype ugraph5
in
- C.MutCase (uri, i, outtype, term', pl'),candidate,s,m,u)
+ C.MutCase (uri, i, outtype, term', pl'),
+ CicReduction.head_beta_reduce
+ (CicMetaSubst.apply_subst subst
+ (Cic.Appl (outtype::right_args@[term']))),
+ subst,metasenv,ugraph)
| _ -> (* easy case *)
let _,_, subst, metasenv,ugraph5 =
type_of_aux subst metasenv context
(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 =
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) 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.lift_meta l (S.lift i t)),None)))::(aux (i+1) 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.lift_meta l (S.lift i t)),
- Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
+ C.Def ((S.subst_meta l (S.lift i t)),
+ Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
try
fo_unif_subst subst context metasenv hetype hetype' ugraph
with exn ->
- prerr_endline (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
+ debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
(CicPp.ppterm hetype)
(CicPp.ppterm hetype')
(CicMetaSubst.ppmetasenv metasenv [])
hete,subst,metasenv,ugraph1
with exn ->
(* we search a coercion from hety to s *)
- let coer = look_for_coercion
+ let coer = CoercGraph.look_for_coercion
(CicMetaSubst.apply_subst subst hety)
(CicMetaSubst.apply_subst subst s)
in
(cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
;;
+let type_of_aux' metasenv context term ugraph =
+ try
+ 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 =
try