2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
18 "z" ^ string_of_int !i
22 let id = if id = "_" then fresh_name () else id in
23 CicNotationPt.Ident (id,None)
26 let rec split_arity ~subst context te =
27 match NCicReduction.whd ~subst context te with
28 | NCic.Prod (name,so,ta) ->
29 split_arity ~subst ((name, (NCic.Decl so))::context) ta
37 | l -> CicNotationPt.Appl l
40 let rec mk_prods l t =
43 | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
46 let rec mk_lambdas l t =
49 | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
52 let rec mk_arrows xs ys selection target =
53 match selection,xs,ys with
55 | false :: l,x::xs,y::ys -> mk_arrows xs ys l target
56 | true :: l,x::xs,y::ys ->
57 CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
58 mk_arrows xs ys l target)
59 | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
62 let subst_metasenv_and_fix_names status =
63 let u,h,metasenv, subst,o = status#obj in
65 NCicUntrusted.map_obj_kind ~skip_body:true
66 (NCicUntrusted.apply_subst subst []) o
68 status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
71 let mk_inverter name it leftno ?selection outsort status baseuri =
72 prerr_endline ("leftno = " ^ string_of_int leftno);
73 let _,ind_name,ty,cl = it in
74 prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
75 let ncons = List.length cl in
76 (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
77 let params = List.rev_map (function name,_ -> mk_id name) params in
78 prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*)
79 let args,sort= split_arity ~subst:[] [] ty in
80 prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort);
81 (*let args = List.rev_map (function name,_ -> mk_id name) args in
82 prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*)
83 let nparams = List.length args in
84 prerr_endline ("nparams = " ^ string_of_int nparams);
86 then raise (Failure "inverter: the type must have at least one right parameter")
88 let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
89 prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
90 let ls, rs = HExtlib.split_nth leftno xs in
91 prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls));
92 prerr_endline ("lunghezza rs = " ^ string_of_int (List.length rs));
93 let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
95 let id_xs = List.map mk_id xs in
96 let id_ls = List.map mk_id ls in
97 let id_rs = List.map mk_id rs in
98 let id_ys = List.map mk_id ys in
100 (* pseudocode let t = Lambda y1 ... yr. xs_ = ys_ -> pred *)
102 (* check: assuming we have more than one right parameter *)
104 let pred = mk_appl ((mk_id "P")::id_ys) in
106 let selection = match selection with
107 None -> HExtlib.mk_list true (List.length ys)
110 let prods = mk_arrows id_rs id_ys selection pred in
112 let lambdas = mk_lambdas (ys@["p"]) prods in
115 let rec hypaux k = function
117 | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
120 prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys));
122 let outsort, suffix = NCicElim.ast_of_sort outsort in
123 let theorem = mk_prods xs
124 (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
125 mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
126 Some (CicNotationPt.Implicit `JustOne)),
127 mk_appl (mk_id "P"::id_rs)))))
129 let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @
130 List.map mk_id hyplist @
131 CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
133 let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri
134 (baseuri ^ name ^ ".def",
135 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some
136 (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) in
137 let uri,height,nmenv,nsubst,nobj = theorem in
138 let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
139 let status = status#set_obj theorem in
140 let status = status#set_stack ninitial_stack in
141 let status = subst_metasenv_and_fix_names status in
144 let rs = List.map (fun x -> mk_id x) rs in
145 mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
147 let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
148 CicNotationPt.Implicit (`Tagged "end"));
149 CicNotationPt.Implicit (`Tagged "cut")] in
150 let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
152 let status = NTactics.block_tac
153 (NTactics.branch_tac::
154 NTactics.case_tac "inv"::
156 [NTactics.apply_tac ("",0,cut);
158 NTactics.case_tac "end";
159 NTactics.apply_tac ("",0,mk_id "Hcut");
160 NTactics.apply_tac ("",0,mk_id "refl_eq");
162 NTactics.case_tac "cut";
163 NTactics.apply_tac ("",0,t)
167 NTactics.skip_tac*)])) status in