X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=207b26a233d139773815234a62843838e115020d;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=79316319a7a7c42385d2f7dc4951f9ddde7d1e14;hpb=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 79316319a..207b26a23 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -29,6 +29,9 @@ type pattern_id = int type interpretation_id = pattern_id type pretty_printer_id = pattern_id +let default_prec = 50 +let default_assoc = Gramext.NonA + type term_info = { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t; uri: (Cic.id, string) Hashtbl.t; @@ -62,6 +65,7 @@ let constructor_of_inductive_type uri i j = with Not_found -> assert false) module Ast = CicNotationPt +module Parser = CicNotationParser let string_of_name = function | Cic.Name s -> s @@ -71,17 +75,49 @@ 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 + | `Lambda -> "\\lambda" + | `Pi -> "\\Pi" + | `Forall -> "\\forall" + | `Exists -> "\\exists" + let pp_ast0 t k = - prerr_endline "pp_ast0"; - let rec aux t = CicNotationUtil.visit_ast ~special_k k t + let reset_href t = Ast.AttributedTerm (`Href [], t) in + let builtin_symbol s = reset_href (Ast.Literal (`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.Binder (`Forall, (Ast.Ident ("_", _), ty), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.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.Binder (binder_kind, (id, ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.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 ]))]))) + | t -> CicNotationUtil.visit_ast ~special_k k t + and aux_ty = function + | None -> builtin_symbol "?" + | Some ty -> k ty and special_k = function - | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t) + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) | _ -> assert false in 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 = @@ -221,10 +257,11 @@ let get_compiled32 () = let set_compiled21 f = compiled21 := Some f let set_compiled32 f = compiled32 := Some f -let instantiate21 env precedence associativity l1 = - prerr_endline "instantiate21"; - let rec subst last_box env = function - | Ast.AttributedTerm (_, t) -> subst last_box env t +let instantiate21 env (* precedence associativity *) l1 = + let rec subst_singleton env t = + CicNotationUtil.boxify (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 let ty, value = @@ -236,12 +273,12 @@ let instantiate21 env precedence associativity l1 = (* following assertion should be a conditional that makes this * instantiation fail *) assert (CicNotationEnv.well_typed expected_ty value); - CicNotationEnv.term_of_value value - | Ast.Magic m -> subst_magic last_box env m - | Ast.Literal _ as t -> t - | Ast.Layout l -> Ast.Layout (subst_layout last_box env l) - | t -> CicNotationUtil.visit_ast (subst last_box env) t - and subst_magic last_box env = function + [ CicNotationEnv.term_of_value value ] + | Ast.Magic m -> subst_magic env m + | 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 | Ast.List0 (p, sep_opt) | Ast.List1 (p, sep_opt) -> let rec_decls = CicNotationEnv.declarations_of_term p in @@ -256,12 +293,16 @@ let instantiate21 env precedence associativity l1 = 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) [] | value_set :: tl -> let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list ([subst last_box env p] @ sep @ acc) tl + instantiate_list + ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl in - let children = instantiate_list [] values in - CicNotationPt.Layout (CicNotationPt.Box (last_box, children)) + instantiate_list [] values | Ast.Opt p -> let opt_decls = CicNotationEnv.declarations_of_term p in let env = @@ -275,23 +316,24 @@ let instantiate21 env precedence associativity l1 = in try build_env opt_decls with Exit -> [] in - let children = - if env = [] then [] - else [subst last_box env p] - in - CicNotationPt.Layout (CicNotationPt.Box (last_box, children)) + begin + match env with + | [] -> [] + | _ -> subst env p + end | _ -> assert false (* impossible *) - and subst_layout last_box env l = - CicNotationUtil.visit_layout (subst last_box env) l - (* TODO ZACK here we need to remember the last box traversed, but - * visit_layout is opaque :-((( *) + and subst_layout env = function + | Ast.Box (kind, tl) -> + Ast.Box (kind, List.concat (List.map (subst env) tl)) + | l -> CicNotationUtil.visit_layout (subst_singleton env) l in - subst CicNotationPt.H env l1 + subst_singleton env l1 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) -> @@ -302,15 +344,21 @@ 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 (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 - instantiate21 (ast_env_of_env env) precedence associativity l1 + 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 let instantiate32 term_info env symbol args = let rec instantiate_arg = function @@ -340,12 +388,15 @@ 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 = + let symbol, args, uris = try Hashtbl.find level2_patterns32 pid with Not_found -> assert false in - instantiate32 term_info env' symbol args + let ast = instantiate32 term_info env' symbol args in + match uris with + | [] -> ast + | _ -> Ast.AttributedTerm (`Href uris, ast) let load_patterns32 t = set_compiled32 (CicNotationMatcher.Matcher32.compiler t) @@ -368,12 +419,15 @@ let fresh_id = let add_interpretation (symbol, args) appl_pattern = let id = fresh_id () in - Hashtbl.add level2_patterns32 id (symbol, args); + let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in + Hashtbl.add level2_patterns32 id (symbol, args, uris); pattern32_matrix := (appl_pattern, id) :: !pattern32_matrix; load_patterns32 !pattern32_matrix; id -let add_pretty_printer ?precedence ?associativity l2 l1 = +let add_pretty_printer + ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1 += let id = fresh_id () in let l2' = CicNotationUtil.strip_attributes l2 in Hashtbl.add level1_patterns21 id (precedence, associativity, l1);