Skip to content

GitLab

C
cduce
Commit bcb7506c authored by Pietro Abate's avatar Pietro Abate
Browse files
Options

Add sigma to Lambda and Vaue languages

parent 7f09389f
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 220 additions and 173 deletions
compile/compile.ml
View file @ bcb7506c
......@@ -4,6 +4,8 @@ open Lambda
type env = {
cu: Compunit.t option; (* None: toplevel *)
vars: var_loc Env.t;
sigma : sigma; (* symbolic substitutions (Lambda.sigma) *)
gamma : var_loc Env.t; (* map of type variables to types *)
stack_size: int;
max_stack: int ref;
global_size: int
......@@ -11,7 +13,15 @@ type env = {
let global_size env = env.global_size
let mk cu = { cu = cu; vars = Env.empty; stack_size = 0; max_stack = ref 0; global_size = 0 }
let mk cu = {
cu = cu;
vars = Env.empty;
sigma = `List [];
gamma = Env.empty;
stack_size = 0;
max_stack = ref 0;
global_size = 0
}
let empty_toplevel = mk None
let empty x = mk (Some x)
......@@ -48,6 +58,7 @@ let enter_global_cu cu env x =
vars = Env.add x (Ext (cu,env.global_size)) env.vars;
global_size = env.global_size + 1 }
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
let rec compile env e = compile_aux env e.Typed.exp_descr
and compile_aux env = function
| Typed.Forget (e,_) -> compile env e
......@@ -55,7 +66,11 @@ and compile_aux env = function
let d = Patterns.Compile.make_checker !t0 (Types.descr t) in
Check (compile env e, d)
| Typed.Var x -> Var (find x env)
| Typed.TVar x -> Var (find x env)
| Typed.TVar x ->
let v = find x env in
if env.sigma = (`List []) (* && not (find v dom(env.sigma)) *) then Var (v)
else TVar(v,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = `Comp(env.sigma,`List sl) } e
| Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
| Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
| Typed.Abstraction a -> compile_abstr env a
......@@ -122,22 +137,27 @@ and compile_abstr env a =
let slots = Array.of_list (List.rev slots) in
let env = { env with vars = fun_env; stack_size = 0; max_stack = ref 0 } in
let body = compile_branches env a.Typed.fun_body in
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, List [[]])
let sigma = (* `Sel (x,t,env.sigma) *) `List [] in
if equal (inter vars(t) dom(env.sigma)) empty then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma)
else
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been
type checked. *)
(* Don't compile unused branches, because they have not been type checked. *)
let used = List.filter (fun br -> br.Typed.br_used) brs.Typed.br_branches in
let b = List.map (compile_branch env) used in
let (disp,rhs) = Patterns.Compile.make_branches brs.Typed.br_typ b in
{ brs_stack_pos = env.stack_size;
brs_accept_chars = not (Types.Char.is_empty brs.Typed.br_accept);
brs_disp = disp;
brs_rhs = rhs }
brs_rhs = rhs
}
(* p_i / t_i br.Typed.br_pat / br.Typed.br_type *)
and compile_branch env br =
let env = List.fold_left enter_local env (Patterns.fv br.Typed.br_pat) in
(br.Typed.br_pat, compile env br.Typed.br_body)
(br.Typed.br_pat, br.Typed.br_type, compile env br.Typed.br_body)
let enter_globals env n = match env.cu with
| None -> List.fold_left enter_global_toplevel env n
......
compile/lambda.ml
View file @ bcb7506c
......@@ -22,17 +22,19 @@ type var_loc =
(* Only for the toplevel *)
| Dummy
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (fv * Types.t * sigma)
(* only TVar (polymorphic type variable) and Abstraction have
* a sigma annotation *)
type sigma = [
| `List of Types.Tallying.CS.sl
| `Comp of (sigma * sigma)
| `Sel of (fv * Types.t * sigma) ]
type expr =
| Var of var_loc
| PVar of (var_loc * sigma)
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
(* environment, interface, branches, size of locals *)
(* environment, interface, branches, size of locals, eval flag, substitutions *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......
compile/lambda.mli
View file @ bcb7506c
......@@ -29,7 +29,7 @@ type sigma =
type expr =
| Var of var_loc
| PVar of (var_loc * sigma)
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
(* environment, interface, branches, size of locals *)
......
runtime/eval.ml
View file @ bcb7506c
......@@ -11,11 +11,10 @@ let eval_op = Hashtbl.find ops
(* To write tail-recursive map-like iteration *)
let make_accu () = Value.Pair(nil,Absent)
let make_accu () = Value.Pair(nil,Absent,esigma)
let get_accu a = snd (Obj.magic a)
let map f v = let acc0 = make_accu () in set_cdr (f acc0 v) nil; get_accu acc0
let rec ensure a i =
let n = Array.length !a in
if i >= n then (
......@@ -34,7 +33,6 @@ let set a i x =
let globs = ref (Array.create 64 Value.Absent)
let nglobs = ref 0
let get_globals = ref (fun cu -> assert false)
let get_external = ref (fun cu pos -> assert false)
let set_external = ref (fun cu pos -> assert false)
......@@ -66,6 +64,16 @@ let eval_var env locals = function
let tag_op_resolved = Obj.tag (Obj.repr (OpResolved ((fun _ -> assert false), [])))
let tag_const = Obj.tag (Obj.repr (Const (Obj.magic 0)))
let apply_sigma sigma = function
|Value.Pair(v1,v2,sigma') -> Value.Pair(v1,v2,`Comp(sigma,sigma'))
|Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,f,`Comp(sigma,sigma'))
|Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,`Comp(sigma,sigma'))
|Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,`Comp(sigma,sigma'))
|Value.Record(m,sigma') -> Value.Record(m,`Comp(sigma,sigma'))
|v -> v
;;
(* env is an array implementing de bruines indexes *)
let rec eval env locals = function
| Var ((Global _ | Ext _ | External _ | Builtin _) as x) as e ->
let v = eval_var env locals x in
......@@ -73,10 +81,11 @@ let rec eval env locals = function
Obj.set_tag (Obj.repr e) tag_const;
v
(* variable evaluation will be split in PEnv and Env.
* PEnv and Env belong to the runtime labmda language
* PEnv and Env belong to the runtime lambda language
* from the parsing ast + typing information *)
| Var x -> eval_var env locals x
| PVar (x,sigma) -> eval_var env locals x
| TVar (x,sigma) -> (* delayed sigma application *)
apply_sigma sigma (eval_var env locals x)
| Apply (e1,e2) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
......@@ -87,19 +96,19 @@ let rec eval env locals = function
| Pair (e1,e2) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
Value.Pair (v1,v2)
Value.Pair (v1,v2,Value.esigma)
| Xml (e1,e2,e3) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
let v3 = eval env locals e3 in
Value.Xml (v1,v2,v3)
Value.Xml (v1,v2,v3,Value.esigma)
| XmlNs (e1,e2,e3,ns) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
let v3 = eval env locals e3 in
Value.XmlNs (v1,v2,v3,ns)
Value.XmlNs (v1,v2,v3,ns,Value.esigma)
| Record r ->
Value.Record (Imap.map (eval env locals) r)
Value.Record (Imap.map (eval env locals) r, Value.esigma)
| String (i,j,s,q) -> Value.substring_utf8 i j s (eval env locals q)
(* let is encoded as a match *)
| Match (e,brs) -> eval_branches env locals brs (eval env locals e)
......@@ -130,12 +139,12 @@ and eval_abstraction env locals slots iface body lsize =
let f arg =
eval_branches local_env (Array.create lsize Value.Absent) body arg
in
let a = Value.Abstraction (Some iface,f) in
let a = Value.Abstraction (Some iface,f,Value.esigma) in
local_env.(0) <- a;
a
and eval_apply f arg = match f with
| Value.Abstraction (_,f) -> f arg
| Value.Abstraction (_,f,sigma) -> f arg
| _ -> assert false
and eval_branches env locals brs arg =
......@@ -165,9 +174,9 @@ and eval_map env locals brs v =
map (eval_map_aux env locals brs) v
and eval_map_aux env locals brs acc = function
| Value.Pair (x,y) ->
| Value.Pair (x,y,sigma) ->
let x = eval_branches env locals brs x in
let acc' = Value.Pair (x, Absent) in
let acc' = Value.Pair (x, Absent,sigma) in
set_cdr acc acc';
eval_map_aux env locals brs acc' y
| Value.String_latin1 (_,_,_,_) | Value.String_utf8 (_,_,_,_) as v ->
......@@ -181,7 +190,7 @@ and eval_transform env locals brs v =
map (eval_transform_aux env locals brs) v
and eval_transform_aux env locals brs acc = function
| Value.Pair (x,y) ->
| Value.Pair (x,y,sigma) ->
(match eval_branches env locals brs x with
| Value.Absent -> eval_transform_aux env locals brs acc y
| x -> eval_transform_aux env locals brs (append_cdr acc x) y)
......@@ -215,19 +224,19 @@ and eval_xtrans_aux env locals brs acc = function
| Value.Concat (x,y) ->
let acc = eval_xtrans_aux env locals brs acc x in
eval_xtrans_aux env locals brs acc y
| Value.Pair (x,y) ->
| Value.Pair (x,y,sigma) ->
let acc =
match eval_branches env locals brs x with
| Value.Absent ->
let x = match x with
| Value.Xml (tag, attr, child) ->
| Value.Xml (tag, attr, child,sigma) ->
let child = eval_xtrans env locals brs child in
Value.Xml (tag, attr, child)
| Value.XmlNs (tag, attr, child, ns) ->
Value.Xml (tag, attr, child,sigma)
| Value.XmlNs (tag, attr, child, ns,sigma) ->
let child = eval_xtrans env locals brs child in
Value.XmlNs (tag, attr, child, ns)
Value.XmlNs (tag, attr, child, ns,sigma)
| x -> x in
let acc' = Value.Pair (x, Absent) in
let acc' = Value.Pair (x, Absent,sigma) in
set_cdr acc acc';
acc'
| x -> append_cdr acc x
......@@ -236,16 +245,15 @@ and eval_xtrans_aux env locals brs acc = function
| _ -> acc
and eval_dot l = function
| Value.Record r
| Value.Xml (_,Value.Record r,_)
| Value.XmlNs (_,Value.Record r,_,_) -> Imap.find_lower r (Upool.int l)
| Value.Record (r,_)
| Value.Xml (_,Value.Record (r,_),_,_)
| Value.XmlNs (_,Value.Record (r,_),_,_,_) -> Imap.find_lower r (Upool.int l)
| v -> assert false
and eval_remove_field l = function
| Value.Record r -> Value.Record (Imap.remove r (Upool.int l))
| Value.Record (r,sigma) -> Value.Record (Imap.remove r (Upool.int l),sigma)
| _ -> assert false
let expr e lsize = eval [||] (Array.create lsize Value.Absent) e
(* Evaluation in the toplevel *)
......
runtime/explain.ml
View file @ bcb7506c
......@@ -47,18 +47,18 @@ and run_disp pt d v =
run_dispatcher ((v, d.expected_type)::pt) d v
and run_disp_kind pt d actions = function
| Pair (v1,v2) -> run_disp_prod pt d v1 v2 actions.prod
| Xml (v1,v2,v3) | XmlNs (v1,v2,v3,_) -> run_disp_prod pt d v1 (Pair(v2,v3)) actions.xml
| Record r -> run_disp_record pt d 0 r actions.record
| Pair (v1,v2,sigma) -> run_disp_prod pt d v1 v2 actions.prod
| Xml (v1,v2,v3,sigma) | XmlNs (v1,v2,v3,_,sigma) -> run_disp_prod pt d v1 (Pair(v2,v3,sigma)) actions.xml
| Record (r,sigma) -> run_disp_record pt d 0 r actions.record
| Atom q -> make_result pt d (Atoms.get_map q actions.atoms)
| Char c -> make_result pt d (Chars.get_map c actions.chars)
| Integer i ->
run_disp_basic pt d (fun t -> Types.Int.has_int t i) actions.basic
| Abstraction (None,_) ->
| Abstraction (None,_,sigma) ->
run_disp_basic pt d
(fun t -> failwith "Run-time inspection of external abstraction")
actions.basic
| Abstraction (Some iface,_) ->
| Abstraction (Some iface,_,sigma) ->
run_disp_basic pt d (fun t -> Types.Arrow.check_iface iface t)
actions.basic
| Absent ->
......
runtime/run_dispatch.ml
View file @ bcb7506c
......@@ -56,7 +56,8 @@ let make_result_prod v1 v2 v (code,r,pop) =
| Recompose (i,j) ->
Pair (
(match i with (-1) -> v1 | (-2) -> nil | _ -> buf.(c - i)),
(match j with (-1) -> v2 | (-2) -> nil | _ -> buf.(c - j))
(match j with (-1) -> v2 | (-2) -> nil | _ -> buf.(c - j)),
esigma
)
in
buf.(c + a) <- x
......@@ -124,7 +125,8 @@ let make_result_string_latin1 i j s q (code,r,pop) =
(match m with
| (-1) -> tail_string_latin1 i j s q
| (-2) -> nil
| _ -> buf.(c - m))
| _ -> buf.(c - m)),
esigma
)
in
buf.(c + a) <- x
......@@ -160,7 +162,8 @@ let make_result_string_utf8 i j s q (code,r,pop) =
(match m with
| (-1) -> tail_string_utf8 i j s q
| (-2) -> nil
| _ -> buf.(c - m))
| _ -> buf.(c - m)),
esigma
)
in
buf.(c + a) <- x
......@@ -187,10 +190,10 @@ let rec run_dispatcher d v =
and run_disp_kind actions v =
match v with
| Pair (v1,v2) -> run_disp_prod v v1 v2 actions.prod
| Xml (v1,v2,v3)
| XmlNs (v1,v2,v3,_) -> run_disp_prod v v1 (Pair (v2,v3)) actions.xml
| Record r -> run_disp_record 0 v r actions.record
| Pair (v1,v2,sigma) -> run_disp_prod v v1 v2 actions.prod
| Xml (v1,v2,v3,sigma)
| XmlNs (v1,v2,v3,_,sigma) -> run_disp_prod v v1 (Pair (v2,v3,sigma)) actions.xml (* ??? *)
| Record (r,sigma) -> run_disp_record 0 v r actions.record
| String_latin1 (i,j,s,q) ->
(* run_disp_kind actions (Value.normalize v) *)
run_disp_string_latin1 i j s q actions
......@@ -201,10 +204,10 @@ and run_disp_kind actions v =
| Char c -> make_result_basic v (Chars.get_map c actions.chars)
| Integer i ->
run_disp_basic v (fun t -> Types.Int.has_int t i) actions.basic
| Abstraction (None,_) ->
| Abstraction (None,_,_) ->
run_disp_basic v (fun t -> failwith "Run-time inspection of external abstraction")
actions.basic
| Abstraction (Some iface,_) ->
| Abstraction (Some iface,_,sigma) ->
run_disp_basic v (fun t -> Types.Arrow.check_iface iface t)
actions.basic
| Abstract (abs,_) ->
......
runtime/value.ml
View file @ bcb7506c
This diff is collapsed.
schema/schema_common.ml
View file @ bcb7506c
......@@ -128,11 +128,11 @@ type to_be_visited =
let stream_of_value v =
let stack = ref [Fully v] in
let f _ = (* lazy visit of a tree of CDuce XML values, stack keeps track of
what has still to be visited *)
match !stack with
| (Fully ((Value.Xml (Value.Atom atom, attrs, _))
|(Value.XmlNs (Value.Atom atom, attrs, _, _)) as v)) :: tl ->
(* lazy visit of a tree of CDuce XML values, stack keeps track of
what has still to be visited *)
let f _ = match !stack with
| (Fully ((Value.Xml (Value.Atom atom, attrs, _,sigma))
|(Value.XmlNs (Value.Atom atom, attrs, _, _,sigma)) as v)) :: tl ->
stack := (Half v) :: tl;
let children = ref [] in (* TODO inefficient *)
let push v s = (s := v :: !s) in
......
schema/schema_validator.ml
View file @ bcb7506c
......@@ -59,7 +59,7 @@ let concat ctx v = ctx.ctx_current <- Value.concat ctx.ctx_current v
let append ctx v = ctx.ctx_current <- Value.append ctx.ctx_current v
let xml qname attrs content =
Value.Xml (Value.Atom qname, attrs, content)
Value.Xml (Value.Atom qname, attrs, content, Value.esigma)
let peek ctx =
......@@ -194,7 +194,7 @@ struct
* and no Concat, but just Pair *)
let length v =
let rec aux acc = function
| Pair (_, rest) -> aux (succ acc) rest
| Pair (_, rest,sigma) -> aux (succ acc) rest
| _ -> 0
in
aux 0 v
......@@ -539,7 +539,7 @@ let validate_type def value =
let attrs = get_attributes ctx in
let (attrs, content) = validate_complex_type ctx attrs ct_def in
expect_end_tag ctx;
Value.Xml (Value.Atom start_tag, attrs, content)
Value.Xml (Value.Atom start_tag, attrs, content,Value.esigma)
(*
let validate_attribute decl value =
......@@ -599,7 +599,7 @@ let validate_model_group { mg_def = mg } value =
if not (Value.is_seq value) then
error
"Only sequence values could be validated against model groups";
let stream = stream_of_value (Value.Xml (foo_atom, empty_record, value)) in
let stream = stream_of_value (Value.Xml (foo_atom, empty_record, value,Value.esigma)) in
Stream.junk stream;
let ctx = ctx stream in
validate_model_group ctx mg;
......
tests/eval/src/compile.ml
View file @ bcb7506c
......@@ -46,7 +46,7 @@ let parse_to_lambda expr =
let new_env = mk_env ~parent:(Some env) ~max_size:env.max_size ~map:map
nbrparams (env.global_size + nbrparams) in
let brs = compile_func_body new_env body (nbrparams - 1) in
Abstraction(params, [], brs, nbrparams, true, List [[]])
Abstraction(params, [], brs, nbrparams, true, `List [[]])
| Var(loc, vname) ->
(try let index = env_find env vname in Var(Local(index))
with Not_found ->
......@@ -62,9 +62,9 @@ let parse_to_lambda expr =
String(Ident.U.start_index s, Ident.U.end_index s, s,
Const(Value.Atom(nil_atom)))
| Pair(_, e1, e2) -> Pair(_parse_to_lambda env e1,
_parse_to_lambda env e2)
_parse_to_lambda env e2)
| Match(_, e, branches) ->
Match(_parse_to_lambda env e, compile_branches env branches)
Match(_parse_to_lambda env e, compile_branches env branches)
| Let(_, x, e1, e2) -> (* TODO: Define the "_" *)
let newloc = Camlp4.PreCast.Loc.ghost in
Apply(_parse_to_lambda env (Abstract(newloc, "_", [x], e2)),
......
tests/eval/src/main.ml
View file @ bcb7506c
......@@ -12,15 +12,15 @@ let load_file f =
s
let rec print_value v = match v with
| Value.Pair(v1, v2) -> printf "("; print_value v1; printf ", ";
| Value.Pair(v1, v2,_) -> printf "("; print_value v1; printf ", ";
print_value v2; printf ")"
| Xml(_,_,_) -> printf "Xml"
| XmlNs(_,_,_,_) -> printf "XmlNs"
| Record(_) -> printf "Record"
| Xml(_,_,_,_) -> printf "Xml"
| XmlNs(_,_,_,_,_) -> printf "XmlNs"
| Record(_,_) -> printf "Record"
| Atom(_) -> printf "Atom"
| Integer(i) -> printf "%d" (Big_int.int_of_big_int i)
| Char(i) -> printf "Char(%d)" i
| Abstraction(_, _) -> printf "Abstraction()"
| Abstraction(_,_,_) -> printf "Abstraction()"
| Abstract((name, _)) -> printf "Abstract(%s)" name
| String_latin1(i1, i2, s, v) -> printf "String_latin1(%d, %d, %s)" i1 i2 s;
print_value v
......
types/types.mli
View file @ bcb7506c
......@@ -161,7 +161,7 @@ sig
val times: v -> v -> v
val xml: v -> v -> v
val decompose : t -> v
(* val decompose : t -> v *)
val substitute : t -> (Var.var * t) -> t
val substituterec : t -> Var.var -> t
val solve: v -> Node.t
......
typing/typed.ml
View file @ bcb7506c
......@@ -15,12 +15,15 @@ open Ident
type tpat = Patterns.node
type ttyp = Types.Node.t
type sigma = Types.Tallying.CS.sl
type texpr =
{ exp_loc : loc;
mutable exp_typ : Types.t;
(* Currently exp_typ is not used. It will be used for compilation ! *)
exp_descr : texpr';
mutable exp_descr : texpr';
}
and texpr' =
| Forget of texpr * ttyp
| Check of (Types.t ref) * texpr * ttyp
......@@ -28,6 +31,8 @@ and texpr' =
| Var of id
(* polymorphic variable *)
| TVar of id
(* lazy substutiutions *)
| Subst of (texpr * sigma)
| ExtVar of Compunit.t * id * Types.t
| Apply of texpr * texpr
| Abstraction of abstr
......@@ -79,7 +84,10 @@ and branch = {
mutable br_used : bool;
br_ghost : bool;
mutable br_vars_empty : fv;
br_pat : tpat;
br_pat : tpat;
(*
mutable br_type : Types.t; (* Type accepted by this branch *)
*)
br_body : texpr
}
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