*)
module H = HExtlib
+module U = UriManager
module C = Content
module G = GrafiteAst
module N = CicNotationPt
let l1, l2 = list_split (pred n) (List.tl l) in
List.hd l :: l1, l2
+let cont sep a = match sep with
+ | None -> a
+ | Some sep -> sep :: a
+
+let list_rev_map_concat map sep a l =
+ let rec aux a = function
+ | [] -> a
+ | [x] -> map a x
+ | x :: y :: l -> aux (sep :: map a x) (y :: l)
+ in
+ aux a l
+
(****************************************************************************)
type name = string
| Qed of note
| Intros of count option * name list * note
| Elim of what * using option * note
+ | LetIn of name * what * note
| Exact of what * note
| Branch of step list list * note
+(* annterm constructors *****************************************************)
+
+let mk_arel i b = Cic.ARel ("", "", i, b)
+
(* level 2 transformation ***************************************************)
let mk_name = function
| Some name -> name
- | None -> "_"
+ | None -> "UNUSED" (**)
let mk_intros_arg = function
| `Declaration {C.dec_name = name}
let l1, l2 = list_split (int_of_string n) tl in
List.hd (List.rev l2), l1
-let mk_what rpac = function
+let rec mk_apply_term aref ac ds cargs =
+ let step0 = mk_arg true (ac, [], ds) (List.hd cargs) in
+ let _, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
+ Cic.AAppl (aref, List.rev row), ds
+
+and mk_delta p ds =
+ let cmethod = p.C.proof_conclude.C.conclude_method in
+ let cargs = p.C.proof_conclude.C.conclude_args in
+ let capply = p.C.proof_apply_context in
+ let ccont = p.C.proof_context in
+ let caref = p.C.proof_conclude.C.conclude_aref in
+ match cmethod with
+ | "Exact"
+ | "Apply" when ccont = [] ->
+ let what, ds = mk_apply_term caref capply ds cargs in
+ let name = "PREVIOUS" in
+ mk_arel 1 name, LetIn (name, what, "") :: ds
+ | _ -> mk_arel 1 "COMPOUND", ds
+
+and mk_arg first (ac, row, ds) = function
+ | C.Lemma {C.lemma_id = aref; C.lemma_uri = uri} ->
+ ac, Cic.AConst (aref, U.uri_of_string uri, []) :: row, ds
| C.Premise {C.premise_n = Some i; C.premise_binder = Some b} ->
- Cic.ARel ("", "", i, b)
+ ac, mk_arel i b :: row, ds
| C.Premise {C.premise_n = None; C.premise_binder = None} ->
- Cic.ARel ("", "", 1, "COMPOUND")
- | C.Term t -> t
- | C.Premise _ -> assert false
- | C.ArgMethod _ -> assert false
- | C.ArgProof _ -> assert false
- | C.Lemma _ -> assert false
- | C.Aux _ -> assert false
+ begin match first, ac with
+ | _, hd :: tl ->
+ let arg, ds = mk_delta hd ds in
+ tl, arg :: row, ds
+ | false, [] -> ac, Cic.AImplicit ("", None) :: row, ds
+ | _ -> assert false
+ end
+ | C.Term t when first -> ac, t :: row, ds
+ | C.Term _ -> ac, Cic.AImplicit ("", None) :: row, ds
+ | C.Premise _ -> assert false
+ | C.ArgMethod _ -> assert false
+ | C.ArgProof _ -> assert false
+ | C.Aux _ -> assert false
let rec mk_proof p =
let names = mk_intros_args p.C.proof_context in
match cmethod, cargs with
| "Intros+LetTac", [C.ArgProof p] -> mk_proof p
| "ByInduction", C.Aux n :: C.Term (Cic.AAppl (_, using :: _)) :: tl ->
- let rpac = List.rev capply in
let whatm, ms = split_inductive n tl in (* actual rx params here *)
- let what, qs = mk_what rpac whatm, List.map mk_subproof ms in
- [Elim (what, Some using, ""); Branch (qs, "")]
+ let _, row, ds = mk_arg true (List.rev capply, [], []) whatm in
+ let what, qs = List.hd row, List.map mk_subproof ms in
+ List.rev ds @ [Elim (what, Some using, ""); Branch (qs, "")]
| _ ->
- [Note (Printf.sprintf "%s %u" cmethod (List.length cargs))]
+ let text =
+ Printf.sprintf "UNEXPANDED %s %u" cmethod (List.length cargs)
+ in [Note text]
and mk_subproof = function
| C.ArgProof ({C.proof_name = Some n} as p) -> Note n :: mk_proof p
let tactic = G.Elim (floc, what, using, Some 0, []) in
mk_tactic tactic
+let mk_letin name what =
+ let tactic = G.LetIn (floc, what, name) in
+ mk_tactic tactic
+
let mk_exact t =
let tactic = G.Exact (floc, t) in
mk_tactic tactic
(* rendering ****************************************************************)
-let cont sep a = match sep with
- | None -> a
- | Some sep -> sep :: a
-
-let list_rev_map_concat map sep a l =
- let rec aux a = function
- | [] -> a
- | [x] -> map a x
- | x :: y :: l -> aux (sep :: map a x) (y :: l)
- in
- aux a l
-
let rec render_step sep a = function
| Note s -> mk_note s :: a
| Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a
| Qed s -> mk_note s :: mk_qed :: a
| Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
| Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
+ | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
| Exact (t, s) -> mk_note s :: cont sep (mk_exact t :: a)
-(* | Branch ([], s) -> mk_note s :: cont sep a
- | Branch ([ps], s) -> mk_note s :: cont sep (render_steps a ps)
-*) | Branch (pss, s) ->
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps a ps
+ | Branch (pss, s) ->
let a = mk_ob :: a in
let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
mk_note s :: cont sep body
and render_steps a = function
- | [] -> a
- | [p] -> render_step None a p
- | (Note _ | Theorem _ | Qed _ as p) :: ps ->
+ | [] -> a
+ | [p] -> render_step None a p
+ | (Note _ | Theorem _ | Qed _ as p) :: ps ->
render_steps (render_step None a p) ps
- | p :: ((Branch _ :: _) as ps) ->
+ | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
render_steps (render_step (Some mk_sc) a p) ps
- | p :: ps ->
+ | p :: ps ->
render_steps (render_step (Some mk_dot) a p) ps
(* interface functions ******************************************************)
let content2procedural ~ids_to_inner_sorts prefix cobj =
- prerr_endline "Phase 2 transformation";
+ prerr_endline "Level 2 transformation";
let steps = mk_obj ids_to_inner_sorts prefix cobj in
prerr_endline "grafite rendering";
List.rev (render_steps [] steps)
+
projects / helm.git / commitdiff