[(Cic.Rel 1)] uri typeno )
;;
+let build_one typeno inversor_uri indty_uri nleft arity cons_list selections =
+ (*check if there are right parameters, else return void*)
+ if List.length (list_of_prod arity) = (nleft + 1) then
+ None
+ else
+ try
+ let arity_l = cut_last (list_of_prod arity) in
+ let rightparam_tys = cut_first nleft arity_l in
+ let theorem = build_theorem rightparam_tys arity_l arity cons_list
+ [](*created_vars*) [](*created_vars_ty*) nleft indty_uri typeno in
+ debug_print
+ (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
+ let (ref_theorem,_,metasenv,_) =
+ CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in
+ (*DEBUG*) debug_print
+ (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
+ let goal = CicMkImplicit.new_meta metasenv [] in
+ let metasenv' = (goal,[],ref_theorem)::metasenv in
+ let attrs = [`Class (`InversionPrinciple); `Generated] in
+ let _subst = [] in
+ let proof=
+ Some inversor_uri,metasenv',_subst,
+ lazy (Cic.Meta(goal,[])),ref_theorem, attrs in
+ let _,applies =
+ List.fold_right
+ (fun _ (i,applies) ->
+ i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies
+ ) cons_list (2,[]) in
+ let proof1,gl1 =
+ ProofEngineTypes.apply_tactic
+ (Tacticals.then_
+ ~start:(PrimitiveTactics.intros_tac ())
+ (*if the number of applies is 1, we cannot use
+ thens, but then_*)
+ ~continuation:
+ (match List.length applies with
+ 0 -> Inversion.private_inversion_tac (Cic.Rel 1) selections
+ | 1 ->
+ Tacticals.then_
+ ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections)
+ ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
+ | _ ->
+ Tacticals.thens
+ ~start:(Inversion.private_inversion_tac (Cic.Rel 1) selections)
+ ~continuations:applies))
+ (proof,goal) in
+ let _,metasenv,_subst,bo,ty, attrs = proof1 in
+ assert (metasenv = []);
+ Some
+ (inversor_uri,
+ Cic.Constant
+ (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[]))
+ with
+ Inversion.EqualityNotDefinedYet ->
+ HLog.warn "No default equality, no inversion principle";
+ None
+ | CicRefine.RefineFailure ls ->
+ HLog.warn
+ ("CicRefine.RefineFailure during generation of inversion principle: " ^
+ Lazy.force ls) ;
+ None
+ | CicRefine.Uncertain ls ->
+ HLog.warn
+ ("CicRefine.Uncertain during generation of inversion principle: " ^
+ Lazy.force ls) ;
+ None
+ | CicRefine.AssertFailure ls ->
+ HLog.warn
+ ("CicRefine.AssertFailure during generation of inversion principle: " ^
+ Lazy.force ls) ;
+ None
+;;
+
+let build_inverter ~add_obj status u indty_uri params =
+ let indty_uri, indty_no, _ = UriManager.ind_uri_split indty_uri in
+ let indty_no = match indty_no with None -> raise (Invalid_argument "not an inductive type")| Some n -> n in
+ let indty, univ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph indty_uri
+ in
+ match indty with
+ | Cic.InductiveDefinition (tys,_,nleft,attrs) ->
+ let _,inductive,_,_ = List.hd tys in
+ if not inductive then raise (Invalid_argument "not an inductive type")
+ else
+ let name,_,arity,cons_list = List.nth tys (indty_no-1) in
+ (match build_one (indty_no-1) u indty_uri nleft arity cons_list params with
+ | None -> status,[]
+ | Some (uri, obj) ->
+ let status, added = add_obj uri obj status in
+ status, uri::added)
+ | _ -> assert false
+;;
+
let build_inversion ~add_obj ~add_coercion uri obj =
match obj with
| Cic.InductiveDefinition (tys,_,nleft,attrs) ->
let _,inductive,_,_ = List.hd tys in
if not inductive then []
else
- let build_one typeno name nleft arity cons_list =
- (*check if there are right parameters, else return void*)
- if List.length (list_of_prod arity) = (nleft + 1) then
- None
- else
- try
- let arity_l = cut_last (list_of_prod arity) in
- let rightparam_tys = cut_first nleft arity_l in
- let theorem = build_theorem rightparam_tys arity_l arity cons_list
- [](*created_vars*) [](*created_vars_ty*) nleft uri typeno in
- debug_print
- (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
- let (ref_theorem,_,metasenv,_) =
- CicRefine.type_of_aux' [] [] theorem CicUniv.oblivion_ugraph in
- (*DEBUG*) debug_print
- (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
- let buri = UriManager.buri_of_uri uri in
- let inversor_uri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
- let goal = CicMkImplicit.new_meta metasenv [] in
- let metasenv' = (goal,[],ref_theorem)::metasenv in
- let attrs = [`Class (`InversionPrinciple); `Generated] in
- let _subst = [] in
- let proof=
- Some inversor_uri,metasenv',_subst,
- lazy (Cic.Meta(goal,[])),ref_theorem, attrs in
- let _,applies =
- List.fold_right
- (fun _ (i,applies) ->
- i+1,PrimitiveTactics.apply_tac (Cic.Rel i)::applies
- ) cons_list (2,[]) in
- let proof1,gl1 =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(PrimitiveTactics.intros_tac ())
- (*if the number of applies is 1, we cannot use
- thens, but then_*)
- ~continuation:
- (match List.length applies with
- 0 -> Inversion.private_inversion_tac (Cic.Rel 1)
- | 1 ->
- Tacticals.then_
- ~start:(Inversion.private_inversion_tac (Cic.Rel 1))
- ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
- | _ ->
- Tacticals.thens
- ~start:(Inversion.private_inversion_tac (Cic.Rel 1))
- ~continuations:applies))
- (proof,goal) in
- let _,metasenv,_subst,bo,ty, attrs = proof1 in
- assert (metasenv = []);
- Some
- (inversor_uri,
- Cic.Constant
- (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[]))
- with
- Inversion.EqualityNotDefinedYet ->
- HLog.warn "No default equality, no inversion principle";
- None
- | CicRefine.RefineFailure ls ->
- HLog.warn
- ("CicRefine.RefineFailure during generation of inversion principle: " ^
- Lazy.force ls) ;
- None
- | CicRefine.Uncertain ls ->
- HLog.warn
- ("CicRefine.Uncertain during generation of inversion principle: " ^
- Lazy.force ls) ;
- None
- | CicRefine.AssertFailure ls ->
- HLog.warn
- ("CicRefine.AssertFailure during generation of inversion principle: " ^
- Lazy.force ls) ;
- None
- in
let counter = ref (List.length tys) in
let all_inverters =
List.fold_right
(fun (name,_,arity,cons_list) res ->
+ let arity_l = cut_last (list_of_prod arity) in
+ let rightparam_tys = cut_first nleft arity_l in
+ let params = HExtlib.mk_list true (List.length rightparam_tys) in
+ let buri = UriManager.buri_of_uri uri in
+ let inversor_uri =
+ UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
counter := !counter-1;
- match build_one !counter name nleft arity cons_list with
+ match build_one !counter inversor_uri uri nleft arity cons_list params with
None -> res
| Some inv -> inv::res
) tys []
| _ -> []
;;
-
let init () =
LibrarySync.add_object_declaration_hook build_inversion;;
projects / helm.git / blobdiff