-requires=""
+requires="helm-extlib"
version="0.0.1"
archive(byte)="ng_kernel.cma"
archive(native)="ng_kernel.cmxa"
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN = \
- test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt
+ test_parser test_parser.opt test_dep test_dep.opt
-all: test_parser test_dep print_grammar
+all: test_parser test_dep
$(H)echo -n
-opt: test_parser.opt test_dep.opt print_grammar.opt
+opt: test_parser.opt test_dep.opt
$(H)echo -n
test_parser: test_parser.ml
$(H)$(OCAMLFIND) ocamlopt \
-I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
-print_grammar: print_grammar.ml
- $(H)echo " OCAMLC $<"
- $(H)$(OCAMLFIND) ocamlc \
- -I ../../tactics/paramodulation/ -rectypes -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
-
-print_grammar.opt: print_grammar.ml
- $(H)echo " OCAMLOPT $<"
- $(H)$(OCAMLFIND) ocamlopt \
- -I ../../tactics/paramodulation/ -thread -package "$(REQUIRES)" -linkpkg -o $@ $<
-
clean:
$(H)rm -f *.cm[iox] *.a *.o
- $(H)rm -f test_parser test_parser.opt test_dep test_dep.opt print_grammar print_grammar.opt
+ $(H)rm -f test_parser test_parser.opt test_dep test_dep.opt
depend:
depend.opt:
+++ /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/
- *)
-
-(* $Id$ *)
-
-open Gramext
-
-let rec flatten_tree = function
- | DeadEnd -> []
- | LocAct _ -> [[]]
- | Node {node = n; brother = b; son = s} ->
- List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
-
-let tex_of_unicode s = s
-
-let rec clean_dummy_desc = function
- | Dlevels l -> Dlevels (clean_levels l)
- | x -> x
-
-and clean_levels = function
- | [] -> []
- | l :: tl -> clean_level l @ clean_levels tl
-
-and clean_level = function
- | x ->
- let pref = clean_tree x.lprefix in
- let suff = clean_tree x.lsuffix in
- match pref,suff with
- | DeadEnd, DeadEnd -> []
- | _ -> [{x with lprefix = pref; lsuffix = suff}]
-
-and clean_tree = function
- | Node n -> clean_node n
- | x -> x
-
-and clean_node = function
- | {node=node;son=son;brother=brother} ->
- let bn = is_symbol_dummy node in
- let bs = is_tree_dummy son in
- let bb = is_tree_dummy brother in
- let son = if bs then DeadEnd else son in
- let brother = if bb then DeadEnd else brother in
- if bb && bs && bn then
- DeadEnd
- else
- if bn then
- Node {node=Sself;son=son;brother=brother}
- else
- Node {node=node;son=son;brother=brother}
-
-and is_level_dummy = function
- | {lsuffix=lsuffix;lprefix=lprefix} ->
- is_tree_dummy lsuffix && is_tree_dummy lprefix
-
-and is_desc_dummy = function
- | Dlevels l -> List.for_all is_level_dummy l
- | Dparser _ -> true
-
-and is_entry_dummy = function
- | {edesc=edesc} -> is_desc_dummy edesc
-
-and is_symbol_dummy = function
- | Stoken ("DUMMY", _) -> true
- | Stoken _ -> false
- | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
- | Snterm e | Snterml (e, _) -> is_entry_dummy e
- | Slist1 x | Slist0 x -> is_symbol_dummy x
- | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
- | Sopt x -> is_symbol_dummy x
- | Sself | Snext -> false
- | Stree t -> is_tree_dummy t
- | _ -> assert false
-
-and is_tree_dummy = function
- | Node {node=node} -> is_symbol_dummy node
- | _ -> true
-
-let needs_brackets t =
- let rec count_brothers = function
- | Node {brother = brother} -> 1 + count_brothers brother
- | _ -> 0
- in
- count_brothers t > 1
-
-let visit_description desc fmt self =
- let skip s = true in
- let inline s = List.mem s [ "int" ] in
-
- let rec visit_entry e ?level todo is_son =
- let { ename = ename; edesc = desc } = e in
- if inline ename then
- visit_desc desc todo is_son
- else
- begin
- (match level with
- | None -> Format.fprintf fmt "%s " ename;
- | Some _ -> Format.fprintf fmt "%s " ename;);
- if skip ename then
- todo
- else
- todo @ [e]
- end
-
- and visit_desc d todo is_son =
- match d with
- | Dlevels l ->
- List.fold_left
- (fun acc l ->
- Format.fprintf fmt "@ ";
- visit_level l acc is_son )
- todo l;
- | Dparser _ -> todo
-
- and visit_level l todo is_son =
- let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
- visit_tree name
- (List.map
- (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
- todo is_son
-
- and visit_tree name t todo is_son =
- if List.for_all (List.for_all is_symbol_dummy) t then todo else (
- Format.fprintf fmt "@[<v>";
- (match name with
- |Some name -> Format.fprintf fmt "Precedence %s:@ " name
- | None -> ());
- Format.fprintf fmt "@[<v>";
- let todo =
- List.fold_left
- (fun acc x ->
- if List.for_all is_symbol_dummy x then todo else (
- Format.fprintf fmt "@[<h> | ";
- let todo =
- List.fold_left
- (fun acc x ->
- let todo = visit_symbol x acc true in
- Format.fprintf fmt "@ ";
- todo)
- acc x
- in
- Format.fprintf fmt "@]@ ";
- todo))
- todo t
- in
- Format.fprintf fmt "@]";
- Format.fprintf fmt "@]";
- todo)
-
- and visit_symbol s todo is_son =
- match s with
- | Smeta (name, sl, _) ->
- Format.fprintf fmt "%s " name;
- List.fold_left (
- fun acc s ->
- let todo = visit_symbol s acc is_son in
- if is_son then
- Format.fprintf fmt "@ ";
- todo)
- todo sl
- | Snterm entry -> visit_entry entry todo is_son
- | Snterml (entry,level) -> visit_entry entry ~level todo is_son
- | Slist0 symbol ->
- Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "@]} @ ";
- todo
- | Slist0sep (symbol,sep) ->
- Format.fprintf fmt "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol sep todo is_son in
- Format.fprintf fmt " ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "@]} @]] @ ";
- todo
- | Slist1 symbol ->
- Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "@]}+ @ ";
- todo
- | Slist1sep (symbol,sep) ->
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "{@[<hov2> ";
- let todo = visit_symbol sep todo is_son in
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "@]} @ ";
- todo
- | Sopt symbol ->
- Format.fprintf fmt "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son in
- Format.fprintf fmt "@]] @ ";
- todo
- | Sself -> Format.fprintf fmt "%s " self; todo
- | Snext -> Format.fprintf fmt "next "; todo
- | Stoken pattern ->
- let constructor, keyword = pattern in
- if keyword = "" then
- (if constructor <> "DUMMY" then
- Format.fprintf fmt "`%s' " constructor)
- else
- Format.fprintf fmt "%s " (tex_of_unicode keyword);
- todo
- | Stree tree ->
- visit_tree None (flatten_tree tree) todo is_son
- | _ -> assert false
- in
- visit_desc desc [] false
-;;
-
-
-let rec visit_entries fmt todo pped =
- match todo with
- | [] -> ()
- | hd :: tl ->
- let todo =
- if not (List.memq hd pped) then
- begin
- let { ename = ename; edesc = desc } = hd in
- Format.fprintf fmt "@[<hv 2>%s ::= " ename;
- let desc = clean_dummy_desc desc in
- let todo = visit_description desc fmt ename @ todo in
- Format.fprintf fmt "@]\n\n";
- todo
- end
- else
- todo
- in
- let clean_todo todo =
- let name_of_entry e = e.ename in
- let pped = hd :: pped in
- let todo = tl @ todo in
- let todo = List.filter (fun e -> not(List.memq e pped)) todo in
- HExtlib.list_uniq
- ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
- (List.sort
- (fun e1 e2 ->
- Pervasives.compare (name_of_entry e1) (name_of_entry e2))
- todo),
- pped
- in
- let todo,pped = clean_todo todo in
- visit_entries fmt todo pped
-;;
-
-let ebnf_of_term () =
- let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
- let buff = Buffer.create 100 in
- let fmt = Format.formatter_of_buffer buff in
- visit_entries fmt [g_entry] [];
- Format.fprintf fmt "@?";
- let s = Buffer.contents buff in
- s
-;;
cicNotation2.mli \
nEstatus.mli \
grafiteDisambiguate.mli \
- print_grammar.mli \
+ print_grammar.mli \
$(NULL)
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
--- /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/
+ *)
+
+(* $Id$ *)
+
+open Gramext
+
+let rec flatten_tree = function
+ | DeadEnd -> []
+ | LocAct _ -> [[]]
+ | Node {node = n; brother = b; son = s} ->
+ List.map (fun l -> n :: l) (flatten_tree s) @ flatten_tree b
+
+let tex_of_unicode s = s
+
+let rec clean_dummy_desc = function
+ | Dlevels l -> Dlevels (clean_levels l)
+ | x -> x
+
+and clean_levels = function
+ | [] -> []
+ | l :: tl -> clean_level l @ clean_levels tl
+
+and clean_level = function
+ | x ->
+ let pref = clean_tree x.lprefix in
+ let suff = clean_tree x.lsuffix in
+ match pref,suff with
+ | DeadEnd, DeadEnd -> []
+ | _ -> [{x with lprefix = pref; lsuffix = suff}]
+
+and clean_tree = function
+ | Node n -> clean_node n
+ | x -> x
+
+and clean_node = function
+ | {node=node;son=son;brother=brother} ->
+ let bn = is_symbol_dummy node in
+ let bs = is_tree_dummy son in
+ let bb = is_tree_dummy brother in
+ let son = if bs then DeadEnd else son in
+ let brother = if bb then DeadEnd else brother in
+ if bb && bs && bn then
+ DeadEnd
+ else
+ if bn then
+ Node {node=Sself;son=son;brother=brother}
+ else
+ Node {node=node;son=son;brother=brother}
+
+and is_level_dummy = function
+ | {lsuffix=lsuffix;lprefix=lprefix} ->
+ is_tree_dummy lsuffix && is_tree_dummy lprefix
+
+and is_desc_dummy = function
+ | Dlevels l -> List.for_all is_level_dummy l
+ | Dparser _ -> true
+
+and is_entry_dummy = function
+ | {edesc=edesc} -> is_desc_dummy edesc
+
+and is_symbol_dummy = function
+ | Stoken ("DUMMY", _) -> true
+ | Stoken _ -> false
+ | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
+ | Snterm e | Snterml (e, _) -> is_entry_dummy e
+ | Slist1 x | Slist0 x -> is_symbol_dummy x
+ | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+ | Sopt x -> is_symbol_dummy x
+ | Sself | Snext -> false
+ | Stree t -> is_tree_dummy t
+ | _ -> assert false
+
+and is_tree_dummy = function
+ | Node {node=node} -> is_symbol_dummy node
+ | _ -> true
+
+let needs_brackets t =
+ let rec count_brothers = function
+ | Node {brother = brother} -> 1 + count_brothers brother
+ | _ -> 0
+ in
+ count_brothers t > 1
+
+let visit_description desc fmt self =
+ let skip s = true in
+ let inline s = List.mem s [ "int" ] in
+
+ let rec visit_entry e ?level todo is_son =
+ let { ename = ename; edesc = desc } = e in
+ if inline ename then
+ visit_desc desc todo is_son
+ else
+ begin
+ (match level with
+ | None -> Format.fprintf fmt "%s " ename;
+ | Some _ -> Format.fprintf fmt "%s " ename;);
+ if skip ename then
+ todo
+ else
+ todo @ [e]
+ end
+
+ and visit_desc d todo is_son =
+ match d with
+ | Dlevels l ->
+ List.fold_left
+ (fun acc l ->
+ Format.fprintf fmt "@ ";
+ visit_level l acc is_son )
+ todo l;
+ | Dparser _ -> todo
+
+ and visit_level l todo is_son =
+ let { lname = name ; lsuffix = suff ; lprefix = pref } = l in
+ visit_tree name
+ (List.map
+ (fun x -> Sself :: x) (flatten_tree suff) @ flatten_tree pref)
+ todo is_son
+
+ and visit_tree name t todo is_son =
+ if List.for_all (List.for_all is_symbol_dummy) t then todo else (
+ Format.fprintf fmt "@[<v>";
+ (match name with
+ |Some name -> Format.fprintf fmt "Precedence %s:@ " name
+ | None -> ());
+ Format.fprintf fmt "@[<v>";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ if List.for_all is_symbol_dummy x then todo else (
+ Format.fprintf fmt "@[<h> | ";
+ let todo =
+ List.fold_left
+ (fun acc x ->
+ let todo = visit_symbol x acc true in
+ Format.fprintf fmt "@ ";
+ todo)
+ acc x
+ in
+ Format.fprintf fmt "@]@ ";
+ todo))
+ todo t
+ in
+ Format.fprintf fmt "@]";
+ Format.fprintf fmt "@]";
+ todo)
+
+ and visit_symbol s todo is_son =
+ match s with
+ | Smeta (name, sl, _) ->
+ Format.fprintf fmt "%s " name;
+ List.fold_left (
+ fun acc s ->
+ let todo = visit_symbol s acc is_son in
+ if is_son then
+ Format.fprintf fmt "@ ";
+ todo)
+ todo sl
+ | Snterm entry -> visit_entry entry todo is_son
+ | Snterml (entry,level) -> visit_entry entry ~level todo is_son
+ | Slist0 symbol ->
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @ ";
+ todo
+ | Slist0sep (symbol,sep) ->
+ Format.fprintf fmt "[@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol sep todo is_son in
+ Format.fprintf fmt " ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @]] @ ";
+ todo
+ | Slist1 symbol ->
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]}+ @ ";
+ todo
+ | Slist1sep (symbol,sep) ->
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "{@[<hov2> ";
+ let todo = visit_symbol sep todo is_son in
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]} @ ";
+ todo
+ | Sopt symbol ->
+ Format.fprintf fmt "[@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son in
+ Format.fprintf fmt "@]] @ ";
+ todo
+ | Sself -> Format.fprintf fmt "%s " self; todo
+ | Snext -> Format.fprintf fmt "next "; todo
+ | Stoken pattern ->
+ let constructor, keyword = pattern in
+ if keyword = "" then
+ (if constructor <> "DUMMY" then
+ Format.fprintf fmt "`%s' " constructor)
+ else
+ Format.fprintf fmt "%s " (tex_of_unicode keyword);
+ todo
+ | Stree tree ->
+ visit_tree None (flatten_tree tree) todo is_son
+ | _ -> assert false
+ in
+ visit_desc desc [] false
+;;
+
+
+let rec visit_entries fmt todo pped =
+ match todo with
+ | [] -> ()
+ | hd :: tl ->
+ let todo =
+ if not (List.memq hd pped) then
+ begin
+ let { ename = ename; edesc = desc } = hd in
+ Format.fprintf fmt "@[<hv 2>%s ::= " ename;
+ let desc = clean_dummy_desc desc in
+ let todo = visit_description desc fmt ename @ todo in
+ Format.fprintf fmt "@]\n\n";
+ todo
+ end
+ else
+ todo
+ in
+ let clean_todo todo =
+ let name_of_entry e = e.ename in
+ let pped = hd :: pped in
+ let todo = tl @ todo in
+ let todo = List.filter (fun e -> not(List.memq e pped)) todo in
+ HExtlib.list_uniq
+ ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
+ (List.sort
+ (fun e1 e2 ->
+ Pervasives.compare (name_of_entry e1) (name_of_entry e2))
+ todo),
+ pped
+ in
+ let todo,pped = clean_todo todo in
+ visit_entries fmt todo pped
+;;
+
+let ebnf_of_term () =
+ let g_entry = Grammar.Entry.obj (CicNotationParser.term ()) in
+ let buff = Buffer.create 100 in
+ let fmt = Format.formatter_of_buffer buff in
+ visit_entries fmt [g_entry] [];
+ Format.fprintf fmt "@?";
+ let s = Buffer.contents buff in
+ s
+;;
let set_default_eqP() = eqPref := default_eqP
-let set_reference_of_oxuri f =
- let eqnew = function
- _ ->
- let r = f(UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
- in
- NCic.Const r
- in
- eqPref := eqnew
-;;
-
-
module type NCicContext =
sig
val metasenv : NCic.metasenv
(* $Id: terms.mli 9822 2009-06-03 15:37:06Z tassi $ *)
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
val set_eqP: NCic.term -> unit
val set_default_eqP: unit -> unit
(*prerr_endline "setting default sig";*)
eqsig := default_sig
-let set_reference_of_oxuri reference_of_oxuri =
- prerr_endline "setting oxuri in nCicProof";
- let nsig = function
- | Eq ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
- | EqInd_l ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_ind.con"))
- | EqInd_r ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_elim_r.con"))
- | Refl ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
- in eqsig:= nsig
- ;;
-
(* let debug c r = prerr_endline r; c *)
let debug c _ = c;;
type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
-val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
val set_default_sig: unit -> unit
val get_sig: eq_sig_type -> NCic.term
projects / helm.git / commitdiff