From: Stefano Zacchiroli Date: Wed, 14 Sep 2005 08:45:30 +0000 (+0000) Subject: added hyperlinks on case pattern heads and outtype X-Git-Tag: V_0_1_2_1~4 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98d5d40127827a5c40e58cb0c9654066f940b0ea;p=helm.git added hyperlinks on case pattern heads and outtype --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 58927e53b..5096789d9 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -134,7 +134,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | CicNotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux loc context term in let cic_outtype = aux_option loc context None outtype in - let do_branch ((head, args), term) = + let do_branch ((head, _, args), term) = let rec do_branch' context = function | [] -> aux loc context term | (name, typ) :: tl -> @@ -151,7 +151,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = in let (indtype_uri, indtype_no) = match indty_ident with - | Some indty_ident -> + | Some (indty_ident, _) -> (match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> (uri, tyno) | Cic.Implicit _ -> raise Try_again @@ -159,7 +159,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast = | None -> let fst_constructor = match branches with - | ((head, _), _) :: _ -> head + | ((head, _, _), _) :: _ -> head | [] -> raise Invalid_choice in (match resolve env (Id fst_constructor) () with @@ -485,9 +485,9 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function let outtype_dom = domain_rev_of_term_option loc context outtype in let get_first_constructor = function | [] -> [] - | ((head, _), _) :: _ -> [ Id head ] + | ((head, _, _), _) :: _ -> [ Id head ] in - let do_branch ((head, args), term) = + let do_branch ((head, _, args), term) = let (term_context, args_domain) = List.fold_left (fun (cont, dom) (name, typ) -> @@ -505,7 +505,7 @@ let rec domain_rev_of_term ?(loc = dummy_floc) context = function branches_dom @ outtype_dom @ term_dom @ (match indty_ident with | None -> get_first_constructor branches - | Some ident -> [ Id ident ]) + | Some (ident, _) -> [ Id ident ]) | CicNotationPt.Cast (term, ty) -> let term_dom = domain_rev_of_term ~loc context term in let ty_dom = domain_rev_of_term ~loc context ty in diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index 2e5121b92..3ef1ff7e0 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -114,8 +114,8 @@ let instantiate_level2 env term = and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt) and aux_branch env (pattern, term) = (aux_pattern env pattern, aux env term) - and aux_pattern env (head, vars) = - (head, List.map (aux_capture_var env) vars) + and aux_pattern env (head, hrefs, vars) = + (head, hrefs, List.map (aux_capture_var env) vars) and aux_definition env (var, term, i) = (aux_capture_var env var, aux env term, i) and aux_substs env substs = diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 90324541d..933397067 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -445,9 +445,9 @@ EXTEND ] ]; match_pattern: [ - [ id = IDENT -> id, [] + [ id = IDENT -> id, None, [] | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN -> - id, vars + id, None, vars ] ]; binder: [ @@ -578,7 +578,7 @@ EXTEND | s = sort -> return_term loc (Ast.Sort s) | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ]; "match"; t = term; - indty_ident = OPT [ "in"; id = IDENT -> id ]; + indty_ident = OPT [ "in"; id = IDENT -> id, None ]; "with"; SYMBOL "["; patterns = LIST0 [ lhs = match_pattern; SYMBOL <:unicode> (* ⇒ *); diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index d51d1a65e..e784a8302 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -53,8 +53,10 @@ let pp_literal = function (* debugging version *) let rec pp_term ?(pp_parens = true) t = let t_pp = match t with - | Ast.AttributedTerm (`Href _, term) when debug_printing -> - sprintf "#[%s]" (pp_term ~pp_parens:false term) + | Ast.AttributedTerm (`Href hrefs, term) when debug_printing -> + sprintf "#(%s)[%s]" + (String.concat "," (List.map UriManager.string_of_uri hrefs)) + (pp_term ~pp_parens:false term) | Ast.AttributedTerm (`IdRef id, term) when debug_printing -> sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term) | Ast.AttributedTerm (_, term) when debug_printing -> @@ -73,9 +75,18 @@ let rec pp_term ?(pp_parens = true) t = sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable var) (pp_term body) | Ast.Case (term, indtype, typ, patterns) -> - sprintf "%smatch %s with %s" + sprintf "%smatch %s%s with %s" (match typ with None -> "" | Some t -> sprintf "[%s]" (pp_term t)) - (pp_term term) (pp_patterns patterns) + (pp_term term) + (match indtype with + | None -> "" + | Some (ty, href_opt) -> + sprintf " in %s%s" ty + (match debug_printing, href_opt with + | true, Some uri -> + sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "")) + (pp_patterns patterns) | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term t1) (pp_term t2) | Ast.LetIn (var, t1, t2) -> sprintf "let %s = %s in %s" (pp_capture_variable var) (pp_term t1) @@ -120,12 +131,18 @@ let rec pp_term ?(pp_parens = true) t = and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) and pp_substs substs = String.concat "; " (List.map pp_subst substs) -and pp_pattern ((head, vars), term) = +and pp_pattern ((head, href, vars), term) = + let head_pp = + head ^ + (match debug_printing, href with + | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "") + in sprintf "%s \\Rightarrow %s" (match vars with - | [] -> head + | [] -> head_pp | _ -> - sprintf "(%s %s)" head + sprintf "(%s %s)" head_pp (String.concat " " (List.map pp_capture_variable vars))) (pp_term term) diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index 60ee0dfb3..633d702a9 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -245,7 +245,7 @@ let render ids_to_uris = | A.Uri (literal, subst) -> let attrs = (RenderingAttrs.ident_attributes `MathML) - @ make_href xmlattrs xref (ref []) + @ make_href xmlattrs xref uris in let name = Mpres.Mi (attrs, to_unicode literal) in (match subst with diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 68ad7d83d..ca00d3539 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -39,10 +39,12 @@ let fail floc msg = let (x, y) = loc_of_floc floc in failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) +type href = UriManager.uri + type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) - | `Href of UriManager.uri list (* hyperlinks for literals *) + | `Href of href list (* hyperlinks for literals *) | `Level of int * Gramext.g_assoc (* precedence, associativity *) | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) @@ -55,6 +57,8 @@ type literal = | `Number of string ] +type case_indtype = string * href option + type term = (* CIC AST *) @@ -62,7 +66,8 @@ type term = | Appl of term list | Binder of binder_kind * capture_variable * term (* kind, name, body *) - | Case of term * string option * term option * (case_pattern * term) list + | Case of term * case_indtype option * term option * + (case_pattern * term) list (* what to match, inductive type, out type, list *) | Cast of term * term | LetIn of capture_variable * term * term (* name, body, where *) @@ -95,7 +100,7 @@ and capture_variable = term * term option and meta_subst = term option and subst = string * term -and case_pattern = string * capture_variable list +and case_pattern = string * href option * capture_variable list and box_kind = H | V | HV | HOV and box_spec = box_kind * bool * bool (* kind, spacing, indent *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 159d3451e..73f66771f 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -27,6 +27,9 @@ open Printf module Ast = CicNotationPt +let debug = false +let debug_print = if debug then prerr_endline else ignore + type pattern_id = int type interpretation_id = pattern_id type pretty_printer_id = pattern_id @@ -78,10 +81,13 @@ let rec remove_level_info = | 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 @@ -91,12 +97,20 @@ let break = Ast.Layout Ast.Break 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 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) @@ -129,7 +143,7 @@ let pp_ast0 t k = let indty_box = match indty_opt with | None -> [] - | Some indty -> [ keyword "in"; ident indty ] + | Some (indty, href) -> [ keyword "in"; ident_w_href href indty ] in let match_box = hvbox false true [ @@ -137,8 +151,8 @@ let pp_ast0 t k = 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) + 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 @@ -311,9 +325,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) -> @@ -324,6 +336,13 @@ 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 @@ -332,14 +351,16 @@ let ast_of_acic0 term_info acic k = (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 -> + incr j; let (capture_variables, rhs) = eat_branch ty pat in - ((name, capture_variables), rhs)) + ((name, Some (ctor_puri !j), capture_variables), rhs)) constructors patterns 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 @@ -547,11 +568,13 @@ let load_patterns21 t = let ast_of_acic id_to_sort 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 term = -(* prerr_endline ("pp_ast <- : " ^ CicNotationPp.pp_term term); *) - pp_ast1 term +let pp_ast ast = + let ast' = pp_ast1 ast in + debug_print ("pp_ast -> " ^ CicNotationPp.pp_term ast'); + ast' let fresh_id = let counter = ref ~-1 in diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli index 22b4f64e8..651606138 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.mli +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -33,15 +33,15 @@ val ast_of_acic: (** level 2 -> level 1 *) val pp_ast: CicNotationPt.term -> CicNotationPt.term -(** level 1 -> level 0: see CicNotationPres.render *) + (** for level 1 -> level 0: see CicNotationPres.render *) type interpretation_id type pretty_printer_id val add_interpretation: - string -> (* id / description *) + string -> (* id / description *) string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *) - CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) interpretation_id (** @raise Interpretation_not_found *) @@ -53,8 +53,8 @@ val lookup_interpretations: val add_pretty_printer: precedence:int -> associativity:Gramext.g_assoc -> - CicNotationPt.term -> (* level 2 pattern *) - CicNotationPt.term -> (* level 1 pattern *) + CicNotationPt.term -> (* level 2 pattern *) + CicNotationPt.term -> (* level 1 pattern *) pretty_printer_id exception Interpretation_not_found diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index 29edf6e7c..426846877 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -63,8 +63,8 @@ let visit_ast ?(special_k = fun _ -> assert false) k = | Some term -> Some (k term) and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt and aux_patterns patterns = List.map aux_pattern patterns - and aux_pattern ((head, vars), term) = - ((head, List.map aux_capture_variable vars), k term) + and aux_pattern ((head, hrefs, vars), term) = + ((head, hrefs, List.map aux_capture_variable vars), k term) and aux_subst (name, term) = (name, k term) and aux_substs substs = List.map aux_subst substs in @@ -203,7 +203,7 @@ let meta_names_of_term term = and aux_branch (pattern, term) = aux_pattern pattern ; aux term - and aux_pattern (head, vars) = + and aux_pattern (head, _, vars) = List.iter aux_capture_var vars and aux_definition (var, term, i) = aux_capture_var var ;