(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
-(*let pp m = prerr_endline (Lazy.force m);;*)
-let pp _ = ();;
+let pp m = prerr_endline (Lazy.force m);;
+(* let pp _ = ();; *)
let fresh_name =
let i = ref 0 in
| hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
;;
-let rec mk_arrows ?(pattern=false) xs ys selection target =
+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 =
match selection,xs,ys with
[],[],[] -> target
- | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target
+ | false :: l,x::xs,y::ys -> mk_arrows xs ys l target
| true :: l,x::xs,y::ys ->
- 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)
+ CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
+ mk_arrows 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 is_ind it leftno ?selection outsort status baseuri =
+let mk_inverter name 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));
let ncons = List.length cl in
- (**)let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
+ (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
let params = List.rev_map (function name,_ -> mk_id name) params in
- pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**)
+ pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));*)
let args,sort= split_arity ~subst:[] [] ty in
pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort));
- (**)let args = List.rev_map (function name,_ -> mk_id name) args in
- pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**)
+ (*let args = List.rev_map (function name,_ -> mk_id name) args in
+ pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));*)
let nparams = List.length args in
-
pp (lazy ("nparams = " ^ string_of_int nparams));
- if nparams = 0
+ if nparams <= leftno
then raise (Failure "inverter: the type must have at least one right parameter")
else
- let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
+ let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
let ls, rs = HExtlib.split_nth leftno xs in
pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
- let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (leftno+nparams+1)) in
+ let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
let _id_xs = List.map mk_id xs in
let id_ls = List.map mk_id ls in
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)))), mk_appl (mk_id "P"::id_rs)))))
- in
- let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
- (baseuri ^ name ^ ".def",0,
- CicNotationPt.Theorem
- (`Theorem,name,theorem,
- Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+ 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)))))
in
+ let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @
+ List.map mk_id hyplist @
+ CicNotationPt.Implicit `Vector::[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 uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
-
-CicNotationPt.Implicit (`Tagged "end"));
+ 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 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 ~force:true] @
- 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
+ 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_eq");
+ NTactics.shift_tac;
+ (*NTactics.case_tac "cut";*)
+ NTactics.apply_tac ("",0,t);
+ NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.skip_tac])) status in
pp (lazy "inv 3");
status,status#obj
;;
projects / helm.git / blobdiff