--- /dev/null
+requires="helm-cic_proof_checking helm-acic_content helm-grafite"
+version="0.0.1"
+archive(byte)="acic_procedural.cma"
+archive(native)="acic_procedural.cmxa"
library \
acic_content \
grafite \
+ acic_procedural \
content_pres \
cic_unification \
whelp \
--- /dev/null
+cicClassify.cmo: cicClassify.cmi
+cicClassify.cmx: cicClassify.cmi
+proceduralConversion.cmo: proceduralConversion.cmi
+proceduralConversion.cmx: proceduralConversion.cmi
+proceduralTypes.cmo: proceduralTypes.cmi
+proceduralTypes.cmx: proceduralTypes.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
+ cicClassify.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
+ cicClassify.cmx acic2Procedural.cmi
--- /dev/null
+cicClassify.cmo: cicClassify.cmi
+cicClassify.cmx: cicClassify.cmi
+proceduralConversion.cmo: proceduralConversion.cmi
+proceduralConversion.cmx: proceduralConversion.cmi
+proceduralTypes.cmo: proceduralTypes.cmi
+proceduralTypes.cmx: proceduralTypes.cmi
+acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \
+ cicClassify.cmi acic2Procedural.cmi
+acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \
+ cicClassify.cmx acic2Procedural.cmi
--- /dev/null
+PACKAGE = acic_procedural
+PREDICATES =
+
+INTERFACE_FILES = \
+ cicClassify.mli \
+ proceduralConversion.mli \
+ proceduralTypes.mli \
+ acic2Procedural.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ $(INTERFACE_FILES:%.mli=%.ml)
+
+include ../../Makefile.defs
+include ../Makefile.common
--- /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 D = Deannotate
+module DTI = DoubleTypeInference
+module TC = CicTypeChecker
+module Un = CicUniv
+module UM = UriManager
+module Obj = LibraryObjects
+module HObj = HelmLibraryObjects
+module A = Cic2acic
+module Ut = CicUtil
+module E = CicEnvironment
+
+module Cl = CicClassify
+module T = ProceduralTypes
+module Cn = ProceduralConversion
+
+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;
+ intros: string list;
+ ety: C.annterm option
+}
+
+(* helpers ******************************************************************)
+
+let id x = x
+
+let comp f g x = f (g x)
+
+let cic = D.deannotate_term
+
+let split2_last l1 l2 =
+try
+ let n = pred (List.length l1) in
+ let before1, after1 = T.list_split n l1 in
+ let before2, after2 = T.list_split n l2 in
+ before1, before2, List.hd after1, List.hd after2
+with Invalid_argument _ -> failwith "A2P.split2_last"
+
+let string_of_head = function
+ | C.ASort _ -> "sort"
+ | C.AConst _ -> "const"
+ | C.AMutInd _ -> "mutind"
+ | C.AMutConstruct _ -> "mutconstruct"
+ | C.AVar _ -> "var"
+ | C.ARel _ -> "rel"
+ | C.AProd _ -> "prod"
+ | C.ALambda _ -> "lambda"
+ | C.ALetIn _ -> "letin"
+ | C.AFix _ -> "fix"
+ | C.ACoFix _ -> "cofix"
+ | C.AAppl _ -> "appl"
+ | C.ACast _ -> "cast"
+ | C.AMutCase _ -> "mutcase"
+ | C.AMeta _ -> "meta"
+ | C.AImplicit _ -> "implict"
+
+let clear st = {st with intros = []; ety = None}
+
+let next st = {(clear st) with depth = succ st.depth}
+
+let set_ety st ety =
+ if st.ety = None then {st with ety = ety} else st
+
+let add st entry intro ety =
+ let st = set_ety st ety in
+ {st with context = entry :: st.context; intros = intro :: st.intros}
+
+let test_depth st =
+try
+ let msg = Printf.sprintf "Depth %u: " st.depth in
+ match st.max_depth with
+ | None -> true, ""
+ | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: "
+with Invalid_argument _ -> failwith "A2P.test_depth"
+
+let is_rewrite_right = function
+ | C.AConst (_, uri, []) ->
+ UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
+ | _ -> false
+
+let is_rewrite_left = function
+ | C.AConst (_, uri, []) ->
+ UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
+ | _ -> false
+(*
+let get_ind_name uri tno xcno =
+try
+ let ts = match E.get_obj Un.empty_ugraph uri with
+ | C.InductiveDefinition (ts, _, _,_), _ -> ts
+ | _ -> assert false
+ in
+ let tname, cs = match List.nth ts tno with
+ | (name, _, _, cs) -> name, cs
+ in
+ match xcno with
+ | None -> tname
+ | Some cno -> fst (List.nth cs (pred cno))
+with Invalid_argument _ -> failwith "A2P.get_ind_name"
+*)
+let get_inner_types st v =
+try
+ let id = Ut.id_of_annterm v in
+ try match Hashtbl.find st.types id with
+ | {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"
+
+let get_inner_sort st v =
+try
+ let id = Ut.id_of_annterm v in
+ try Hashtbl.find st.sorts id
+ with Not_found -> `Type (CicUniv.fresh())
+with Invalid_argument _ -> failwith "A2P.get_sort"
+
+(* proof construction *******************************************************)
+
+let unused_premise = "UNUSED"
+
+let defined_premise = "DEFINED"
+
+let assumed_premise = "ASSUMED"
+
+let expanded_premise = "EXPANDED"
+
+let eta_expand n t =
+ let ty = C.AImplicit ("", None) in
+ let name i = Printf.sprintf "%s%u" expanded_premise i in
+ let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in
+ let arg i n = T.mk_arel (n - i) (name i) in
+ let rec aux i f a =
+ if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
+ in
+ let absts, args = aux 0 id [] in
+ match Cn.lift 1 n t with
+ | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
+ | t -> absts (C.AAppl ("", t :: args))
+
+let appl_expand n = function
+ | C.AAppl (id, ts) ->
+ let before, after = T.list_split (List.length ts + n) ts in
+ C.AAppl ("", C.AAppl (id, before) :: after)
+ | _ -> assert false
+
+let get_intro name t =
+try
+match name with
+ | C.Anonymous -> unused_premise
+ | C.Name s ->
+ if DTI.does_not_occur 1 (cic t) then unused_premise else s
+with Invalid_argument _ -> failwith "A2P.get_intro"
+
+let mk_intros st script =
+try
+ if st.intros = [] then script else
+ let count = List.length st.intros in
+ let p0 = T.Whd (count, "") in
+ let p1 = T.Intros (Some count, List.rev st.intros, "") in
+ match st.ety with
+ | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
+ | _ -> p1 :: script
+with Invalid_argument _ -> failwith "A2P.mk_intros"
+
+let rec mk_atomic st dtext what =
+ if T.is_atomic what then [], what else
+ let name = defined_premise in
+ mk_fwd_proof st dtext name what, T.mk_arel 0 name
+
+and mk_fwd_rewrite st dtext name tl direction =
+ let what, where = List.nth tl 5, List.nth tl 3 in
+ let rewrite premise =
+ let script, what = mk_atomic st dtext what in
+ T.Rewrite (direction, what, Some (premise, name), dtext) :: script
+ in
+ match where with
+ | C.ARel (_, _, _, binder) -> rewrite binder
+ | _ ->
+ assert (get_inner_sort st where = `Prop);
+ let pred, old = List.nth tl 2, List.nth tl 1 in
+ let pred_name = defined_premise in
+ let pred_text = "extracted" in
+ let p1 = T.LetIn (pred_name, pred, pred_text) in
+ let cut_name = assumed_premise in
+ let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
+ let cut_text = "" in
+ let p2 = T.Cut (cut_name, cut_type, cut_text) in
+ let qs = [rewrite cut_name; mk_proof (next st) where] in
+ [T.Branch (qs, ""); p2; p1]
+
+and mk_fwd_proof st dtext name = function
+ | C.AAppl (_, hd :: tl) as v ->
+ if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
+ if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
+ begin match get_inner_types st v with
+ | Some (ity, _) ->
+ let qs = [[T.Id ""]; mk_proof (next st) v] in
+ [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
+ | None ->
+ let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+ let (classes, rc) as h = Cl.classify st.context ty in
+ let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
+ [T.LetIn (name, v, dtext ^ text)]
+ end
+ | v ->
+ [T.LetIn (name, v, dtext)]
+
+and mk_proof st = function
+ | C.ALambda (_, name, v, t) as what ->
+ let entry = Some (name, C.Decl (cic v)) in
+ let intro = get_intro name t in
+ let ety = match get_inner_types st what with
+ | Some (_, ety) -> Some ety
+ | None -> None
+ in
+ mk_proof (add st entry intro ety) t
+ | C.ALetIn (_, name, v, t) as what ->
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let entry = Some (name, C.Def (cic v, None)) in
+ let intro = get_intro name t in
+ let q = mk_proof (next (add st entry intro None)) t in
+ List.rev_append (mk_fwd_proof st dtext intro v) q
+ else
+ [T.Apply (what, dtext)]
+ in
+ mk_intros st script
+ | C.ARel _ as what ->
+ let _, dtext = test_depth st in
+ let text = "assumption" in
+ let script = [T.Apply (what, dtext ^ text)] in
+ mk_intros st script
+ | C.AMutConstruct _ as what ->
+ let _, dtext = test_depth st in
+ let script = [T.Apply (what, dtext)] in
+ mk_intros st script
+ | C.AAppl (_, hd :: tl) as t ->
+ let proceed, dtext = test_depth st in
+ let script = if proceed then
+ let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
+ let (classes, rc) as h = Cl.classify st.context ty in
+ let decurry = List.length classes - List.length tl in
+ if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
+ if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
+ let synth = Cl.S.singleton 0 in
+ let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
+ match rc with
+ | Some (i, j) when i > 1 && i <= List.length classes ->
+ let classes, tl, _, what = split2_last classes tl in
+ let script, what = mk_atomic st dtext what in
+ let synth = Cl.S.add 1 synth in
+ let qs = mk_bkd_proofs (next st) synth classes tl in
+ if is_rewrite_right hd then
+ List.rev script @
+ [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
+ else if is_rewrite_left hd then
+ List.rev script @
+ [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
+ else
+ let using = Some hd in
+ List.rev script @
+ [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
+ | _ ->
+ let qs = mk_bkd_proofs (next st) synth classes tl in
+ let script, hd = mk_atomic st dtext hd in
+ List.rev script @
+ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
+ else
+ [T.Apply (t, dtext)]
+ in
+ mk_intros st script
+ | t ->
+ let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
+ let script = [T.Note text] in
+ mk_intros st script
+
+and mk_bkd_proofs st synth classes ts =
+try
+ let _, dtext = test_depth st in
+ let aux inv v =
+ if Cl.overlaps synth inv then None else
+ if Cl.S.is_empty inv then Some (mk_proof st v) else
+ Some [T.Apply (v, dtext ^ "dependent")]
+ in
+ T.list_map2_filter aux classes ts
+with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
+
+(* object costruction *******************************************************)
+
+let is_theorem pars =
+ List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
+ List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
+
+let mk_obj st = function
+ | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
+ let ast = mk_proof (set_ety st (Some t)) v in
+ let count = T.count_steps 0 ast in
+ let text = Printf.sprintf "tactics: %u" count in
+ T.Theorem (s, t, text) :: ast @ [T.Qed ""]
+ | _ ->
+ failwith "not a theorem"
+
+(* interface functions ******************************************************)
+
+let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
+ let st = {
+ sorts = ids_to_inner_sorts;
+ types = ids_to_inner_types;
+ prefix = prefix;
+ max_depth = depth;
+ depth = 0;
+ context = [];
+ intros = [];
+ ety = None
+ } in
+ prerr_endline "Level 2 transformation";
+ let steps = mk_obj st aobj in
+ prerr_endline "grafite rendering";
+ List.rev (T.render_steps [] 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/.
+ *)
+
+val acic2procedural:
+ 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.annobj ->
+ (Cic.annterm, Cic.annterm,
+ Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
+ GrafiteAst.statement list
+
--- /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 R = CicReduction
+module D = Deannotate
+module Int = struct
+ type t = int
+ let compare = compare
+end
+module S = Set.Make (Int)
+
+type conclusion = (int * int) option
+
+(* debugging ****************************************************************)
+
+let string_of_entry inverse =
+ if S.mem 0 inverse then "C" else
+ if S.is_empty inverse then "I" else "P"
+
+let to_string (classes, rc) =
+ let linearize = String.concat " " (List.map string_of_entry classes) in
+ match rc with
+ | None -> linearize
+ | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
+
+let out_table b =
+ let map i (_, inverse) =
+ let map i tl = Printf.sprintf "%2u" i :: tl in
+ let iset = String.concat " " (S.fold map inverse []) in
+ Printf.eprintf "%2u|%s\n" i iset
+ in
+ Array.iteri map b;
+ prerr_newline ()
+
+(****************************************************************************)
+
+let id x = x
+
+let rec list_fold_left g map = function
+ | [] -> g
+ | hd :: tl -> map (list_fold_left g map tl) hd
+
+let get_rels h t =
+ let rec aux d g = function
+ | C.Sort _
+ | C.Implicit _ -> g
+ | C.Rel i ->
+ if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
+ | C.Appl ss -> list_fold_left g (aux d) ss
+ | C.Const (_, ss)
+ | C.MutInd (_, _, ss)
+ | C.MutConstruct (_, _, _, ss)
+ | C.Var (_, ss) ->
+ let map g (_, t) = aux d g t in
+ list_fold_left g map ss
+ | C.Meta (_, ss) ->
+ let map g = function
+ | None -> g
+ | Some t -> aux d g t
+ in
+ list_fold_left g map ss
+ | C.Cast (t1, t2) -> aux d (aux d g t2) t1
+ | C.LetIn (_, t1, t2)
+ | C.Lambda (_, t1, t2)
+ | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
+ | C.MutCase (_, _, t1, t2, ss) ->
+ aux d (aux d (list_fold_left g (aux d) ss) t2) t1
+ | C.Fix (_, ss) ->
+ let k = List.length ss in
+ let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
+ list_fold_left g map ss
+ | C.CoFix (_, ss) ->
+ let k = List.length ss in
+ let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
+ list_fold_left g map ss
+ in
+ let g a = a in
+ aux 1 g t S.empty
+
+let split c t =
+ let add s v c = Some (s, C.Decl v) :: c in
+ let rec aux whd a n c = function
+ | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
+ | v when whd -> v :: a, n
+ | v -> aux true a n c (R.whd ~delta:true c v)
+ in
+ aux false [] 0 c t
+
+let classify_conclusion = function
+ | C.Rel i -> Some (i, 0)
+ | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
+ | _ -> None
+
+let classify c t =
+try
+ let vs, h = split c t in
+ let rc = classify_conclusion (List.hd vs) in
+ let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
+ let l, h = List.fold_left map ([], 0) vs in
+ let b = Array.of_list (List.rev l) in
+ let mk_closure b h =
+ let map j = if j < h then S.union (fst b.(j)) else id in
+ for i = pred h downto 0 do
+ let direct, unused = b.(i) in
+ b.(i) <- S.fold map direct direct, unused
+ done; b
+ in
+ let b = mk_closure b h in
+ let rec mk_inverse i direct =
+ if S.is_empty direct then () else
+ let j = S.choose direct in
+ if j < h then
+ let unused, inverse = b.(j) in
+ b.(j) <- unused, S.add i inverse
+ else ();
+ mk_inverse i (S.remove j direct)
+ in
+ let map i (direct, _) = mk_inverse i direct in
+ Array.iteri map b;
+(* out_table b; *)
+ List.rev_map snd (List.tl (Array.to_list b)), rc
+with Invalid_argument _ -> failwith "Classify.classify"
+
+let overlaps s1 s2 =
+ let predicate x = S.mem x s1 in
+ S.exists predicate s2
--- /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 S : Set.S with type elt = int
+
+type conclusion = (int * int) option
+
+val classify: Cic.context -> Cic.term -> S.t list * conclusion
+
+val to_string: S.t list * conclusion -> string
+
+val overlaps: S.t -> S.t -> bool
--- /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
+
+let rec need_whd i = function
+ | C.ACast (_, t, _) -> need_whd i t
+ | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
+ | _ when i > 0 -> true
+ | _ -> false
+
+let lift k n =
+ let rec lift_xns k (uri, t) = uri, lift_term k t
+ and lift_ms k = function
+ | None -> None
+ | Some t -> Some (lift_term k t)
+ and lift_fix len k (id, name, i, ty, bo) =
+ id, name, i, lift_term k ty, lift_term (k + len) bo
+ and lift_cofix len k (id, name, ty, bo) =
+ id, name, lift_term k ty, lift_term (k + len) bo
+ and lift_term k = function
+ | C.ASort _ as t -> t
+ | C.AImplicit _ as t -> t
+ | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b)
+ | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
+ | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
+ | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
+ | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
+ | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
+ | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
+ | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
+ | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
+ | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
+ | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
+ | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
+ | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
+ | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
+ in
+ lift_term k
--- /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/.
+ *)
+
+val need_whd: int -> Cic.annterm -> bool
+
+val lift: int -> int -> Cic.annterm -> Cic.annterm
--- /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 H = HExtlib
+module C = Cic
+module G = GrafiteAst
+module N = CicNotationPt
+
+(* functions to be moved ****************************************************)
+
+let list_map2_filter map l1 l2 =
+ let rec filter l = function
+ | [] -> l
+ | None :: tl -> filter l tl
+ | Some a :: tl -> filter (a :: l) tl
+ in
+ filter [] (List.rev_map2 map l1 l2)
+
+let rec list_split n l =
+ if n = 0 then [], l else
+ 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
+
+let is_atomic = function
+ | C.ASort _
+ | C.AConst _
+ | C.AMutInd _
+ | C.AMutConstruct _
+ | C.AVar _
+ | C.ARel _
+ | C.AMeta _
+ | C.AImplicit _ -> true
+ | _ -> false
+
+(****************************************************************************)
+
+type name = string
+type what = Cic.annterm
+type how = bool
+type using = Cic.annterm
+type count = int
+type note = string
+type where = (name * name) option
+
+type step = Note of note
+ | Theorem of name * what * note
+ | Qed of note
+ | Id of note
+ | Intros of count option * name list * note
+ | Cut of name * what * note
+ | LetIn of name * what * note
+ | Rewrite of how * what * where * note
+ | Elim of what * using option * note
+ | Apply of what * note
+ | Whd of count * note
+ | Branch of step list list * note
+
+(* annterm constructors *****************************************************)
+
+let mk_arel i b = Cic.ARel ("", "", i, b)
+
+(* grafite ast constructors *************************************************)
+
+let floc = H.dummy_floc
+
+let hole = C.AImplicit ("", Some `Hole)
+
+let mk_note str = G.Comment (floc, G.Note (floc, str))
+
+let mk_theorem name t =
+ let obj = N.Theorem (`Theorem, name, t, None) in
+ G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+
+let mk_qed =
+ G.Executable (floc, G.Command (floc, G.Qed floc))
+
+let mk_tactic tactic =
+ G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None))
+
+let mk_id =
+ let tactic = G.IdTac floc in
+ mk_tactic tactic
+
+let mk_intros xi ids =
+ let tactic = G.Intros (floc, xi, ids) in
+ mk_tactic tactic
+
+let mk_cut name what =
+ let tactic = G.Cut (floc, Some name, what) in
+ mk_tactic tactic
+
+let mk_letin name what =
+ let tactic = G.LetIn (floc, what, name) in
+ mk_tactic tactic
+
+let mk_rewrite direction what where =
+ let direction = if direction then `RightToLeft else `LeftToRight in
+ let pattern, rename = match where with
+ | None -> (None, [], Some hole), []
+ | Some (premise, name) -> (None, [premise, hole], None), [name]
+ in
+ let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
+ mk_tactic tactic
+
+let mk_elim what using =
+ let tactic = G.Elim (floc, what, using, Some 0, []) in
+ mk_tactic tactic
+
+let mk_apply t =
+ let tactic = G.Apply (floc, t) in
+ mk_tactic tactic
+
+let mk_whd i =
+ let pattern = None, [], Some hole in
+ let tactic = G.Reduce (floc, `Whd, pattern) in
+ mk_tactic tactic
+
+let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
+
+let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
+
+let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None))
+
+let mk_cb = G.Executable (floc, G.Tactical (floc, G.Merge floc, None))
+
+let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
+
+(* rendering ****************************************************************)
+
+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
+ | Id s -> mk_note s :: cont sep (mk_id :: a)
+ | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
+ | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)
+ | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
+ | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
+ | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
+ | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
+ | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a)
+ | Branch ([], s) -> a
+ | Branch ([ps], s) -> render_steps sep a ps
+ | Branch (pss, s) ->
+ let a = mk_ob :: a in
+ let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in
+ mk_note s :: cont sep body
+
+and render_steps sep a = function
+ | [] -> a
+ | [p] -> render_step sep a p
+ | p :: Branch ([], _) :: ps ->
+ render_steps sep a (p :: ps)
+ | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
+ render_steps sep (render_step (Some mk_sc) a p) ps
+ | p :: ps ->
+ render_steps sep (render_step (Some mk_dot) a p) ps
+
+let render_steps a = render_steps None a
+
+(* counting *****************************************************************)
+
+let rec count_step a = function
+ | Note _
+ | Theorem _
+ | Qed _ -> a
+ | Branch (pps, _) -> List.fold_left count_steps a pps
+ | _ -> succ a
+
+and count_steps a = List.fold_left count_step a
--- /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/.
+ *)
+
+(* functions to be moved ****************************************************)
+
+val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
+
+val list_split: int -> 'a list -> 'a list * 'a list
+
+val mk_arel: int -> string -> Cic.annterm
+
+val is_atomic:Cic.annterm -> bool
+
+(****************************************************************************)
+
+type name = string
+type what = Cic.annterm
+type how = bool
+type using = Cic.annterm
+type count = int
+type note = string
+type where = (name * name) option
+
+type step = Note of note
+ | Theorem of name * what * note
+ | Qed of note
+ | Id of note
+ | Intros of count option * name list * note
+ | Cut of name * what * note
+ | LetIn of name * what * note
+ | Rewrite of how * what * where * note
+ | Elim of what * using option * note
+ | Apply of what * note
+ | Whd of count * note
+ | Branch of step list list * note
+
+val render_steps:
+ (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list ->
+ step list ->
+ (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list
+
+val count_steps:
+ int -> step list -> int
cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
cicNotationPres.cmx box.cmx content2pres.cmi
-cicClassify.cmo: cicClassify.cmi
-cicClassify.cmx: cicClassify.cmi
-proceduralConversion.cmo: proceduralConversion.cmi
-proceduralConversion.cmx: proceduralConversion.cmi
-proceduralTypes.cmo: proceduralTypes.cmi
-proceduralTypes.cmx: proceduralTypes.cmi
-acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi
-objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \
- acic2Procedural.cmi objPp.cmi
-objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \
- acic2Procedural.cmx objPp.cmi
sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
box.cmi sequent2pres.cmi
sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
cicNotationPres.cmi box.cmi content2pres.cmi
content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
cicNotationPres.cmx box.cmx content2pres.cmi
-cicClassify.cmo: cicClassify.cmi
-cicClassify.cmx: cicClassify.cmi
-proceduralConversion.cmo: proceduralConversion.cmi
-proceduralConversion.cmx: proceduralConversion.cmi
-proceduralTypes.cmo: proceduralTypes.cmi
-proceduralTypes.cmx: proceduralTypes.cmi
-acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi
-acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi
-objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \
- acic2Procedural.cmi objPp.cmi
-objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \
- acic2Procedural.cmx objPp.cmi
sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
box.cmi sequent2pres.cmi
sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
cicNotationPres.mli \
boxPp.mli \
content2pres.mli \
- cicClassify.mli \
- proceduralConversion.mli \
- proceduralTypes.mli \
- acic2Procedural.mli \
- objPp.mli \
sequent2pres.mli \
$(NULL)
IMPLEMENTATION_FILES = \
+++ /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 D = Deannotate
-module DTI = DoubleTypeInference
-module TC = CicTypeChecker
-module Un = CicUniv
-module UM = UriManager
-module Obj = LibraryObjects
-module HObj = HelmLibraryObjects
-module A = Cic2acic
-module Ut = CicUtil
-module E = CicEnvironment
-
-module Cl = CicClassify
-module T = ProceduralTypes
-module Cn = ProceduralConversion
-
-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;
- intros: string list;
- ety: C.annterm option
-}
-
-(* helpers ******************************************************************)
-
-let id x = x
-
-let comp f g x = f (g x)
-
-let cic = D.deannotate_term
-
-let split2_last l1 l2 =
-try
- let n = pred (List.length l1) in
- let before1, after1 = T.list_split n l1 in
- let before2, after2 = T.list_split n l2 in
- before1, before2, List.hd after1, List.hd after2
-with Invalid_argument _ -> failwith "A2P.split2_last"
-
-let string_of_head = function
- | C.ASort _ -> "sort"
- | C.AConst _ -> "const"
- | C.AMutInd _ -> "mutind"
- | C.AMutConstruct _ -> "mutconstruct"
- | C.AVar _ -> "var"
- | C.ARel _ -> "rel"
- | C.AProd _ -> "prod"
- | C.ALambda _ -> "lambda"
- | C.ALetIn _ -> "letin"
- | C.AFix _ -> "fix"
- | C.ACoFix _ -> "cofix"
- | C.AAppl _ -> "appl"
- | C.ACast _ -> "cast"
- | C.AMutCase _ -> "mutcase"
- | C.AMeta _ -> "meta"
- | C.AImplicit _ -> "implict"
-
-let clear st = {st with intros = []; ety = None}
-
-let next st = {(clear st) with depth = succ st.depth}
-
-let set_ety st ety =
- if st.ety = None then {st with ety = ety} else st
-
-let add st entry intro ety =
- let st = set_ety st ety in
- {st with context = entry :: st.context; intros = intro :: st.intros}
-
-let test_depth st =
-try
- let msg = Printf.sprintf "Depth %u: " st.depth in
- match st.max_depth with
- | None -> true, ""
- | Some d -> if st.depth < d then true, msg else false, "DEPTH EXCEDED: "
-with Invalid_argument _ -> failwith "A2P.test_depth"
-
-let is_rewrite_right = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri
- | _ -> false
-
-let is_rewrite_left = function
- | C.AConst (_, uri, []) ->
- UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri
- | _ -> false
-(*
-let get_ind_name uri tno xcno =
-try
- let ts = match E.get_obj Un.empty_ugraph uri with
- | C.InductiveDefinition (ts, _, _,_), _ -> ts
- | _ -> assert false
- in
- let tname, cs = match List.nth ts tno with
- | (name, _, _, cs) -> name, cs
- in
- match xcno with
- | None -> tname
- | Some cno -> fst (List.nth cs (pred cno))
-with Invalid_argument _ -> failwith "A2P.get_ind_name"
-*)
-let get_inner_types st v =
-try
- let id = Ut.id_of_annterm v in
- try match Hashtbl.find st.types id with
- | {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"
-
-let get_inner_sort st v =
-try
- let id = Ut.id_of_annterm v in
- try Hashtbl.find st.sorts id
- with Not_found -> `Type (CicUniv.fresh())
-with Invalid_argument _ -> failwith "A2P.get_sort"
-
-(* proof construction *******************************************************)
-
-let unused_premise = "UNUSED"
-
-let defined_premise = "DEFINED"
-
-let assumed_premise = "ASSUMED"
-
-let expanded_premise = "EXPANDED"
-
-let eta_expand n t =
- let ty = C.AImplicit ("", None) in
- let name i = Printf.sprintf "%s%u" expanded_premise i in
- let lambda i t = C.ALambda ("", C.Name (name i), ty, t) in
- let arg i n = T.mk_arel (n - i) (name i) in
- let rec aux i f a =
- if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
- in
- let absts, args = aux 0 id [] in
- match Cn.lift 1 n t with
- | C.AAppl (id, ts) -> absts (C.AAppl (id, ts @ args))
- | t -> absts (C.AAppl ("", t :: args))
-
-let appl_expand n = function
- | C.AAppl (id, ts) ->
- let before, after = T.list_split (List.length ts + n) ts in
- C.AAppl ("", C.AAppl (id, before) :: after)
- | _ -> assert false
-
-let get_intro name t =
-try
-match name with
- | C.Anonymous -> unused_premise
- | C.Name s ->
- if DTI.does_not_occur 1 (cic t) then unused_premise else s
-with Invalid_argument _ -> failwith "A2P.get_intro"
-
-let mk_intros st script =
-try
- if st.intros = [] then script else
- let count = List.length st.intros in
- let p0 = T.Whd (count, "") in
- let p1 = T.Intros (Some count, List.rev st.intros, "") in
- match st.ety with
- | Some ety when Cn.need_whd count ety -> p0 :: p1 :: script
- | _ -> p1 :: script
-with Invalid_argument _ -> failwith "A2P.mk_intros"
-
-let rec mk_atomic st dtext what =
- if T.is_atomic what then [], what else
- let name = defined_premise in
- mk_fwd_proof st dtext name what, T.mk_arel 0 name
-
-and mk_fwd_rewrite st dtext name tl direction =
- let what, where = List.nth tl 5, List.nth tl 3 in
- let rewrite premise =
- let script, what = mk_atomic st dtext what in
- T.Rewrite (direction, what, Some (premise, name), dtext) :: script
- in
- match where with
- | C.ARel (_, _, _, binder) -> rewrite binder
- | _ ->
- assert (get_inner_sort st where = `Prop);
- let pred, old = List.nth tl 2, List.nth tl 1 in
- let pred_name = defined_premise in
- let pred_text = "extracted" in
- let p1 = T.LetIn (pred_name, pred, pred_text) in
- let cut_name = assumed_premise in
- let cut_type = C.AAppl ("", [T.mk_arel 0 pred_name; old]) in
- let cut_text = "" in
- let p2 = T.Cut (cut_name, cut_type, cut_text) in
- let qs = [rewrite cut_name; mk_proof (next st) where] in
- [T.Branch (qs, ""); p2; p1]
-
-and mk_fwd_proof st dtext name = function
- | C.AAppl (_, hd :: tl) as v ->
- if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else
- if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else
- begin match get_inner_types st v with
- | Some (ity, _) ->
- let qs = [[T.Id ""]; mk_proof (next st) v] in
- [T.Branch (qs, ""); T.Cut (name, ity, dtext)]
- | None ->
- let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
- let (classes, rc) as h = Cl.classify st.context ty in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- [T.LetIn (name, v, dtext ^ text)]
- end
- | v ->
- [T.LetIn (name, v, dtext)]
-
-and mk_proof st = function
- | C.ALambda (_, name, v, t) as what ->
- let entry = Some (name, C.Decl (cic v)) in
- let intro = get_intro name t in
- let ety = match get_inner_types st what with
- | Some (_, ety) -> Some ety
- | None -> None
- in
- mk_proof (add st entry intro ety) t
- | C.ALetIn (_, name, v, t) as what ->
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let entry = Some (name, C.Def (cic v, None)) in
- let intro = get_intro name t in
- let q = mk_proof (next (add st entry intro None)) t in
- List.rev_append (mk_fwd_proof st dtext intro v) q
- else
- [T.Apply (what, dtext)]
- in
- mk_intros st script
- | C.ARel _ as what ->
- let _, dtext = test_depth st in
- let text = "assumption" in
- let script = [T.Apply (what, dtext ^ text)] in
- mk_intros st script
- | C.AMutConstruct _ as what ->
- let _, dtext = test_depth st in
- let script = [T.Apply (what, dtext)] in
- mk_intros st script
- | C.AAppl (_, hd :: tl) as t ->
- let proceed, dtext = test_depth st in
- let script = if proceed then
- let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in
- let (classes, rc) as h = Cl.classify st.context ty in
- let decurry = List.length classes - List.length tl in
- if decurry < 0 then mk_proof (clear st) (appl_expand decurry t) else
- if decurry > 0 then mk_proof (clear st) (eta_expand decurry t) else
- let synth = Cl.S.singleton 0 in
- let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in
- match rc with
- | Some (i, j) when i > 1 && i <= List.length classes ->
- let classes, tl, _, what = split2_last classes tl in
- let script, what = mk_atomic st dtext what in
- let synth = Cl.S.add 1 synth in
- let qs = mk_bkd_proofs (next st) synth classes tl in
- if is_rewrite_right hd then
- List.rev script @
- [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")]
- else if is_rewrite_left hd then
- List.rev script @
- [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")]
- else
- let using = Some hd in
- List.rev script @
- [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")]
- | _ ->
- let qs = mk_bkd_proofs (next st) synth classes tl in
- let script, hd = mk_atomic st dtext hd in
- List.rev script @
- [T.Apply (hd, dtext ^ text); T.Branch (qs, "")]
- else
- [T.Apply (t, dtext)]
- in
- mk_intros st script
- | t ->
- let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
- let script = [T.Note text] in
- mk_intros st script
-
-and mk_bkd_proofs st synth classes ts =
-try
- let _, dtext = test_depth st in
- let aux inv v =
- if Cl.overlaps synth inv then None else
- if Cl.S.is_empty inv then Some (mk_proof st v) else
- Some [T.Apply (v, dtext ^ "dependent")]
- in
- T.list_map2_filter aux classes ts
-with Invalid_argument _ -> failwith "A2P.mk_bkd_proofs"
-
-(* object costruction *******************************************************)
-
-let is_theorem pars =
- List.mem (`Flavour `Theorem) pars || List.mem (`Flavour `Fact) pars ||
- List.mem (`Flavour `Remark) pars || List.mem (`Flavour `Lemma) pars
-
-let mk_obj st = function
- | C.AConstant (_, _, s, Some v, t, [], pars) when is_theorem pars ->
- let ast = mk_proof (set_ety st (Some t)) v in
- let count = T.count_steps 0 ast in
- let text = Printf.sprintf "tactics: %u" count in
- T.Theorem (s, t, text) :: ast @ [T.Qed ""]
- | _ ->
- failwith "not a theorem"
-
-(* interface functions ******************************************************)
-
-let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj =
- let st = {
- sorts = ids_to_inner_sorts;
- types = ids_to_inner_types;
- prefix = prefix;
- max_depth = depth;
- depth = 0;
- context = [];
- intros = [];
- ety = None
- } in
- prerr_endline "Level 2 transformation";
- let steps = mk_obj st aobj in
- prerr_endline "grafite rendering";
- List.rev (T.render_steps [] 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/.
- *)
-
-val acic2procedural:
- 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.annobj ->
- (Cic.annterm, Cic.annterm,
- Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string)
- GrafiteAst.statement list
-
+++ /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 R = CicReduction
-module D = Deannotate
-module Int = struct
- type t = int
- let compare = compare
-end
-module S = Set.Make (Int)
-
-type conclusion = (int * int) option
-
-(* debugging ****************************************************************)
-
-let string_of_entry inverse =
- if S.mem 0 inverse then "C" else
- if S.is_empty inverse then "I" else "P"
-
-let to_string (classes, rc) =
- let linearize = String.concat " " (List.map string_of_entry classes) in
- match rc with
- | None -> linearize
- | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
-
-let out_table b =
- let map i (_, inverse) =
- let map i tl = Printf.sprintf "%2u" i :: tl in
- let iset = String.concat " " (S.fold map inverse []) in
- Printf.eprintf "%2u|%s\n" i iset
- in
- Array.iteri map b;
- prerr_newline ()
-
-(****************************************************************************)
-
-let id x = x
-
-let rec list_fold_left g map = function
- | [] -> g
- | hd :: tl -> map (list_fold_left g map tl) hd
-
-let get_rels h t =
- let rec aux d g = function
- | C.Sort _
- | C.Implicit _ -> g
- | C.Rel i ->
- if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
- | C.Appl ss -> list_fold_left g (aux d) ss
- | C.Const (_, ss)
- | C.MutInd (_, _, ss)
- | C.MutConstruct (_, _, _, ss)
- | C.Var (_, ss) ->
- let map g (_, t) = aux d g t in
- list_fold_left g map ss
- | C.Meta (_, ss) ->
- let map g = function
- | None -> g
- | Some t -> aux d g t
- in
- list_fold_left g map ss
- | C.Cast (t1, t2) -> aux d (aux d g t2) t1
- | C.LetIn (_, t1, t2)
- | C.Lambda (_, t1, t2)
- | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
- | C.MutCase (_, _, t1, t2, ss) ->
- aux d (aux d (list_fold_left g (aux d) ss) t2) t1
- | C.Fix (_, ss) ->
- let k = List.length ss in
- let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
- list_fold_left g map ss
- | C.CoFix (_, ss) ->
- let k = List.length ss in
- let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
- list_fold_left g map ss
- in
- let g a = a in
- aux 1 g t S.empty
-
-let split c t =
- let add s v c = Some (s, C.Decl v) :: c in
- let rec aux whd a n c = function
- | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
- | v when whd -> v :: a, n
- | v -> aux true a n c (R.whd ~delta:true c v)
- in
- aux false [] 0 c t
-
-let classify_conclusion = function
- | C.Rel i -> Some (i, 0)
- | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
- | _ -> None
-
-let classify c t =
-try
- let vs, h = split c t in
- let rc = classify_conclusion (List.hd vs) in
- let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
- let l, h = List.fold_left map ([], 0) vs in
- let b = Array.of_list (List.rev l) in
- let mk_closure b h =
- let map j = if j < h then S.union (fst b.(j)) else id in
- for i = pred h downto 0 do
- let direct, unused = b.(i) in
- b.(i) <- S.fold map direct direct, unused
- done; b
- in
- let b = mk_closure b h in
- let rec mk_inverse i direct =
- if S.is_empty direct then () else
- let j = S.choose direct in
- if j < h then
- let unused, inverse = b.(j) in
- b.(j) <- unused, S.add i inverse
- else ();
- mk_inverse i (S.remove j direct)
- in
- let map i (direct, _) = mk_inverse i direct in
- Array.iteri map b;
-(* out_table b; *)
- List.rev_map snd (List.tl (Array.to_list b)), rc
-with Invalid_argument _ -> failwith "Classify.classify"
-
-let overlaps s1 s2 =
- let predicate x = S.mem x s1 in
- S.exists predicate s2
+++ /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 S : Set.S with type elt = int
-
-type conclusion = (int * int) option
-
-val classify: Cic.context -> Cic.term -> S.t list * conclusion
-
-val to_string: S.t list * conclusion -> string
-
-val overlaps: S.t -> S.t -> bool
+++ /dev/null
-(* Copyright (C) 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://helm.cs.unibo.it/
- *)
-
-let remove_closed_substs s =
- Pcre.replace ~pat:"{...}" ~templ:"" s
-
-let term2pres n ids_to_inner_sorts annterm =
- let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
- in
- let bobj =
- CicNotationPres.box_of_mpres (
- CicNotationPres.render ~prec:90 ids_to_uris
- (TermContentPres.pp_ast ast)
- )
- in
- let render = function _::x::_ -> x | _ -> assert false in
- let mpres = CicNotationPres.mpres_of_box bobj in
- let s = BoxPp.render_to_string render n mpres in
- remove_closed_substs s
-
-let obj_to_string n style prefix obj =
- let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
- try Cic2acic.acic_object_of_cic_object obj
- with e ->
- let msg = "Cic2ACic: " ^ Printexc.to_string e in
- failwith msg
- in
- match style with
- | GrafiteAst.Declarative ->
- let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
- let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
- remove_closed_substs ("\n\n" ^
- BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
- )
- | GrafiteAst.Procedural depth ->
- let term_pp = term2pres (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 ~term_pp ~lazy_term_pp ~obj_pp in
- let script = Acic2Procedural.acic2procedural
- ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
- "\n\n" ^ String.concat "" (List.map aux script)
+++ /dev/null
-(* Copyright (C) 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://helm.cs.unibo.it/
- *)
-
-(* columns, rendering style, name prefix, object *)
-val obj_to_string:
- int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string
+++ /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
-
-let rec need_whd i = function
- | C.ACast (_, t, _) -> need_whd i t
- | C.AProd (_, _, _, t) when i > 0 -> need_whd (pred i) t
- | _ when i > 0 -> true
- | _ -> false
-
-let lift k n =
- let rec lift_xns k (uri, t) = uri, lift_term k t
- and lift_ms k = function
- | None -> None
- | Some t -> Some (lift_term k t)
- and lift_fix len k (id, name, i, ty, bo) =
- id, name, i, lift_term k ty, lift_term (k + len) bo
- and lift_cofix len k (id, name, ty, bo) =
- id, name, lift_term k ty, lift_term (k + len) bo
- and lift_term k = function
- | C.ASort _ as t -> t
- | C.AImplicit _ as t -> t
- | C.ARel (id, rid, m, b) as t -> if m < k then t else C.ARel (id, rid, m + n, b)
- | C.AConst (id, uri, xnss) -> C.AConst (id, uri, List.map (lift_xns k) xnss)
- | C.AVar (id, uri, xnss) -> C.AVar (id, uri, List.map (lift_xns k) xnss)
- | C.AMutInd (id, uri, tyno, xnss) -> C.AMutInd (id, uri, tyno, List.map (lift_xns k) xnss)
- | C.AMutConstruct (id, uri, tyno, consno, xnss) -> C.AMutConstruct (id, uri,tyno,consno, List.map (lift_xns k) xnss)
- | C.AMeta (id, i, mss) -> C.AMeta(id, i, List.map (lift_ms k) mss)
- | C.AAppl (id, ts) -> C.AAppl (id, List.map (lift_term k) ts)
- | C.ACast (id, te, ty) -> C.ACast (id, lift_term k te, lift_term k ty)
- | C.AMutCase (id, sp, i, outty, t, pl) -> C.AMutCase (id, sp, i, lift_term k outty, lift_term k t, List.map (lift_term k) pl)
- | C.AProd (id, n, s, t) -> C.AProd (id, n, lift_term k s, lift_term (succ k) t)
- | C.ALambda (id, n, s, t) -> C.ALambda (id, n, lift_term k s, lift_term (succ k) t)
- | C.ALetIn (id, n, s, t) -> C.ALetIn (id, n, lift_term k s, lift_term (succ k) t)
- | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (lift_fix (List.length fl) k) fl)
- | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (lift_cofix (List.length fl) k) fl)
- in
- lift_term k
+++ /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/.
- *)
-
-val need_whd: int -> Cic.annterm -> bool
-
-val lift: int -> int -> Cic.annterm -> Cic.annterm
+++ /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 H = HExtlib
-module C = Cic
-module G = GrafiteAst
-module N = CicNotationPt
-
-(* functions to be moved ****************************************************)
-
-let list_map2_filter map l1 l2 =
- let rec filter l = function
- | [] -> l
- | None :: tl -> filter l tl
- | Some a :: tl -> filter (a :: l) tl
- in
- filter [] (List.rev_map2 map l1 l2)
-
-let rec list_split n l =
- if n = 0 then [], l else
- 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
-
-let is_atomic = function
- | C.ASort _
- | C.AConst _
- | C.AMutInd _
- | C.AMutConstruct _
- | C.AVar _
- | C.ARel _
- | C.AMeta _
- | C.AImplicit _ -> true
- | _ -> false
-
-(****************************************************************************)
-
-type name = string
-type what = Cic.annterm
-type how = bool
-type using = Cic.annterm
-type count = int
-type note = string
-type where = (name * name) option
-
-type step = Note of note
- | Theorem of name * what * note
- | Qed of note
- | Id of note
- | Intros of count option * name list * note
- | Cut of name * what * note
- | LetIn of name * what * note
- | Rewrite of how * what * where * note
- | Elim of what * using option * note
- | Apply of what * note
- | Whd of count * note
- | Branch of step list list * note
-
-(* annterm constructors *****************************************************)
-
-let mk_arel i b = Cic.ARel ("", "", i, b)
-
-(* grafite ast constructors *************************************************)
-
-let floc = H.dummy_floc
-
-let hole = C.AImplicit ("", Some `Hole)
-
-let mk_note str = G.Comment (floc, G.Note (floc, str))
-
-let mk_theorem name t =
- let obj = N.Theorem (`Theorem, name, t, None) in
- G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
-
-let mk_qed =
- G.Executable (floc, G.Command (floc, G.Qed floc))
-
-let mk_tactic tactic =
- G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None))
-
-let mk_id =
- let tactic = G.IdTac floc in
- mk_tactic tactic
-
-let mk_intros xi ids =
- let tactic = G.Intros (floc, xi, ids) in
- mk_tactic tactic
-
-let mk_cut name what =
- let tactic = G.Cut (floc, Some name, what) in
- mk_tactic tactic
-
-let mk_letin name what =
- let tactic = G.LetIn (floc, what, name) in
- mk_tactic tactic
-
-let mk_rewrite direction what where =
- let direction = if direction then `RightToLeft else `LeftToRight in
- let pattern, rename = match where with
- | None -> (None, [], Some hole), []
- | Some (premise, name) -> (None, [premise, hole], None), [name]
- in
- let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
- mk_tactic tactic
-
-let mk_elim what using =
- let tactic = G.Elim (floc, what, using, Some 0, []) in
- mk_tactic tactic
-
-let mk_apply t =
- let tactic = G.Apply (floc, t) in
- mk_tactic tactic
-
-let mk_whd i =
- let pattern = None, [], Some hole in
- let tactic = G.Reduce (floc, `Whd, pattern) in
- mk_tactic tactic
-
-let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
-
-let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
-
-let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None))
-
-let mk_cb = G.Executable (floc, G.Tactical (floc, G.Merge floc, None))
-
-let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
-
-(* rendering ****************************************************************)
-
-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
- | Id s -> mk_note s :: cont sep (mk_id :: a)
- | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
- | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a)
- | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a)
- | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a)
- | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a)
- | Apply (t, s) -> mk_note s :: cont sep (mk_apply t :: a)
- | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a)
- | Branch ([], s) -> a
- | Branch ([ps], s) -> render_steps sep a ps
- | Branch (pss, s) ->
- let a = mk_ob :: a in
- let body = mk_cb :: list_rev_map_concat (render_steps None) mk_vb a pss in
- mk_note s :: cont sep body
-
-and render_steps sep a = function
- | [] -> a
- | [p] -> render_step sep a p
- | p :: Branch ([], _) :: ps ->
- render_steps sep a (p :: ps)
- | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
- render_steps sep (render_step (Some mk_sc) a p) ps
- | p :: ps ->
- render_steps sep (render_step (Some mk_dot) a p) ps
-
-let render_steps a = render_steps None a
-
-(* counting *****************************************************************)
-
-let rec count_step a = function
- | Note _
- | Theorem _
- | Qed _ -> a
- | Branch (pps, _) -> List.fold_left count_steps a pps
- | _ -> succ a
-
-and count_steps a = List.fold_left count_step a
+++ /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/.
- *)
-
-(* functions to be moved ****************************************************)
-
-val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
-
-val list_split: int -> 'a list -> 'a list * 'a list
-
-val mk_arel: int -> string -> Cic.annterm
-
-val is_atomic:Cic.annterm -> bool
-
-(****************************************************************************)
-
-type name = string
-type what = Cic.annterm
-type how = bool
-type using = Cic.annterm
-type count = int
-type note = string
-type where = (name * name) option
-
-type step = Note of note
- | Theorem of name * what * note
- | Qed of note
- | Id of note
- | Intros of count option * name list * note
- | Cut of name * what * note
- | LetIn of name * what * note
- | Rewrite of how * what * where * note
- | Elim of what * using option * note
- | Apply of what * note
- | Whd of count * note
- | Branch of step list list * note
-
-val render_steps:
- (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list ->
- step list ->
- (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list
-
-val count_steps:
- int -> step list -> int
| BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
| BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
+let out = ref ignore
+
+let set_callback f = out := f
+
EXTEND
GLOBAL: term statement;
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
fun ~include_paths status ->
- let status = LexiconEngine.eval_command status scom in
+ !out scom;
+ let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file
]
LexiconEngine.status ->
LexiconEngine.status * ast_statement localized_option
+(* this callback is called on every lexicon command *)
+val set_callback: (LexiconAst.command -> unit) -> unit
+
val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *)
val statement: statement Grammar.Entry.e
Topo.topological_sort uris
(fun uri -> fst (List.split (direct_deps ~dbd uri)))
+let sorted_uris_of_baseuri ~dbd baseuri =
+ let sql_pat =
+ Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" baseuri ^ "%"
+ in
+ let query =
+ Printf.sprintf
+ ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^
+ "SELECT source FROM %s WHERE source LIKE \"%s\"")
+ (MetadataTypes.name_tbl ()) sql_pat
+ MetadataTypes.library_name_tbl sql_pat
+ in
+ let result = HMysql.exec dbd query in
+ let map cols = match cols.(0) with
+ | Some s -> UriManager.uri_of_string s
+ | _ -> assert false
+ in
+ let uris = HMysql.map result map in
+ let sorted_uris = topological_sort ~dbd uris in
+ let filter_map uri =
+ let s =
+ Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
+ (UriManager.string_of_uri uri)
+ in
+ try ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s); None
+ with Not_found -> Some (UriManager.uri_of_string s)
+ in
+ HExtlib.filter_map filter_map sorted_uris
+
module DepGraph =
struct
module UriTbl = UriManager.UriHashtbl
val topological_sort:
dbd:HMysql.dbd -> UriManager.uri list -> UriManager.uri list
+val sorted_uris_of_baseuri:
+ dbd:HMysql.dbd -> string -> UriManager.uri list
+
(** Representation of a (lazy) dependency graph.
* Imperative data structure. *)
module DepGraph:
matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \
- matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi
+ matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi \
+ applyTransformation.cmi matitacLib.cmi
matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
- matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi
+ matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitacLib.cmi
matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \
- matitacLib.cmi gragrep.cmi
+ matitacLib.cmi matitaWiki.cmo gragrep.cmi
matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
- matitacLib.cmx gragrep.cmx
+ matitacLib.cmx matitaWiki.cmx gragrep.cmx
matitadep.cmo: matitaInit.cmi matitadep.cmi
matitadep.cmx: matitaInit.cmx matitadep.cmi
matitaEngine.cmo: matitaEngine.cmi
matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi
matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi
matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
- matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi
+ matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \
+ applyTransformation.cmi
matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
- matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx
+ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \
+ applyTransformation.cmx
matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
buildTimeConf.cmi matitaprover.cmi
matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
applyTransformation.cmx matitaScript.cmi
matitaTypes.cmo: matitaTypes.cmi
matitaTypes.cmx: matitaTypes.cmi
+matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
+ buildTimeConf.cmi applyTransformation.cmi
+matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
+ buildTimeConf.cmx applyTransformation.cmx
matitaGtkMisc.cmi: matitaGeneratedGui.cmo
matitaGui.cmi: matitaGuiTypes.cmi
matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo
matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \
- matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi
+ matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi \
+ applyTransformation.cmi matitacLib.cmi
matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \
- matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi
+ matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitacLib.cmi
matitac.cmo: matitaprover.cmi matitamake.cmi matitadep.cmi matitaclean.cmi \
- matitacLib.cmi gragrep.cmi
+ matitacLib.cmi matitaWiki.cmx gragrep.cmi
matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \
- matitacLib.cmx gragrep.cmx
+ matitacLib.cmx matitaWiki.cmx gragrep.cmx
matitadep.cmo: matitaInit.cmi matitadep.cmi
matitadep.cmx: matitaInit.cmx matitadep.cmi
matitaEngine.cmo: matitaEngine.cmi
matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi
matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi
matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
- matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi
+ matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi \
+ applyTransformation.cmi
matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
- matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx
+ matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx \
+ applyTransformation.cmx
matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
buildTimeConf.cmi matitaprover.cmi
matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
applyTransformation.cmx matitaScript.cmi
matitaTypes.cmo: matitaTypes.cmi
matitaTypes.cmx: matitaTypes.cmi
+matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
+ buildTimeConf.cmi applyTransformation.cmi
+matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
+ buildTimeConf.cmx applyTransformation.cmx
matitaGtkMisc.cmi: matitaGeneratedGui.cmx
matitaGui.cmi: matitaGuiTypes.cmi
matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx
matitaInit.cmo \
matitaExcPp.cmo \
matitaEngine.cmo \
+ applyTransformation.cmo \
matitacLib.cmo \
matitaprover.cmo \
- applyTransformation.cmo \
matitaGtkMisc.cmo \
matitaScript.cmo \
matitaGeneratedGui.cmo \
matitaInit.cmo \
matitaExcPp.cmo \
matitaEngine.cmo \
- matitacLib.cmo \
applyTransformation.cmo \
+ matitacLib.cmo \
matitaWiki.cmo \
matitaprover.cmo \
$(NULL)
let txt_of_cic_term size metasenv context t =
let fake_sequent = (-1,context,t) in
txt_of_cic_sequent_conclusion size metasenv fake_sequent
+
+(****************************************************************************)
+(* txt_of_cic_object: IMPROVE ME *)
+
+let remove_closed_substs s =
+ Pcre.replace ~pat:"{...}" ~templ:"" s
+
+let term2pres n ids_to_inner_sorts annterm =
+ let ast, ids_to_uris =
+ TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+ in
+ let bobj =
+ CicNotationPres.box_of_mpres (
+ CicNotationPres.render ~prec:90 ids_to_uris
+ (TermContentPres.pp_ast ast)
+ )
+ in
+ let render = function _::x::_ -> x | _ -> assert false in
+ let mpres = CicNotationPres.mpres_of_box bobj in
+ let s = BoxPp.render_to_string render n mpres in
+ remove_closed_substs s
+
+let txt_of_cic_object n style prefix obj =
+ let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+ try Cic2acic.acic_object_of_cic_object obj
+ with e ->
+ let msg = "Cic2ACic: " ^ Printexc.to_string e in
+ failwith msg
+ in
+ match style with
+ | GrafiteAst.Declarative ->
+ let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
+ let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
+ remove_closed_substs ("\n\n" ^
+ BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
+ )
+ | GrafiteAst.Procedural depth ->
+ let term_pp = term2pres (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 ~term_pp ~lazy_term_pp ~obj_pp in
+ let script = Acic2Procedural.acic2procedural
+ ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
+ "\n\n" ^ String.concat "" (List.map aux script)
+
+let txt_of_inline_macro style suri prefix =
+ let dbd = LibraryDb.instance () in
+ let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
+ let map uri =
+ try txt_of_cic_object 78 style prefix (* FG: mi pare meglio 78 *)
+ (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+ with
+ | e ->
+ Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n"
+ (UriManager.string_of_uri uri) (Printexc.to_string e)
+ in
+ String.concat "\n\n" (List.map map sorted_uris)
val txt_of_cic_sequent_conclusion:
int -> Cic.metasenv -> Cic.conjecture -> string
+(* columns, rendering style, name prefix, object *)
+val txt_of_cic_object:
+ int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string
+
+(* presentation_style, uri or baseuri, name prefix *)
+val txt_of_inline_macro:
+ GrafiteAst.presentation_style -> string -> string -> string
addDebugItem "Print current proof (natural language) to stderr"
(fun _ ->
prerr_endline
- (ObjPp.obj_to_string 120 GrafiteAst.Declarative ""
+ (ApplyTransformation.txt_of_cic_object 120 GrafiteAst.Declarative ""
(match
(MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
with
exception TryingToAdd of string
+let out = ref ignore
+
+let set_callback f = out := f
+
let eval_from_stream ~first_statement_only ~include_paths ?(prompt=false)
?do_heavy_checks ?clean_baseuri ?(enforce_no_new_aliases=true)
?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb
loop lexicon_status grafite_status
(((grafite_status,lexicon_status),None)::statuses)
| GrafiteParser.LSome ast ->
+ !out ast;
cb grafite_status ast;
let new_statuses =
eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) option
) list
+(* this callback is called on every grafite command *)
+val set_callback: (GrafiteParser.ast_statement -> unit) -> unit
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
[], "", parsed_text_length
| TA.Inline (_,style,suri,prefix) ->
- let dbd = LibraryDb.instance () in
- let uris =
- let sql_pat =
- (Pcre.replace ~rex:(Pcre.regexp "_") ~templ:"\\_" suri) ^ "%" in
- let query =
- sprintf ("SELECT source FROM %s WHERE source LIKE \"%s\" UNION "^^
- "SELECT source FROM %s WHERE source LIKE \"%s\"")
- (MetadataTypes.name_tbl ()) sql_pat
- MetadataTypes.library_name_tbl sql_pat in
- let result = HMysql.exec dbd query in
- HMysql.map result
- (function cols ->
- match cols.(0) with
- Some s -> UriManager.uri_of_string s
- | _ -> assert false)
- in
-prerr_endline "Inizio sorting";
- let sorted_uris = MetadataDeps.topological_sort ~dbd uris in
-prerr_endline "Fine sorting";
- let sorted_uris_without_xpointer =
- HExtlib.filter_map
- (function uri ->
- let s =
- Pcre.replace ~rex:(Pcre.regexp "#xpointer\\(1/1\\)") ~templ:""
- (UriManager.string_of_uri uri) in
- try
- ignore (Pcre.exec ~rex:(Pcre.regexp"#xpointer") s);
- None
- with
- Not_found ->
- Some (UriManager.uri_of_string s)
- ) sorted_uris
- in
- let declarative =
- String.concat "\n\n"
- (List.map
- (fun uri ->
-prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
- try
- ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
- (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
- with
- | e (* BRRRRRRRRR *) ->
- Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n"
- (UriManager.string_of_uri uri) (Printexc.to_string e)
- ) sorted_uris_without_xpointer)
- in
- [],declarative,String.length parsed_text
+ let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+ [], str, String.length parsed_text
and eval_executable include_paths (buffer : GText.buffer) guistuff
lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
exception AttemptToInsertAnAlias
+let out = ref ignore
+
+let set_callback f = out := f
+
let pp_ast_statement =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
"matita.includes"))
with
| GrafiteEngine.Drop -> pp_ocaml_mode ()
- | GrafiteEngine.Macro (floc,_) ->
- let x, y = HExtlib.loc_of_floc floc in
+ | GrafiteEngine.Macro (floc, f) ->
+ begin match snd (f []) with
+ | GrafiteAst.Inline (_, style, suri, prefix) ->
+ let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+ !out str
+ | _ -> ()
+ end;
+ let x, y = HExtlib.loc_of_floc floc in
HLog.error
(sprintf "A macro has been found in a script at %d-%d" x y);
interactive_loop ()
otherwise it performs the clean-up without exiting
*)
val clean_exit : int option -> unit
+
+(* this callback is called on the expansion of every inline macro *)
+val set_callback: (string -> unit) -> unit
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/test/letrecand".
+set "baseuri" "cic:/matita/tests/letrecand".
include "nat/nat.ma".
lemma test_dispari2: dispari2 (S O).
simplify.
constructor 1.
-qed.
\ No newline at end of file
+qed.
projects / helm.git / commitdiff