From df3c83c772b9aede0503d57757899b34a7847e6f Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 19 Sep 2005 12:39:28 +0000 Subject: [PATCH] - bugfix: when backtracking restore the appropriate matched terms instead of keeping the current ones - changed column order while matching constructors, this should speed up the matching since often application head discriminate if a row can be applied or not --- helm/ocaml/cic_notation/cicNotationMatcher.ml | 101 +++++++++--------- helm/ocaml/cic_notation/cicNotationTag.ml | 2 +- 2 files changed, 53 insertions(+), 50 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index a10d0a8bd..8ac7dcdf5 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -116,47 +116,47 @@ struct | _ -> assert false) t - let variable_closure k = + let variable_closure ksucc = (fun matched_terms terms -> +(* prerr_endline "variable_closure"; *) match terms with - | hd :: tl -> k (hd :: matched_terms) tl + | hd :: tl -> ksucc (hd :: matched_terms) tl | _ -> assert false) - let success_closure ks k = + let success_closure ksucc = (fun matched_terms terms -> - match ks matched_terms with - None -> - begin - (* the match has failed, we rollback the last matched term - * into the unmatched ones and call the failure continuation - *) - match matched_terms with - hd :: tl -> k tl (hd :: terms) - | _ -> assert false - end - | Some v -> Some v) - - let constructor_closure ks k = +(* prerr_endline "success_closure"; *) + ksucc matched_terms) + + let constructor_closure ksuccs = (fun matched_terms terms -> +(* prerr_endline "constructor_closure"; *) match terms with | t :: tl -> (try let tag, subterms = P.tag_of_term t in - let k' = List.assoc tag ks in + let k' = List.assoc tag ksuccs in k' matched_terms (subterms @ tl) - with Not_found -> k matched_terms terms) + with Not_found -> None) | [] -> assert false) + let backtrack_closure ksucc kfail = + (fun matched_terms terms -> +(* prerr_endline "backtrack_closure"; *) + match ksucc matched_terms terms with + | Some x -> Some x + | None -> kfail matched_terms terms) + let compiler rows match_cb fail_k = - let rec aux t k = + let rec aux t = if t = [] then - k + (fun _ _ -> fail_k ()) else if are_empty t then - success_closure (match_cb (matched t)) k + success_closure (match_cb (matched t)) else match horizontal_split t with | _, [], _ -> assert false - | Variable, t', [] -> variable_closure (aux (vertical_split t') k) + | Variable, t', [] -> variable_closure (aux (vertical_split t')) | Constructor, t', [] -> let tagl = List.map @@ -166,7 +166,7 @@ struct t' in let clusters = partition t' tagl in - let ks = + let ksuccs = List.map (fun (tag, cluster) -> let cluster' = @@ -178,14 +178,14 @@ struct | _ -> assert false) cluster in - tag, aux cluster' k) + tag, aux cluster') clusters in - constructor_closure ks k - | _, t', t'' -> aux t' (aux t'' k) + constructor_closure ksuccs + | _, t', t'' -> backtrack_closure (aux t') (aux t'') in let t = List.map (fun (p, pid) -> [], [p], pid) rows in - let matcher = aux t (fun _ _ -> fail_k ()) in + let matcher = aux t in (fun term -> matcher [] [term]) end @@ -203,7 +203,7 @@ struct | Ast.Literal _ as t -> assert false | _ -> Constructor let tag_of_pattern = CicNotationTag.get_tag - let tag_of_term = CicNotationTag.get_tag + let tag_of_term t = CicNotationTag.get_tag t end module M = Matcher (Pattern21) @@ -227,17 +227,19 @@ struct term', !magic_map let env_of_matched pl tl = - 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 + 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 = @@ -255,8 +257,7 @@ struct (fun env -> match m_checker (Env.lookup_term env name) env with | None -> None - | Some env' -> - f env')) + | Some env' -> f env')) (fun env -> Some env) map in @@ -286,7 +287,7 @@ struct pid, pl, magichecker magic_map) rows in - magichooser candidates + magichooser candidates in M.compiler rows' match_cb (fun _ -> None) @@ -400,13 +401,15 @@ struct let pl, pid = try List.hd rows with Not_found -> assert false in (fun matched_terms -> let env = - List.map2 - (fun p t -> - match p with - | Ast.ImplicitPattern -> Util.fresh_name (), t - | Ast.VarPattern name -> name, t - | _ -> assert false) - pl matched_terms + try + List.map2 + (fun p t -> + match p with + | Ast.ImplicitPattern -> Util.fresh_name (), t + | Ast.VarPattern name -> name, t + | _ -> assert false) + pl matched_terms + with Invalid_argument _ -> assert false in Some (env, pid)) in diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml index 53ac5e2d1..3cbffa2db 100644 --- a/helm/ocaml/cic_notation/cicNotationTag.ml +++ b/helm/ocaml/cic_notation/cicNotationTag.ml @@ -41,5 +41,5 @@ let get_tag term0 = in let term_mask = aux term0 in let tag = Hashtbl.hash term_mask in - tag, !subterms + tag, List.rev !subterms -- 2.39.2