* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
-*
+ *
* HELM is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
let build_inversion uri obj =
(*uri e obj of InductiveDefinition *)
let module PET = ProofEngineTypes in
- let typeno = 0 in
- let name,nleft,arity,cons_list =
- match obj with
- Cic.InductiveDefinition (tys,_,nleft,_) ->
- let (name,_,arity,cons_list) = List.nth tys typeno in
- (*we suppose there is only one inductiveType, so typeno=0 identically *)
- (name,nleft,arity,cons_list)
- |_ -> assert false
+ 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.empty_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,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 =
+ PET.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,bo,ty, attrs =
+ match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
+ in
+ assert (metasenv = []);
+ Some
+ (inversor_uri,
+ Cic.Constant
+ (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
+ with
+ Inversion.EqualityNotDefinedYet -> 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
- (*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*) debug_print (lazy ("theorem prima di refine: " ^ (CicPp.ppterm
- theorem)));
- let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem
- CicUniv.empty_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 proof= (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem) 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 =
- PET.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,bo,ty =
- match proof1 with (_,metasenv,bo,ty) -> metasenv,bo,ty
- in
- assert (metasenv = []);
- Some
- (inversor_uri,
- Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
- with
- Inversion.EqualityNotDefinedYet -> None
+ match obj with
+ | Cic.InductiveDefinition (tys,_,nleft,_) ->
+ let counter = ref (List.length tys) in
+ List.fold_right
+ (fun (name,_,arity,cons_list) res ->
+ counter := !counter-1;
+ match build_one !counter name nleft arity cons_list with
+ | None -> res
+ | Some inv -> inv::res)
+ tys []
+ |_ -> assert false
+
;;
let init () = ();;
projects / helm.git / blobdiff