let get_type msg st t = H.get_type msg st.context (H.cic t)
+let get_uri_of_head = function
+ | C.AConst (_, u, _)
+ | C.AAppl (_, C.AConst (_, u, _) :: _) -> Some (u, 0, 0)
+ | C.AMutInd (_, u, i, _)
+ | C.AAppl (_, C.AMutInd (_, u, i, _) :: _) -> Some (u, succ i, 0)
+ | C.AMutConstruct (_, u, i, j, _)
+ | C.AAppl (_, C.AMutConstruct (_, u, i, j, _) :: _) -> Some (u, succ i, j)
+ | _ -> None
+
+let get_uri_of_apply = function
+ | T.Exact (t, _)
+ | T.Apply (t, _) -> get_uri_of_head t
+ | _ -> None
+
+let is_reflexivity st step =
+ match get_uri_of_apply step with
+ | None -> false
+ | Some (uri, i, j) -> st.defaults && Obj.is_eq_URI uri && i = 1 && j = 1
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "UNNAMED"
let exp = ref 0 in
let meta id = C.AImplicit (id, None) in
let map v (cl, b) =
- if I.overlaps synth cl then
- let w = if H.is_atomic (H.cic v) then v else meta "" in
- if b then v, v else meta "", w
- else
- meta "", meta ""
+ if I.overlaps synth cl
+ then if b then v, v else meta "", v
+ else meta "", meta ""
in
let rec rev a = function
| [] -> a
| C.Name s -> Some s
let mk_preamble st what script = match script with
+ | step :: script when is_reflexivity st step ->
+ convert st what @ T.Reflexivity (T.note_of_step step) :: script
| T.Exact _ :: _ -> script
| _ -> convert st what @ script
if n < 0 then a else mk_synth (I.S.add n a) (pred n)
in
let synth = mk_synth I.S.empty decurry in
- let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in
+ let text = if !debug
+ then Printf.sprintf "%u %s" parsno (Cl.to_string synth (classes, rc))
+ else ""
+ in
let script = List.rev (mk_arg st hd) in
let tactic b t n = if b then T.Apply (t, n) else T.Exact (t, n) in
match rc with