From dbcc29c0e46454c7e31b485135900ceab38627e1 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 2 Jun 2005 15:23:49 +0000 Subject: [PATCH] snapshot (first working implementation of parttern matching from level 2 to level 1) --- helm/ocaml/cic_notation/.depend | 14 +- helm/ocaml/cic_notation/Makefile | 1 + helm/ocaml/cic_notation/cicNotationLexer.ml | 3 + helm/ocaml/cic_notation/cicNotationParser.ml | 4 +- helm/ocaml/cic_notation/cicNotationPp.ml | 4 + helm/ocaml/cic_notation/cicNotationRew.ml | 283 ++++++++++++++++--- helm/ocaml/cic_notation/cicNotationRew.mli | 16 ++ helm/ocaml/cic_notation/cicNotationTag.ml | 58 ++++ helm/ocaml/cic_notation/cicNotationTag.mli | 31 ++ helm/ocaml/cic_notation/cicNotationUtil.ml | 85 ++++++ helm/ocaml/cic_notation/cicNotationUtil.mli | 13 + helm/ocaml/cic_notation/test_parser.conf.xml | 12 + helm/ocaml/cic_notation/test_parser.ml | 33 ++- 13 files changed, 513 insertions(+), 44 deletions(-) create mode 100644 helm/ocaml/cic_notation/cicNotationTag.ml create mode 100644 helm/ocaml/cic_notation/cicNotationTag.mli create mode 100644 helm/ocaml/cic_notation/test_parser.conf.xml diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 9e2292de1..18171c9da 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -1,10 +1,14 @@ +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 @@ -15,8 +19,10 @@ cicNotationFwd.cmo: cicNotationUtil.cmi 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 \ diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index a976a283d..7102f2ea7 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -10,6 +10,7 @@ REQUIRES = \ $(NULL) INTERFACE_FILES = \ cicNotationUtil.mli \ + cicNotationTag.mli \ cicNotationLexer.mli \ cicNotationEnv.mli \ cicNotationPp.mli \ diff --git a/helm/ocaml/cic_notation/cicNotationLexer.ml b/helm/ocaml/cic_notation/cicNotationLexer.ml index 8ad805c8d..3c262ceec 100644 --- a/helm/ocaml/cic_notation/cicNotationLexer.ml +++ b/helm/ocaml/cic_notation/cicNotationLexer.ml @@ -43,6 +43,8 @@ let regexp keyword = '"' ident '"' let regexp implicit = '?' let regexp meta = implicit number +let regexp csymbol = '\'' ident + let regexp uri = ("cic:/" | "theory:/") (* schema *) ident ('/' ident)* (* path *) @@ -114,6 +116,7 @@ let rec token = lexer | 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 *) diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index b408e6e3b..767aa3d15 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -510,6 +510,7 @@ EXTEND [ "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) @@ -572,8 +573,7 @@ EXTEND ] ]; interpretation: [ - [ s = SYMBOL; args = LIST1 argument; SYMBOL "="; - t = level3_term -> + [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term -> (s, args, t) ] ]; diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index 5befd8ed2..4f7989516 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -28,6 +28,8 @@ open Printf open CicNotationEnv open CicNotationPt +let print_attributes = true + let pp_binder = function | `Lambda -> "lambda" | `Pi -> "Pi" @@ -42,6 +44,8 @@ let pp_literal l = | `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 -> diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index b979e84c9..e037ca2a9 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -27,6 +27,7 @@ open Printf 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; @@ -48,9 +49,15 @@ let int_set_of_int_list l = 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 = [] @@ -58,16 +65,66 @@ module Patterns = 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 @@ -162,6 +219,15 @@ let ident_of_name n = Ast.Ident (string_of_name n, None) 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 @@ -278,18 +344,27 @@ let ast_of_acic0 term_info acic k = (* 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: @@ -369,27 +444,27 @@ let uri_closure ks k = 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 @@ -407,7 +482,7 @@ let compiler32 (t: Patterns.t) success_k fail_k = 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) -> @@ -447,7 +522,7 @@ let compiler32 (t: Patterns.t) success_k fail_k = 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) -> @@ -470,12 +545,127 @@ let compiler32 (t: Patterns.t) success_k fail_k = 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 @@ -496,7 +686,7 @@ let instantiate term_info name_env term_env pid = 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)) -> @@ -513,7 +703,7 @@ let load_patterns t = 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) @@ -522,11 +712,22 @@ let load_patterns t = 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 () -> @@ -535,19 +736,37 @@ let fresh_id = 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 [] diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index fbd0ea166..21877d0c3 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -23,21 +23,37 @@ * 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 + diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml new file mode 100644 index 000000000..67e966823 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationTag.ml @@ -0,0 +1,58 @@ +(* 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 + diff --git a/helm/ocaml/cic_notation/cicNotationTag.mli b/helm/ocaml/cic_notation/cicNotationTag.mli new file mode 100644 index 000000000..62f9ca091 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationTag.mli @@ -0,0 +1,31 @@ +(* 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 + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index ff0b7fc73..271b0df21 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -23,6 +23,8 @@ * 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 @@ -30,3 +32,86 @@ let fresh_name = 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 + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index 14cec5826..b5e242b7f 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -25,3 +25,16 @@ 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 + diff --git a/helm/ocaml/cic_notation/test_parser.conf.xml b/helm/ocaml/cic_notation/test_parser.conf.xml new file mode 100644 index 000000000..ea371f06d --- /dev/null +++ b/helm/ocaml/cic_notation/test_parser.conf.xml @@ -0,0 +1,12 @@ + +
+ false + + file:///projects/helm/library/coq_contribs + + /tmp/zack/cache + /projects/helm/var + /projects/helm/xml/dtd + +
+ diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 26ece217d..722748a96 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -26,8 +26,8 @@ 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 @@ -80,15 +80,29 @@ let _ = | -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 @@ -114,7 +128,14 @@ let _ = 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 -> -- 2.39.2