Commit 16dc0902 authored by Andrei Paskevich's avatar Andrei Paskevich

actually put labels in idents

parent c77c69c8
......@@ -133,13 +133,13 @@ let rec pattern_env env p = match p.dp_node with
| Pwild -> env
| Papp (_, pl) -> List.fold_left pattern_env env pl
| Por (p, _) -> pattern_env env p
| Pvar { id = x ; id_loc = loc } ->
| Pvar { id = x ; id_lab = labels ; id_loc = loc } ->
let ty = ty_of_dty p.dp_ty in
let vs = create_vsymbol (id_user x loc) ty in
let vs = create_vsymbol (id_user ~labels x loc) ty in
Mstr.add x vs env
| Pas (p, { id = x ; id_loc = loc }) ->
| Pas (p, { id = x ; id_lab = labels ; id_loc = loc }) ->
let ty = ty_of_dty p.dp_ty in
let vs = create_vsymbol (id_user x loc) ty in
let vs = create_vsymbol (id_user ~labels x loc) ty in
pattern_env (Mstr.add x vs env) p
let get_pat_var env p x = try Mstr.find x env with Not_found ->
......@@ -194,10 +194,10 @@ let rec term env t = match t.dt_node with
t_app s (List.map (term env) tl) (ty_of_dty t.dt_ty)
| Tif (f, t1, t2) ->
t_if (fmla env f) (term env t1) (term env t2)
| Tlet (e1, { id = x ; id_loc = loc }, e2) ->
| Tlet (e1, { id = x ; id_lab = labels ; id_loc = loc }, e2) ->
let ty = ty_of_dty e1.dt_ty in
let e1 = term env e1 in
let v = create_vsymbol (id_user x loc) ty in
let v = create_vsymbol (id_user ~labels x loc) ty in
let env = Mstr.add x v env in
let e2 = term env e2 in
t_let_close v e1 e2
......@@ -209,9 +209,9 @@ let rec term env t = match t.dt_node with
| Tnamed (x, e1) ->
let e1 = term env e1 in
t_label_add x e1
| Teps ({ id = x ; id_loc = loc }, ty, e1) ->
| Teps ({ id = x ; id_lab = labels ; id_loc = loc }, ty, e1) ->
let ty = ty_of_dty ty in
let v = create_vsymbol (id_user x loc) ty in
let v = create_vsymbol (id_user ~labels x loc) ty in
let env = Mstr.add x v env in
let e1 = fmla env e1 in
t_eps_close v e1
......@@ -228,9 +228,9 @@ and fmla env = function
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, uqu, trl, f1) ->
let uquant env ({ id = x ; id_loc = loc },ty) =
let uquant env ({ id = x ; id_lab = labels ; id_loc = loc },ty) =
let ty = ty_of_dty ty in
let v = create_vsymbol (id_user x loc) ty in
let v = create_vsymbol (id_user ~labels x loc) ty in
Mstr.add x v env, v
in
let env, vl = map_fold_left uquant env uqu in
......@@ -242,10 +242,10 @@ and fmla env = function
f_quant_close q vl trl (fmla env f1)
| Fapp (s, tl) ->
f_app s (List.map (term env) tl)
| Flet (e1, { id = x ; id_loc = loc }, f2) ->
| Flet (e1, { id = x ; id_lab = labels ; id_loc = loc }, f2) ->
let ty = ty_of_dty e1.dt_ty in
let e1 = term env e1 in
let v = create_vsymbol (id_user x loc) ty in
let v = create_vsymbol (id_user ~labels x loc) ty in
let env = Mstr.add x v env in
let f2 = fmla env f2 in
f_let_close v e1 f2
......
......@@ -286,12 +286,12 @@ decl:
{ LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
{ IndDecl $2 }
| AXIOM uident COLON lexpr
{ PropDecl (loc (), Kaxiom, $2, $4) }
| LEMMA uident COLON lexpr
{ PropDecl (loc (), Klemma, $2, $4) }
| GOAL uident COLON lexpr
{ PropDecl (loc (), Kgoal, $2, $4) }
| AXIOM uident labels COLON lexpr
{ PropDecl (loc (), Kaxiom, add_lab $2 $3, $5) }
| LEMMA uident labels COLON lexpr
{ PropDecl (loc (), Klemma, add_lab $2 $3, $5) }
| GOAL uident labels COLON lexpr
{ PropDecl (loc (), Kgoal, add_lab $2 $3, $5) }
| USE use
{ UseClone (loc (), $2, None) }
| CLONE use clone_subst
......
......@@ -653,10 +653,11 @@ let add_projections th d = match d.td_def with
| Some t -> t
in
let per_param acc ty (n,_) = match n with
| Some id when not (Mstr.mem id.id acc) ->
let fn = id_user id.id id.id_loc in
| Some { id = id ; id_lab = labels ; id_loc = loc }
when not (Mstr.mem id acc) ->
let fn = id_user ~labels id loc in
let fs = create_fsymbol fn [tc] ty in
Mstr.add id.id (fs,tc,ty) acc
Mstr.add id (fs,tc,ty) acc
| _ -> acc
in
List.fold_left2 per_param acc cs.ls_args pl
......@@ -690,15 +691,14 @@ let add_types dl th =
let vars = Hashtbl.create 17 in
let vl =
List.map
(fun v ->
if Hashtbl.mem vars v.id then
error ~loc:v.id_loc (DuplicateTypeVar v.id);
let i = create_tvsymbol (id_user v.id v.id_loc) in
Hashtbl.add vars v.id i;
(fun { id = v ; id_lab = labels ; id_loc = loc } ->
if Hashtbl.mem vars v then error ~loc (DuplicateTypeVar v);
let i = create_tvsymbol (id_user ~labels v loc) in
Hashtbl.add vars v i;
i)
d.td_params
in
let id = id_user id d.td_loc in
let id = id_user id ~labels:d.td_ident.id_lab d.td_loc in
let ts = match d.td_def with
| TDalias ty ->
let rec apply = function
......@@ -754,11 +754,11 @@ let add_types dl th =
Tabstract
| TDalgebraic cl ->
let ty = ty_app ts (List.map ty_var ts.ts_args) in
let constructor (loc, id, pl) =
let constructor (loc, { id = id ; id_lab = labels }, pl) =
let param (_,t) = ty_of_dty (dty th' t) in
let tyl = List.map param pl in
Hashtbl.replace csymbols id.id loc;
create_fsymbol (id_user id.id loc) tyl ty
Hashtbl.replace csymbols id loc;
create_fsymbol (id_user ~labels id loc) tyl ty
in
Talgebraic (List.map constructor cl)
in
......@@ -779,7 +779,7 @@ let add_logics dl th =
(* 1. create all symbols and make an environment with these symbols *)
let create_symbol th d =
let id = d.ld_ident.id in
let v = id_user id d.ld_loc in
let v = id_user ~labels:d.ld_ident.id_lab id d.ld_loc in
let denv = create_denv th in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty_of_dty (dty denv t) in
......@@ -810,7 +810,7 @@ let add_logics dl th =
let create_var (x, _) ty =
let id = match x with
| None -> id_fresh "%x"
| Some id -> id_user id.id id.id_loc
| Some id -> id_user ~labels:id.id_lab id.id id.id_loc
in
create_vsymbol id ty
in
......@@ -862,7 +862,7 @@ let type_fmla denv env f =
let fmla uc = type_fmla (create_denv uc) Mstr.empty
let add_prop k loc s f th =
let pr = create_prsymbol (id_user s.id loc) in
let pr = create_prsymbol (id_user ~labels:s.id_lab s.id loc) in
try add_prop_decl th k pr (fmla th f)
with ClashSymbol s -> error ~loc (Clash s)
......@@ -875,7 +875,7 @@ let add_inductives dl th =
let psymbols = Hashtbl.create 17 in
let create_symbol th d =
let id = d.in_ident.id in
let v = id_user id d.in_loc in
let v = id_user ~labels:d.in_ident.id_lab id d.in_loc in
let denv = create_denv th in
let type_ty (_,t) = ty_of_dty (dty denv t) in
let pl = List.map type_ty d.in_params in
......@@ -890,9 +890,9 @@ let add_inductives dl th =
let type_decl d =
let id = d.in_ident.id in
let ps = Hashtbl.find psymbols id in
let clause (loc, id, f) =
Hashtbl.replace propsyms id.id loc;
create_prsymbol (id_user id.id loc), fmla th' f
let clause (loc, { id = id ; id_lab = labels }, f) =
Hashtbl.replace propsyms id loc;
create_prsymbol (id_user ~labels id loc), fmla th' f
in
ps, List.map clause d.in_def
in
......
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