| Ast.AttributedTerm (a, t) -> Ast.AttributedTerm (a, remove_level_info t)
| t -> t
-let add_xml_attrs attrs t =
- if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t)
+let add_xml_attrs attrs t = t
+(* if attrs = [] then t else Ast.AttributedTerm (`XmlAttrs attrs, t) *)
-let add_keyword_attrs =
- add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
+let add_keyword_attrs t = t
+(* add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) *)
let box kind spacing indent content =
Ast.Layout (Ast.Box ((kind, spacing, indent), content))
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 (None,`Symbol (" ", (None,None)))
+let builtin_symbol s = Ast.Literal (None,`Symbol (s,(None,None)))
+let keyword k = add_keyword_attrs (Ast.Literal (None,`Keyword (k,(None,None))))
let number s =
- add_xml_attrs (RenderingAttrs.number_attributes `MathML)
- (Ast.Literal (`Number s))
+ add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
+ (Ast.Literal (None,`Number (s,(None,None))))
let ident i =
- add_xml_attrs (RenderingAttrs.ident_attributes `MathML)
+ add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
(Ast.Ident (i,`Ambiguous))
let ident_w_href href i =
add_xml_attrs [Some "xlink", "href", href] (ident i)
let binder_symbol s =
- add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
+ add_xml_attrs (* (RenderingAttrs.builtin_symbol_attributes `MathML) *) ()
(builtin_symbol s)
let xml_of_sort x =
let to_string x = Ast.Ident (x, `Ambiguous) in
let identify x =
- add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
+ add_xml_attrs (* (RenderingAttrs.keyword_attributes `MathML) *) () (to_string x)
in
let lvl t = Ast.AttributedTerm (`Level 90,t) in
match x with
method content_pres_db: db
end
-class virtual status =
+class virtual status uid =
object
- inherit NCic.status
+ inherit NCic.status uid
val content_pres_db = initial_db
method content_pres_db = content_pres_db
method set_content_pres_db v = {< content_pres_db = v >}
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 =
in
[ 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 ])
+ | Ast.Literal (csym,l) as t ->
+ let enrich_literal l (_,uri,desc) =
+ let desc = Some desc in
+ match l with
+ | `Keyword (k,_) -> [ Ast.Literal (csym,`Keyword (k,(uri,desc))) ]
+ | `Symbol (s,_) -> [ Ast.Literal (csym,`Symbol (s,(uri,desc))) ]
+ | `Number (n,_) -> [ Ast.Literal (csym,`Number (n,(uri,desc))) ]
+ in
+ (match csym,idrefs with
+ | None, [] -> [t]
+ | None,disamb::_ -> enrich_literal l disamb
+ | Some cs,_ ->
+ (try
+ let disamb = List.find (fun (cs',_,_) -> cs = cs') idrefs in
+ enrich_literal l disamb
+ with Not_found ->
+ (* prerr_endline ("can't find idref for " ^ cs ^ ". Will now print idrefs");
+ List.iter
+ (fun (cs'',_,_) -> prerr_endline ("idref " ^ cs''))
+ idrefs;*)
+ [t]))
| 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
let sep =
match sep_opt with
| None -> []
- | Some l -> [ Ast.Literal l; break; space ]
+ | Some l -> [ Ast.Literal (None,l); break; space ]
in
let rec instantiate_list acc = function
| [] -> List.rev acc
| 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 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
with Not_found -> assert false
in
instantiate21 idrefs (ast_env_of_env env) l1)
+ in
+ (* prerr_endline ("### pattern matching finished: " ^ NotationPp.pp_term
+ * status res);*)
+ res
let load_patterns21 status t =
set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t))
let head_names names env =
let rec aux acc = function
- | (name, (ty, v)) :: tl when List.mem name names ->
+ | (name, (ty, v)) as x :: tl when List.mem name names ->
(match ty, v with
| Env.ListType ty, Env.ListValue (v :: _) ->
- aux ((name, (ty, v)) :: acc) tl
+ aux ((name, (ty,v)):: acc) tl
| Env.TermType _, Env.TermValue _ ->
- aux ((name, (ty, v)) :: acc) tl
+ aux (x :: acc) tl
| Env.OptType _, Env.OptValue _ ->
- aux ((name, (ty, v)) :: acc) tl
+ aux (x :: acc) tl
| _ -> assert false)
+ | (_,(_,Env.DisambiguationValue _)) as x :: tl ->
+ aux (x::acc) tl
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
| [] -> acc
in
aux [] env
-let instantiate_level2 status env (loc,uri,desc) term =
+let instantiate_level2 status env (* (loc,uri,desc) *) term =
(* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
| Ast.Num _
| Ast.Sort _
| Ast.UserInput -> term
- | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc)
+ | Ast.Symbol (s,_) -> aux_symbol s (List.map (fun (_,(_,x)) -> x) env)
| Ast.Magic magic -> aux_magic env magic
| Ast.Variable var -> aux_variable env var
| Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
| _ -> assert false
- and aux_symbol s loc = function
- | _, None -> Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
- | uri, Some desc ->
- Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
+ and aux_symbol s env =
+ (* XXX: it's totally unclear why the env we receive here is in reverse
+ * order (a diff with the previous revision shows no obvious reason).
+ * This one-line patch is needed so that the default symbol chosen for
+ * storing the interpretation is the leftmost, rather than the rightmost *)
+ let env = List.rev env in
+ try
+ (let dv =
+ try List.find (function
+ | Env.DisambiguationValue(Some s',_,_,_) when s = s' -> true
+ | _ -> false) env
+ with Not_found ->
+ List.find (function
+ | Env.DisambiguationValue(None,_,_,_) -> true
+ | _ -> false) env
+ in
+ match dv with
+ | Env.DisambiguationValue(_,loc,uri,Some desc) ->
+ Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
+ | Env.DisambiguationValue(_,loc,_,_) ->
+ (* The important disambiguation info for symbols is the desc,
+ * if we don't have it, we won't use the uri either *)
+ Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
+ | _ -> assert false) (* vacuous *)
+ with Not_found ->
+ (* Ast.AttributedTerm (`Loc Stdpp.dummy_loc, Ast.Symbol (s, None))*)
+ Ast.Symbol (s, None)
and aux_opt env = function
| Some term -> Some (aux env term)
| None -> None
projects / helm.git / blobdiff