let get_type msg st t = H.get_type msg st.context (H.cic t)
+let clear_absts m =
+ let rec aux k n = function
+ | C.ALambda (id, s, v, t) when k > 0 ->
+ C.ALambda (id, s, v, aux (pred k) n t)
+ | C.ALambda (_, _, _, t) when n > 0 ->
+ aux 0 (pred n) (Cn.lift 1 (-1) t)
+ | t when n > 0 ->
+ Printf.eprintf "A2P.clear_absts: %u %s\n" n (Pp.ppterm (H.cic t));
+ assert false
+ | t -> t
+ in
+ aux m
+
(* proof construction *******************************************************)
-let anonymous_premise = C.Name "PREMISE"
+let anonymous_premise = C.Name "UNNAMED"
let mk_exp_args hd tl classes synth =
let meta id = C.AImplicit (id, None) in
| None ->
if !debug then [T.Note "NORMAL: NO INNER TYPES"] else []
| Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
-
-let convert_elim st ?name t v pattern =
- match t, get_inner_types st t, get_inner_types st v with
- | _, None, _
- | _, _, None -> [(* T.Note "ELIM: NO INNER TYPES"*)]
- | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
- let where = List.hd (List.rev tl) in
- let cty = Cn.elim_inferred_type
- st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
- in
- mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
- | _, Some _, Some _ -> assert false
let get_intro = function
| C.Anonymous -> None
if (Cn.does_not_occur e) then st, [] else
match where with
| C.ARel (_, _, i, premise) as w ->
-(* let _script = convert_elim st ~name:(premise, i) v w e in *)
let script name =
let where = Some (premise, name) in
- let script = mk_arg st what @ mk_arg st w (* @ script *) in
+ let script = mk_arg st what @ mk_arg st w in
T.Rewrite (direction, what, where, e, dtext) :: script
in
if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
let ity = H.acic_bc st.context ity in
let br1 = [T.Id ""] in
let br2 = List.rev (T.Apply (w, "assumption") :: script None) in
- let text = "non linear rewrite" in
+ let text = "non-linear rewrite" in
st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)]
end
| _ -> assert false
let predicate = List.nth tl 2 in
let e = Cn.mk_pattern 1 predicate in
let script = [T.Branch (qs, "")] in
- if (Cn.does_not_occur e) then script else
-(* let script = convert_elim st t t e in *)
+ if (Cn.does_not_occur e) then script else
T.Rewrite (direction, where, None, e, dtext) :: script
let rec proc_lambda st what name v t =
let predicate = List.nth tl2 (parsno - i) in
let e = Cn.mk_pattern j predicate in
let using = Some hd in
- (* convert_elim st what what e @ *) script2 @
+ script2 @
[T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
| None ->
let names = get_sub_names hd tl in
in
mk_preamble st what script
+and proc_case st what uri tyno u v ts =
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let synth, classes = I.S.empty, Cl.make ts in
+ let names = H.get_ind_names uri tyno in
+ let qs = proc_bkd_proofs (next st) synth names classes ts in
+ let lpsno, _ = H.get_ind_type uri tyno in
+ let ps, sort_disp = H.get_ind_parameters st.context (H.cic v) in
+ let _, rps = HEL.split_nth lpsno ps in
+ let rpsno = List.length rps in
+ let predicate = clear_absts rpsno (1 - sort_disp) u in
+ let e = Cn.mk_pattern rpsno predicate in
+ let text = "" in
+ let script = List.rev (mk_arg st v) in
+ script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_preamble st what script
+
and proc_other st what =
let _, dtext = test_depth st in
let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in
{st with context = context}
in
match t with
- | C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t
- | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
- | C.ARel _ as what -> proc_rel (f st) what
- | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
- | C.AConst _ as what -> proc_const (f st) what
- | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
- | what -> proc_other (f st) what
+ | C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t
+ | C.ALetIn (_, name, v, w, t) as what -> proc_letin (f st) what name v w t
+ | C.ARel _ as what -> proc_rel (f st) what
+ | C.AMutConstruct _ as what -> proc_mutconstruct (f st) what
+ | C.AConst _ as what -> proc_const (f st) what
+ | C.AAppl (_, hd :: tl) as what -> proc_appl (f st) what hd tl
+ | C.AMutCase (_, uri, i, u, v, ts) as what -> proc_case (f st) what uri i u v ts
+ | what -> proc_other (f st) what
and proc_bkd_proofs st synth names classes ts =
try
| Some fl -> fl
| None -> aux attrs
-let proc_obj ?flavour st = function
+let proc_obj ?flavour ?(info="") st = function
| C.AConstant (_, _, s, Some v, t, [], attrs) ->
begin match get_flavour ?flavour attrs with
| flavour when List.mem flavour th_flavours ->
let ast = proc_proof st v in
let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
- let text = Printf.sprintf "tactics: %u\nnodes: %u" steps nodes in
+ let text = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ in
T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
| flavour when List.mem flavour def_flavours ->
[T.Statement (flavour, Some s, t, Some v, "")]
(* interface functions ******************************************************)
-let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
- ?flavour prefix anobj =
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
+ ?info ?depth ?flavour prefix anobj =
let st = {
sorts = ids_to_inner_sorts;
types = ids_to_inner_types;
} in
L.time_stamp "P : LEVEL 2 ";
HLog.debug "Procedural: level 2 transformation";
- let steps = proc_obj st ?flavour anobj in
+ let steps = proc_obj st ?flavour ?info anobj in
L.time_stamp "P : RENDERING";
HLog.debug "Procedural: grafite rendering";
let r = List.rev (T.render_steps [] steps) in