* http://cs.unibo.it/helm/.
*)
-module L = Librarian
+module C = Cic
+module L = Librarian
+module G = GrafiteAst
+module H = ProceduralHelpers
module T = ProceduralTypes
+module P1 = Procedural1
module P2 = Procedural2
module X = ProceduralTeX
let tex_formatter = ref None
+(* object costruction *******************************************************)
+
+let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
+
+let def_flavours = [`Definition; `Variant]
+
+let get_flavour sorts params context v attrs =
+ let rec aux = function
+ | [] ->
+ if H.is_acic_proof sorts context v then List.hd th_flavours
+ else List.hd def_flavours
+ | `Flavour fl :: _ -> fl
+ | _ :: tl -> aux tl
+ in
+ let flavour_map x y = match x, y with
+ | None, G.IPAs flavour -> Some flavour
+ | _ -> x
+ in
+ match List.fold_left flavour_map None params with
+ | Some fl -> fl
+ | None -> aux attrs
+
+let rec is_record = function
+ | [] -> None
+ | `Class (`Record fields) :: _ -> Some fields
+ | _ :: tl -> is_record tl
+
+let proc_obj ?(info="") proc_proof sorts params context = function
+ | C.AConstant (_, _, s, Some v, t, [], attrs) ->
+ begin match get_flavour sorts params context v attrs with
+ | flavour when List.mem flavour th_flavours ->
+ let ast = proc_proof v in
+ let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
+ let text =
+ if List.mem G.IPComments params then
+ Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ else
+ ""
+ 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, "")]
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"
+ end
+ | C.AConstant (_, _, s, None, t, [], attrs) ->
+ [T.Statement (`Axiom, Some s, t, None, "")]
+ | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
+ begin match is_record attrs with
+ | None -> [T.Inductive (types, lpsno, "")]
+ | Some fs -> [T.Record (types, lpsno, fs, "")]
+ end
+ | _ ->
+ failwith "not a theorem, definition, axiom or inductive type"
+
(* interface functions ******************************************************)
+let get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context =
+ let level_map x y = match x, y with
+ | None, G.IPLevel level -> Some level
+ | _ -> x
+ in
+ match List.fold_left level_map None params with
+ | None
+ | Some 2 ->
+ P2.proc_proof
+ (P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
+ | Some 1 ->
+ P1.proc_proof
+ (P1.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
+ | Some n ->
+ failwith (
+ "Procedural reconstruction level not supported: " ^
+ string_of_int n
+ )
+
let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
?info params anobj =
- let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params [] in
+ let proc_proof =
+ get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params []
+ in
L.time_stamp "P : LEVEL 2 ";
HLog.debug "Procedural: level 2 transformation";
- let steps = P2.proc_obj st ?info anobj in
+ let steps = proc_obj ?info proc_proof ids_to_inner_sorts params [] anobj in
let _ = match !tex_formatter with
| None -> ()
| Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
context annterm =
- let st = P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context in
+ let proc_proof =
+ get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context
+ in
HLog.debug "Procedural: level 2 transformation";
- let steps = P2.proc_proof st annterm in
+ let steps = proc_proof annterm in
let _ = match !tex_formatter with
| None -> ()
| Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
in
HLog.debug "Procedural: grafite rendering";
List.rev (T.render_steps [] steps)
+
+let rec is_debug n = function
+ | [] -> false
+ | G.IPDebug debug :: _ -> n <= debug
+ | _ :: tl -> is_debug n tl