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
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 \
cicNotationLexer.mli \
cicNotationEnv.mli \
cicNotationPp.mli \
+ cicNotationMatcher.mli \
cicNotationFwd.mli \
cicNotationRew.mli \
cicNotationParser.mli \
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
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
+
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
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 *)
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
+
--- /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 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
+
--- /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/
+ *)
+
+module T21 :
+ sig
+ val compiler :
+ (CicNotationPt.term * int) list ->
+ (CicNotationPt.term -> (CicNotationEnv.t * int) option)
+ end
+
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 =
[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) ->
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
| 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 ->
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
| 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))
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 *)
(* 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:
* <name environment, term environment, pattern id>, where
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
| _ -> 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
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";
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
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
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
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
let _ =
load_patterns21 [];
- load_patterns32 []
+(* load_patterns32 [] *)
*)
(** 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 ->
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
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
| 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)
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) ->
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
| 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
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 ->
projects / helm.git / commitdiff