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 $ *)
14 (*let pp m = prerr_endline (Lazy.force m);;*)
21 "z" ^ string_of_int !i
25 let id = if id = "_" then fresh_name () else id in
26 NotationPt.Ident (id,None)
29 let mk_sym s = NotationPt.Symbol (s,0);;
31 let rec split_arity status ~subst context te =
32 match NCicReduction.whd status ~subst context te with
33 | NCic.Prod (name,so,ta) ->
34 split_arity status ~subst ((name, (NCic.Decl so))::context) ta
42 | l -> NotationPt.Appl l
45 let rec mk_prods l t =
48 | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
51 let rec leibpatt = function
52 | [] -> NotationPt.UserInput
53 | false::sel -> leibpatt sel
54 | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
55 Some (mk_appl [NotationPt.Implicit `JustOne
56 ;NotationPt.Implicit `JustOne
57 ;NotationPt.Implicit `JustOne
58 ;NotationPt.UserInput])),
60 let rec jmeqpatt = function
61 | [] -> NotationPt.UserInput
62 | false::sel -> jmeqpatt sel
63 | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
64 Some (mk_appl [NotationPt.Implicit `JustOne
65 ;NotationPt.Implicit `JustOne
66 ;NotationPt.Implicit `JustOne
68 ;NotationPt.UserInput])),
71 let rec mk_arrows ~jmeq xs ys selection target =
72 match selection,xs,ys with
74 | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target
75 | true :: l,x::xs,y::ys when jmeq ->
76 NotationPt.Binder (`Forall, (mk_id "_",
77 Some (mk_appl [mk_sym "jmsimeq" ;
78 NotationPt.Implicit `JustOne;x;
79 NotationPt.Implicit `JustOne;y])),
80 mk_arrows ~jmeq xs ys l target)
81 | true :: l,x::xs,y::ys ->
82 NotationPt.Binder (`Forall, (mk_id "_",
83 Some (mk_appl [mk_sym "eq" ;
84 NotationPt.Implicit `JustOne;x;y])),
85 mk_arrows ~jmeq xs ys l target)
86 | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
89 let subst_metasenv_and_fix_names status =
90 let u,h,metasenv, subst,o = status#obj in
92 NCicUntrusted.map_obj_kind ~skip_body:true
93 (NCicUntrusted.apply_subst status subst []) o
95 status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
98 let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
99 pp (lazy ("leftno = " ^ string_of_int leftno));
100 let _,ind_name,ty,cl = it in
101 pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
102 let ncons = List.length cl in
103 (**)let params,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in
104 let params = List.rev_map (function name,_ -> mk_id name) params in
105 pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**)
106 let args,sort= split_arity status ~subst:[] [] ty in
107 pp (lazy ("arity sort: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:args sort));
108 (**)let args = List.rev_map (function name,_ -> mk_id name) args in
109 pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**)
110 let nparams = List.length args in
112 (* the default is a dependent inversion *)
113 (*let is_dependent = selection = None in*)
114 let is_dependent = true in
116 pp (lazy ("nparams = " ^ string_of_int nparams));
118 then raise (Failure "inverter: the type must have at least one right parameter")
120 let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
121 pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
122 let ls, rs = HExtlib.split_nth leftno xs in
123 pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
124 pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
126 (* dependent -> add Hterm to rs *)
127 let rs = if is_dependent then (rs@["Hterm"]) else rs in
129 let _id_xs = List.map mk_id xs in
130 let id_rs = List.map mk_id rs in
135 None -> HExtlib.mk_list true (List.length rs)
140 let rec hypaux k = function
142 | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
146 let outsort, suffix = NCicElim.ast_of_sort outsort in
149 (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))),
150 (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length rs)) (NotationPt.Sort outsort))),
151 mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
153 let status, theorem =
154 GrafiteDisambiguate.disambiguate_nobj status ~baseuri
155 (baseuri ^ name ^ ".def",0,
157 (`Theorem,name,theorem,
158 Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
160 let uri,height,nmenv,nsubst,nobj = theorem in
161 let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
162 let status = status#set_obj theorem in
163 let status = status#set_stack ninitial_stack in
164 let status = subst_metasenv_and_fix_names status in
167 let rs = List.map (fun x -> mk_id x) rs in
168 mk_arrows ~jmeq rs rs selection (mk_appl (mk_id "P"::rs)) in
170 let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
172 NotationPt.Implicit (`Tagged "end"));
173 NotationPt.Implicit (`Tagged "cut")] in
174 let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["Hterm";"P"]@hyplist) in
177 Some (if jmeq then jmeqpatt selection
178 else leibpatt selection)) in
179 let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
182 (NTactics.branch_tac ::
183 NTactics.case_tac "inv" ::
185 [NTactics.apply_tac ("",0,cut);
187 NTactics.case_tac "end";
188 NTactics.apply_tac ("",0,mk_id "Hcut");
189 NTactics.apply_tac ("",0,mk_sym "refl");
191 elim_tac ~what:("",0,mk_id "Hterm") ~where;
192 NTactics.branch_tac ~force:true] @
193 HExtlib.list_concat ~sep:[NTactics.shift_tac]
194 (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
198 NTactics.skip_tac])) status in
203 let mk_inverter name is_ind it leftno ?selection outsort status baseuri =
204 try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri
205 with NTacStatus.Error (s,_) ->
206 mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri