X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=28edd491c84e7e32e97425176cb728e007e723e3;hb=5a7ff7a3ce24bd14385d2295a1c77fad4b876cb8;hp=91b40fbee1fc1faa92868d8d01a774db3591b66f;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 91b40fbee..28edd491c 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -29,9 +29,6 @@ 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 = @@ -72,50 +69,188 @@ 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 add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) + +let rec remove_level_info = + function + | Ast.AttributedTerm (`Level _, t) -> remove_level_info t + | Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t) + | t -> t + +let add_xml_attrs attrs t = Ast.AttributedTerm (`XmlAttrs attrs, t) +let add_keyword_attrs = + add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) +let box kind spacing indent content = + Ast.Layout (Ast.Box ((kind, spacing, indent), content)) +let hbox = box Ast.H +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 number s = + reset_href + (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)) +let binder_symbol s = + add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML) + (builtin_symbol s) + +let string_of_sort_kind = function + | `Prop -> "Prop" + | `Set -> "Set" + | `CProp -> "CProp" + | `Type -> "Type" 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 (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 (Ast.binder_prec, Ast.binder_assoc), - Ast.Layout (Ast.Box ((Ast.HV, false, true), [ - aux_ty ty; - Ast.Layout Ast.Break; - binder_symbol "\\to"; - k body]))) + add_level_info Ast.apply_prec Ast.apply_assoc + (hovbox true true (CicNotationUtil.dress break (List.map k ts))) | Ast.Binder (binder_kind, (id, ty), body) -> - Ast.AttributedTerm (`Level (Ast.binder_prec, Ast.binder_assoc), - Ast.Layout (Ast.Box ((Ast.HV, false, true), [ - binder_symbol (resolve_binder binder_kind); - k id; - builtin_symbol ":"; - aux_ty ty; - Ast.Layout Ast.Break; - builtin_symbol "."; - k body ]))) + add_level_info Ast.binder_prec Ast.binder_assoc + (hvbox false true + [ binder_symbol (resolve_binder binder_kind); + k id; builtin_symbol ":"; aux_ty ty; break; + builtin_symbol "."; k body ]) + | Ast.Case (what, indty_opt, outty_opt, patterns) -> + let outty_box = + match outty_opt with + | None -> [] + | Some outty -> + [ builtin_symbol "["; remove_level_info (k outty); + builtin_symbol "]"; break ] + in + let indty_box = + match indty_opt with + | None -> [] + | Some indty -> [ keyword "in"; ident indty ] + in + let match_box = + hvbox false true [ + keyword "match"; break; + hvbox false false ([ k what ] @ indty_box); break; + keyword "with" ] + in + let mk_case_pattern (head, vars) = + hbox true false (ident head :: List.map aux_var vars) + in + let patterns' = + List.map + (fun (lhs, rhs) -> + remove_level_info + (hvbox false true [ + hbox false true [ + mk_case_pattern lhs; builtin_symbol "\\Rightarrow" ]; + break; k rhs ])) + patterns + in + let patterns'' = + let rec aux_patterns = function + | [] -> assert false + | [ last ] -> + [ break; + hbox false false [ + builtin_symbol "|"; + last; builtin_symbol "]" ] ] + | hd :: tl -> + [ break; hbox false false [ builtin_symbol "|"; hd ] ] + @ aux_patterns tl + in + match patterns' with + | [] -> + [ hbox false false [ builtin_symbol "["; builtin_symbol "]" ] ] + | [ one ] -> + [ hbox false false [ + builtin_symbol "["; one; builtin_symbol "]" ] ] + | hd :: tl -> + hbox false false [ builtin_symbol "["; hd ] + :: aux_patterns tl + in + add_level_info Ast.simple_prec Ast.simple_assoc + (hvbox false false [ + hvbox false false (outty_box @ [ match_box ]); break; + hbox false false [ hvbox false false patterns'' ] ]) + | Ast.Cast (bo, ty) -> + add_level_info Ast.simple_prec Ast.simple_assoc + (hvbox false true [ + builtin_symbol "("; k bo; break; builtin_symbol ":"; k ty; + builtin_symbol ")"]) + | Ast.LetIn (var, s, t) -> + add_level_info Ast.let_in_prec Ast.let_in_assoc + (hvbox false true [ + hvbox false true [ + keyword "let"; + hvbox false true [ + aux_var var; builtin_symbol "\\def"; break; k s ]; + break; keyword "in" ]; + k t ]) + | Ast.LetRec (rec_kind, funs, where) -> + let rec_op = + match rec_kind with `Inductive -> "rec" | `CoInductive -> "corec" + in + let mk_fun (var, body, _) = aux_var var, k body in + let mk_funs = List.map mk_fun in + let fst_fun, tl_funs = + match mk_funs funs with hd :: tl -> hd, tl | [] -> assert false + in + let fst_row = + let (name, body) = fst_fun in + hvbox false true [ + keyword "let"; keyword rec_op; name; builtin_symbol "\\def"; break; + body ] + in + let tl_rows = + List.map + (fun (name, body) -> + [ break; + hvbox false true [ + keyword "and"; name; builtin_symbol "\\def"; break; body ] ]) + tl_funs + in + add_level_info Ast.let_in_prec Ast.let_in_assoc + ((hvbox false false + (fst_row :: List.flatten tl_rows + @ [ break; keyword "in"; break; k where ]))) + | Ast.Implicit -> builtin_symbol "?" + | Ast.Meta (n, l) -> + let local_context l = + CicNotationUtil.dress (builtin_symbol ";") + (List.map (function None -> builtin_symbol "_" | Some t -> k t) l) + in + hbox false false + ([ builtin_symbol "?"; number (string_of_int n) ] + @ (if l <> [] then local_context l else [])) + | Ast.Sort sort -> aux_sort sort + | Ast.Num _ + | Ast.Symbol _ + | Ast.Ident (_, None) | Ast.Ident (_, Some []) + | Ast.Uri (_, None) | Ast.Uri (_, Some []) + | Ast.Literal _ + | Ast.UserInput as leaf -> leaf | t -> CicNotationUtil.visit_ast ~special_k k t + and aux_sort sort_kind = + add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) + (Ast.Ident (string_of_sort_kind sort_kind, None)) and aux_ty = function | None -> builtin_symbol "?" | Some ty -> k ty + and aux_var = function + | name, Some ty -> + hvbox false true [ + builtin_symbol "("; name; builtin_symbol ":"; break; k ty; + builtin_symbol ")" ] + | name, None -> name and special_k = function | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) - | _ -> assert false + | t -> + prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t); + assert false in aux t @@ -125,7 +260,9 @@ let ast_of_acic0 term_info acic k = let sort_of_id id = try Hashtbl.find term_info.sort id - with Not_found -> assert false + with Not_found -> + prerr_endline (sprintf "warning: sort of id %s not found, using Type" id); + `Type in let aux_substs substs = Some @@ -220,7 +357,8 @@ let ast_of_acic0 term_info acic k = | Cic.ACoFix (id, no, funs) -> let defs = List.map - (fun (_, n, ty, bo) -> ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) + (fun (_, n, ty, bo) -> + ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) funs in let name = @@ -276,9 +414,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.Literal (`Keyword k) as t -> [ (*reset_href*) (add_keyword_attrs t) ] + | Ast.Literal _ as t -> [ (*reset_href*) t ] | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ] | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ] and subst_magic env = function @@ -298,10 +435,11 @@ let instantiate21 env (* precedence associativity *) l1 = | [] -> List.rev acc | value_set :: [] -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list (CicNotationUtil.group (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.group ((subst env p) @ sep) :: acc) tl + instantiate_list + (CicNotationUtil.group ((subst env p) @ sep) :: acc) tl in instantiate_list [] values | Ast.Opt p -> @@ -348,18 +486,15 @@ let rec pp_ast1 term = match term with | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t) | _ -> - 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 - Ast.AttributedTerm (`Level (precedence, associativity), - (instantiate21 (ast_env_of_env env) l1)) - end + (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 @@ -379,8 +514,10 @@ let instantiate32 term_info env symbol args = in add_lambda t (n - count_lambda t) in - let args' = List.map instantiate_arg args in - Ast.Appl (Ast.Symbol (symbol, 0) :: args') + let head = Ast.Symbol (symbol, 0) in + match args with + | [] -> head + | _ -> Ast.Appl (head :: List.map instantiate_arg args) let rec ast_of_acic1 term_info annterm = match (get_compiled32 ()) annterm with @@ -395,9 +532,10 @@ let rec ast_of_acic1 term_info annterm = with Not_found -> assert false in let ast = instantiate32 term_info env' symbol args in - match uris with - | [] -> ast - | _ -> Ast.AttributedTerm (`Href uris, ast) + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), + (match uris with + | [] -> ast + | _ -> Ast.AttributedTerm (`Href uris, ast))) let load_patterns32 t = set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t)) @@ -410,7 +548,9 @@ let ast_of_acic id_to_sort annterm = let ast = ast_of_acic1 term_info annterm in ast, term_info.uri -let pp_ast term = pp_ast1 term +let pp_ast term = +(* prerr_endline ("pp_ast <- : " ^ CicNotationPp.pp_term term); *) + pp_ast1 term let fresh_id = let counter = ref ~-1 in @@ -433,9 +573,17 @@ let add_interpretation dsc (symbol, args) appl_pattern = exception Interpretation_not_found exception Pretty_printer_not_found +let rec list_uniq = function + | [] -> [] + | h::[] -> [h] + | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl + let lookup_interpretations symbol = try - List.map + list_uniq + (List.sort Pervasives.compare + (List.map (fun id -> let (dsc, _, args, appl_pattern, _) = try @@ -443,12 +591,10 @@ let lookup_interpretations symbol = with Not_found -> assert false in dsc, args, appl_pattern) - !(Hashtbl.find interpretations symbol) + !(Hashtbl.find interpretations symbol))) with Not_found -> raise Interpretation_not_found -let add_pretty_printer - ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1 -= +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);