type status = {
sorts : (C.id, A.sort_kind) Hashtbl.t;
types : (C.id, A.anntypes) Hashtbl.t;
- prefix: string;
max_depth: int option;
depth: int;
context: C.context;
- clears: string list;
- clears_note: string;
- case: int list;
- skip_thm_and_qed : bool;
+ case: int list
}
-let debug = true
+let debug = false
(* helpers ******************************************************************)
| (_, _, _, cs) -> List.map fst cs
with Invalid_argument _ -> failwith "A2P.get_ind_names"
+let string_of_atomic = function
+ | C.ARel (_, _, _, s) -> s
+ | C.AVar (_, uri, _) -> H.name_of_uri uri None None
+ | C.AConst (_, uri, _) -> H.name_of_uri uri None None
+ | C.AMutInd (_, uri, i, _) -> H.name_of_uri uri (Some i) None
+ | C.AMutConstruct (_, uri, i, j, _) -> H.name_of_uri uri (Some i) (Some j)
+ | _ -> ""
+
+let get_sub_names head l =
+ let s = string_of_atomic head in
+ if s = "" then [] else
+ let map (names, i) _ =
+ let name = Printf.sprintf "%s_%u" s i in name :: names, succ i
+ in
+ let names, _ = List.fold_left map ([], 1) l in
+ List.rev names
+
(* proof construction *******************************************************)
let anonymous_premise = C.Name "PREMISE"
| C.Name s -> Some s
let mk_preamble st what script =
- let clears st script =
- if true (* st.clears = [] *) then script else T.Clear (st.clears, st.clears_note) :: script
- in
- clears st (convert st what @ script)
+ convert st what @ script
let mk_arg st = function
| C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what
(* convert_elim st what what e @ *) script2 @
[T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
| None ->
- let qs = proc_bkd_proofs (next st) synth [] classes tl in
+ let names = get_sub_names hd tl in
+ let qs = proc_bkd_proofs (next st) synth names classes tl in
let hd = mk_exp_args hd tl classes synth in
script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
else
(Pp.ppterm (H.cic it)) (Pp.ppterm (H.cic et)))
| None -> None, "\nNo types"
in
- let context, clears = Cn.get_clears st.context (H.cic t) xtypes in
- let note = Pp.ppcontext st.context ^ note in
- {st with context = context; clears = clears; clears_note = note; }
+ let context, _clears = Cn.get_clears st.context (H.cic t) xtypes in
+ {st with context = context}
in
match t with
| C.ALambda (_, name, w, t) as what -> proc_lambda (f st) what name w t
let aux (inv, _) v =
if I.overlaps synth inv then None else
if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else
- Some (fun _ -> [T.Apply (v, dtext ^ "dependent")])
+ Some (get_note (fun _ -> [T.Apply (v, dtext ^ "dependent")]))
in
let ps = T.list_map2_filter aux classes ts in
let b = List.length ps > 1 in
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
- if st.skip_thm_and_qed then ast
- else T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
+ T.Statement (`Theorem, Some s, t, None, "") :: ast @ [T.Qed text]
| C.AConstant (_, _, s, Some v, t, [], pars) when is_definition pars ->
[T.Statement (`Definition, Some s, t, Some v, "")]
| C.AConstant (_, _, s, None, t, [], pars) ->
(* interface functions ******************************************************)
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth
-?(skip_thm_and_qed=false) prefix aobj =
+let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+ prefix anobj =
let st = {
sorts = ids_to_inner_sorts;
types = ids_to_inner_types;
- prefix = prefix;
max_depth = depth;
depth = 0;
context = [];
- clears = [];
- clears_note = "";
- case = [];
- skip_thm_and_qed = skip_thm_and_qed;
+ case = []
+ } in
+ HLog.debug "Procedural: level 2 transformation";
+ let steps = proc_obj st anobj in
+ HLog.debug "Procedural: grafite rendering";
+ List.rev (T.render_steps [] steps)
+
+let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth
+ prefix context annterm =
+ let st = {
+ sorts = ids_to_inner_sorts;
+ types = ids_to_inner_types;
+ max_depth = depth;
+ depth = 0;
+ context = context;
+ case = []
} in
HLog.debug "Procedural: level 2 transformation";
- let steps = proc_obj st aobj in
+ let steps = proc_proof st annterm in
HLog.debug "Procedural: grafite rendering";
List.rev (T.render_steps [] steps)
* http://cs.unibo.it/helm/.
*)
-val acic2procedural:
+val procedural_of_acic_object:
ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t ->
- ?depth:int -> ?skip_thm_and_qed:bool ->
- string -> Cic.annobj ->
+ ?depth:int -> string -> Cic.annobj ->
(Cic.annterm, Cic.annterm,
Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
GrafiteAst.statement list
+val procedural_of_acic_term:
+ ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
+ ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t ->
+ ?depth:int -> string -> Cic.context -> Cic.annterm ->
+ (Cic.annterm, Cic.annterm,
+ Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
+ GrafiteAst.statement list
let get_default_eliminator context uri tyno ty =
let _, (name, _, _, _) = get_ind_type uri tyno in
let ext = match get_tail context (get_type context ty) with
- | C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort (C.CProp _) -> "_rect"
- | C.Sort (C.Type _) -> "_rect"
- | t ->
+ | C.Sort C.Prop -> "_ind"
+ | C.Sort C.Set -> "_rec"
+ | C.Sort (C.CProp _) -> "_rect"
+ | C.Sort (C.Type _) -> "_rect"
+ | t ->
Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
assert false
in
let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
!result
+let name_of_uri uri tyno cno =
+ let get_ind_type tys tyno =
+ let s, _, _, cs = List.nth tys tyno in s, cs
+ in
+ match (fst (E.get_obj Un.oblivion_ugraph uri)), tyno, cno with
+ | C.Variable (s, _, _, _, _), _, _ -> s
+ | C.Constant (s, _, _, _, _), _, _ -> s
+ | C.InductiveDefinition (tys, _, _, _), Some i, None ->
+ let s, _ = get_ind_type tys i in s
+ | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
+ let _, cs = get_ind_type tys i in
+ let s, _ = List.nth cs (pred j) in s
+ | _ -> assert false
+
(* Ensuring Barendregt convenction ******************************************)
let rec add_entries map c = function
Cic.annterm -> Cic.term
val occurs:
Cic.context -> what:Cic.term -> where:Cic.term -> bool
+val name_of_uri:
+ UriManager.uri -> int option -> int option -> string
val cic_bc:
Cic.context -> Cic.term -> Cic.term
val acic_bc:
let aux = GrafiteAstPp.pp_statement
~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
let script =
- Acic2Procedural.acic2procedural
+ Acic2Procedural.procedural_of_acic_object
~ids_to_inner_sorts ~ids_to_inner_types
- ?depth ?skip_thm_and_qed prefix aobj
+ ?depth prefix aobj
in
"\n\n" ^ String.concat "" (List.map aux script)
let _, baseuri, _, _ =
Librarian.baseuri_of_script ~include_paths name
in
- baseuri
+ baseuri ^ "/"
in
txt_of_inline_uri ~map_unicode_to_tex style suri prefix
-
-
+
+(****************************************************************************)
+(* procedural_txt_of_cic_term *)
+
+let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
+ let annterm, ids_to_inner_sorts, ids_to_inner_types =
+ try Cic2acic.acic_term_of_cic_term context term
+ with e ->
+ let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
+ failwith msg
+ in
+ let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
+ let lazy_term_pp = term_pp in
+ let obj_pp = CicNotationPp.pp_obj term_pp in
+ let aux = GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
+ let script =
+ Acic2Procedural.procedural_of_acic_term
+ ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm
+ in
+ String.concat "" (List.map aux script)
val txt_of_inline_macro:
map_unicode_to_tex:bool ->
GrafiteAst.presentation_style -> string -> string -> string
+
+(* columns, rendering depth, context, term *)
+val procedural_txt_of_cic_term:
+ map_unicode_to_tex:bool -> int -> ?depth:int ->
+ Cic.context -> Cic.term ->
+ string
cic2grafite cc menv proof_term
else
(* alternative using FG stuff *)
- let proof_term, how_many_lambdas =
- Auto.lambda_close ~prefix_name:"orrible_hack_"
- proof_term menv cc
- in
- let ty,_ =
- CicTypeChecker.type_of_aux'
- menv [] proof_term CicUniv.empty_ugraph
- in
- let obj =
- Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma])
- in
- Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+"
- (strip_comments
- (ApplyTransformation.txt_of_cic_object
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- ~skip_thm_and_qed:true
- ~skip_initial_lambdas:how_many_lambdas
- 80 (GrafiteAst.Procedural None) "" obj))
+ let map_unicode_to_tex =
+ Helm_registry.get_bool "matita.paste_unicode_as_tex"
+ in
+ ApplyTransformation.procedural_txt_of_cic_term
+ ~map_unicode_to_tex 78 cc proof_term
in
let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
[],text,parsed_text_length
(* *)
(**************************************************************************)
-
-include "coq.ma".
-
-alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-alias id "le" = "cic:/matita/tests/fguidi/le.ind#xpointer(1/1)".
-alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
-alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
-alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)".
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
-
-alias symbol "and" (instance 0) = "Coq's logical and".
-alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
-alias symbol "exists" (instance 0) = "Coq's exists".
+include "logic/connectives.ma".
+include "nat/nat.ma".
definition is_S: nat \to Prop \def
\lambda n. match n with
theorem le_gen_S_x_cc: \forall m,x. (\exists n. x = (S n) \land (le m n)) \to
(le (S m) x).
-intros. elim H. elim H1. cut ((S x1) = x). elim Hcut. autobatch.
+intros. elim H. elim H1. cut ((S a) = x). elim Hcut. autobatch.
elim H2. autobatch.
qed.
projects / helm.git / commitdiff