From 6ab174a7f866b87921e66fcc3fdd137a01456c78 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 20 Sep 2005 15:29:00 +0000 Subject: [PATCH] bugfix in default magic handling: consider as having option type only names which appear in the some branch and in the none one (previously all names appearing in the some branch where considered optional) --- helm/ocaml/cic_notation/cicNotationFwd.ml | 19 +++++++++++++++---- helm/ocaml/cic_notation/cicNotationMatcher.ml | 19 +++++++++++++++++-- 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index 3ef1ff7e0..bf4b3e38e 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -35,8 +35,7 @@ let unopt_names names env = | Env.OptType ty, Env.OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl | _ -> assert false) - | _ :: tl -> aux acc tl - (* some pattern may contain only meta names, thus we trash all others *) + | hd :: tl -> aux (hd :: acc) tl | [] -> acc in aux [] env @@ -77,6 +76,7 @@ let instantiate_level2 env term = new_name in let rec aux env term = +(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *) match term with | Ast.AttributedTerm (_, term) -> aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) @@ -129,7 +129,14 @@ let instantiate_level2 env term = | Ast.Ascription (term, name) -> assert false and aux_magic env = function | Ast.Default (some_pattern, none_pattern) -> - (match CicNotationUtil.names_of_term some_pattern with + let some_pattern_names = CicNotationUtil.names_of_term some_pattern in + let none_pattern_names = CicNotationUtil.names_of_term none_pattern in + let opt_names = + List.filter + (fun name -> not (List.mem name none_pattern_names)) + some_pattern_names + in + (match opt_names with | [] -> assert false (* some pattern must contain at least 1 name *) | (name :: _) as names -> (match Env.lookup_value env name with @@ -139,7 +146,11 @@ let instantiate_level2 env term = *) aux (unopt_names names env) some_pattern | Env.OptValue None -> aux env none_pattern - | _ -> assert false)) + | _ -> + prerr_endline (sprintf + "lookup of %s in env %s did not return an optional value" + name (CicNotationPp.pp_env env)); + assert false)) | Ast.Fold (`Left, base_pattern, names, rec_pattern) -> let acc_name = List.hd names in (* names can't be empty, cfr. parser *) let meta_names = diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 8ac7dcdf5..318361c44 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -324,12 +324,27 @@ struct | Ast.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 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 + in + let none_env = List.map Env.opt_binding_of_name p_opt_decls in let compiled = compiler [p_some, 0] in (fun term env -> match compiled term with | None -> Some none_env (* LUCA: @ env ??? *) - | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) + | Some (env', 0) -> + let env' = + List.map + (fun (name, (ty, v)) as binding -> + if List.exists (fun (name', _) -> name = name') p_opt_decls + then Env.opt_binding_some binding + else binding) + env' + in + Some (env' @ env) | _ -> assert false) | Ast.If (p_test, p_true, p_false) -> -- 2.39.2