X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=b7322afd4964d1a5dd3c1667a7ab66eb38cbc466;hb=e5014674aed0dab6f3aa43773c8caeffcfe0ac32;hp=180a8c912f05484c451d856c30a3151586b71b58;hpb=ea7808d83a7d6e03c0e163f0691e268dcd7c2ea4;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 180a8c912..b7322afd4 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -29,16 +29,13 @@ type pattern_id = int type interpretation_id = pattern_id type pretty_printer_id = pattern_id -let default_prec = 50 -let default_assoc = Gramext.NonA +module Ast = CicNotationPt type term_info = - { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t; + { sort: (Cic.id, Ast.sort_kind) Hashtbl.t; uri: (Cic.id, string) Hashtbl.t; } -let warning s = prerr_endline ("CicNotation WARNING: " ^ s) - let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with @@ -64,15 +61,6 @@ let constructor_of_inductive_type uri i j = fst (List.nth (constructors_of_inductive_type uri i) (j-1)) with Not_found -> assert false) -module Ast = CicNotationPt -module Parser = CicNotationParser - -let string_of_name = function - | Cic.Name s -> s - | Cic.Anonymous -> "_" - -let ident_of_name n = Ast.Ident (string_of_name n, None) - let idref id t = Ast.AttributedTerm (`IdRef id, t) let resolve_binder = function @@ -81,32 +69,43 @@ let resolve_binder = function | `Forall -> "\\forall" | `Exists -> "\\exists" +let binder_attributes = [None, "mathcolor", "blue"] +let atop_attributes = [None, "linethickness", "0pt"] +let indent_attributes = [None, "indent", "1em"] +let keyword_attributes = [None, "mathcolor", "blue"] + let pp_ast0 t k = let reset_href t = Ast.AttributedTerm (`Href [], t) in let builtin_symbol s = reset_href (Ast.Literal (`Symbol s)) in + let binder_symbol s = + Ast.AttributedTerm (`XmlAttrs binder_attributes, builtin_symbol s) + in let rec aux = function | Ast.Appl ts -> - Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), - Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts))) + Ast.AttributedTerm (`Level (Ast.apply_prec, Ast.apply_assoc), + Ast.Layout + (Ast.Box ((Ast.HOV, true, true), + (CicNotationUtil.dress + (Ast.Layout Ast.Break) + (List.map k ts))))) | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body) | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> - Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), Ast.Layout (Ast.Box ((Ast.HV, false, true), [ aux_ty ty; - Ast.Layout (Ast.Box ((Ast.H, false, false), [ - builtin_symbol "\\to"; - k body]))]))) + Ast.Layout Ast.Break; + binder_symbol "\\to"; + k body]))) | Ast.Binder (binder_kind, (id, ty), body) -> - Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), Ast.Layout (Ast.Box ((Ast.HV, false, true), [ - Ast.Layout (Ast.Box ((Ast.H, false, false), [ - builtin_symbol (resolve_binder binder_kind); - k id; - builtin_symbol ":"; - aux_ty ty ])); - Ast.Layout (Ast.Box ((Ast.H, false, false), [ - builtin_symbol "."; - k body ]))]))) + binder_symbol (resolve_binder binder_kind); + k id; + builtin_symbol ":"; + aux_ty ty; + Ast.Layout Ast.Break; + builtin_symbol "."; + k body ]))) | t -> CicNotationUtil.visit_ast ~special_k k t and aux_ty = function | None -> builtin_symbol "?" @@ -118,7 +117,6 @@ let pp_ast0 t k = aux t let ast_of_acic0 term_info acic k = -(* prerr_endline "ast_of_acic0"; *) let k = k term_info in let register_uri id uri = Hashtbl.add term_info.uri id uri in let sort_of_id id = @@ -156,13 +154,15 @@ let ast_of_acic0 term_info acic k = | `Set | `Type -> `Pi | `Prop | `CProp -> `Forall in - idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t)) - | Cic.ACast (id,v,t) -> - idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t]) + idref id (Ast.Binder (binder_kind, + (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) + | Cic.ACast (id,v,t) -> idref id (Ast.Cast (k v, k t)) | Cic.ALambda (id,n,s,t) -> - idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t)) + idref id (Ast.Binder (`Lambda, + (CicNotationUtil.name_of_cic_name n, Some (k s)), k t)) | Cic.ALetIn (id,n,s,t) -> - idref id (Ast.LetIn ((ident_of_name n, None), k s, k t)) + idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None), + k s, k t)) | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args)) | Cic.AConst (id,uri,substs) -> register_uri id (UriManager.string_of_uri uri); @@ -188,7 +188,7 @@ let ast_of_acic0 term_info acic k = match (ty, pat) with | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> let (cv, rhs) = eat_branch t t' in - (ident_of_name name, Some (k s)) :: cv, rhs + (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs | _, _ -> [], k pat in let patterns = @@ -235,13 +235,10 @@ let ast_of_acic0 term_info acic k = let level1_patterns21 = Hashtbl.create 211 let level2_patterns32 = Hashtbl.create 211 +let interpretations = Hashtbl.create 211 (* symb -> id list ref *) -let (compiled21: (CicNotationPt.term -> (CicNotationEnv.t * int) option) -option ref) = - ref None -let (compiled32: (Cic.annterm -> ((string * Cic.annterm) list * int) option) -option ref) = - ref None +let compiled21 = ref None +let compiled32 = ref None let pattern21_matrix = ref [] let pattern32_matrix = ref [] @@ -249,23 +246,22 @@ let pattern32_matrix = ref [] let get_compiled21 () = match !compiled21 with | None -> assert false - | Some f -> f + | Some f -> Lazy.force f let get_compiled32 () = match !compiled32 with | None -> assert false - | Some f -> f + | Some f -> Lazy.force f let set_compiled21 f = compiled21 := Some f let set_compiled32 f = compiled32 := Some f let instantiate21 env (* precedence associativity *) l1 = let rec subst_singleton env t = - CicNotationUtil.boxify (subst env t) + CicNotationUtil.group (subst env t) and subst env = function | 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 @@ -277,6 +273,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 -> + [ Ast.AttributedTerm (`XmlAttrs keyword_attributes, t) ] | Ast.Literal _ as t -> [ t ] | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] @@ -290,19 +288,17 @@ let instantiate21 env (* precedence associativity *) l1 = let values = CicNotationUtil.ncombine rec_values in let sep = match sep_opt with - | None -> [] - | Some l -> [ CicNotationPt.Literal l ] - in + | None -> [] + | Some l -> [ Ast.Literal l ] + in let rec instantiate_list acc = function | [] -> List.rev acc | value_set :: [] -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list - ((CicNotationUtil.boxify (subst env p)) :: acc) [] + instantiate_list (CicNotationUtil.group (subst env p) :: acc) [] | value_set :: tl -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list - ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl + instantiate_list (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl in instantiate_list [] values | Ast.Opt p -> @@ -325,7 +321,8 @@ let instantiate21 env (* precedence associativity *) l1 = end | _ -> assert false (* impossible *) and subst_layout env = function - | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl)) + | Ast.Box (kind, tl) -> + Ast.Box (kind, List.concat (List.map (subst env) tl)) | l -> CicNotationUtil.visit_layout (subst_singleton env) l in subst_singleton env l1 @@ -357,15 +354,9 @@ let rec pp_ast1 term = 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 + Ast.AttributedTerm (`Level (precedence, associativity), + (instantiate21 (ast_env_of_env env) l1)) end - let instantiate32 term_info env symbol args = let rec instantiate_arg = function @@ -395,7 +386,7 @@ let rec ast_of_acic1 term_info annterm = let env' = List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env in - let symbol, args, uris = + let _, symbol, args, _, uris = try Hashtbl.find level2_patterns32 pid with Not_found -> assert false @@ -406,10 +397,10 @@ let rec ast_of_acic1 term_info annterm = | _ -> Ast.AttributedTerm (`Href uris, ast) let load_patterns32 t = - set_compiled32 (CicNotationMatcher.Matcher32.compiler t) + set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) let load_patterns21 t = - set_compiled21 (CicNotationMatcher.Matcher21.compiler t) + set_compiled21 (lazy (CicNotationMatcher.Matcher21.compiler t)) let ast_of_acic id_to_sort annterm = let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in @@ -424,17 +415,35 @@ let fresh_id = incr counter; !counter -let add_interpretation (symbol, args) appl_pattern = +let add_interpretation dsc (symbol, args) appl_pattern = let id = fresh_id () in let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in - Hashtbl.add level2_patterns32 id (symbol, args, uris); + Hashtbl.add level2_patterns32 id (dsc, symbol, args, appl_pattern, uris); pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; + (try + let ids = Hashtbl.find interpretations symbol in + ids := id :: !ids + with Not_found -> Hashtbl.add interpretations symbol (ref [id])); id -let add_pretty_printer - ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1 -= +exception Interpretation_not_found +exception Pretty_printer_not_found + +let lookup_interpretations symbol = + try + List.map + (fun id -> + let (dsc, _, args, appl_pattern, _) = + try + Hashtbl.find level2_patterns32 id + with Not_found -> assert false + in + dsc, args, appl_pattern) + !(Hashtbl.find interpretations symbol) + with Not_found -> raise Interpretation_not_found + +let add_pretty_printer ~precedence ~associativity l2 l1 = let id = fresh_id () in let l2' = CicNotationUtil.strip_attributes l2 in Hashtbl.add level1_patterns21 id (precedence, associativity, l1); @@ -442,11 +451,11 @@ let add_pretty_printer load_patterns21 !pattern21_matrix; id -exception Interpretation_not_found -exception Pretty_printer_not_found - let remove_interpretation id = (try + let _, symbol, _, _, _ = Hashtbl.find level2_patterns32 id in + let ids = Hashtbl.find interpretations symbol in + ids := List.filter ((<>) id) !ids; Hashtbl.remove level2_patterns32 id; with Not_found -> raise Interpretation_not_found); pattern32_matrix := List.filter (fun (_, id') -> id <> id') !pattern32_matrix;