;;
let compute_keys uri height kind =
- let mk_item orig_ty spec =
- let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in
- let keys =
- match ty with
- | NCic.Const (NReference.Ref (_,NReference.Def h))
- | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_)
- when h > 0 ->
- let ty',_,_=
- NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in
- [ty;ty']
- | _ -> [ty]
- in
- keys,NCic.Const(NReference.reference_of_spec uri spec)
- in
- let data =
- match kind with
- | NCic.Fixpoint (ind,ifl,_) ->
- HExtlib.list_mapi
- (fun (_,_,rno,ty,_) i ->
- if ind then mk_item ty (NReference.Fix (i,rno,height))
- else mk_item ty (NReference.CoFix height)) ifl
- | NCic.Inductive (b,lno,itl,_) ->
- HExtlib.list_mapi
- (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl
- @
- List.map
- (fun ((_,_,ty),i,j) ->
- mk_item ty (NReference.Con (i,j+1,lno)))
- (List.flatten
- (HExtlib.list_mapi
- (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
- itl))
- | NCic.Constant (_,_,Some _, ty, _) ->
- [ mk_item ty (NReference.Def height) ]
- | NCic.Constant (_,_,None, ty, _) ->
- [ mk_item ty NReference.Decl ]
- in
- let data = HExtlib.filter_map
- (fun (keys, t) ->
- let keys = List.filter
- (function
- | (NCic.Meta _)
- | (NCic.Appl (NCic.Meta _::_)) -> false
- | _ -> true)
- keys
- in
- if keys <> [] then
- begin
- HLog.debug ("Indexing:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
- HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
- Some (keys,t)
- end
- else
- begin
- HLog.debug ("Not indexing:" ^
- NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
- None
- end)
- data
- in data
+ let mk_item orig_ty spec =
+ let keys = NnAuto.keys_of_cic_term [] [] [] orig_ty in
+ keys,NCic.Const(NReference.reference_of_spec uri spec)
+ in
+ let data =
+ match kind with
+ | NCic.Fixpoint (ind,ifl,_) ->
+ HExtlib.list_mapi
+ (fun (_,_,rno,ty,_) i ->
+ if ind then mk_item ty (NReference.Fix (i,rno,height))
+ else mk_item ty (NReference.CoFix height)) ifl
+ | NCic.Inductive (b,lno,itl,_) ->
+ HExtlib.list_mapi
+ (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl
+ @
+ List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
+ (List.flatten (HExtlib.list_mapi
+ (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
+ itl))
+ | NCic.Constant (_,_,Some _, ty, _) ->
+ [ mk_item ty (NReference.Def height) ]
+ | NCic.Constant (_,_,None, ty, _) ->
+ [ mk_item ty NReference.Decl ]
+ in
+ HExtlib.filter_map
+ (fun (keys, t) ->
+ let keys = List.filter
+ (function
+ | (NCic.Meta _)
+ | (NCic.Appl (NCic.Meta _::_)) -> false
+ | _ -> true)
+ keys
+ in
+ if keys <> [] then
+ begin
+ HLog.debug ("Indexing:" ^
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
+ Some (keys,t)
+ end
+ else
+ begin
+ HLog.debug ("Not indexing:" ^
+ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
+ None
+ end)
+ data
;;
let index_obj_for_auto status (uri, height, _, _, kind) =
) (status,`New [] (* uris *)) boxml in
let _,_,_,_,nobj = obj in
let status = match nobj with
- NCic.Inductive (true,leftno,[it],_) ->
+ NCic.Inductive (is_ind,leftno,[it],_) ->
let _,ind_name,ty,cl = it in
List.fold_left
(fun status outsort ->
let status = status#set_ng_mode `ProofMode in
try
- (let status,invobj = NInversion.mk_inverter
- (ind_name ^ "_inv_" ^ (snd (NCicElim.ast_of_sort outsort)))
- it leftno outsort status status#baseuri in
+ (let status,invobj =
+ NInversion.mk_inverter
+ (ind_name ^ "_inv_" ^
+ (snd (NCicElim.ast_of_sort outsort)))
+ is_ind it leftno outsort status status#baseuri in
let _,_,menv,_,_ = invobj in
fst (match menv with
[] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
indtyno, NCicEnvironment.get_checked_indtys r
| _ -> prerr_endline ("engine: indty =" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in
let it = List.nth tys indtyno in
- let status,obj = NInversion.mk_inverter name it leftno ?selection sort
+ let status,obj = NInversion.mk_inverter name true it leftno ?selection sort
status status#baseuri in
let _,_,menv,_,_ = obj in
(match menv with
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-(* let pp m = prerr_endline (Lazy.force m);;*)
+(*let pp m = prerr_endline (Lazy.force m);;*)
let pp _ = ();;
let fresh_name =
| hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
;;
-let rec mk_lambdas l t =
- match l with
- [] -> t
- | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
-;;
-
-let rec mk_arrows xs ys selection target =
+let rec mk_arrows ?(pattern=false) xs ys selection target =
match selection,xs,ys with
[],[],[] -> target
- | false :: l,x::xs,y::ys -> mk_arrows xs ys l target
+ | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target
| true :: l,x::xs,y::ys ->
- CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
- mk_arrows xs ys l target)
+ CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then CicNotationPt.Implicit `JustOne else mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
+ mk_arrows ~pattern xs ys l target)
| _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
;;
status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
;;
-let mk_inverter name it leftno ?selection outsort status baseuri =
+let mk_inverter name is_ind it leftno ?selection outsort status baseuri =
pp (lazy ("leftno = " ^ string_of_int leftno));
let _,ind_name,ty,cl = it in
pp (lazy ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
in
let prods = mk_arrows id_rs id_ys selection pred in
- let lambdas = mk_lambdas (ys@["p"]) prods in
-
let hyplist =
let rec hypaux k = function
0 -> []
pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys)));
let outsort, suffix = NCicElim.ast_of_sort outsort in
- let theorem = mk_prods xs
- (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
- mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
- Some (CicNotationPt.Implicit `JustOne)),
- mk_appl (mk_id "P"::id_rs)))))
+ let theorem =
+ mk_prods xs
+ (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
+ mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs)))))
in
- let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @
- List.map mk_id hyplist @
- HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [mk_id "Hterm"] ) in
- let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri
- (baseuri ^ name ^ ".def",
- 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some
- (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) in
+ let status, theorem =
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ (baseuri ^ name ^ ".def",0,
+ CicNotationPt.Theorem
+ (`Theorem,name,theorem,
+ Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+ in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
CicNotationPt.Implicit (`Tagged "end"));
CicNotationPt.Implicit (`Tagged "cut")] in
let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
- let status = NTactics.block_tac
- (NTactics.branch_tac ::
- NTactics.case_tac "inv" ::
- (intros @
- [NTactics.apply_tac ("",0,cut);
- NTactics.branch_tac;
- NTactics.case_tac "end";
- NTactics.apply_tac ("",0,mk_id "Hcut");
- NTactics.apply_tac ("",0,mk_id "refl");
- NTactics.shift_tac;
- (*NTactics.case_tac "cut";*)
- NTactics.apply_tac ("",0,t);
- NTactics.merge_tac;
- NTactics.merge_tac;
- NTactics.skip_tac])) status in
+ let where =
+ "",0,(None,[],
+ Some (
+ mk_arrows ~pattern:true
+ (HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys))
+ (HExtlib.mk_list CicNotationPt.UserInput (List.length ys))
+ selection CicNotationPt.UserInput)) in
+ let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
+ let status =
+ NTactics.block_tac
+ (NTactics.branch_tac ::
+ NTactics.case_tac "inv" ::
+ (intros @
+ [NTactics.apply_tac ("",0,cut);
+ NTactics.branch_tac;
+ NTactics.case_tac "end";
+ NTactics.apply_tac ("",0,mk_id "Hcut");
+ NTactics.apply_tac ("",0,mk_id "refl");
+ NTactics.shift_tac;
+ elim_tac ~what:("",0,mk_id "Hterm") ~where;
+ NTactics.branch_tac] @
+ HExtlib.list_concat ~sep:[NTactics.shift_tac]
+ (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
+ [NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.skip_tac])) status in
pp (lazy "inv 3");
status,status#obj
;;
projects / helm.git / commitdiff