-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) =
- 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 =
- 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
-
- (* 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)
-
-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
-
- (* acic -> ast auxiliary function s *)
-