-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 ... +|
+ let env_of_matched pl tl =
+ try
+ List.map2
+ (fun p t ->
+ match p, t with
+ Ast.Variable (Ast.TermVar name), _ ->
+ name, (Env.TermType, Env.TermValue t)
+ | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
+ name, (Env.NumType, Env.NumValue s)
+ | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
+ name, (Env.StringType, Env.StringValue s)
+ | _ -> assert false)
+ pl tl
+ with Invalid_argument _ -> assert false
+
+ 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 ctors ->
+ match m_checker (Env.lookup_term env name) env ctors with
+ | None -> None
+ | Some (env, ctors) -> f env ctors))
+ (fun env ctors -> Some (env, ctors))
+ map
+ in
+ let magichooser candidates =
+ List.fold_left
+ (fun f (pid, pl, checker) ->
+ (fun matched_terms constructors ->
+ let env = env_of_matched pl matched_terms in
+ match checker env constructors with
+ | None -> f matched_terms constructors
+ | Some (env, ctors') ->
+ let magic_map =
+ try List.assoc pid magic_maps with Not_found -> assert false
+ in
+ let env' = Env.remove_names env (List.map fst magic_map) in
+ Some (env', ctors', pid)))
+ (fun _ _ -> None)
+ (List.rev candidates)
+ in
+ let match_cb 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
+ magichooser candidates
+ in
+ M.compiler rows' match_cb (fun _ -> None)
+
+ and compile_magic = function
+ | Ast.Fold (kind, p_base, names, p_rec) ->
+ let p_rec_decls = Env.declarations_of_term p_rec in
+ (* LUCA: p_rec_decls should not contain "names" *)
+ let acc_name = try List.hd names with Failure _ -> assert false in
+ let compiled_base = compiler [p_base, 0]
+ and compiled_rec = compiler [p_rec, 0] in
+ (fun term env ctors ->
+ let aux_base term =
+ match compiled_base term with
+ | None -> None
+ | Some (env', ctors', _) -> Some (env', ctors', [])
+ in
+ let rec aux term =
+ match compiled_rec term with
+ | None -> aux_base term
+ | Some (env', ctors', _) ->
+ begin
+ let acc = Env.lookup_term env' acc_name in
+ let env'' = Env.remove_name env' acc_name in
+ match aux acc with
+ | None -> aux_base term
+ | Some (base_env, ctors', rec_envl) ->
+ let ctors'' = ctors' @ ctors in
+ Some (base_env, ctors'',env'' :: rec_envl)
+ end
+ in
+ match aux term with
+ | None -> None
+ | Some (base_env, ctors, rec_envl) ->
+ let env' =
+ base_env @ Env.coalesce_env p_rec_decls rec_envl @ env
+ (* @ env LUCA!!! *)
+ in
+ Some (env', ctors))
+
+ | Ast.Default (p_some, p_none) -> (* p_none can't bound names *)
+ let p_some_decls = Env.declarations_of_term p_some in
+ let p_none_decls = Env.declarations_of_term p_none in
+ let p_opt_decls =
+ List.filter
+ (fun decl -> not (List.mem decl p_none_decls))
+ p_some_decls