| 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 (`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))
+ add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
+ (Ast.Literal (`Number (s,(None,None))))
let ident i =
- add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+ add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
+ (Ast.Ident (i,`Ambiguous))
let ident_w_href href i =
match href with
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, None) in
+ 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
| Ast.Sort sort -> aux_sort sort
| Ast.Num _
| Ast.Symbol _
- | Ast.Ident (_, None) | Ast.Ident (_, Some [])
- | Ast.Uri (_, None) | Ast.Uri (_, Some [])
+ | Ast.Ident _
| Ast.Literal _
| Ast.UserInput as leaf -> leaf
| t -> NotationUtil.visit_ast ~special_k k t
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.OptValue (Some (pp_value v))
| NotationEnv.ListValue vl ->
NotationEnv.ListValue (List.map pp_value vl)
+ | 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))
in
aux [] env
-let instantiate_level2 status env 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.LetRec (kind, definitions, body) ->
Ast.LetRec (kind, List.map (aux_definition env) definitions,
aux env body)
- | Ast.Uri (name, None) -> Ast.Uri (name, None)
- | Ast.Uri (name, Some substs) ->
- Ast.Uri (name, Some (aux_substs env substs))
- | Ast.Ident (name, Some substs) ->
- Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
| Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _
- | Ast.Symbol _
| Ast.UserInput -> term
+ | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc)
| 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_opt env = function
| Some term -> Some (aux env term)
| None -> None
List.map (fun (name, term) -> (name, aux env term)) substs
and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
and aux_variable env = function
- | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
+ | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, None)
| Ast.IdentVar name ->
(match Env.lookup_string env name with
- Env.Ident x -> Ast.Ident (x, None)
+ Env.Ident x -> Ast.Ident (x, `Ambiguous)
| Env.Var x -> Ast.Variable (Ast.IdentVar x))
| Ast.TermVar (name,(Ast.Level l|Ast.Self l)) ->
Ast.AttributedTerm (`Level l,Env.lookup_term env name)
- | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
+ | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, `Ambiguous)
| Ast.Ascription (term, name) -> assert false
and aux_magic env = function
| Ast.Default (some_pattern, none_pattern) ->
projects / helm.git / blobdiff