Skip to content

GitLab

Commit 6a9c5169 authored by Pietro Abate's avatar Pietro Abate
Browse files

Minor refactoring

parent 1deb9afa
Hide whitespace changes
Inline Side-by-side
tests/lambda/src/compute.ml
View file @ 6a9c5169
......@@ -18,45 +18,47 @@ let rec _to_typed env l expr =
(* From Camlp4 locations to CDuce locations *)
let loc = caml_loc_to_cduce (get_loc expr) in
match expr with
| Subst (_, e, s) ->
let _, _, e = _to_typed env l e in
(env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=(Subst (e, make_sigma s)) })
| Apply (_, e1, e2) ->
let _, _, e1 = _to_typed env l e1 in
let _, _, e2 = _to_typed env l e2 in
env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=Apply(e1, e2) }
| Abstr (_, fun_name, params, rtype, body) ->
parse_abstr env l [] loc (Some(0, fun_name)) params rtype body
| Match (_, e, t, b) ->
let b = parse_branches env l t b [] in
let t = type_of_ptype t in
let brs = { br_typ=t; br_accept=t; br_branches=b } in
let _, _, exp_descr = _to_typed env l e in
(env, l, { exp_loc=loc; exp_typ=t; exp_descr=Match(exp_descr, brs) })
| Pair (_, e1, e2) ->
let _, _, exp_descr1 = _to_typed env l e1 in
let _, _, exp_descr2 = _to_typed env l e2 in
(env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=Pair(exp_descr1, exp_descr2) })
| Var (origloc, vname) ->
if vname = "`nil" then
let nil_atom = Atoms.V.mk_ascii "nil" in
env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom)); exp_descr=(Cst (Types.Atom nil_atom)) }
else
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
let index = (try Locals.find vname l with Not_found -> Printf.eprintf
"File %s, line %d, characters %d-%d:\nUnbound identifier %s\n"
(Loc.file_name origloc) line cbegin cend vname; raise Error)
in
(env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=Var(index, vname) })
| Int (_, i) ->
let i = Big_int.big_int_of_int i in
(env, l, { exp_loc=loc; exp_typ=(type_of_string "Int"); exp_descr=Cst(Types.Integer i) })
| String (_, s) ->
let i = Big_int.big_int_of_int 0 in
let s = Types.String (0, (String.length s) - 1, s, Types.Integer i) in
(env, l, { exp_loc=loc; exp_typ=(type_of_string "String"); exp_descr=Cst s })
| Subst (_, e, s) ->
let _, _, e = _to_typed env l e in
(env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=(Subst (e, make_sigma s)) })
| Apply (_, e1, e2) ->
let _, _, e1 = _to_typed env l e1 in
let _, _, e2 = _to_typed env l e2 in
env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=Apply(e1, e2) }
| Abstr (_, fun_name, params, rtype, body) ->
parse_abstr env l [] loc (Some(0, fun_name)) params rtype body
| Match (_, e, t, b) ->
let b = parse_branches env l t [] b in
let t = type_of_ptype t in
let brs = { br_typ=t; br_accept=t; br_branches=b } in
let _, _, exp_descr = _to_typed env l e in
(env, l, { exp_loc=loc; exp_typ=t; exp_descr=Match(exp_descr, brs) })
| Pair (_, e1, e2) ->
let _, _, exp_descr1 = _to_typed env l e1 in
let _, _, exp_descr2 = _to_typed env l e2 in
(env, l, { exp_loc=loc; exp_typ=Types.empty; exp_descr=Pair(exp_descr1, exp_descr2) })
| Var (origloc, vname) ->
if vname = "`nil" then
let nil_atom = Atoms.V.mk_ascii "nil" in
env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom)); exp_descr=(Cst (Types.Atom nil_atom)) }
else
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
let index = (try Locals.find vname l with Not_found -> Printf.eprintf
"File %s, line %d, characters %d-%d:\nUnbound identifier %s\n"
(Loc.file_name origloc) line cbegin cend vname; raise Error)
in
let t = (* Ident.Env.find index env.Compile.gamma *) Types.any in
let v = if Types.no_var t then Var(index, vname) else TVar(index, vname) in
(env, l, { exp_loc=loc; exp_typ=t; exp_descr=v })
| Int (_, i) ->
let i = Big_int.big_int_of_int i in
(env, l, { exp_loc=loc; exp_typ=(type_of_string "Int"); exp_descr=Cst(Types.Integer i) })
| String (_, s) ->
let i = Big_int.big_int_of_int 0 in
let s = Types.String (0, (String.length s) - 1, s, Types.Integer i) in
(env, l, { exp_loc=loc; exp_typ=(type_of_string "String"); exp_descr=Cst s })
and make_sigma s =
let rec aux acc = function
......@@ -145,39 +147,49 @@ and itype acc =
| (_, _, t) :: rest -> itype (arrow (cons acc) (cons (type_of_ptype t))) rest
| [] -> acc
and parse_branches env l toptype brs res = match brs with
and parse_branches env l toptype acc = function
| (loc, p, e) :: rest ->
let brloc = caml_loc_to_cduce loc in
let t, d, list, br_locals, br_used =
parse_match_value env l [] p toptype in
let t, d, fv, br_locals, br_used = parse_match_value env l [] toptype p in
let line = Loc.start_line loc in
let cbegin = Loc.start_off loc - Loc.start_bol loc in
let cend = Loc.stop_off loc - Loc.start_bol loc in
let _, _, br_body = _to_typed env br_locals e in
let fname = Loc.file_name loc in
let node =
(if not br_used then
(Printf.eprintf
"File %s, line %d, characters %d-%d:\nWarning: This branch is not used\n"
fname line cbegin cend; make_patterns t [] d)
else make_patterns t list d) in
let b = { Typed.br_loc=brloc; br_used=br_used; br_ghost=false; br_vars_empty=[];
br_pat=node; br_body=br_body} in
parse_branches env l toptype rest (res @ [b])
| [] -> res
and make_patterns t fv d = incr Patterns.counter;
let tpat =
if not br_used then begin
Printf.eprintf
"File %s, line %d, characters %d-%d:\nWarning: This branch is not used\n"
fname line cbegin cend;
make_patterns t [] d
end else
make_patterns t fv d
in
let b = {
Typed.br_loc = caml_loc_to_cduce loc;
br_used = br_used;
br_ghost = false;
br_vars_empty = [];
br_pat = tpat;
br_body = br_body}
in
parse_branches env l toptype (acc @ [b]) rest
| [] -> acc
and make_patterns t fv d =
incr Patterns.counter;
{ Patterns.id=(!Patterns.counter);
Patterns.descr=(t, fv, d);
Patterns.accept=(Types.cons t); fv=fv }
descr=(t, fv, d);
accept=(Types.cons t);
fv=fv
}
and parse_match_value env l list p toptype = match p with
and parse_match_value env l list toptype = function
| MPair (_, m1, m2) ->
let top1, top2 =
(match toptype with | TPair(t1, t2) -> t1, t2 | TSeq(t) -> t, TSeq(t)
| _ -> Type("Empty"), Type("Empty")) in
let t1, d1, list1, l, b1 = parse_match_value env l list m1 top1 in
let t2, d2, list2, l, b2 = parse_match_value env l list m2 top2 in
let t1, d1, list1, l, b1 = parse_match_value env l list top1 m1 in
let t2, d2, list2, l, b2 = parse_match_value env l list top2 m2 in
Types.times (Types.cons t1) (Types.cons t2),
Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
(list1 @ list2), l, b1 && b2;
......
tests/lambda/src/parse.ml
View file @ 6a9c5169
......@@ -3,10 +3,10 @@ open Camlp4.PreCast
type expr =
| Subst of Loc.t * expr * (string * ptype) list
| Apply of Loc.t * expr * expr
| Apply of Loc.t * expr * expr
| Abstr of Loc.t * fun_name * params * ptype * expr
| Match of Loc.t * expr * ptype * branches
| Pair of Loc.t * expr * expr
| Pair of Loc.t * expr * expr
| Var of Loc.t * string
| Int of Loc.t * int
| String of Loc.t * string
......@@ -40,16 +40,16 @@ module ExprParser = struct
expression:
[
"abstr" RIGHTA
[ "fun"; x = LIDENT; p = LIST1 param; ":"; t = type_id; "->";
e = SELF -> Abstr(_loc, x, p, t, e)
| "match"; e = SELF; ":"; t = type_id; "with"; b = LIST1 branch ->
Match(_loc, e, t, b) ]
[ "fun"; x = LIDENT; p = LIST1 param; ":"; t = type_id; "->"; e = SELF ->
Abstr(_loc, x, p, t, e)
| "match"; e = SELF; ":"; t = type_id; "with"; b = LIST1 branch ->
Match(_loc, e, t, b) ]
| "pair" LEFTA
[ e1 = SELF; ","; e2 = SELF -> Pair(_loc, e1, e2)
| e1 = SELF ; "."; e2 = SELF -> Apply(_loc, e1, e2) ]
[ e1 = SELF; ","; e2 = SELF -> Pair(_loc, e1, e2)
| e1 = SELF ; "."; e2 = SELF -> Apply(_loc, e1, e2) ]
| "list" LEFTA [ "["; le = listexpr; "]" -> le ]
| "paren" [ "("; e = SELF; ")" -> e ]
| "var" [ x = LIDENT -> Var(_loc, x) ]
| "var" [ x = LIDENT -> Var(_loc, x) ]
| "int" [ x = INT -> Int(_loc, int_of_string x) ]
| "string" [ x = STRING -> String(_loc, x) ]
| "subst" NONA
......@@ -63,8 +63,9 @@ module ExprParser = struct
param:[[p = LIDENT; ":"; t = type_id -> _loc, p, t]];
branch:[ "branch" [ "|"; t = match_value; "->"; e = expression ->
_loc, t, e ]];
branch:[ "branch"
[ "|"; t = match_value; "->"; e = expression -> _loc, t, e ]
];
match_value:
[
......@@ -76,22 +77,21 @@ module ExprParser = struct
| "string" [ x = STRING -> MString(_loc, x) ]
];
type_id: [ "atom_type" [ t = UIDENT -> Type(t) ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" ->
PType(t1, s) ]
| [ "("; t = complex_type_id; ")" -> t ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]];
complex_type_id: [ "complex_type" LEFTA [ t = UIDENT -> Type(t)
| "("; t = SELF; ")" -> t ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" ->
PType(t1, s) ]
| [ t1 = SELF; "*"; t2 = SELF -> TPair(t1, t2)
| t1 = SELF; "->"; t2 = SELF -> TArrow(t1, t2) ]
| [ t1 = SELF; "|"; t2 = SELF -> TUnion(t1, t2)
| t1 = SELF; "&"; t2 = SELF -> TInter(t1, t2) ]
| [ "!"; t = SELF -> TNot(t) ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]];
type_id: [ "atom_type"
[ t = UIDENT -> Type(t) ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" -> PType(t1, s) ]
| [ "("; t = complex_type_id; ")" -> t ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]
];
complex_type_id: [ "complex_type" LEFTA
[ t = UIDENT -> Type(t) | "("; t = SELF; ")" -> t ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" -> PType(t1, s) ]
| [ t1 = SELF; "*"; t2 = SELF -> TPair(t1, t2) | t1 = SELF; "->"; t2 = SELF -> TArrow(t1, t2) ]
| [ t1 = SELF; "|"; t2 = SELF -> TUnion(t1, t2) | t1 = SELF; "&"; t2 = SELF -> TInter(t1, t2) ]
| [ "!"; t = SELF -> TNot(t) ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]
];
END;;
......
tests/lambda/src/printer.ml
View file @ 6a9c5169
......@@ -29,6 +29,10 @@ and pp_typed_aux ppf e =
match e.Typed.exp_descr with
| Typed.Forget(e, _) -> Format.fprintf ppf "Forget(%a)" pp_typed e
| Typed.Check(_, e, _) -> Format.fprintf ppf "Check(%a)" pp_typed e
| Typed.TVar(id, name) ->
Format.fprintf ppf "TVar(%s,%s)"
(string_of_int (Upool.int id))
(Encodings.Utf8.to_string name)
| Typed.Var(id, name) ->
Format.fprintf ppf "Var(%s,%s)"
(string_of_int (Upool.int id))
......
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