From: Stefano Zacchiroli Date: Tue, 20 Sep 2005 15:27:04 +0000 (+0000) Subject: - bugfix: eta abstractions ignores attributed node while counting lambdas X-Git-Tag: LAST_BEFORE_NEW~82 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;p=helm.git - bugfix: eta abstractions ignores attributed node while counting lambdas - permit pattern matching on attributed asts (since attributes are transparent to pattern matching) - wrapped with assert false some unsafe function invocations (e.g. List.map2) - removed reset_href (no longer needed) --- diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 73f66771f..d65eb0a50 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -93,15 +93,12 @@ let vbox = box Ast.V let hvbox = box Ast.HV let hovbox = box Ast.HOV let break = Ast.Layout Ast.Break -(* let reset_href t = Ast.AttributedTerm (`Href [], t) *) -let reset_href t = t -let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) -let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k))) +let builtin_symbol s = Ast.Literal (`Symbol s) +let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) let number s = - reset_href - (add_xml_attrs (RenderingAttrs.number_attributes `MathML) - (Ast.Literal (`Number s))) + add_xml_attrs (RenderingAttrs.number_attributes `MathML) + (Ast.Literal (`Number s)) let ident i = add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None)) @@ -122,7 +119,8 @@ let string_of_sort_kind = function | `Type -> "Type" let pp_ast0 t k = - let rec aux = function + let rec aux = + function | Ast.Appl ts -> add_level_info Ast.apply_prec Ast.apply_assoc (hovbox true true (CicNotationUtil.dress break (List.map k ts))) @@ -353,12 +351,14 @@ let ast_of_acic0 term_info acic k = in let j = ref 0 in let patterns = - List.map2 - (fun (name, ty) pat -> - incr j; - let (capture_variables, rhs) = eat_branch ty pat in - ((name, Some (ctor_puri !j), capture_variables), rhs)) - constructors patterns + try + List.map2 + (fun (name, ty) pat -> + incr j; + let (capture_variables, rhs) = eat_branch ty pat in + ((name, Some (ctor_puri !j), capture_variables), rhs)) + constructors patterns + with Invalid_argument _ -> assert false in idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns)) | Cic.AFix (id, no, funs) -> @@ -428,7 +428,9 @@ let instantiate21 env (* precedence associativity *) l1 = let ty, value = try List.assoc name env - with Not_found -> assert false + with Not_found -> + prerr_endline ("name " ^ name ^ " not found in environment"); + assert false in assert (CicNotationEnv.well_typed ty value); (* INVARIANT *) (* following assertion should be a conditional that makes this @@ -436,8 +438,8 @@ let instantiate21 env (* precedence associativity *) l1 = assert (CicNotationEnv.well_typed expected_ty value); [ CicNotationEnv.term_of_value value ] | Ast.Magic m -> subst_magic env m - | Ast.Literal (`Keyword k) as t -> [ (*reset_href*) (add_keyword_attrs t) ] - | Ast.Literal _ as t -> [ (*reset_href*) t ] + | Ast.Literal (`Keyword k) as t -> [ add_keyword_attrs t ] + | Ast.Literal _ as t -> [ t ] | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] and subst_magic env = function @@ -460,8 +462,8 @@ let instantiate21 env (* precedence associativity *) l1 = instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] | value_set :: tl -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list - (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl + let terms = subst env p in + instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl in instantiate_list [] values | Ast.Opt p -> @@ -505,24 +507,23 @@ let rec pp_ast1 term = let ast_env_of_env env = List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in - 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 prec, assoc, l1 = - try - Hashtbl.find level1_patterns21 pid - with Not_found -> assert false - in - add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1)) +(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *) + (match (get_compiled21 ()) term with + | None -> pp_ast0 term pp_ast1 + | Some (env, pid) -> + let prec, assoc, l1 = + try + Hashtbl.find level1_patterns21 pid + with Not_found -> assert false + in + add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1)) let instantiate32 term_info env symbol args = let rec instantiate_arg = function | Ast.IdentArg (n, name) -> let t = (try List.assoc name env with Not_found -> assert false) in let rec count_lambda = function + | Ast.AttributedTerm (_, t) -> count_lambda t | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body | _ -> 0 in @@ -566,12 +567,15 @@ let load_patterns21 t = set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t)) let ast_of_acic id_to_sort annterm = + debug_print ("ast_of_acic <- " + ^ CicPp.ppterm (Deannotate.deannotate_term annterm)); let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in let ast = ast_of_acic1 term_info annterm in debug_print ("ast_of_acic -> " ^ CicNotationPp.pp_term ast); ast, term_info.uri let pp_ast ast = + debug_print "pp_ast <-"; let ast' = pp_ast1 ast in debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast'); ast'