| {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et)
| {A.annsynthesized = st; A.annexpected = None} -> Some (st, st)
with Not_found -> None
-with Invalid_argument _ -> failwith "A2P.get_inner_types"
+with Invalid_argument _ -> failwith "P2.get_inner_types"
let get_entry st id =
let rec aux = function
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
let proceed, dtext = test_depth st in
let script = if proceed then
let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with
- | Some (C.ALetIn _, _), _ ->
+ | Some (C.ALetIn (_, _, iv, iw, _), _), _ when
+ H.alpha_equivalence ~flatten:true st.context (H.cic v) (H.cic iv) &&
+ H.alpha_equivalence ~flatten:true st.context (H.cic w) (H.cic iw)
+ ->
st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)]
- | _, Some (ity, ety) ->
+ | _, Some (ity, ety) ->
let st, rqv = match v with
| C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl ->
mk_fwd_rewrite st dtext intro tl true v t ity ety
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