| 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 ->
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
| None ->
let fst_constructor =
match branches with
- | ((head, _), _) :: _ -> head
+ | ((head, _, _), _) :: _ -> head
| [] -> raise Invalid_choice
in
(match resolve env (Id fst_constructor) () with
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) ->
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
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 =
]
];
match_pattern: [
- [ id = IDENT -> id, []
+ [ id = IDENT -> id, None, []
| LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
- id, vars
+ id, None, vars
]
];
binder: [
| 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<Rightarrow>> (* ⇒ *);
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 ->
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)
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)
| 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
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 *)
| `Number of string
]
+type case_indtype = string * href option
+
type term =
(* CIC AST *)
| 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, <pattern,action> list *)
| Cast of term * term
| LetIn of capture_variable * term * term (* name, body, where *)
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 *)
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
| 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 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)
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 [
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
| 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) ->
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
(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
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
(** 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 *)
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
| 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
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 ;
projects / helm.git / commitdiff