+procedural1.cmi: proceduralTypes.cmi
procedural2.cmi: proceduralTypes.cmi
proceduralTeX.cmi: proceduralTypes.cmi
proceduralHelpers.cmo: proceduralHelpers.cmi
proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi
proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi
+procedural1.cmo: procedural1.cmi
+procedural1.cmx: procedural1.cmi
procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi
procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
proceduralTeX.cmi
proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
proceduralTeX.cmi
-acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural2.cmi \
- acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural2.cmx \
- acic2Procedural.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi \
+ proceduralHelpers.cmi procedural2.cmi procedural1.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \
+ proceduralHelpers.cmx procedural2.cmx procedural1.cmx acic2Procedural.cmi
+procedural1.cmi: proceduralTypes.cmi
procedural2.cmi: proceduralTypes.cmi
proceduralTeX.cmi: proceduralTypes.cmi
proceduralHelpers.cmo: proceduralHelpers.cmi
proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi
proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi
proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi
+procedural1.cmo: procedural1.cmi
+procedural1.cmx: procedural1.cmi
procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \
proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi
procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
proceduralTeX.cmi
proceduralTeX.cmx: proceduralTypes.cmx proceduralHelpers.cmx \
proceduralTeX.cmi
-acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi procedural2.cmi \
- acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx procedural2.cmx \
- acic2Procedural.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralTeX.cmi \
+ proceduralHelpers.cmi procedural2.cmi procedural1.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralTeX.cmx \
+ proceduralHelpers.cmx procedural2.cmx procedural1.cmx acic2Procedural.cmi
proceduralTypes.mli \
proceduralMode.mli \
proceduralConversion.mli \
+ procedural1.mli \
procedural2.mli \
proceduralTeX.mli \
acic2Procedural.mli \
* 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 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 = Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
+ "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
+ 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) ->
+ [T.Inductive (types, lpsno, "")]
+ | _ ->
+ 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
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+module C = Cic
+module A = Cic2acic
+module G = GrafiteAst
+
+module T = ProceduralTypes
+
+type status = {
+ sorts : (C.id, A.sort_kind) Hashtbl.t;
+ types : (C.id, A.anntypes) Hashtbl.t;
+ params : G.inline_param list;
+ context : C.context
+}
+
+(* interface functions ******************************************************)
+
+let proc_proof st what =
+ let dtext = "" in
+ [T.Exact (what, dtext)]
+
+let init ~ids_to_inner_sorts ~ids_to_inner_types params context =
+ {
+ sorts = ids_to_inner_sorts;
+ types = ids_to_inner_types;
+ params = params;
+ context = context
+ }
--- /dev/null
+(* Copyright (C) 2003-2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+type status
+
+val init:
+ ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
+ ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t ->
+ GrafiteAst.inline_param list-> Cic.context -> status
+
+val proc_proof:
+ status -> Cic.annterm -> ProceduralTypes.step list
with Not_found -> None
with Invalid_argument _ -> failwith "A2P.get_inner_types"
-let is_proof st v =
-try
- let id = Ut.id_of_annterm v in
- try match Hashtbl.find st.sorts id with
- | `Prop -> true
- | _ -> false
- with Not_found -> H.is_proof st.context (H.cic v)
-with Invalid_argument _ -> failwith "P1.is_proof"
-
let get_entry st id =
let rec aux = function
| [] -> assert false
with Invalid_argument s -> failwith ("A2P.proc_bkd_proofs: " ^ s)
-(* object costruction *******************************************************)
-
-let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
-
-let def_flavours = [`Definition; `Variant]
-
-let get_flavour st v attrs =
- let rec aux = function
- | [] ->
- if is_proof st 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 st.params with
- | Some fl -> fl
- | None -> aux attrs
-
-let proc_obj ?(info="") st = function
- | C.AConstant (_, _, s, Some v, t, [], attrs) ->
- begin match get_flavour st v attrs with
- | flavour when List.mem flavour th_flavours ->
- 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 "%s\n%s%s: %u\n%s: %u\n%s"
- "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
- 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) ->
- [T.Inductive (types, lpsno, "")]
- | _ ->
- failwith "not a theorem, definition, axiom or inductive type"
+(* initialization ***********************************************************)
let init ~ids_to_inner_sorts ~ids_to_inner_types params context =
let depth_map x y = match x, y with
val proc_proof:
status -> Cic.annterm -> ProceduralTypes.step list
-val proc_obj:
- ?info:string -> status -> Cic.annobj -> ProceduralTypes.step list
-
val debug: bool ref
| t -> t
in
bc c t
+
+let is_acic_proof sorts context v =
+ let id = Ut.id_of_annterm v in
+ try match Hashtbl.find sorts id with
+ | `Prop -> true
+ | _ -> false
+ with Not_found -> is_proof context (cic v)
Cic.context -> Cic.term -> Cic.term
val acic_bc:
Cic.context -> Cic.annterm -> Cic.annterm
+val is_acic_proof:
+ (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm ->
+ bool
type print_kind = [ `Env | `Coer ]
type inline_param = IPPrefix of string
- | IPProcedural
- | IPDepth of int
| IPAs of Cic.object_flavour
+ | IPProcedural
| IPNoDefaults
+ | IPLevel of int
+ | IPDepth of int
type ('term,'lazy_term) macro =
(* Whelp's stuff *)
| IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
| IPAs flavour -> flavour_pp flavour
| IPProcedural -> "procedural"
- | IPDepth depth -> "depth = " ^ string_of_int depth
| IPNoDefaults -> "nodefaults"
+ | IPDepth depth -> "depth = " ^ string_of_int depth
+ | IPLevel level -> "level = " ^ string_of_int level
in
let s = String.concat " " (List.map pp_param l) in
if s = "" then s else " " ^ s
inline_params:[
[ params = LIST0
[ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
- | IDENT "procedural" -> G.IPProcedural
| flavour = inline_flavour -> G.IPAs flavour
- | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
+ | IDENT "procedural" -> G.IPProcedural
| IDENT "nodefaults" -> G.IPNoDefaults
+ | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
+ | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
] -> params
]
];
projects / helm.git / commitdiff