+cicNotationUtil.cmi: cicNotationPt.cmo
+cicNotationTag.cmi: cicNotationPt.cmo
cicNotationEnv.cmi: cicNotationPt.cmo
cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi
cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi
cicNotationRew.cmi: cicNotationPt.cmo
cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi
-cicNotationUtil.cmo: cicNotationUtil.cmi
-cicNotationUtil.cmx: cicNotationUtil.cmi
+cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi
+cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi
+cicNotationTag.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationTag.cmi
+cicNotationTag.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationTag.cmi
cicNotationLexer.cmo: cicNotationLexer.cmi
cicNotationLexer.cmx: cicNotationLexer.cmi
cicNotationEnv.cmo: cicNotationPt.cmo cicNotationEnv.cmi
cicNotationFwd.cmi
cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \
cicNotationFwd.cmi
-cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationRew.cmi
-cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationRew.cmi
+cicNotationRew.cmo: cicNotationUtil.cmi cicNotationTag.cmi cicNotationPt.cmo \
+ cicNotationRew.cmi
+cicNotationRew.cmx: cicNotationUtil.cmx cicNotationTag.cmx cicNotationPt.cmx \
+ cicNotationRew.cmi
cicNotationParser.cmo: cicNotationPt.cmo cicNotationPp.cmi \
cicNotationLexer.cmi cicNotationEnv.cmi cicNotationParser.cmi
cicNotationParser.cmx: cicNotationPt.cmx cicNotationPp.cmx \
$(NULL)
INTERFACE_FILES = \
cicNotationUtil.mli \
+ cicNotationTag.mli \
cicNotationLexer.mli \
cicNotationEnv.mli \
cicNotationPp.mli \
let regexp implicit = '?'
let regexp meta = implicit number
+let regexp csymbol = '\'' ident
+
let regexp uri =
("cic:/" | "theory:/") (* schema *)
ident ('/' ident)* (* path *)
| tex_token -> return lexbuf (expand_macro lexbuf)
| uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
| eof -> return lexbuf ("EOI", "")
+ | csymbol -> return lexbuf ("CSYMBOL", Ulexing.utf8_lexeme lexbuf)
| _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)
(* API implementation *)
[ "90" NONA
[ id = IDENT -> return_term loc (Ident (id, None))
| id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
+ | s = CSYMBOL -> return_term loc (Symbol (s, 0))
| u = URI -> return_term loc (Uri (u, None))
| n = NUMBER -> prerr_endline "number"; return_term loc (Num (n, 0))
| IMPLICIT -> return_term loc (Implicit)
]
];
interpretation: [
- [ s = SYMBOL; args = LIST1 argument; SYMBOL "=";
- t = level3_term ->
+ [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
(s, args, t)
]
];
open CicNotationEnv
open CicNotationPt
+let print_attributes = true
+
let pp_binder = function
| `Lambda -> "lambda"
| `Pi -> "Pi"
| `Number s -> s)
let rec pp_term = function
+ | AttributedTerm (_, term) when print_attributes ->
+ sprintf "@[%s]" (pp_term term)
| AttributedTerm (_, term) -> pp_term term
| Appl terms ->
type pattern_id = int
type interpretation_id = pattern_id
+type pretty_printer_id = pattern_id
type term_info =
{ sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
let warning s = prerr_endline ("CicNotation WARNING: " ^ s)
-module Patterns =
+module type PATTERN =
+ sig
+ type pattern_t
+ val compatible : pattern_t -> pattern_t -> bool
+ end
+
+module Patterns (P: PATTERN) =
struct
- type row_t = CicNotationPt.cic_appl_pattern list * pattern_id
+ type row_t = P.pattern_t list * pattern_id
type t = row_t list
let empty = []
let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t
let pattern_ids t = List.map snd t
- let prepend_column t column =
- try
- List.map2 (fun elt (pl, pid) -> (elt :: pl), pid) column t
+ let partition t pidl =
+ let partitions = Hashtbl.create 11 in
+ let add pid row = Hashtbl.add partitions pid row in
+ (try
+ List.iter2 add pidl t
+ with Invalid_argument _ -> assert false);
+ let pidset = int_set_of_int_list pidl in
+ IntSet.fold
+ (fun pid acc ->
+ match Hashtbl.find_all partitions pid with
+ | [] -> acc
+ | patterns -> (pid, List.rev patterns) :: acc)
+ pidset []
+
+ let are_empty t = fst (List.hd t) = []
+ (* if first row has an empty list of patterns, then others will as well *)
+
+ (* return 2 lists of rows, first one containing homogeneous rows according
+ * to "compatible" below *)
+ let horizontal_split t =
+ let ap =
+ match t with
+ | [] -> assert false
+ | ([], _) :: _ ->
+ assert false (* are_empty should have been invoked in advance *)
+ | (hd :: _ , _) :: _ -> hd
+ in
+ let rec aux prev_t = function
+ | [] -> List.rev prev_t, []
+ | ([], _) :: _ -> assert false
+ | (((hd :: _), _) as row) :: tl when P.compatible ap hd ->
+ aux (row :: prev_t) tl
+ | t -> List.rev prev_t, t
+ in
+ aux [] t
- with Invalid_argument _ -> assert false
+ (* return 2 lists, first one representing first column, second one
+ * representing rows stripped of the first element *)
+ let vertical_split t =
+ let l =
+ List.map
+ (function
+ | (hd :: tl, pid) -> hd, (tl, pid)
+ | _ -> assert false)
+ t
+ in
+ List.split l
+ end
+
+module Patterns21 = Patterns (CicNotationTag)
- let prepend_columns t columns =
- List.fold_right
- (fun column rows -> prepend_column rows column)
- columns t
+module Patterns32 =
+ struct
+ type row_t = CicNotationPt.cic_appl_pattern list * pattern_id
+ type t = row_t list
+
+ let empty = []
+
+ let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t
+ let pattern_ids t = List.map snd t
let partition t pidl =
let partitions = Hashtbl.create 11 in
let idref id t = Ast.AttributedTerm (`IdRef id, t)
+let pp_ast0 t k =
+ prerr_endline "pp_ast0";
+ let rec aux t = CicNotationUtil.visit_ast ~special_k k t
+ and special_k = function
+ | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t)
+ | _ -> assert false
+ in
+ aux t
+
let ast_of_acic0 term_info acic k =
(* prerr_endline "ast_of_acic0"; *)
let k = k term_info in
(* persistent state *)
-let level2_patterns = Hashtbl.create 211
+let level1_patterns21 = Hashtbl.create 211
+let level2_patterns32 = Hashtbl.create 211
+let (compiled21: (CicNotationPt.term -> CicNotationPt.term) option ref) =
+ ref None
let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) =
ref None
-let pattern_matrix = ref Patterns.empty
+let pattern21_matrix = ref Patterns21.empty
+let pattern32_matrix = ref Patterns32.empty
+let get_compiled21 () =
+ match !compiled21 with
+ | None -> assert false
+ | Some f -> f
let get_compiled32 () =
match !compiled32 with
| None -> assert false
| Some f -> f
+let set_compiled21 f = compiled21 := Some f
let set_compiled32 f = compiled32 := Some f
(* "envl" is a list of triples:
end))
(* compiler from level 3 to level 2 *)
-let compiler32 (t: Patterns.t) success_k fail_k =
+let compiler32 (t: Patterns32.t) success_k fail_k =
let rec aux t k = (* k is a continuation *)
if t = [] then
k
- else if Patterns.are_empty t then begin
+ else if Patterns32.are_empty t then begin
(match t with
| _::_::_ ->
- (* optimization possible here: throw away all except one of the rules
- * which lead to ambiguity *)
- warning "Ambiguous patterns"
+ (* XXX optimization possible here: throw away all except one of the
+ * rules which lead to ambiguity *)
+ warning "ambiguous interpretation"
| _ -> ());
return_closure success_k
end else
- match Patterns.horizontal_split t with
+ match Patterns32.horizontal_split t with
| t', [] ->
(match t' with
| []
| ([], _) :: _ -> assert false
| (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _
| (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ ->
- let first_column, t'' = Patterns.vertical_split t' in
+ let first_column, t'' = Patterns32.vertical_split t' in
let names =
List.map
(function
t'
in
(* arity partitioning *)
- let clusters = Patterns.partition t' pidl in
+ let clusters = Patterns32.partition t' pidl in
let ks = (* k continuation list *)
List.map
(fun (len, cluster) ->
in
!uidmap, uidl
in
- let clusters = Patterns.partition t' pidl in
+ let clusters = Patterns32.partition t' pidl in
let ks =
List.map
(fun (uid, cluster) ->
matcher term_info [annterm] (List.map (fun (_, pid) -> [], [], pid) t)
with No_match -> fail_k term_info annterm)
+let return_closure21 success_k =
+ (fun terms envl ->
+ prerr_endline "return_closure21";
+ match terms with
+ | [] ->
+ (try
+ success_k (List.hd envl)
+ with Failure _ -> assert false)
+ | _ -> assert false)
+
+let variable_closure21 vars k =
+ (fun terms envl ->
+ prerr_endline "variable_closure21";
+ match terms with
+ | hd :: tl ->
+ let envl' =
+ List.map2 (fun var (env, pid) -> (var, hd) :: env, pid) vars envl
+ in
+ k tl envl'
+ | _ -> assert false)
+
+let constructor_closure21 ks k =
+ (fun terms envl ->
+ prerr_endline "constructor_closure21";
+ (match terms with
+ | p :: tl ->
+ prerr_endline (sprintf "on term %s" (CicNotationPp.pp_term p));
+ (try
+ let tag, subterms = CicNotationTag.get_tag p in
+ let k' = List.assoc tag ks in
+ k' (subterms @ tl) envl
+ with Not_found -> k terms envl)
+ | [] -> assert false))
+
+let compiler21 (t: Patterns21.t) success_k fail_k =
+ let rec aux t k =
+ if t = [] then
+ k
+ else if Patterns21.are_empty t then begin
+ (match t with
+ | _::_::_ ->
+ (* XXX optimization possible here: throw away all except one of the
+ * rules which lead to ambiguity *)
+ warning "ambiguous notation"
+ | _ -> ());
+ return_closure21 success_k
+ end else
+ match Patterns21.horizontal_split t with
+ | t', [] ->
+ (match t' with
+ | []
+ | ([], _) :: _ -> assert false
+ | (Ast.Variable _ :: _, _) :: _ ->
+ let first_column, t'' = Patterns21.vertical_split t' in
+ let vars =
+ List.map
+ (function
+ | Ast.Variable v -> v
+ | _ -> assert false)
+ first_column
+ in
+ variable_closure21 vars (aux t'' k)
+ | _ ->
+ let pidl =
+ List.map
+ (function
+ | p :: _, _ -> fst (CicNotationTag.get_tag p)
+ | [], _ -> assert false)
+ t'
+ in
+ let clusters = Patterns21.partition t' pidl in
+ let ks =
+ List.map
+ (fun (pid, cluster) ->
+ let cluster' =
+ List.map (* add args as patterns heads *)
+ (function
+ | p :: tl, pid ->
+ let _, subpatterns = CicNotationTag.get_tag p in
+ subpatterns @ tl, pid
+ | _ -> assert false)
+ cluster
+ in
+ pid, aux cluster' k)
+ clusters
+ in
+ constructor_closure21 ks k)
+ | t', tl -> aux t' (aux tl k)
+ in
+ let matcher = aux t (fun _ _ -> raise No_match) in
+ (fun ast ->
+ try
+ matcher [ast] (List.map (fun (_, pid) -> [], pid) t)
+ with No_match -> fail_k ast)
+
let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm
-let instantiate term_info name_env term_env pid =
+let pp_ast1 term = (get_compiled21 ()) term
+
+let instantiate21 env pid =
+ prerr_endline "instantiate21";
+ let precedence, associativity, l1 =
+ try
+ Hashtbl.find level1_patterns21 pid
+ with Not_found -> assert false
+ in
+ let rec subst = function
+ | Ast.AttributedTerm (_, t) -> subst t
+ | Ast.Variable var ->
+ (try List.assoc var env with Not_found -> assert false)
+ | (Ast.Literal _
+ | Ast.Magic _) as t -> t
+ | Ast.Layout l -> Ast.Layout (subst_layout l)
+ | t -> CicNotationUtil.visit_ast subst t
+ and subst_layout l = CicNotationUtil.visit_layout subst l in
+ subst l1
+
+let instantiate32 term_info name_env term_env pid =
let symbol, args =
try
- Hashtbl.find level2_patterns pid
+ Hashtbl.find level2_patterns32 pid
with Not_found -> assert false
in
let rec instantiate_arg = function
let args' = List.map instantiate_arg args in
Ast.Appl (Ast.Symbol (symbol, 0) :: args')
-let load_patterns t =
+let load_patterns32 t =
let ast_env_of_name_env term_info name_env =
List.map
(fun (name, (name', ty_opt)) ->
in
let fail_k term_info annterm = ast_of_acic0 term_info annterm ast_of_acic1 in
let success_k term_info (name_env, term_env, pid) =
- instantiate
+ instantiate32
term_info
(ast_env_of_name_env term_info name_env)
(ast_env_of_term_env term_info term_env)
let compiled32 = compiler32 t success_k fail_k in
set_compiled32 compiled32
+let load_patterns21 t =
+ let ast_env_of_env env =
+ List.map (fun (var, term) -> (var, pp_ast1 term)) env
+ in
+ let fail_k term = pp_ast0 term pp_ast1 in
+ let success_k (env, pid) = instantiate21 (ast_env_of_env env) pid in
+ let compiled21 = compiler21 t success_k fail_k in
+ set_compiled21 compiled21
+
let ast_of_acic id_to_sort annterm =
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
let ast = ast_of_acic1 term_info annterm in
ast, term_info.uri
+let pp_ast term = pp_ast1 term
+
let fresh_id =
let counter = ref ~-1 in
fun () ->
let add_interpretation (symbol, args) appl_pattern =
let id = fresh_id () in
- Hashtbl.add level2_patterns id (symbol, args);
- pattern_matrix := ([appl_pattern], id) :: !pattern_matrix;
- load_patterns !pattern_matrix;
+ Hashtbl.add level2_patterns32 id (symbol, args);
+ pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix;
+ load_patterns32 !pattern32_matrix;
+ id
+
+let add_pretty_printer ?precedence ?associativity l2 l1 =
+ let id = fresh_id () in
+ let l2' = CicNotationUtil.strip_attributes l2 in
+ Hashtbl.add level1_patterns21 id (precedence, associativity, l1);
+ pattern21_matrix := ([l2'], id) :: !pattern21_matrix;
+ load_patterns21 !pattern21_matrix;
id
exception Interpretation_not_found
+exception Pretty_printer_not_found
let remove_interpretation id =
(try
- Hashtbl.remove level2_patterns id;
+ Hashtbl.remove level2_patterns32 id;
with Not_found -> raise Interpretation_not_found);
- pattern_matrix := List.filter (fun (_, id') -> id <> id') !pattern_matrix;
- load_patterns !pattern_matrix
+ pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;
+ load_patterns32 !pattern32_matrix
-let _ = load_patterns []
+let remove_pretty_printer id =
+ (try
+ Hashtbl.remove level1_patterns21 id;
+ with Not_found -> raise Pretty_printer_not_found);
+ pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix;
+ load_patterns21 !pattern21_matrix
+
+let _ =
+ load_patterns21 [];
+ load_patterns32 []
* http://helm.cs.unibo.it/
*)
+ (** level 3 -> level 2 *)
val ast_of_acic:
(Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *)
Cic.annterm -> (* acic *)
CicNotationPt.term (* ast *)
* (Cic.id, string) Hashtbl.t (* id -> uri *)
+ (** level 2 -> level 1 *)
+val pp_ast: CicNotationPt.term -> CicNotationPt.term
+
type interpretation_id
+type pretty_printer_id
val add_interpretation:
string * CicNotationPt.argument_pattern list -> (* level 2 pattern *)
CicNotationPt.cic_appl_pattern -> (* level 3 pattern *)
interpretation_id
+val add_pretty_printer:
+ ?precedence:int ->
+ ?associativity:Gramext.g_assoc ->
+ CicNotationPt.term -> (* level 2 pattern *)
+ CicNotationPt.term -> (* level 1 pattern *)
+ pretty_printer_id
+
exception Interpretation_not_found
+exception Pretty_printer_not_found
(** @raise Interpretation_not_found *)
val remove_interpretation: interpretation_id -> unit
+ (** @raise Pretty_printer_not_found *)
+val remove_pretty_printer: pretty_printer_id -> unit
+
--- /dev/null
+(* Copyright (C) 2004-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/
+ *)
+
+open CicNotationPt
+
+type tag = int
+type pattern_t = CicNotationPt.term
+
+let get_tag term0 =
+ prerr_endline "get_tag";
+ let subterms = ref [] in
+ let map_term t =
+ subterms := t :: !subterms ;
+ Implicit
+ in
+ let rec aux t = CicNotationUtil.visit_ast ~special_k map_term t
+ and special_k = function
+ | AttributedTerm (_, t) -> aux t
+ | _ -> assert false
+ in
+ let term_mask = aux term0 in
+ let tag = Hashtbl.hash term_mask in
+ Printf.printf "TAG = %d\n" tag ; flush stdout ;
+ tag, !subterms
+
+let compatible t1 t2 =
+ match t1, t2 with
+ | Variable _, Variable _ -> true
+ | Variable _, _
+ | _, Variable _ -> false
+ | Layout _, _
+ | _, Layout _
+ | Magic _, _
+ | _, Magic _ -> assert false
+ | _ -> true
+
--- /dev/null
+(* Copyright (C) 2004-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/
+ *)
+
+type tag = int
+type pattern_t = CicNotationPt.term
+
+val get_tag: pattern_t -> tag * pattern_t list
+val compatible: pattern_t -> pattern_t -> bool
+
* http://helm.cs.unibo.it/
*)
+open CicNotationPt
+
(* TODO ensure that names generated by fresh_var do not clash with user's *)
let fresh_name =
let index = ref ~-1 in
incr index;
"fresh" ^ string_of_int !index
+let visit_ast ?(special_k = fun _ -> assert false) k =
+ let rec aux = function
+
+ | Appl terms -> Appl (List.map k terms)
+ | Binder (kind, var, body) ->
+ Binder (kind, aux_capture_variable var, k body)
+ | Case (term, indtype, typ, patterns) ->
+ Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+ | LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
+ | LetRec (kind, definitions, term) ->
+ let definitions =
+ List.map
+ (fun (var, ty, n) -> aux_capture_variable var, k ty, n)
+ definitions
+ in
+ LetRec (kind, definitions, k term)
+ | Ident (name, Some substs) -> Ident (name, Some (aux_substs substs))
+ | Uri (name, Some substs) -> Uri (name, Some (aux_substs substs))
+ | Meta (index, substs) -> Meta (index, List.map aux_opt substs)
+
+ | (AttributedTerm _
+ | Layout _
+ | Literal _
+ | Magic _
+ | Variable _) as t -> special_k t
+
+ | (Ident _
+ | Implicit
+ | Num _
+ | Sort _
+ | Symbol _
+ | Uri _
+ | UserInput) as t -> t
+
+ and aux_opt = function
+ | None -> None
+ | Some term -> Some (k term)
+
+ and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
+
+ and aux_patterns patterns = List.map aux_pattern patterns
+
+ and aux_pattern ((head, vars), term) =
+ ((head, List.map aux_capture_variable vars), k term)
+
+ and aux_subst (name, term) = (name, k term)
+
+ and aux_substs substs = List.map aux_subst substs
+
+ in
+
+ aux
+
+let visit_layout k = function
+ | Sub (t1, t2) -> Sub (k t1, k t2)
+ | Sup (t1, t2) -> Sup (k t1, k t2)
+ | Below (t1, t2) -> Below (k t1, k t2)
+ | Above (t1, t2) -> Above (k t1, k t2)
+ | Over (t1, t2) -> Over (k t1, k t2)
+ | Atop (t1, t2) -> Atop (k t1, k t2)
+ | Frac (t1, t2) -> Frac (k t1, k t2)
+ | Sqrt t -> Sqrt (k t)
+ | Root (arg, index) -> Root (k arg, k index)
+ | Break -> Break
+ | Box (kind, terms) -> Box (kind, List.map k terms)
+
+let visit_magic k = function
+ | List0 (t, l) -> List0 (k t, l)
+ | List1 (t, l) -> List1 (k t, l )
+ | Opt t -> Opt (k t)
+ | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
+ | Default (t1, t2) -> Default (k t1, k t2)
+
+let rec strip_attributes t =
+ prerr_endline "strip_attributes";
+ let special_k = function
+ | AttributedTerm (_, term) -> strip_attributes term
+ | Magic m -> Magic (visit_magic strip_attributes m)
+ | Variable _ as t -> t
+ | t -> assert false
+ in
+ visit_ast ~special_k strip_attributes t
+
val fresh_name: unit -> string
+val visit_ast:
+ ?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
+ (CicNotationPt.term -> CicNotationPt.term) ->
+ CicNotationPt.term ->
+ CicNotationPt.term
+
+val visit_layout:
+ (CicNotationPt.term -> CicNotationPt.term) ->
+ CicNotationPt.layout_pattern ->
+ CicNotationPt.layout_pattern
+
+val strip_attributes: CicNotationPt.term -> CicNotationPt.term
+
--- /dev/null
+<helm_registry>
+ <section name="getter">
+ <key name="prefetch">false</key>
+ <key name="servers">
+ file:///projects/helm/library/coq_contribs
+ </key>
+ <key name="cache_dir">/tmp/zack/cache</key>
+ <key name="maps_dir">/projects/helm/var</key>
+ <key name="dtd_dir">/projects/helm/xml/dtd</key>
+<!-- <key name="loglevel">180</key> -->
+ </section>
+</helm_registry>
open Printf
let _ =
- Helm_registry.set "getter.mode" "remote";
- Helm_registry.set "getter.url" "http://helm.cs.unibo.it:58081/"
+ Helm_registry.load_from "test_parser.conf.xml";
+ Http_getter.init ()
let _ =
let module P = CicNotationPt in
| -1 ->
(match CicNotationParser.parse_phrase istream with
| P.Print t ->
- print_endline (CicNotationPp.pp_term t); flush stdout
+ prerr_endline "====";
+ print_endline (CicNotationPp.pp_term t); flush stdout;
+ let t' = CicNotationRew.pp_ast t in
+ print_endline (CicNotationPp.pp_term t'); flush stdout
| P.Notation (l1, associativity, precedence, l2) ->
- print_endline "Extending notation ..."; flush stdout;
+ print_endline "Extending parser ..."; flush stdout;
+ let time1 = Unix.gettimeofday () in
ignore
(CicNotationParser.extend l1 ?precedence ?associativity
(fun env loc ->
prerr_endline "ENV";
prerr_endline (CicNotationPp.pp_env env);
- CicNotationFwd.instantiate_level2 env l2))
+ CicNotationFwd.instantiate_level2 env l2));
+ let time2 = Unix.gettimeofday () in
+ print_endline "Extending pretty printer ..."; flush stdout;
+ let time3 = Unix.gettimeofday () in
+ ignore
+ (CicNotationRew.add_pretty_printer ?precedence ?associativity
+ l2 l1);
+ let time4 = Unix.gettimeofday () in
+ printf "done (extending parser took %f, extending pretty printer took %f)\n"
+ (time2 -. time1) (time4 -. time3);
+ flush stdout
| P.Interpretation (l2, l3) ->
print_endline "Adding interpretation ..."; flush stdout;
let time1 = Unix.gettimeofday () in
in
let time2 = Unix.gettimeofday () in
printf "ast creation took %f seconds\n" (time2 -. time1);
- print_endline (CicNotationPp.pp_term t); flush stdout)
+ prerr_endline "====";
+ print_endline (CicNotationPp.pp_term t); flush stdout;
+ flush stdout;
+ let time3 = Unix.gettimeofday () in
+ let t' = CicNotationRew.pp_ast t in
+ let time4 = Unix.gettimeofday () in
+ printf "pretty printing took %f seconds\n" (time4 -. time3);
+ print_endline (CicNotationPp.pp_term t'); flush stdout)
(* CicNotationParser.print_l2_pattern ()) *)
| 1 -> ignore (CicNotationParser.parse_syntax_pattern istream)
| 2 ->
projects / helm.git / commitdiff