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
| t -> C.Appl [t ; C.Rel 1]) in
(* 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) metasenv subst left_args_no de' term' de ugraph1
+ check_branch (n+1)
+ ((Some (name,(C.Decl so)))::context)
+ metasenv subst left_args_no de' term' de ugraph1
| _ -> raise (AssertFailure "Wrong number of arguments"))
| _ -> raise (AssertFailure "Prod or MutInd expected")
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
(* first, get the inductive type (and noparams)
* in the environment *)
let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
- (*
- let obj =
- try
- CicEnvironment.get_cooked_obj ~trust:true uri
- with Not_found -> assert false
- in
- *)
let obj,u = CicEnvironment.get_obj ugraph uri in
match obj with
C.InductiveDefinition (l,expl_params,parsno,_) ->
(RefineFailure
("Unkown mutual inductive definition " ^
U.string_of_uri uri))
- in
- let rec count_prod t =
- match CicReduction.whd ~subst context t with
- C.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0
- in
- let no_args = count_prod arity in
- (* now, create a "generic" MutInd *)
- let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
- in
- let metasenv,right_args =
- let no_right_params = no_args - no_left_params in
- if no_right_params < 0 then assert false
- else CicMkImplicit.n_fresh_metas
- metasenv subst context no_right_params
- in
- let metasenv,exp_named_subst =
- CicMkImplicit.fresh_subst metasenv subst context expl_params in
- let expected_type =
- if no_args = 0 then
- C.MutInd (uri,i,exp_named_subst)
- else
- C.Appl
- (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
- in
- (* check consistency with the actual type of term *)
- let term',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context term ugraph in
- let expected_type',_, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context expected_type ugraph1
- in
- let actual_type = CicReduction.whd ~subst context actual_type in
- let subst,metasenv,ugraph3 =
- fo_unif_subst subst context metasenv
- expected_type' actual_type ugraph2
- in
- (* TODO: check if the sort elimination
- * is allowed: [(I q1 ... qr)|B] *)
- let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
- List.fold_left
- (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
- let constructor =
- if left_args = [] then
- (C.MutConstruct (uri,i,j,exp_named_subst))
- else
- (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
- in
- let p',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context p ugraph
- in
- let constructor',expected_type, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context constructor ugraph1
- in
- let outtypeinstance,subst,metasenv,ugraph3 =
- check_branch 0 context metasenv subst no_left_params
- actual_type constructor expected_type ugraph2
- in
- (pl @ [p'],j+1,
- outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- ([],1,[],subst,metasenv,ugraph3) pl
- in
- (* we are left to check that the outype matches his instances.
- The easy case is when the outype is specified, that amount
- to a trivial check. Otherwise, we should guess a type from
- its instances *)
-
- (* easy case *)
- let _,_, subst, metasenv,ugraph5 =
- type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
- in
- let (subst,metasenv,ugraph6) =
- List.fold_left
- (fun (subst,metasenv,ugraph) (constructor_args_no,context,instance,args) ->
- let instance' =
- let appl =
- let outtype' =
- CicSubstitution.lift constructor_args_no outtype
- in
- C.Appl (outtype'::args)
+ in
+ let rec count_prod t =
+ match CicReduction.whd ~subst context t with
+ C.Prod (_, _, t) -> 1 + (count_prod t)
+ | _ -> 0
+ in
+ let no_args = count_prod arity in
+ (* now, create a "generic" MutInd *)
+ let metasenv,left_args =
+ CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
+ in
+ let metasenv,right_args =
+ let no_right_params = no_args - no_left_params in
+ if no_right_params < 0 then assert false
+ else CicMkImplicit.n_fresh_metas
+ metasenv subst context no_right_params
+ in
+ let metasenv,exp_named_subst =
+ CicMkImplicit.fresh_subst metasenv subst context expl_params in
+ let expected_type =
+ if no_args = 0 then
+ C.MutInd (uri,i,exp_named_subst)
+ else
+ C.Appl
+ (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
+ in
+ (* check consistency with the actual type of term *)
+ let term',actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context term ugraph in
+ let expected_type',_, subst, metasenv,ugraph2 =
+ type_of_aux subst metasenv context expected_type ugraph1
+ in
+ let actual_type = CicReduction.whd ~subst context actual_type in
+ let subst,metasenv,ugraph3 =
+ 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) =
+ List.fold_left
+ (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+ let constructor =
+ if left_args = [] then
+ (C.MutConstruct (uri,i,j,exp_named_subst))
+ else
+ (C.Appl
+ (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
+ in
+ let p',actual_type,subst,metasenv,ugraph1 =
+ type_of_aux subst metasenv context p ugraph
+ in
+ let constructor',expected_type, subst, metasenv,ugraph2 =
+ type_of_aux subst metasenv context constructor ugraph1
+ in
+ let outtypeinstance,subst,metasenv,ugraph3 =
+ check_branch 0 context metasenv subst no_left_params
+ actual_type constructor' expected_type ugraph2
+ in
+ (pl @ [p'],j+1,
+ outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
+ ([],1,[],subst,metasenv,ugraph3) pl
+ in
+
+ (* we are left to check that the outype matches his instances.
+ The easy case is when the outype is specified, that amount
+ to a trivial check. Otherwise, we should guess a type from
+ its instances
+ *)
+
+ (match outtype with
+ | C.Meta (n,l) ->
+ (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
+ | [] ->
+ 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
- (*
- (* if appl is not well typed then the type_of below solves the
- * problem *)
- let (_, subst, metasenv,ugraph1) =
- type_of_aux subst metasenv context appl ugraph
- in
- *)
- (* DEBUG
- let prova1 = CicMetaSubst.whd subst context appl in
- let prova2 = CicReduction.whd ~subst context appl in
- if not (prova1 = prova2) then
- begin
- prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
- prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
- end;
- *)
- (* CicMetaSubst.whd subst context appl *)
- CicReduction.whd ~subst context appl
- in
- fo_unif_subst subst context metasenv
- instance instance' ugraph)
- (subst,metasenv,ugraph5) outtypeinstances
- in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.whd ~subst context
- (C.Appl(outtype::right_args@[term])),
- subst,metasenv,ugraph6
+ 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',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
+ in
+ let candidate,ugraph,metasenv,subst =
+ List.fold_left (
+ fun (candidate_oty,ugraph,metasenv,subst)
+ (constructor_args_no,_,instance,_) ->
+ match candidate_oty with
+ | None -> None,ugraph,metasenv,subst
+ | Some ty ->
+ try
+ let instance',subst,metasenv =
+ CicMetaSubst.delift_rels subst metasenv
+ constructor_args_no instance
+ in
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv
+ instance' ty ugraph
+ in
+ 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 ->
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv
+ candidate outtype ugraph5
+ in
+ 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
+ (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
+ in
+ let (subst,metasenv,ugraph6) =
+ List.fold_left
+ (fun (subst,metasenv,ugraph)
+ (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+ CicReduction.whd ~subst context appl
+ in
+ fo_unif_subst subst context metasenv
+ instance instance' ugraph)
+ (subst,metasenv,ugraph5) outtypeinstances
+ in
+ C.MutCase (uri, i, outtype, term', pl'),
+ 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 =
List.fold_left
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)
+
+
(* DEBUGGING ONLY
let type_of_aux' metasenv context term =
try
projects / helm.git / blobdiff