+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)
+