Commit 86566a6f authored by Andrei Paskevich's avatar Andrei Paskevich

propagate userloc in logic expressions

parent 7c97e32d
......@@ -444,15 +444,18 @@ let apply_highord loc x tl = match List.rev tl with
| a::tl -> [{pp_loc = loc; pp_desc = PPapp (x, List.rev tl)}; a]
| [] -> assert false
let rec dterm ?(localize=false) uc env { pp_loc = loc; pp_desc = t } =
let rec dterm ?(localize=None) uc env { pp_loc = loc; pp_desc = t } =
let n, ty = dterm_node ~localize loc uc env t in
let t = { dt_node = n; dt_ty = ty } in
let rec down e = match e.dt_node with
| Tnamed (Lstr _, e) -> down e
let rec down loc e = match e.dt_node with
| Tnamed (Lstr _, e) -> down loc e
| Tnamed (Lpos _, _) -> t
| _ -> { dt_node = Tnamed (Lpos loc, t); dt_ty = ty }
in
if localize then down t else t
match localize with
| Some (Some loc) -> down loc t
| Some None -> down loc t
| None -> t
and dterm_node ~localize loc uc env = function
| PPvar (Qident {id=x}) when Mstr.mem x env.dvars ->
......@@ -510,7 +513,7 @@ and dterm_node ~localize loc uc env = function
Tmatch (t1, bl), tb
| PPnamed (x, e1) ->
let localize = match x with
| Lpos _ -> false
| Lpos l -> Some (Some l)
| Lstr _ -> localize
in
let e1 = dterm ~localize uc env e1 in
......@@ -646,14 +649,17 @@ and dterm_node ~localize loc uc env = function
| PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
error ~loc TermExpected
and dfmla ?(localize=false) uc env { pp_loc = loc; pp_desc = f } =
and dfmla ?(localize=None) uc env { pp_loc = loc; pp_desc = f } =
let f = dfmla_node ~localize loc uc env f in
let rec down e = match e with
| Fnamed (Lstr _, e) -> down e
let rec down loc e = match e with
| Fnamed (Lstr _, e) -> down loc e
| Fnamed (Lpos _, _) -> f
| _ -> Fnamed (Lpos loc, f)
in
if localize then down f else f
match localize with
| Some (Some loc) -> down loc f
| Some None -> down loc f
| None -> f
and dfmla_node ~localize loc uc env = function
| PPtrue ->
......@@ -727,7 +733,7 @@ and dfmla_node ~localize loc uc env = function
Fmatch (t1, List.map branch bl)
| PPnamed (x, f1) ->
let localize = match x with
| Lpos _ -> false
| Lpos l -> Some (Some l)
| Lstr _ -> localize
in
let f1 = dfmla ~localize uc env f1 in
......
......@@ -67,8 +67,10 @@ val type_term : theory_uc -> denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val type_fmla : theory_uc -> denv -> vsymbol Mstr.t -> Ptree.lexpr -> term
val dty : theory_uc -> denv -> Ptree.pty -> Denv.dty
val dterm : ?localize:bool -> theory_uc -> denv -> Ptree.lexpr -> Denv.dterm
val dfmla : ?localize:bool -> theory_uc -> denv -> Ptree.lexpr -> Denv.dfmla
val dterm : ?localize:(Ptree.loc option option) ->
theory_uc -> denv -> Ptree.lexpr -> Denv.dterm
val dfmla : ?localize:(Ptree.loc option option) ->
theory_uc -> denv -> Ptree.lexpr -> Denv.dfmla
val dpat : theory_uc -> denv -> Ptree.pattern -> denv * Denv.dpattern
val dpat_list :
theory_uc -> denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
......
......@@ -758,8 +758,8 @@ let check_at_fmla ?(old=false) loc f0 =
if not (check f0) then
errorm ~loc "locally bound variable %a under `at'" print_vs (of_option !v)
let dterm env l = Typing.dterm ~localize:true env l
let dfmla env l = Typing.dfmla ~localize:true env l
let dterm env l = Typing.dterm ~localize:(Some None) env l
let dfmla env l = Typing.dfmla ~localize:(Some None) env l
type ienv = {
i_uc : uc;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment