-requires="helm-library helm-ng_kernel"
+requires="helm-library helm-ng_kernel helm-syntax_extensions"
version="0.0.1"
archive(byte)="content.cma"
archive(native)="content.cmxa"
notationUtil.cmx: notationPt.cmx notationUtil.cmi
notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi
notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi
-notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi
+notationPp.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi \
+ notationPp.cmi
+notationPp.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmx \
+ notationPp.cmi
type binding = string * (value_type * value)
type t = binding list
+(* let rec pp_value = function
+ | TermValue t -> "T#" ^ NotationPp.pp_term (new NCicPp.status) t
+ | StringValue (Ident i) -> "I#" ^ i
+ | StringValue (Var v) -> "V#" ^ v
+ | NumValue n -> "N#" ^ n
+ | OptValue None -> "O#None"
+ | OptValue (Some v) -> "O#" ^ pp_value v
+ | ListValue vl -> "L#[" ^ (String.concat ";" (List.map pp_value vl)) ^ "]"
+ | DisambiguationValue _ -> "D#"
+
+let pp_binding = function
+ | s, (ty,v) -> Printf.sprintf "{ %s := %s : %s }" s (pp_value v) "..."
+
+let pp_env e = String.concat " " (List.map pp_binding e) *)
+
let lookup env name =
try
List.assoc name env
let pp_literal =
if debug_printing then
(function (* debugging version *)
- | `Symbol s -> sprintf "symbol(%s)" s
- | `Keyword s -> sprintf "keyword(%s)" s
- | `Number s -> sprintf "number(%s)" s)
- else
- (function
- | `Symbol s
- | `Keyword s
- | `Number s -> s)
+ | `Symbol _ as t ->
+ sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
+ | `Keyword _ as t ->
+ sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
+ | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+ else NotationUtil.string_of_literal
let pp_pos =
function
]
type literal =
- [ `Symbol of string
- | `Keyword of string
- | `Number of string
+ [ `Symbol of string * (string option * string option)
+ | `Keyword of string * (string option * string option)
+ | `Number of string * (string option * string option)
]
type case_indtype = string * href option
module Ast = NotationPt
-let visit_ast ?(special_k = fun _ -> assert false)
+let visit_ast ?(special_k = fun _ -> assert false)
+ ?(clear_interpretation= false)
?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x)
?(map_case_outtype=
fun k x -> match x with None -> None | Some x -> Some (k x))
| Ast.Literal _
| Ast.Magic _
| Ast.Variable _) as t -> special_k t
- | (Ast.Ident _
+ | Ast.Ident (id,_) when clear_interpretation -> Ast.Ident (id,`Ambiguous)
+ | Ast.Symbol (s,_) when clear_interpretation -> Ast.Symbol (s,None)
+ | Ast.Num (n,_) when clear_interpretation -> Ast.Num (n,None)
+ | ( Ast.Ident _
+ | Ast.Symbol _
+ | Ast.Num _
| Ast.NRef _
| Ast.NCic _
| Ast.Implicit _
- | Ast.Num _
| Ast.Sort _
- | Ast.Symbol _
| Ast.UserInput) as t -> t
and aux_opt = function
| None -> None
let rec aux = function
| Ast.AttributedTerm (_, t) -> aux t
| Ast.Layout l -> Ast.Layout (visit_layout aux l)
- | Ast.Literal (`Keyword k) as t ->
+ | Ast.Literal (`Keyword (k,_)) as t ->
add_keyword k;
t
| Ast.Literal _ as t -> t
let rec get_idrefs =
function
- | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t
- | Ast.AttributedTerm (_, t) -> get_idrefs t
+ | Ast.Symbol (_,Some (_,desc)) -> [desc]
| _ -> []
let meta_names_of_term term =
done;
List.rev !lists
+let href s = function
+ | None, None -> s
+ | Some u, None -> "<A href=\"" ^ u ^ "\">" ^ s ^ "</A>"
+ | None, Some desc ->
+ "<A href=\"cic:/fakeuri.con\" title=\"" ^ desc ^ "\">" ^ s ^ "</A>"
+ | Some u, Some desc ->
+ "<A href=\"" ^ u ^ "\" title=\"" ^ desc ^ "\">" ^ s ^ "</A>"
+
let string_of_literal = function
- | `Symbol s
- | `Keyword s
- | `Number s -> s
+ | `Symbol (s,x)
+ | `Keyword (s,x)
+ | `Number (s,x) -> href s x
+
+let html_of_literal = function
+ | `Symbol (s,x)
+ | `Keyword (s,x)
+ | `Number (s,x) ->
+ href (Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
+ (Utf8Macro.unicode_of_tex s)) x
let boxify = function
| [ a ] -> a
val visit_ast:
?special_k:(NotationPt.term -> NotationPt.term) ->
+ ?clear_interpretation:bool ->
?map_xref_option:(NotationPt.href option -> NotationPt.href option) ->
?map_case_indty:(NotationPt.case_indtype option ->
NotationPt.case_indtype option) ->
val ncombine: 'a list list -> 'a list list
val string_of_literal: NotationPt.literal -> string
+val html_of_literal: NotationPt.literal -> string
val dress: sep:'a -> 'a list -> 'a list
val dressn: sep:'a list -> 'a list -> 'a list
smallLexer.cmi:
cicNotationParser.cmi:
box.cmi:
+content2presMatcher.cmi:
termContentPres.cmi: cicNotationParser.cmi
boxPp.cmi: cicNotationPres.cmi
cicNotationPres.cmi: termContentPres.cmi box.cmi
-content2presMatcher.cmi:
cicNotationLexer.cmo: cicNotationLexer.cmi
cicNotationLexer.cmx: cicNotationLexer.cmi
smallLexer.cmo: smallLexer.cmi
cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
box.cmo: box.cmi
box.cmx: box.cmi
+content2presMatcher.cmo: content2presMatcher.cmi
+content2presMatcher.cmx: content2presMatcher.cmi
termContentPres.cmo: content2presMatcher.cmi cicNotationParser.cmi \
termContentPres.cmi
termContentPres.cmx: content2presMatcher.cmx cicNotationParser.cmx \
boxPp.cmx: box.cmx boxPp.cmi
cicNotationPres.cmo: termContentPres.cmi box.cmi cicNotationPres.cmi
cicNotationPres.cmx: termContentPres.cmx box.cmx cicNotationPres.cmi
-content2presMatcher.cmo: content2presMatcher.cmi
-content2presMatcher.cmx: content2presMatcher.cmi
let render_to_strings ~map_unicode_to_tex choose_action size markup =
prerr_endline ("render size is " ^ string_of_int size);
+ let add_markup attr txt =
+ let txt = Netencoding.Html.encode ~in_enc:`Enc_utf8 () txt in
+ let value_of_attr (_,_,v) = v in
+ let title =
+ try Some (value_of_attr (List.find (fun (_,t,_) -> t = "title") attr))
+ with _ -> None in
+ let href =
+ try Some (value_of_attr (List.find (fun (_,t,_) -> t = "href") attr))
+ with _ -> None in
+ match title,href with
+ | None,None -> txt
+ | None,Some u -> "<A href=\"" ^ u ^ "\">" ^ txt ^ "</A>"
+ | Some t, Some u ->
+ "<A href=\"" ^ u ^ "\" title=\"" ^ t ^ "\">" ^ txt ^ "</A>"
+ | Some t, None ->
+ let u = "cic:/fakeuri.con" in
+ "<A href=\"" ^ u ^ "\" title=\"" ^ t ^ "\">" ^ txt ^ "</A>"
+ in
+
let max_size = max_int in
let rec aux_box =
function
- | Box.Text (_, t) -> fixed_rendering t
+ | Box.Text (attr, t) ->
+ fun x ->
+ (match fixed_rendering t x with
+ | len, [txt] -> len, [add_markup attr txt]
+ | _ -> assert false)
| Box.Space _ -> fixed_rendering string_space
| Box.Ink _ -> fixed_rendering string_ink
| Box.Action (_, []) -> assert false
let gram_of_literal status =
function
- | `Symbol s -> gram_symbol status s
- | `Keyword s -> gram_keyword s
- | `Number s -> gram_number s
+ | `Symbol (s,_) -> gram_symbol status s
+ | `Keyword (s,_) -> gram_keyword s
+ | `Number (s,_) -> gram_number s
let make_action status action bindings =
let rec aux (vl : NotationEnv.t) =
assert false
and aux_literal status =
function
- | `Symbol s -> add_symbol_to_grammar status s
- | `Keyword s -> status
- | `Number s -> status
+ | `Symbol (s,_) -> add_symbol_to_grammar status s
+ | `Keyword _ -> status
+ | `Number _ -> status
and aux_layout status = function
| Ast.Sub (p1, p2) -> aux (aux status p1) p2
| Ast.Sup (p1, p2) -> aux (aux status p1) p2
assert false
and aux_literal =
function
- | `Symbol s -> [NoBinding, gram_symbol status s]
- | `Keyword s ->
+ | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
+ | `Keyword (s,_) ->
(* assumption: s will be registered as a keyword with the lexer *)
[NoBinding, gram_keyword s]
- | `Number s -> [NoBinding, gram_number s]
+ | `Number (s,_) -> [NoBinding, gram_number s]
and aux_layout = function
| Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
| Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
fun l -> List.map (fun x -> x l) p ]
];
literal: [
- [ s = SYMBOL -> `Symbol s
- | k = QKEYWORD -> `Keyword k
- | n = NUMBER -> `Number n
+ [ s = SYMBOL -> `Symbol (s, (None,None))
+ | k = QKEYWORD -> `Keyword (k, (None,None))
+ | n = NUMBER -> `Number (n,(None,None))
]
];
sep: [ [ "sep"; sep = literal -> sep ] ];
| A.AttributedTerm _ ->
aux_attributes [] "" prec t
| A.Num (literal, _) -> Box.Text ([], literal)
- | A.Symbol (literal, Some (None,desc)) ->
- let txt = "<A title=\"" ^ desc ^ "\">" ^ literal ^ "</A>" in
- Box.Text ([], to_unicode txt)
+ | A.Symbol (literal, Some (None,desc)) ->
+ let literal = to_unicode literal in
+ let attr = [ None, "title", desc ] in
+ Box.Text (attr, literal)
| A.Symbol (literal, Some (Some u,desc)) ->
- let txt =
- "<A href=\"" ^ u ^ "\" title=\"" ^ desc ^ "\">" ^ literal ^ "</A>" in
- Box.Text ([], to_unicode txt)
+ let literal = to_unicode literal in
+ let attr = [ None, "title", desc; None, "href", u ] in
+ Box.Text (attr, literal)
| A.Symbol (literal, _) -> Box.Text ([], to_unicode literal)
| A.Ident (literal, `Uri u) ->
- let txt = "<A href=\"" ^ u ^ "\">" ^ literal ^ "</A>" in
- Box.Text ([], to_unicode txt)
+ let attr = [ None, "href", u ] in
+ let literal = to_unicode literal in
+ Box.Text (attr,literal)
| A.Ident (literal, _) -> Box.Text ([], to_unicode literal)
| A.Meta(n, l) ->
let local_context =
Box.H ([],
(Box.Text ([], "?"^string_of_int n)::
(if (l <> []) then [Box.H ([],local_context)] else [])))
- | A.Literal l -> aux_literal prec l
+ | A.Literal (`Symbol (s,x))
+ | A.Literal (`Keyword (s,x))
+ | A.Literal (`Number (s,x)) ->
+ let attr =
+ match x with
+ | None, None -> []
+ | Some u, None -> [ None, "href", u ]
+ | None, Some d -> [ None, "title", d ]
+ | Some u, Some d -> [ None, "href", u; None, "title", d ]
+ in
+ Box.Text (attr, to_unicode s)
| A.UserInput -> Box.Text ([], "%")
| A.Layout l -> aux_layout prec l
| A.Magic _
(* prerr_endline (NotationPp.pp_term t); *)
aux_attribute t
- and aux_literal prec l =
- (match l with
- | `Symbol s -> Box.Text ([], to_unicode s)
- | `Keyword s -> Box.Text ([], to_unicode s)
- | `Number s -> Box.Text ([], to_unicode s))
-
and aux_layout prec l =
let attrs = [] in
let invoke' t = aux prec t in
in
let rec aux t =
NotationUtil.visit_ast
+ ~clear_interpretation:true
~map_xref_option:(fun _ -> None)
~map_case_indty:(fun _ -> None)
~map_case_outtype:(fun _ _ -> None)
let hvbox = box Ast.HV
let hovbox = box Ast.HOV
let break = Ast.Layout Ast.Break
-let space = Ast.Literal (`Symbol " ")
-let builtin_symbol s = Ast.Literal (`Symbol s)
-let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
+let space = Ast.Literal (`Symbol (" ", (None,None)))
+let builtin_symbol s = Ast.Literal (`Symbol (s,(None,None)))
+let keyword k = add_keyword_attrs (Ast.Literal (`Keyword (k,(None,None))))
let number s =
add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
- (Ast.Literal (`Number s))
+ (Ast.Literal (`Number (s,(None,None))))
let ident i =
add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
status#set_content_pres_db
{ status#content_pres_db with compiled21 = Some f }
-let add_idrefs =
- List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
+(* let add_idrefs =
+ List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) *)
let instantiate21 idrefs env l1 =
let rec subst_singleton pos env =
[ value ]
| Ast.Magic m -> subst_magic pos env m
| Ast.Literal l as t ->
- let t = add_idrefs idrefs t in
- (match l with
- | `Keyword k -> [ add_keyword_attrs t ]
- | _ -> [ t ])
+ (match idrefs with
+ | [] -> [t]
+ | desc::_ ->
+ let desc = Some desc in
+ (match l with
+ | `Keyword (k,_) -> [ Ast.Literal (`Keyword (k,(None,desc))) ]
+ | `Symbol (s,_) -> [ Ast.Literal (`Symbol (s,(None,desc))) ]
+ | `Number (n,_) -> [ Ast.Literal (`Number (n,(None,desc))) ]))
| Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
| t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
and subst_magic pos env = function
| NotationEnv.DisambiguationValue _ as v -> v
in
let ast_env_of_env env =
+ prerr_endline ("### pp_env: " ^ NotationPp.pp_env status env);
List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
in
- prerr_endline ("### pattern matching from 2 to 1 on term " ^ NotationPp.pp_term status term);
+(* prerr_endline ("### pattern matching from 2 to 1 on term " ^
+ * NotationPp.pp_term status term); *)
let res =
match term with
| Ast.AttributedTerm (attrs, term') ->
Ast.AttributedTerm (attrs, pp_ast1 status term')
| _ ->
(match get_compiled21 status term with
- | None -> pp_ast0 status term (pp_ast1 status)
+ | None -> (* prerr_endline "### ramo 1"; *)
+ pp_ast0 status term (pp_ast1 status)
| Some (env, ctors, pid) ->
+ (* prerr_endline "### ramo 2";
+ prerr_endline ("### constructors:\n" ^
+ (String.concat "\n\n" (List.map (NotationPp.pp_term status) ctors)) ^
+ "\n\n### constructors end") *)
let idrefs =
List.flatten (List.map NotationUtil.get_idrefs ctors)
in
in
instantiate21 idrefs (ast_env_of_env env) l1)
in
- prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term status res);
+ (* prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term
+ * status res);*)
res
let load_patterns21 status t =
let _,_,metasenv,subst,_ = !status#obj in
let txt = List.fold_left
(fun acc (nmeta,_ as meta) ->
- let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
- (snd (ApplyTransformation.ntxt_of_cic_sequent
- ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
+ let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
+ ~metasenv ~subst ~map_unicode_to_tex:false 80 !status
+ meta) in
+ prerr_endline ("### txt0 = " ^ txt0);
("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
[] metasenv
in
let _,_,metasenv,subst,_ = !status#obj in
let txt = List.fold_left
(fun acc (nmeta,_ as meta) ->
- let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
- (snd (ApplyTransformation.ntxt_of_cic_sequent
- ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
+ let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
+ ~metasenv ~subst ~map_unicode_to_tex:false 80 !status
+ meta) in
+ prerr_endline ("### txt0 = " ^ txt0);
("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
[] metasenv
in
projects / helm.git / commitdiff