From: Luca Padovani Date: Mon, 11 Jul 2005 13:28:21 +0000 (+0000) Subject: * various bug fix related to the environment returned when a match X-Git-Tag: pre_notation~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ea7808d83a7d6e03c0e163f0691e268dcd7c2ea4;p=helm.git * various bug fix related to the environment returned when a match occurs * first implementation of the "if" magic --- diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index f7f11c46d..f914b01d2 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -56,7 +56,10 @@ let lookup_value env name = snd (List.assoc name env) with Not_found -> raise (Value_not_found name) -let remove env name = List.remove_assoc name env +let remove_name env name = List.remove_assoc name env + +let remove_names env names = + List.filter (fun name, _ -> not (List.mem name names)) env let lookup_term env name = match lookup env name with diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli index be3f6d52d..d4f87097e 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.mli +++ b/helm/ocaml/cic_notation/cicNotationEnv.mli @@ -71,7 +71,8 @@ val lookup_num: t -> string -> string val lookup_opt: t -> string -> value option val lookup_list: t -> string -> value list -val remove: t -> string -> t +val remove_name: t -> string -> t +val remove_names: t -> string list -> t (** {2 Bindings mangling} *) diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 204e945fc..6b1266ec8 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -25,6 +25,7 @@ open Printf +module Pp = CicNotationPp module Pt = CicNotationPt module Env = CicNotationEnv module Util = CicNotationUtil @@ -236,22 +237,34 @@ struct let magichecker map = List.fold_left (fun f (name, m) -> + prerr_endline ("compiling magichecker for " ^ name) ; 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) + | Some env' -> + f env')) + (fun env -> + prerr_endline ("all magics processed ENV = " ^ Pp.pp_env env) ; + Some env) map in let magichooser candidates = List.fold_left (fun f (pid, pl, checker) -> + List.iter (fun p -> prerr_endline ("P = " ^ Pp.pp_term p)) pl ; (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))) + | Some env -> + prerr_endline (String.concat " / " (List.map Pp.pp_term pl)) ; + prerr_endline ("magichoose found a match for " ^ Pp.pp_env env ^ " " ^ string_of_int pid) ; + 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', pid))) (fun _ -> None) candidates in @@ -265,44 +278,72 @@ struct pid, pl, magichecker magic_map) rows in - magichooser candidates + magichooser candidates in M.compiler rows' match_cb (fun _ -> None) and compile_magic = function | Pt.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 = compiler [p_base, 0; p_rec, 1] 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)) + let compiled_base = compiler [p_base, 0] + and compiled_rec = compiler [p_rec, 0] in + (fun term env -> + let aux_base term = + match compiled_base term with + | None -> None + | Some (env', _) -> Some (env', []) + in + let rec aux term = + match compiled_rec term with + | None -> aux_base term + | Some (env', _) -> + 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, rec_envl) -> + Some (base_env, env'' :: rec_envl) + end + in + match aux term with + | None -> None + | Some (base_env, rec_envl) -> + Some (base_env @ Env.coalesce_env p_rec_decls rec_envl @ env)) (* @ env LUCA!!! *) + | Pt.Default (p_some, p_none) -> (* p_none can't bound names *) let p_some_decls = Env.declarations_of_term p_some in let none_env = List.map Env.opt_binding_of_name p_some_decls in let compiled = compiler [p_some, 0] in (fun term env -> match compiled term with - | None -> Some none_env + | None -> Some none_env (* LUCA: @ env ??? *) | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) | _ -> assert false) + + | Pt.If (guard, p) -> + prerr_endline ("guard = " ^ CicNotationPp.pp_term guard) ; + prerr_endline ("p = " ^ CicNotationPp.pp_term p) ; + let compiled_guard = compiler [guard, 0] + and compiled_p = compiler [p, 0] in + (fun term env -> + prerr_endline "GUARDIA?" ; + match compiled_guard term with + | None -> + prerr_endline "SONO CAZZI H2SO4" ; + None + | Some _ -> + begin + prerr_endline "OKKKKKKKKKKKKKK" ; + match compiled_p term with + | None -> None + | Some (env', _) -> + prerr_endline "guardia ok" ; + Some (env' @ env) + end) + | _ -> assert false end diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 4dcc77297..3622a8c92 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -474,6 +474,10 @@ EXTEND DELIM "\\["; some = l2_pattern; DELIM "\\]"; DELIM "\\["; none = l2_pattern; DELIM "\\]" -> Default (some, none) + | SYMBOL "\\IF"; + DELIM "\\["; guard = l2_pattern; DELIM "\\]"; + DELIM "\\["; p = l2_pattern; DELIM "\\]" -> + If (guard, p) ] ]; l2_pattern: LEVEL "10" (* let in *) diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index cb67202a5..696580cdc 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -156,6 +156,8 @@ and pp_magic = function (pp_fold_kind k) (pp_term p_base) acc (pp_term p_rec) | Default (p_some, p_none) -> sprintf "\\DEFAULT \\[%s\\] \\[%s\\]" (pp_term p_some) (pp_term p_none) + | If (p_guard, p) -> + sprintf "\\IF \\[%s\\] \\[%s\\]" (pp_term p_guard) (pp_term p) and pp_fold_kind = function | `Left -> "left" diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index ab484c3eb..0a5a12853 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -109,14 +109,15 @@ and layout_pattern = and magic_term = (* level 1 magics *) - | List0 of term * literal option - | List1 of term * literal option + | List0 of term * literal option (* pattern, separator *) + | List1 of term * literal option (* pattern, separator *) | Opt of term (* level 2 magics *) | Fold of fold_kind * term * string list * term (* base case pattern, recursive case bound names, recursive case pattern *) | Default of term * term (* "some" case pattern, "none" case pattern *) + | If of term * term (* guard, pattern *) and pattern_variable = (* level 1 and 2 variables *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index dac2b4c73..180a8c912 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -265,6 +265,7 @@ let instantiate21 env (* precedence associativity *) l1 = | Ast.AttributedTerm (_, t) -> subst env t | Ast.Variable var -> let name, expected_ty = CicNotationEnv.declaration_of_var var in + prerr_endline ("searching for " ^ name); let ty, value = try List.assoc name env @@ -333,6 +334,7 @@ let rec pp_ast1 term = let rec pp_value = function | CicNotationEnv.NumValue _ as v -> v | CicNotationEnv.StringValue _ as v -> v +(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *) | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) | CicNotationEnv.OptValue None as v -> v | CicNotationEnv.OptValue (Some v) -> @@ -346,16 +348,24 @@ let rec pp_ast1 term = match term with | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t) | _ -> - (match (get_compiled21 ()) term with - | None -> pp_ast0 term pp_ast1 - | Some (env, pid) -> - let precedence, associativity, l1 = - try - Hashtbl.find level1_patterns21 pid - with Not_found -> assert false - in - Ast.AttributedTerm (`Level (precedence, associativity), - (instantiate21 (ast_env_of_env env) l1))) + begin + match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, pid) -> + let precedence, associativity, l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + prerr_endline ("IN " ^ CicNotationPp.pp_term term); + (* LUCA: il termine legato e' lo stesso termine di partenza per cui si innesca il loop infinito *) + let res = Ast.AttributedTerm (`Level (precedence, associativity), + (instantiate21 (ast_env_of_env env) l1)) + in + prerr_endline "OUT"; + res + end + let instantiate32 term_info env symbol args = let rec instantiate_arg = function diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 630fb4361..740a9c146 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -166,10 +166,11 @@ let visit_layout k = function let visit_magic k = function | List0 (t, l) -> List0 (k t, l) - | List1 (t, l) -> List1 (k t, l ) + | List1 (t, l) -> List1 (k t, l) | Opt t -> Opt (k t) | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2) | Default (t1, t2) -> Default (k t1, k t2) + | If (t1, t2) -> If (k t1, k t2) let variables_of_term t = let rec vars = ref [] in