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
-module Ast = CicNotationPt
-
type term_info =
{ sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
uri: (Cic.id, string) Hashtbl.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 = 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 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
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 =
| 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