X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=3d684fe39b0ff27f57fd3eb6cd23180d30042f20;hb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;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..3d684fe39 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -25,17 +25,20 @@ open Printf +module Ast = CicNotationPt + +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) else () + type pattern_id = int type interpretation_id = pattern_id type pretty_printer_id = pattern_id 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 @@ -61,33 +64,218 @@ 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 +let idref id t = Ast.AttributedTerm (`IdRef id, t) -let string_of_name = function - | Cic.Name s -> s - | Cic.Anonymous -> "_" +let resolve_binder = function + | `Lambda -> "\\lambda" + | `Pi -> "\\Pi" + | `Forall -> "\\forall" + | `Exists -> "\\exists" -let ident_of_name n = Ast.Ident (string_of_name n, None) +let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) -let idref id t = Ast.AttributedTerm (`IdRef id, 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 builtin_symbol s = Ast.Literal (`Symbol s) +let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) + +let 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)) + +let ident_w_href href i = + match href with + | None -> ident i + | Some href -> Ast.AttributedTerm (`Href [href], ident i) + +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 = - prerr_endline "pp_ast0"; - let rec aux t = CicNotationUtil.visit_ast ~special_k k t + 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))) + | Ast.Binder (binder_kind, (id, ty), 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, href) -> [ keyword "in"; ident_w_href href 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, href, vars) = + hbox true false (ident_w_href href 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" ]; + break; + 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, aux t) - | _ -> assert false + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) + | t -> + prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term 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 = 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 @@ -119,13 +307,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); @@ -133,9 +323,7 @@ let ast_of_acic0 term_info acic k = | Cic.AMutInd (id,uri,i,substs) as t -> let name = name_of_inductive_type uri i in let uri_str = UriManager.string_of_uri uri in - let puri_str = - uri_str ^ "#xpointer(1/" ^ (string_of_int (i + 1)) ^ ")" - in + let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in register_uri id puri_str; idref id (Ast.Ident (name, aux_substs substs)) | Cic.AMutConstruct (id,uri,i,j,substs) -> @@ -146,22 +334,33 @@ let ast_of_acic0 term_info acic k = idref id (Ast.Ident (name, aux_substs substs)) | Cic.AMutCase (id,uri,typeno,ty,te,patterns) -> let name = name_of_inductive_type uri typeno in + let uri_str = UriManager.string_of_uri uri in + let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in + let ctor_puri j = + UriManager.uri_of_string + (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) + in + let case_indty = name, Some (UriManager.uri_of_string puri_str) in let constructors = constructors_of_inductive_type uri typeno in let rec eat_branch ty pat = 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 j = ref 0 in let patterns = - List.map2 - (fun (name, ty) pat -> - let (capture_variables, rhs) = eat_branch ty pat in - ((name, 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 name, Some (k ty), patterns)) + idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns)) | Cic.AFix (id, no, funs) -> let defs = List.map @@ -180,7 +379,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 = @@ -198,13 +398,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 [] @@ -212,36 +409,40 @@ 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 = - 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.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 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 * 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 (`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 | Ast.List0 (p, sep_opt) | Ast.List1 (p, sep_opt) -> let rec_decls = CicNotationEnv.declarations_of_term p in @@ -251,17 +452,20 @@ 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.group (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 + let terms = subst env p in + instantiate_list (CicNotationUtil.group (terms @ 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 +479,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,21 +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 (get_compiled21 ()) term with +(* 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 precedence, associativity, l1 = + let prec, assoc, l1 = try Hashtbl.find level1_patterns21 pid with Not_found -> assert false in - instantiate21 (ast_env_of_env env) precedence associativity l1 + 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 @@ -330,8 +537,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 @@ -340,25 +549,36 @@ 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 + Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm), + (match uris with + | [] -> ast + | _ -> 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 = + debug_print (lazy ("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 (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); ast, term_info.uri -let pp_ast term = pp_ast1 term +let pp_ast ast = + debug_print (lazy "pp_ast <-"); + let ast' = pp_ast1 ast in + debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast')); + ast' let fresh_id = let counter = ref ~-1 in @@ -366,14 +586,43 @@ 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 - Hashtbl.add level2_patterns32 id (symbol, args); + let uris = CicNotationUtil.find_appl_pattern_uris appl_pattern in + 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 ?associativity l2 l1 = +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_uniq + (List.sort Pervasives.compare + (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); @@ -381,11 +630,11 @@ let add_pretty_printer ?precedence ?associativity l2 l1 = 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;