From: Stefano Zacchiroli Date: Sat, 4 Jun 2005 14:34:18 +0000 (+0000) Subject: snapshot X-Git-Tag: PRE_INDEX_1~71 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;p=helm.git snapshot - regression, but better (and working!) implementation of ML pattern matching - not yet ported 3 -> 2 pattern matching ... the dunwich horror ... --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index 18171c9da..980ae1260 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -2,6 +2,7 @@ cicNotationUtil.cmi: cicNotationPt.cmo cicNotationTag.cmi: cicNotationPt.cmo cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationMatcher.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationRew.cmi: cicNotationPt.cmo cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi @@ -15,14 +16,20 @@ cicNotationEnv.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi +cicNotationMatcher.cmo: cicNotationUtil.cmi cicNotationTag.cmi \ + cicNotationPt.cmo cicNotationPp.cmi cicNotationEnv.cmi \ + cicNotationMatcher.cmi +cicNotationMatcher.cmx: cicNotationUtil.cmx cicNotationTag.cmx \ + cicNotationPt.cmx cicNotationPp.cmx cicNotationEnv.cmx \ + cicNotationMatcher.cmi cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ cicNotationFwd.cmi cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \ cicNotationFwd.cmi -cicNotationRew.cmo: cicNotationUtil.cmi cicNotationTag.cmi cicNotationPt.cmo \ - cicNotationRew.cmi -cicNotationRew.cmx: cicNotationUtil.cmx cicNotationTag.cmx cicNotationPt.cmx \ - cicNotationRew.cmi +cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ + cicNotationMatcher.cmi cicNotationEnv.cmi cicNotationRew.cmi +cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ + cicNotationMatcher.cmx cicNotationEnv.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 7102f2ea7..76048ac80 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -14,6 +14,7 @@ INTERFACE_FILES = \ cicNotationLexer.mli \ cicNotationEnv.mli \ cicNotationPp.mli \ + cicNotationMatcher.mli \ cicNotationFwd.mli \ cicNotationRew.mli \ cicNotationParser.mli \ diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index b6ae4e6be..749e9148b 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -50,6 +50,8 @@ let lookup_value env name = snd (List.assoc name env) with Not_found -> raise (Value_not_found name) +let remove env name = List.remove_assoc name env + let lookup_term env name = match lookup_value env name with | TermValue x -> x @@ -100,3 +102,22 @@ let rec well_typed ty value = List.for_all (fun value' -> well_typed ty' value') vl | _ -> false +let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty)) + +let coalesce_env declarations env_list = + let env0 = List.map list_binding_of_name declarations in + let grow_env_entry env n v = + List.map + (function + | (n', (ty, ListValue vl)) as entry -> + if n' = n then n', (ty, ListValue (v :: vl)) else entry + | _ -> assert false) + env + in + let grow_env env_i env = + List.fold_left + (fun env (n, (_, v)) -> grow_env_entry env n v) + env env_i + in + List.fold_right grow_env env_list env0 + diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli index 877a16f52..7729caef9 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.mli +++ b/helm/ocaml/cic_notation/cicNotationEnv.mli @@ -50,6 +50,8 @@ val value_of_term: CicNotationPt.term -> value val term_of_value: value -> CicNotationPt.term val well_typed: value_type -> value -> bool +val declarations_of_env: t -> declaration list + (** {2 Environment lookup} *) val lookup_value: t -> string -> value @@ -57,6 +59,8 @@ val lookup_num: t -> string -> string val lookup_string: t -> string -> string val lookup_term: t -> string -> CicNotationPt.term +val remove: t -> string -> t + (** {2 Bindings mangling} *) val opt_binding_some: binding -> binding (* v -> Some v *) @@ -68,3 +72,8 @@ val list_binding_of_name: declaration -> binding (* [] binding *) val opt_declaration: declaration -> declaration (* t -> OptType t *) val list_declaration: declaration -> declaration (* t -> ListType t *) +(** given a list of environments bindings a set of names n_1, ..., n_k, returns + * a single environment where n_i is bound to the list of values bound in the + * starting environments *) +val coalesce_env: declaration list -> t list -> t + diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml new file mode 100644 index 000000000..8da7a483d --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -0,0 +1,333 @@ +(* 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 Printf + +module Pt = CicNotationPt +module Env = CicNotationEnv +module Util = CicNotationUtil + +type pattern_id = int + +exception No_match + +module OrderedInt = + struct + type t = int + let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) + end + +module IntSet = Set.Make (OrderedInt) + +let int_set_of_int_list l = + List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l + +module type PATTERN = + sig + type pattern_t + val compatible : pattern_t -> pattern_t -> bool + end + +module Patterns (P: PATTERN) = + struct + type row_t = P.pattern_t list * P.pattern_t list * pattern_id + type t = row_t list + + let empty = [] + + let matched = List.map (fun (matched, _, pid) -> matched, pid) + + 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 = + match t with + | (_, [], _) :: _ -> true + (* if first row has an empty list of patterns, then others have as well *) + | _ -> false + + (* return 2 lists of rows, first one containing homogeneous rows according + * to "compatible" below *) + let horizontal_split t = + let ap, first_row, t' = + match t with + | [] -> assert false + | (_, [], _) :: _ -> + assert false (* are_empty should have been invoked in advance *) + | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl + 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 [first_row] t' + + (* return 2 lists, first one representing first column, second one + * representing a new pattern matrix where matched patterns have been moved + * to decl *) + let vertical_split t = + List.map + (function + | decls, hd :: tl, pid -> hd :: decls, tl, pid + | _ -> assert false) + t + end + +module T21 = +struct + +module P = Patterns (CicNotationTag) + +(* let return_closure matched = + (fun matched_terms terms -> + prerr_endline "T21.return_closure"; + match terms with + | [] -> matched_terms, matched + | _ -> assert false) *) + +let variable_closure k = + (fun matched_terms terms -> + prerr_endline "T21.variable_closure"; + match terms with + | hd :: tl -> + prerr_endline (sprintf "binding: %s" (CicNotationPp.pp_term hd)); + k (hd :: matched_terms) tl + | _ -> assert false) + +let constructor_closure ks k = + (fun matched_terms terms -> + prerr_endline "T21.constructor_closure"; + match terms with + | t :: tl -> + prerr_endline (sprintf "on term %s" (CicNotationPp.pp_term t)); + (try + let tag, subterms = CicNotationTag.get_tag t in + let k' = List.assoc tag ks in + k' matched_terms (subterms @ tl) + with Not_found -> k matched_terms terms) + | [] -> assert false) + +(* let fold_closure kind p_names names matcher success_k k = + let acc_name = try List.hd names with Failure _ -> assert false in +|+ List.iter (fun (name, _) -> Printf.printf "/// %s\n" name) p_names ; +| + (fun matched_terms terms -> + prerr_endline "T21.fold_closure"; + (match terms with + | t :: tl -> + let rec aux t = + prerr_endline "PORCA TORCIA SONO IN AUX" ; + match matcher t with + | _, [] -> None + | matched_terms, [matched_p, 0] -> Some (matched_terms, []) + | matched_terms, [matched_p, 1] -> + let acc = CicNotationEnv.lookup_term env acc_name in + let env = CicNotationEnv.remove env acc_name in + (match aux acc with + | None -> None + | Some env' -> Some (env :: env')) + | envl -> + List.iter + (fun (env, pid) -> + Printf.printf "*** %s %d\n" (CicNotationPp.pp_env env) pid) + envl ; + flush stdout ; + assert false |+ overlapping patterns, to be handled ... +| + in + (match aux t with + | None -> k terms envl + | Some env -> + let magic_env = CicNotationEnv.coalesce_env p_names env in + List.map (fun (env, pid) -> magic_env @ env, pid) envl) + | [] -> assert false)) *) + +let compiler0 rows match_cb fail_k = + let rec aux t k = + if t = [] then + k + else if P.are_empty t then + match_cb (P.matched t) + else + match P.horizontal_split t with + | t', [] -> + (match t' with + | [] + | (_, [], _) :: _ -> assert false + | (_, Pt.Variable _ :: _, _) :: _ -> + variable_closure (aux (P.vertical_split t') k) + | _ -> + let tagl = + List.map + (function + | _, p :: _, _ -> fst (CicNotationTag.get_tag p) + | _ -> assert false) + t' + in + let clusters = P.partition t' tagl in + let ks = + List.map + (fun (tag, cluster) -> + let cluster' = + List.map (* add args as patterns heads *) + (function + | matched_p, p :: tl, pid -> + let _, subpatterns = CicNotationTag.get_tag p in + matched_p, subpatterns @ tl, pid + | _ -> assert false) + cluster + in + tag, aux cluster' k) + clusters + in + constructor_closure ks k) + | t', tl -> aux t' (aux tl k) + in + let t = List.map (fun (p, pid) -> [], [p], pid) rows in + let matcher = aux t (fun _ _ -> fail_k ()) in + (fun term -> matcher [] [term]) + +let extract_magic term = + let magic_map = ref [] in + let add_magic m = + let name = Util.fresh_name () in + magic_map := (name, m) :: !magic_map; + Pt.Variable (Pt.TermVar name) + in + let rec aux = function + | Pt.AttributedTerm (_, t) -> aux t + | Pt.Literal _ + | Pt.Layout _ -> assert false + | Pt.Variable v -> Pt.Variable v + | Pt.Magic m -> add_magic m + | t -> Util.visit_ast aux t + in + let term' = aux term in + term', !magic_map + +let env_of_matched pl tl = + List.map2 + (fun p t -> + match p, t with + Pt.Variable (Pt.TermVar name), _ -> + name, (Env.TermType, Env.TermValue t) + | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> + name, (Env.NumType, Env.NumValue s) + | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> + name, (Env.StringType, Env.StringValue s) + | _ -> assert false) + pl tl + +let decls_of_pattern p = + List.map Env.declaration_of_var (Util.variables_of_term p) + +let rec compiler rows = + let rows', magic_maps = + List.split + (List.map + (fun (p, pid) -> + let p', map = extract_magic p in + (p', pid), (pid, map)) + rows) + in + let magichecker map = + List.fold_left + (fun f (name, m) -> + let m_checker = compile_magic m in + (fun env -> + match m_checker (Env.lookup_term env name) env with + | None -> None + | Some env' -> f env')) + (fun env -> Some env) + map + in + let magichooser candidates = + List.fold_left + (fun f (pid, pl, checker) -> + (fun matched_terms -> + let env = env_of_matched pl matched_terms in + match checker env with + | None -> f matched_terms + | Some env -> Some (env, pid))) + (fun _ -> None) + candidates + in + let match_cb rows = + prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); + let candidates = + List.map + (fun (pl, pid) -> + let magic_map = + try List.assoc pid magic_maps with Not_found -> assert false + in + pid, pl, magichecker magic_map) + rows + in + (fun matched_terms _ -> magichooser candidates matched_terms) + in + compiler0 rows match_cb (fun _ -> None) + +and compile_magic = function + | Pt.Fold (kind, p_base, names, p_rec) -> + let p_rec_decls = decls_of_pattern p_rec in + let acc_name = try List.hd names with Failure _ -> assert false in + let t_magic = [p_base, 0; p_rec, 1] in + let compiled = compiler t_magic in + (fun term env -> + let rec aux term = + match compiled term with + | None -> None + | Some (env', 0) -> Some (env', []) + | Some (env', 1) -> + begin + let acc = Env.lookup_term env' acc_name in + let env'' = Env.remove env' acc_name in + match aux acc with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env, env'' :: rec_envl ) + end + | _ -> assert false + in + match aux term with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env @ Env.coalesce_env p_rec_decls rec_envl)) + | _ -> assert false + +end + diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli new file mode 100644 index 000000000..e999b3c6a --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli @@ -0,0 +1,32 @@ +(* 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/ + *) + +module T21 : + sig + val compiler : + (CicNotationPt.term * int) list -> + (CicNotationPt.term -> (CicNotationEnv.t * int) option) + end + diff --git a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml index fcbc081a7..7b90be54a 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.expanded.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.expanded.ml @@ -54,37 +54,27 @@ ttype binding = llet make_action action bindings = let rec aux (vl : env_type) = function - [] -> - prerr_endline "aux: make_action"; - Gramext.action (fun (loc : location) -> action vl loc) - | NoBinding :: tl -> - prerr_endline "aux: none"; Gramext.action (fun _ -> aux vl tl) + [] -> Gramext.action (fun (loc : location) -> action vl loc) + | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) | Binding (name, TermType) :: tl -> - prerr_endline "aux: term"; Gramext.action (fun (v : term) -> aux ((name, (TermType, TermValue v)) :: vl) tl) | Binding (name, StringType) :: tl -> - prerr_endline "aux: string"; Gramext.action (fun (v : string) -> aux ((name, (StringType, StringValue v)) :: vl) tl) | Binding (name, NumType) :: tl -> - prerr_endline "aux: num"; Gramext.action (fun (v : string) -> aux ((name, (NumType, NumValue v)) :: vl) tl) | Binding (name, OptType t) :: tl -> - prerr_endline "aux: opt"; Gramext.action (fun (v : 'a option) -> aux ((name, (OptType t, OptValue v)) :: vl) tl) | Binding (name, ListType t) :: tl -> - prerr_endline "aux: list"; Gramext.action (fun (v : 'a list) -> aux ((name, (ListType t, ListValue v)) :: vl) tl) - | Env _ :: tl -> - prerr_endline "aux: env"; - Gramext.action (fun (v : env_type) -> aux (v @ vl) tl) + | Env _ :: tl -> Gramext.action (fun (v : env_type) -> aux (v @ vl) tl) in aux [] (List.rev bindings) llet flatten_opt = @@ -975,8 +965,7 @@ let _ = [Gramext.Stoken ("NUMBER", "")], Gramext.action (fun (n : string) (loc : Lexing.position * Lexing.position) -> - (prerr_endline "number"; return_term loc (Num (n, 0)) : - 'l2_pattern)); + (return_term loc (Num (n, 0)) : 'l2_pattern)); [Gramext.Stoken ("URI", "")], Gramext.action (fun (u : string) (loc : Lexing.position * Lexing.position) -> diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index fa8b65ed0..ea66d6af4 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -79,38 +79,28 @@ type binding = let make_action action bindings = let rec aux (vl : CicNotationEnv.t) = function - [] -> - prerr_endline "aux: make_action"; - Gramext.action (fun (loc: location) -> action vl loc) - | NoBinding :: tl -> - prerr_endline "aux: none"; - Gramext.action (fun _ -> aux vl tl) + [] -> Gramext.action (fun (loc: location) -> action vl loc) + | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) (* LUCA: DEFCON 5 BEGIN *) | Binding (name, TermType) :: tl -> - prerr_endline "aux: term"; Gramext.action (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl) | Binding (name, StringType) :: tl -> - prerr_endline "aux: string"; Gramext.action (fun (v:string) -> aux ((name, (StringType, StringValue v)) :: vl) tl) | Binding (name, NumType) :: tl -> - prerr_endline "aux: num"; Gramext.action (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl) | Binding (name, OptType t) :: tl -> - prerr_endline "aux: opt"; Gramext.action (fun (v:'a option) -> aux ((name, (OptType t, OptValue v)) :: vl) tl) | Binding (name, ListType t) :: tl -> - prerr_endline "aux: list"; Gramext.action (fun (v:'a list) -> aux ((name, (ListType t, ListValue v)) :: vl) tl) | Env _ :: tl -> - prerr_endline "aux: env"; Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl) (* LUCA: DEFCON 5 END *) in @@ -172,9 +162,8 @@ let extract_term_production pattern = | List0 (p, _) | List1 (p, _) -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let env0 = List.map list_binding_of_name p_names in +(* let env0 = List.map list_binding_of_name p_names in let grow_env_entry env n v = - prerr_endline "grow_env_entry"; List.map (function | (n', (ty, ListValue vl)) as entry -> @@ -183,14 +172,12 @@ let extract_term_production pattern = env in let grow_env env_i env = - prerr_endline "grow_env"; List.fold_left (fun env (n, (_, v)) -> grow_env_entry env n v) env env_i - in + in *) let action (env_list : CicNotationEnv.t list) (loc : location) = - prerr_endline "list action"; - List.fold_right grow_env env_list env0 + CicNotationEnv.coalesce_env p_names env_list in let g_symbol s = match magic with @@ -512,7 +499,7 @@ EXTEND | 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)) + | n = NUMBER -> return_term loc (Num (n, 0)) | IMPLICIT -> return_term loc (Implicit) | m = META -> return_term loc (Meta (int_of_string m, [])) | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s)) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 7dd973989..ec385efce 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -34,153 +34,20 @@ type term_info = uri: (Cic.id, string) Hashtbl.t; } -exception No_match - -module OrderedInt = - struct - type t = int - let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) - end - -module IntSet = Set.Make (OrderedInt) - -let int_set_of_int_list l = - List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l - let warning s = prerr_endline ("CicNotation WARNING: " ^ s) -module type PATTERN = - sig - type pattern_t - val compatible : pattern_t -> pattern_t -> bool - end - -module Patterns (P: PATTERN) = +(* module Pattern32 = struct - 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 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, first_row, t' = - match t with - | [] -> assert false - | ([], _) :: _ -> - assert false (* are_empty should have been invoked in advance *) - | ((hd :: _ , _) as row) :: tl -> hd, row, tl - 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 [first_row] t' - - (* 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 + type pattern_t = CicNotationPt.cic_appl_pattern + let compatible ap1 ap2 = + match ap1, ap2 with + | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ + | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ + | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true + | _ -> false end -module Patterns21 = Patterns (CicNotationTag) - -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 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 compatible ap1 ap2 = - match ap1, ap2 with - | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ - | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ - | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true - | _ -> false - in - 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 compatible ap hd -> - aux (row :: prev_t) tl - | t -> List.rev prev_t, t - in - aux [] t - - (* 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 Patterns32 = Patterns (Pattern32) *) (* acic -> ast auxiliary function s *) @@ -345,27 +212,28 @@ let ast_of_acic0 term_info acic k = (* persistent state *) let level1_patterns21 = Hashtbl.create 211 -let level2_patterns32 = 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) = +let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * pattern_id) option) +option ref) = ref None +(* let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) = + ref None *) -let pattern21_matrix = ref Patterns21.empty -let pattern32_matrix = ref Patterns32.empty +let pattern21_matrix = ref [] +(* let pattern32_matrix = ref Patterns32.empty *) let get_compiled21 () = match !compiled21 with | None -> assert false | Some f -> f -let get_compiled32 () = +(* let get_compiled32 () = match !compiled32 with | None -> assert false - | Some f -> f + | Some f -> f *) let set_compiled21 f = compiled21 := Some f -let set_compiled32 f = compiled32 := Some f +(* let set_compiled32 f = compiled32 := Some f *) (* "envl" is a list of triples: * , where @@ -444,15 +312,15 @@ let uri_closure ks k = end)) (* compiler from level 3 to level 2 *) -let compiler32 (t: Patterns32.t) success_k fail_k = - let rec aux t k = (* k is a continuation *) +(* let compiler32 (t: Patterns32.t) success_k fail_k = + let rec aux t k = |+ k is a continuation +| if t = [] then k else if Patterns32.are_empty t then begin (match t with | _::_::_ -> - (* XXX optimization possible here: throw away all except one of the - * rules which lead to ambiguity *) + |+ XXX optimization possible here: throw away all except one of the + * rules which lead to ambiguity +| warning "ambiguous interpretation" | _ -> ()); return_closure success_k @@ -481,16 +349,16 @@ let compiler32 (t: Patterns32.t) success_k fail_k = | _ -> assert false) t' in - (* arity partitioning *) + |+ arity partitioning +| let clusters = Patterns32.partition t' pidl in - let ks = (* k continuation list *) + let ks = |+ k continuation list +| List.map (fun (len, cluster) -> let cluster' = - List.map (* add args as patterns heads *) + List.map |+ add args as patterns heads +| (function | (Ast.ApplPattern args) :: tl, pid -> - (* let's throw away "teste di cluster" *) + |+ let's throw away "teste di cluster" +| args @ tl, pid | _ -> assert false) cluster @@ -545,107 +413,7 @@ let compiler32 (t: Patterns32.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 (name, ty) (env, pid) -> - (name, (ty, CicNotationEnv.value_of_term 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 -> CicNotationEnv.declaration_of_var 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 pp_ast1 term = (get_compiled21 ()) term +let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm *) let instantiate21 env pid = prerr_endline "instantiate21"; @@ -675,7 +443,25 @@ let instantiate21 env pid = and subst_layout l = CicNotationUtil.visit_layout subst l in subst l1 -let instantiate32 term_info name_env term_env pid = +let rec pp_ast1 term = + let rec pp_value = function + | CicNotationEnv.NumValue _ as v -> v + | CicNotationEnv.StringValue _ as v -> v + | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) + | CicNotationEnv.OptValue None as v -> v + | CicNotationEnv.OptValue (Some v) -> + CicNotationEnv.OptValue (Some (pp_value v)) + | CicNotationEnv.ListValue vl -> + CicNotationEnv.ListValue (List.map pp_value vl) + in + let ast_env_of_env env = + List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env + in + match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, pid) -> instantiate21 (ast_env_of_env env) pid + +(* let instantiate32 term_info name_env term_env pid = let symbol, args = try Hashtbl.find level2_patterns32 pid @@ -684,7 +470,7 @@ let instantiate32 term_info name_env term_env pid = let rec instantiate_arg = function | Ast.IdentArg name -> (try List.assoc name term_env with Not_found -> assert false) - | Ast.EtaArg (None, _) -> assert false (* TODO *) + | Ast.EtaArg (None, _) -> assert false |+ TODO +| | Ast.EtaArg (Some name, arg) -> let (name', ty_opt) = try List.assoc name name_env with Not_found -> assert false @@ -723,31 +509,15 @@ let load_patterns32 t = pid in let compiled32 = compiler32 t success_k fail_k in - set_compiled32 compiled32 + set_compiled32 compiled32 *) let load_patterns21 t = - let rec pp_value = function - | CicNotationEnv.NumValue _ as v -> v - | CicNotationEnv.StringValue _ as v -> v - | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) - | CicNotationEnv.OptValue None as v -> v - | CicNotationEnv.OptValue (Some v) -> - CicNotationEnv.OptValue (Some (pp_value v)) - | CicNotationEnv.ListValue vl -> - CicNotationEnv.ListValue (List.map pp_value vl) - in - let ast_env_of_env env = - List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) 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 + set_compiled21 (CicNotationMatcher.T21.compiler t) -let ast_of_acic id_to_sort annterm = +(* 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 + ast, term_info.uri *) let pp_ast term = pp_ast1 term @@ -757,30 +527,30 @@ let fresh_id = incr counter; !counter -let add_interpretation (symbol, args) appl_pattern = +(* let add_interpretation (symbol, args) appl_pattern = let id = fresh_id () in Hashtbl.add level2_patterns32 id (symbol, args); pattern32_matrix := ([appl_pattern], id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; - id + 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; + pattern21_matrix := (l2', id) :: !pattern21_matrix; load_patterns21 !pattern21_matrix; id exception Interpretation_not_found exception Pretty_printer_not_found -let remove_interpretation id = +(* let remove_interpretation id = (try Hashtbl.remove level2_patterns32 id; with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix; - load_patterns32 !pattern32_matrix + load_patterns32 !pattern32_matrix *) let remove_pretty_printer id = (try @@ -791,5 +561,5 @@ let remove_pretty_printer id = let _ = load_patterns21 []; - load_patterns32 [] +(* load_patterns32 [] *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 21877d0c3..a57ddd0de 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -24,22 +24,22 @@ *) (** 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 *) +(* 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 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_interpretation: + string * CicNotationPt.argument_pattern list -> |+ level 2 pattern +| + CicNotationPt.cic_appl_pattern -> |+ level 3 pattern +| + interpretation_id *) val add_pretty_printer: ?precedence:int -> @@ -52,7 +52,7 @@ exception Interpretation_not_found exception Pretty_printer_not_found (** @raise Interpretation_not_found *) -val remove_interpretation: interpretation_id -> unit +(* 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/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 271b0df21..18e04640a 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -32,6 +32,72 @@ let fresh_name = incr index; "fresh" ^ string_of_int !index +(* let meta_names_of term = *) +(* let rec names = ref [] in *) +(* let add_name n = *) +(* if List.mem n !names then () *) +(* else names := n :: !names *) +(* in *) +(* let rec aux = function *) +(* | AttributedTerm (_, term) -> aux term *) +(* | Appl terms -> List.iter aux terms *) +(* | Binder (_, _, body) -> aux body *) +(* | Case (term, indty, outty_opt, patterns) -> *) +(* aux term ; *) +(* aux_opt outty_opt ; *) +(* List.iter aux_branch patterns *) +(* | LetIn (_, t1, t2) -> *) +(* aux t1 ; *) +(* aux t2 *) +(* | LetRec (_, definitions, body) -> *) +(* List.iter aux_definition definitions ; *) +(* aux body *) +(* | Uri (_, Some substs) -> aux_substs substs *) +(* | Ident (_, Some substs) -> aux_substs substs *) +(* | Meta (_, substs) -> aux_meta_substs substs *) + +(* | Implicit *) +(* | Ident _ *) +(* | Num _ *) +(* | Sort _ *) +(* | Symbol _ *) +(* | Uri _ *) +(* | UserInput -> () *) + +(* | Magic magic -> aux_magic magic *) +(* | Variable var -> aux_variable var *) + +(* | _ -> assert false *) +(* and aux_opt = function *) +(* | Some term -> aux term *) +(* | None -> () *) +(* and aux_capture_var (_, ty_opt) = aux_opt ty_opt *) +(* and aux_branch (pattern, term) = *) +(* aux_pattern pattern ; *) +(* aux term *) +(* and aux_pattern (head, vars) = *) +(* List.iter aux_capture_var vars *) +(* and aux_definition (var, term, i) = *) +(* aux_capture_var var ; *) +(* aux term *) +(* and aux_substs substs = List.iter (fun (_, term) -> aux term) substs *) +(* and aux_meta_substs meta_substs = List.iter aux_opt meta_substs *) +(* and aux_variable = function *) +(* | NumVar name -> add_name name *) +(* | IdentVar name -> add_name name *) +(* | TermVar name -> add_name name *) +(* | FreshVar _ -> () *) +(* | Ascription _ -> assert false *) +(* and aux_magic = function *) +(* | Default (t1, t2) *) +(* | Fold (_, t1, _, t2) -> *) +(* aux t1 ; *) +(* aux t2 *) +(* | _ -> assert false *) +(* in *) +(* aux term ; *) +(* !names *) + let visit_ast ?(special_k = fun _ -> assert false) k = let rec aux = function @@ -105,8 +171,41 @@ let visit_magic k = function | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2) | Default (t1, t2) -> Default (k t1, k t2) +let variables_of_term t = + let rec vars = ref [] in + let add_variable v = + if List.mem v !vars then () + else vars := v :: !vars + in + let rec aux = function + | Magic m -> Magic (visit_magic aux m) + | Layout l -> Layout (visit_layout aux l) + | Variable v -> Variable (aux_variable v) + | Literal _ as t -> t + | AttributedTerm (_, t) -> aux t + | t -> visit_ast aux t + and aux_variable = function + | (NumVar _ + | IdentVar _ + | TermVar _) as t -> + add_variable t ; + t + | FreshVar _ as t -> t + | Ascription _ -> assert false + in + ignore (aux t) ; + !vars + +let names_of_term t = + let aux = function + | NumVar s + | IdentVar s + | TermVar s -> s + | _ -> assert false + in + List.map aux (variables_of_term t) + 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) diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli index b5e242b7f..92eaf8e8b 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.mli +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -25,6 +25,9 @@ val fresh_name: unit -> string +val variables_of_term: CicNotationPt.term -> CicNotationPt.pattern_variable list +val names_of_term: CicNotationPt.term -> string list + val visit_ast: ?special_k:(CicNotationPt.term -> CicNotationPt.term) -> (CicNotationPt.term -> CicNotationPt.term) -> diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 722748a96..5b42822c2 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -89,10 +89,7 @@ let _ = 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)); + (fun env loc -> CicNotationFwd.instantiate_level2 env l2)); let time2 = Unix.gettimeofday () in print_endline "Extending pretty printer ..."; flush stdout; let time3 = Unix.gettimeofday () in @@ -106,13 +103,14 @@ let _ = | P.Interpretation (l2, l3) -> print_endline "Adding interpretation ..."; flush stdout; let time1 = Unix.gettimeofday () in - ignore (CicNotationRew.add_interpretation l2 l3); +(* ignore (CicNotationRew.add_interpretation l2 l3); *) let time2 = Unix.gettimeofday () in printf "done (patterns compilation took %f seconds)\n" (time2 -. time1); flush stdout | P.Render uri -> - let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + assert false +(* let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let annobj, _, _, id_to_sort, _, _, _ = Cic2acic.acic_object_of_cic_object obj in @@ -135,7 +133,8 @@ let _ = 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) + print_endline (CicNotationPp.pp_term t'); flush stdout *) + ) (* CicNotationParser.print_l2_pattern ()) *) | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream) | 2 ->