Commit b9aa225f authored by Pietro Abate's avatar Pietro Abate

Propagate type information from Typed to Value

- redifine sigma (Value.sigma and Lamda.sigma)
- add sigma application in eval
- fix typing rules for abstraction and match
- XXX This commit breaks all tests !!!
parent e98b1638
......@@ -16,7 +16,7 @@ let global_size env = env.global_size
let mk cu = {
cu = cu;
vars = Env.empty;
sigma = `List [];
sigma = List [];
gamma = IdMap.empty;
stack_size = 0;
max_stack = ref 0;
......@@ -59,9 +59,15 @@ let enter_global_cu cu env x =
global_size = env.global_size + 1 }
let rec domain = function
|`List l -> Types.Tallying.domain l
|`Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|`Sel(x,t,s) -> (domain s)
|List l -> Types.Tallying.domain l
|Comp (s1,s2) -> Var.Set.union (domain s1) (domain s2)
|Sel(_,_,s) -> (domain s)
let count_name = ref 0
let fresh_arg () =
incr count_name;
let s = ("__abstr_arg" ^ (string_of_int !count_name)) in
(0,Ns.U.mk s)
(* from intermediate explicitely typed language to Evaluation language (lambda) *)
let rec compile env e = compile_aux env e.Typed.exp_descr
......@@ -80,7 +86,7 @@ and compile_aux env = function
in
if Var.Set.is_empty polyvars then Var (v)
else TVar(v,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = `Comp(env.sigma,`List sl) } e
| 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
......@@ -125,7 +131,11 @@ and compile_abstr env a =
let fun_env, fun_name =
match a.Typed.fun_name with
| Some x -> Env.add x (Env 0) Env.empty, [x, Types.cons a.Typed.fun_typ]
| None -> Env.empty, [] in
| None -> Env.empty, []
in
(* here is were we add a fresh variable to compture the argument of an abstraction *)
let fun_env = Env.add (fresh_arg ()) (Env 1) fun_env in
let (slots,nb_slots,fun_env) =
List.fold_left
......@@ -141,14 +151,20 @@ and compile_abstr env a =
Env.add x p fun_env
| Dummy -> assert false
)
([Dummy],1,fun_env) (IdSet.get a.Typed.fun_fv) in
([Dummy],2,fun_env) (IdSet.get a.Typed.fun_fv)
in
let slots = Array.of_list (List.rev slots) in
let env = { env with vars = fun_env; gamma = IdMap.merge (fun _ v2 -> v2) env.gamma fun_name;
stack_size = 0; max_stack = ref 0 } in
let env =
{ env with vars = fun_env;
gamma = IdMap.merge (fun _ v2 -> v2) env.gamma fun_name;
stack_size = 0;
max_stack = ref 0 }
in
let body = compile_branches env a.Typed.fun_body in
let sigma = `Sel(a.Typed.fun_fv,a.Typed.fun_iface,env.sigma) in
(* we add a fresh variable to this abstraction *)
let argvar = Local 1 in
let sigma = Sel(argvar,a.Typed.fun_iface,env.sigma) in
let polyvars =
let vs =
List.fold_left (fun acc (t1,t2) ->
......@@ -160,9 +176,9 @@ and compile_abstr env a =
Var.Set.inter (domain(env.sigma)) vs
in
if Var.Set.is_empty polyvars then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma)
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma, argvar)
else
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma)
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma, argvar)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been type checked. *)
......
......@@ -24,17 +24,17 @@ type var_loc =
(* 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 * Types.t) list * sigma) ]
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * (Types.t * Types.t) list * sigma)
type expr =
| Var of var_loc
| 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, eval flag, substitutions *)
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma * var_loc
(* environment, interface, branches, size of locals, eval flag, substitutions, variable *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
......
......@@ -24,16 +24,16 @@ type var_loc =
(* 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 * Types.t) list * sigma) ]
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (var_loc * (Types.t * Types.t) list * sigma)
type expr =
| Var of var_loc
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma * var_loc
(* environment, interface, branches, size of locals *)
| Check of expr * Auto_pat.state
| Const of Value.t
......
......@@ -46,7 +46,7 @@ let register_cst op t v =
let register_fun op dom codom eval =
register_cst op
(Types.arrow (Types.cons dom) (Types.cons codom))
(Value.Abstraction (Some [(dom,codom)],eval, `List([])))
(Value.Abstraction (Some [(dom,codom)],eval, Value.Identity))
let register_fun2 op dom1 dom2 codom eval =
let t2 = Types.arrow (Types.cons dom2) (Types.cons codom) in
......@@ -55,7 +55,7 @@ let register_fun2 op dom1 dom2 codom eval =
(Types.arrow (Types.cons dom1) (Types.cons t2))
(Value.Abstraction (Some [(dom1,t2)],(fun v1 ->
Value.Abstraction (iface2,
eval v1, `List([]))), `List([])))
eval v1, Value.Identity)), Value.Identity))
let register_op op ?(expect=Types.any) typ eval =
register_unary op
(fun tf _ _ -> let t = tf expect true in typ t)
......
......@@ -11,7 +11,7 @@ let eval_op = Hashtbl.find ops
(* To write tail-recursive map-like iteration *)
let make_accu () = Value.Pair(nil,Absent,esigma)
let make_accu () = Value.Pair(nil,Absent,Value.Identity)
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
......@@ -28,7 +28,6 @@ let set a i x =
ensure a i;
!a.(i) <- x
(* For the toplevel *)
let globs = ref (Array.create 64 Value.Absent)
let nglobs = ref 0
......@@ -65,15 +64,21 @@ 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'))
|Value.Pair(v1,v2,sigma') -> Value.Pair(v1,v2,Value.Comp(sigma,sigma'))
|Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,f,Value.Comp(sigma,sigma'))
|Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,Value.Comp(sigma,sigma'))
|Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,Value.Comp(sigma,sigma'))
|Value.Record(m,sigma') -> Value.Record(m,Value.Comp(sigma,sigma'))
|v -> v
;;
let rec eval_sigma env locals = function
|Lambda.Comp(s1,s2) -> Value.Comp(eval_sigma env locals s1,eval_sigma env locals s2)
|Lambda.List l -> Value.List l
|Lambda.Sel(x,iface,sigma) -> Value.Sel(eval_var env locals x,iface,eval_sigma env locals sigma)
(* env is an array implementing de bruines indexes *)
(* Evaluation rules : Lamda -> Value *)
let rec eval env locals = function
| Var ((Global _ | Ext _ | External _ | Builtin _) as x) as e ->
let v = eval_var env locals x in
......@@ -85,30 +90,34 @@ let rec eval env locals = function
* from the parsing ast + typing information *)
| Var x -> eval_var env locals x
| TVar (x,sigma) -> (* delayed sigma application *)
apply_sigma sigma (eval_var env locals x)
let sigma' = eval_sigma env locals sigma in
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
eval_apply v1 v2
| Abstraction (slots,iface,body,lsize,flag,sigma) ->
eval_abstraction env locals slots iface body lsize
| Abstraction (slots,iface,body,lsize,flag,sigma,var) ->
let sigma' = eval_sigma env locals sigma in
eval_abstraction env locals slots iface body lsize sigma'
| Const c -> c
| Pair (e1,e2) ->
| Pair (e1,e2) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
Value.Pair (v1,v2,Value.esigma)
(* This is the empty substitution. sigma is associated to a pair only
* when is from a variable x_sigma *)
Value.Pair (v1,v2,Value.Identity)
| 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.esigma)
Value.Xml (v1,v2,v3,Value.Identity)
| 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.esigma)
Value.XmlNs (v1,v2,v3,ns,Value.Identity)
| Record r ->
Value.Record (Imap.map (eval env locals) r, Value.esigma)
Value.Record (Imap.map (eval env locals) r, Value.Identity)
| 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)
......@@ -133,14 +142,11 @@ let rec eval env locals = function
and eval_check env locals e d =
Explain.do_check d (eval env locals e)
and eval_abstraction env locals slots iface body lsize =
(* this is the sigma of the clousure *)
let local_env = Array.map (eval_var env locals) slots in
let f arg =
eval_branches local_env (Array.create lsize Value.Absent) body arg
in
let a = Value.Abstraction (Some iface,f,Value.esigma) in
local_env.(0) <- a;
and eval_abstraction env locals slots iface body lsize sigma =
let clousure = Array.map (eval_var env locals) slots in
let f arg = eval_branches clousure (Array.create lsize Value.Absent) body arg in
let a = Value.Abstraction (Some iface,f,sigma) in
clousure.(0) <- a;
a
and eval_apply f arg = match f with
......
......@@ -54,7 +54,7 @@ and run_disp_kind pt d actions = function
| 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,_,sigma) ->
| Abstraction (None,_,_) ->
run_disp_basic pt d
(fun t -> failwith "Run-time inspection of external abstraction")
actions.basic
......
......@@ -48,9 +48,9 @@ let attrib att =
let elem ns tag att child =
if !keep_ns then
XmlNs (Atom tag, Record (attrib att, `List([])), child, ns, `List([]))
XmlNs (Atom tag, Record (attrib att, Value.Identity), child, ns, Value.Identity)
else
Xml (Atom tag, Record (attrib att, `List([])), child, `List([]))
Xml (Atom tag, Record (attrib att, Value.Identity), child, Value.Identity)
type stack =
| Element of Value.t * stack
......@@ -64,7 +64,7 @@ let ns_table = ref Ns.empty_table
let rec create_elt accu = function
| String (s,st) -> create_elt (string s accu) st
| Element (x,st) -> create_elt (Pair (x,accu, `List([]))) st
| Element (x,st) -> create_elt (Pair (x,accu, Value.Identity)) st
| Start (ns,name,att,old_table,st) ->
stack := Element (elem ns name att accu, st);
ns_table := old_table
......@@ -132,7 +132,7 @@ let load_html s =
| Nethtml.Element (tag, att, child) ->
let att = List.map (fun (n,v) -> (Label.mk (Ns.empty, U.mk n), U.mk v)) att in
Pair (elem Ns.empty_table (Atoms.V.mk (Ns.empty,U.mk tag) )
att (val_of_docs child), q, `List([]))
att (val_of_docs child), q, Value.Identity)
and val_of_docs = function
| [] -> nil
| h::t -> val_of_doc (val_of_docs t) h
......
......@@ -59,7 +59,7 @@ module H = Hashtbl.Make(Ns.Uri)
let exn_print_xml = CDuceExn (Pair (
Atom (Atoms.V.mk_ascii "Invalid_argument"),
string_latin1 "print_xml", `List([])))
string_latin1 "print_xml", Value.Identity))
let blank = U.mk " "
let true_literal = U.mk "true"
......
......@@ -57,7 +57,7 @@ let make_result_prod v1 v2 v (code,r,pop) =
Pair (
(match i with (-1) -> v1 | (-2) -> nil | _ -> buf.(c - i)),
(match j with (-1) -> v2 | (-2) -> nil | _ -> buf.(c - j)),
esigma
Value.Identity
)
in
buf.(c + a) <- x
......@@ -126,7 +126,7 @@ let make_result_string_latin1 i j s q (code,r,pop) =
| (-1) -> tail_string_latin1 i j s q
| (-2) -> nil
| _ -> buf.(c - m)),
esigma
Value.Identity
)
in
buf.(c + a) <- x
......@@ -163,7 +163,7 @@ let make_result_string_utf8 i j s q (code,r,pop) =
| (-1) -> tail_string_utf8 i j s q
| (-2) -> nil
| _ -> buf.(c - m)),
esigma
Value.Identity
)
in
buf.(c + a) <- x
......@@ -180,20 +180,35 @@ let rec run_disp_basic v f = function
Format.fprintf Format.std_formatter "ERR: %a@." Value.print v;
assert false
(* apply sigma to a value *)
let (@@) v sigma =
if sigma = Value.Identity then v else
match v with
|Value.Pair (v1,v2,Value.Identity) -> Value.Pair (v1,v2,sigma)
|Pair (v1,v2,s) -> Value.Pair (v1,v2,Value.Comp(sigma,s))
|Xml (v1,v2,v3,Value.Identity) -> Value.Xml (v1,v2,v3,sigma)
|Xml (v1,v2,v3,s) -> Xml (v1,v2,v3,Value.Comp(sigma,s))
|XmlNs (v1,v2,v3,a,Value.Identity) -> Value.XmlNs (v1,v2,v3,a,sigma)
|XmlNs (v1,v2,v3,a,s) -> Value.XmlNs (v1,v2,v3,a,Value.Comp(sigma,s))
|Record (r,Value.Identity) -> Value.Record (r,sigma)
|Record (r,s) -> Value.Record (r,Value.Comp(sigma,s))
|Abstraction (iface,t,Value.Identity) -> Value.Abstraction (iface,t,sigma)
|Abstraction (iface,t,s) -> Value.Abstraction (iface,t,Value.Comp(sigma,s))
|_ -> v
let rec run_dispatcher d v =
(* Format.fprintf Format.std_formatter "Matching (%a) with:@." Value.print v;
Patterns.Compile.print_dispatcher Format.std_formatter d; *)
match d.actions with
| AIgnore r -> make_result_basic v r
| AKind k -> run_disp_kind k v
and run_disp_kind actions v =
match v with
| Value.Pair (v1,v2,sigma) -> run_disp_prod v v1 v2 actions.prod
| Value.Pair (v1,v2,sigma) -> run_disp_prod v (v1 @@ sigma) (v2 @@ sigma) 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
| XmlNs (v1,v2,v3,_,sigma) -> run_disp_prod v (v1 @@ sigma) ((Pair (v2,v3,sigma)) @@ sigma) actions.xml
| Record (r,sigma) -> run_disp_record 0 v r actions.record (* XXX !!!! apply sigma here *)
| String_latin1 (i,j,s,q) ->
(* run_disp_kind actions (Value.normalize v) *)
run_disp_string_latin1 i j s q actions
......
open Ident
open Encodings
type sigma = [
| `List of Types.Tallying.CS.sl
| `Comp of (sigma * sigma)
| `Sel of (fv * (Types.t * Types.t) list * sigma) ]
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (t * (Types.t * Types.t) list * sigma)
| Identity
type t =
and t =
| Pair of t * t * sigma
| Xml of t * t * t * sigma
| XmlNs of t * t * t * Ns.table * sigma
......@@ -30,8 +31,6 @@ let dump_forward = ref (fun _ _ -> assert false)
exception CDuceExn of t
let esigma = `List []
let nil = Atom Sequence.nil_atom
let string_latin1 s =
if String.length s = 0 then nil
......@@ -48,7 +47,7 @@ let vbool x = if x then vtrue else vfalse
let vrecord l =
let l = List.map (fun (lab,v) -> Upool.int lab, v) l in
Record (Imap.create (Array.of_list l),esigma)
Record (Imap.create (Array.of_list l),Identity)
let get_fields = function
| Record (map,_) -> Obj.magic (Imap.elements map)
......@@ -56,24 +55,24 @@ let get_fields = function
let rec sequence = function
| [] -> nil
| h::t -> Pair (h, sequence t,esigma)
| h::t -> Pair (h, sequence t,Identity)
let rec sequence_rev accu = function
| [] -> accu
| h::t -> sequence_rev (Pair (h,accu,esigma)) t
| h::t -> sequence_rev (Pair (h,accu,Identity)) t
let sequence_rev l = sequence_rev nil l
let sequence_of_array a =
let rec aux accu i =
if (i = 0) then accu
else let i = pred i in aux (Pair (a.(i), accu,esigma)) i in
else let i = pred i in aux (Pair (a.(i), accu,Identity)) i in
aux nil (Array.length a)
let tuple_of_array a =
let rec aux accu i =
if (i = 0) then accu
else let i = pred i in aux (Pair (a.(i), accu,esigma)) i in
else let i = pred i in aux (Pair (a.(i), accu,Identity)) i in
let n = Array.length a in
aux a.(n) (pred n)
......@@ -83,7 +82,7 @@ let concat v1 v2 =
| (v1,v2) -> Concat (v1,v2)
let append v1 v2 =
concat v1 (Pair (v2,nil,esigma))
concat v1 (Pair (v2,nil,Identity))
let raise' v = raise (CDuceExn v)
let failwith' s = raise' (string_latin1 s)
......@@ -93,12 +92,12 @@ let rec const = function
| Types.Integer i -> Integer i
| Types.Atom a -> Atom a
| Types.Char c -> Char c
| Types.Pair (x,y) -> Pair (const x, const y,esigma)
| Types.Xml (x, Types.Pair (y, z)) -> Xml (const x, const y, const z,esigma)
| Types.Pair (x,y) -> Pair (const x, const y,Identity)
| Types.Xml (x, Types.Pair (y, z)) -> Xml (const x, const y, const z,Identity)
| Types.Xml (_,_) -> assert false
| Types.Record x ->
let x = LabelMap.mapi_to_list (fun l c -> (Upool.int l,const c)) x in
Record (Imap.create (Array.of_list x),esigma)
Record (Imap.create (Array.of_list x),Identity)
| Types.String (i,j,s,c) -> String_utf8 (i,j,s, const c)
let rec inv_const = function
......@@ -126,13 +125,13 @@ let rec inv_const = function
let normalize_string_latin1 i j s q =
if i = j then q else
Pair (Char (Chars.V.mk_char (String.unsafe_get s i)), String_latin1 (succ i,j,s,q),esigma)
Pair (Char (Chars.V.mk_char (String.unsafe_get s i)), String_latin1 (succ i,j,s,q),Identity)
let normalize_string_utf8 i j s q =
if Utf8.equal_index i j then q
else
let (c,i) = Utf8.next s i in
Pair (Char (Chars.V.mk_int c), String_utf8 (i,j,s,q),esigma)
Pair (Char (Chars.V.mk_int c), String_utf8 (i,j,s,q),Identity)
......@@ -176,7 +175,7 @@ let rec flatten = function
| q -> q
let eval_lazy_concat v =
let accu = Obj.magic (Pair (nil,Absent,esigma)) in
let accu = Obj.magic (Pair (nil,Absent,Identity)) in
let rec aux accu = function
| Concat (x,y) -> aux (append_cdr accu x) y
| v -> set_cdr accu v
......@@ -551,9 +550,9 @@ let map_xml map_pcdata map_other =
let tagged_tuple tag vl =
let ct = sequence vl in
let at = Record (Imap.empty,esigma) in
let at = Record (Imap.empty,Identity) in
let tag = Atom (Atoms.V.mk_ascii tag) in
Xml (tag, at, ct,esigma)
Xml (tag, at, ct,Identity)
(** set of values *)
......@@ -626,7 +625,7 @@ let label_ascii s =
Label.mk_ascii s
let record (l : (label * t) list) =
Record (Imap.create (Array.of_list (Obj.magic l)),esigma)
Record (Imap.create (Array.of_list (Obj.magic l)),Identity)
let record_ascii l =
record (List.map (fun (l,v) -> (label_ascii l, v)) l)
......@@ -653,22 +652,20 @@ let mk_rf ~get ~set =
let mk_ref t v =
let r = ref v in
let get = Abstraction (Some [Sequence.nil_type, t], (fun _ -> !r),esigma)
and set = Abstraction (Some [t, Sequence.nil_type], (fun x -> r := x; nil),esigma) in
Record (mk_rf ~get ~set,esigma)
let get = Abstraction (Some [Sequence.nil_type, t], (fun _ -> !r),Identity)
and set = Abstraction (Some [t, Sequence.nil_type], (fun x -> r := x; nil),Identity) in
Record (mk_rf ~get ~set,Identity)
let mk_ext_ref t get set =
let get = Abstraction (
(match t with Some t -> Some [Sequence.nil_type, t] | None -> None),
(fun _ -> get ()),
esigma)
(fun _ -> get ()),Identity)
and set = Abstraction (
(match t with Some t -> Some [t, Sequence.nil_type] | None -> None),
(fun v -> set v; nil),
esigma)
(fun v -> set v; nil),Identity)
in
Record (mk_rf ~get ~set,esigma)
Record (mk_rf ~get ~set,Identity)
let ocaml2cduce_int i =
Integer (Intervals.V.from_int i)
......@@ -737,18 +734,18 @@ let cduce2ocaml_option f v =
let ocaml2cduce_option f = function
| Some x -> Pair (f x, nil,esigma)
| Some x -> Pair (f x, nil,Identity)
| None -> nil
let add v1 v2 = match (v1,v2) with
| (Integer x, Integer y) -> Integer (Intervals.V.add x y)
| (Record (r1,sigma1), Record (r2,sigma2)) -> Record (Imap.merge r1 r2,esigma) (* XXX *)
| (Record (r1,sigma1), Record (r2,sigma2)) -> Record (Imap.merge r1 r2,Identity) (* XXX *)
| _ -> assert false
let merge v1 v2 = match (v1,v2) with
| (Record (r1,sigma1), Record (r2,sigma2)) -> Record (Imap.merge r1 r2,esigma) (* XXX *)
| (Record (r1,sigma1), Record (r2,sigma2)) -> Record (Imap.merge r1 r2,Identity) (* XXX *)
| _ -> assert false
let sub v1 v2 = match (v1,v2) with
......@@ -768,8 +765,8 @@ let modulo v1 v2 = match (v1,v2) with
| _ -> assert false
let pair v1 v2 = Pair (v1,v2,esigma)
let xml v1 v2 v3 = Xml (v1,v2,v3,esigma)
let pair v1 v2 = Pair (v1,v2,Identity)
let xml v1 v2 v3 = Xml (v1,v2,v3,Identity)
let mk_record labels fields =
let l = ref [] in
......@@ -820,7 +817,7 @@ let remove_field l = function
let rec ocaml2cduce_list f = function
| [] -> nil
| hd::tl -> Pair (f hd, ocaml2cduce_list f tl,esigma)
| hd::tl -> Pair (f hd, ocaml2cduce_list f tl,Identity)
let rec cduce2ocaml_list f v =
match normalize v with
......@@ -830,10 +827,10 @@ let rec cduce2ocaml_list f v =
let ocaml2cduce_array f x = ocaml2cduce_list f (Array.to_list x)
let cduce2ocaml_array f x = Array.of_list (cduce2ocaml_list f x)
let no_attr = Record (Imap.empty,esigma)
let no_attr = Record (Imap.empty,Identity)
let ocaml2cduce_constr tag va =
Xml (tag, no_attr, sequence_of_array va,esigma)
Xml (tag, no_attr, sequence_of_array va,Identity)
let rec cduce2ocaml_constr m = function
| Atom q ->
......@@ -856,17 +853,16 @@ let rec cduce2ocaml_variant m = function
let ocaml2cduce_fun farg fres f =
Abstraction (None, (fun x -> fres (f (farg x))),esigma)
Abstraction (None, (fun x -> fres (f (farg x))),Identity)
let cduce2ocaml_fun farg fres = function
| Abstraction (_, f,sigma) -> (fun x -> fres (f (farg x)))
| Abstraction (_,f,_) -> (fun x -> fres (f (farg x)))
| _ -> assert false
let apply f arg = match f with
| Abstraction (_,f,_) -> f arg
| _ -> assert false
type pools = Ns.Uri.value array * Ns.Label.value array
let extract_all () =
......
open Ident
open Encodings
type sigma = [
| `List of Types.Tallying.CS.sl
| `Comp of (sigma * sigma)
| `Sel of (fv * (Types.t * Types.t) list * sigma) ]
type sigma =
| List of Types.Tallying.CS.sl
| Comp of (sigma * sigma)
| Sel of (t * (Types.t * Types.t) list * sigma)
| Identity
val esigma : sigma
type t =
and t =
(* Canonical representation *)
| Pair of t * t * sigma
| Xml of t * t * t * sigma
......
......@@ -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.esigma)
Value.Xml (Value.Atom qname, attrs, content, Value.Identity)
let peek ctx =
......@@ -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.esigma)
Value.Xml (Value.Atom start_tag, attrs, content,Value.Identity)
(*
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,Value.esigma)) in
let stream = stream_of_value (Value.Xml (foo_atom, empty_record, value,Value.Identity)) in
Stream.junk stream;
let ctx = ctx stream in
validate_model_group ctx mg;
......
......@@ -179,11 +179,12 @@ let rec pp_sigma ppf =
) ppf
in
function
|`List ll -> Types.Tallying.CS.pp_sl ppf ll
|`Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|`Sel(x,tl,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_fv x pp_aux tl pp_sigma s
|Value.List ll -> Types.Tallying.CS.pp_sl ppf ll
|Value.Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Value.Sel(x,tl,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_value x pp_aux tl pp_sigma s
|Value.Identity -> Format.fprintf ppf "Id"
let rec pp_value ppf = function
and pp_value ppf = function
| Value.Pair(v1, v2, sigma) ->
Format.fprintf ppf "(%a, %a, %a)"
pp_value v1
......@@ -210,13 +211,26 @@ let rec pp_value ppf = function
pp_value v2
| Absent -> Format.fprintf ppf "Absent"
let rec pp_lambda ppf =
let rec pp_lambda_sigma ppf =
let pp_aux ppf =
print_lst (fun ppf (t1,t2) ->
Format.fprintf ppf "(%a -> %a)"
Types.Print.print t1
Types.Print.print t2
) ppf
in
function
|Lambda.List ll -> Types.Tallying.CS.pp_sl ppf ll