lambdajs.ds

module trans/lambdajs

imports
  src-gen/ds-signatures/lambdaJS-sig

signature
	sorts
		V

	constructors
		ObjV : Map(V,V) -> V
		StrV : String -> V
		NumV : INT -> V
		BoolV : BOOLEAN -> V
		UndefV : V
		NullV : V
		ProtoV : V
		LocV : Int -> V
		LocWrap : V -> Exp
		ObjWrap : V -> Exp
		ClosV : List(String) * Exp * Env -> V 
		
	native operators
		printV: V -> V

	sort aliases
		Address = Int
		Env = Map(String, V)
		Heap = Map(Address, V)
		Global = Map(String, Address)

	components
		E : Env
		O : Map(V,V)
		H : Heap
		G : Global
		
	variables
	    v : V
  
  	arrows
		bindVar(String, V) --> Env
		readVar(String) --> V
		
		bindProperty(V, V) --> Map(V,V)
		removeProperty(V) --> Map(V,V)
		getProperty(V) --> V
		
		bindGlobal(String, Address) --> Global
		readGlobal(String) --> Address
		
		bindFuncArgs(List(String), List(Exp)) --> Env
		
		setRef(Address, V) --> Heap
		
		listToObj(List(Field)) --> Map(V,V)
		
		evaluate(List(Exp), List(V)) --> List(V)
		
		Start -init-> List(V)
		Exp --> V
		Val --> V
		Field --> V

	rules
		//Not in the paper, but necessary to give output for tests
		Print(e) --> printV(e)
	
		O |- bindProperty(v1, v2) --> {v1 |--> v2, O}	
		O |- removeProperty(strv) --> O \ strv
		O |- getProperty(strv) --> O[strv]

		E |- bindVar(name, v) --> {name |--> v, E}
		E |- readVar(name) --> E[name]
		
		E |- bindFuncArgs([], []) --> E
		E |- bindFuncArgs([arg | args], [e | exps]) --> E3
		where
			E |- e --> v;
			E |- bindVar(arg, v) --> E2;
			E E2 |- bindFuncArgs(args, exps) --> E3
		
		bindGlobal(name, addr) :: G --> {name |--> addr, G}
		readGlobal(name) :: G --> G[name]
		
		setRef(addr, v) :: H --> {addr |--> v, H}
		
		//dirty way of passing values as expressions
		LocWrap(LocV(addr)) --> LocV(addr)
		ObjWrap(ObjV(o)) --> ObjV(o)
		
		Program(e) -init-> vals
		where
			evaluate(e, []) :: G {}, H {} --> vals
			
		evaluate([], vals) --> vals
		
		evaluate([e | exps], vals) --> newVals
		where
			E {} |- e --> v;
			evaluate(exps, vals ++ [v]) --> newVals
			
		Value(e) --> val
		where
			e --> val
		
		INT(i) --> NumV(i)
		
		BOOLEAN(i) --> BoolV(i)
		
		UNDEFINED(_) --> UndefV()
		
		NULL(_) --> NullV()
		
		Proto(_) --> ProtoV()
		
		STRING(i) --> StrV(i)
		
		E |- Identifier(name) :: G, H --> v
		where
			case E[name?] of {
				true =>
					E |- readVar(name) --> v
				false =>
					readGlobal(name) :: G --> addr;
					H[addr] => v
			}
		
		Obj(propList) --> ObjV(obj)
		where
			{} => O;
			O |- listToObj(propList) --> obj
		
		Prop(name, _) --> StrV(name)
		
		O |- listToObj([]) --> O
			
		O |- listToObj([Prop(name, val) | listRest]) --> obj2
		where
			Prop(name, val) --> v1;
			val --> v2;
			O |- bindProperty(v1,v2) --> O2;
			O2 |- listToObj(listRest) --> obj2
		
		//Special case for proto property in object
		O |- listToObj([PropProto(_, val) | listRest]) --> obj2
		where
			val --> v;
			case v of{
				LocV(_) =>
					O |- bindProperty(ProtoV(),v) --> O2;
					O2 |- listToObj(listRest) --> obj2
				NullV() =>
					O |- bindProperty(ProtoV(),v) --> O2;
					O2 |- listToObj(listRest) --> obj2
			}
			
		E |- Func(args, e) --> ClosV(args, e, E)
		
		//Special case where explicitly a get is done for proto, 
		//which will return a LocV or UndefV instead of a normal value
		Get(e1, e2) --> vout
		where
			e1 --> ObjV(O);
			e2 --> ProtoV();
			case O[ProtoV()?] of {
				true =>
					O |- getProperty(ProtoV()) --> v;
					case v of {
						NullV() =>
							UndefV() => vout
						LocV(addr) =>
							LocV(addr) => vout
					}		
				false =>
					UndefV() => vout
			}

		//Fig.1 E-GETFIELD, Fig.4 E-GETFIELD-NOTFOUND, E-GETFIELD-PROTO, E-GETFIELD-PROTO-NULL
		Get(e1, e2) --> vout
		where
			e1 --> ObjV(O);
			e2 --> StrV(str);
			case O[StrV(str)?] of {
				true =>
					O |- getProperty(StrV(str)) --> vout		
				false =>
					case O[ProtoV()?] of {
						true =>
							O |- getProperty(ProtoV()) --> v;
							case v of {
								NullV() =>
									UndefV() => vout
								LocV(addr) =>
									Deref(LocWrap(LocV(addr))) --> obj;
									Get(ObjWrap(obj), e2) --> vout
							}
						false =>
							UndefV() => vout
					}
			}
		
		//Fig.1 E-UPDATEFIELD, E-CREATEFIELD
		Instantiation(e1, e2, e3) :: G, H --> ObjV(obj2) :: G, H''''
		where
			e1 :: H --> ObjV(O) ::H';
			e2 :: H' --> v1 :: H'';
			e3 :: H'' --> v2 :: H''';
			case v1 of {
				ProtoV() =>
					O |- bindProperty(v1, v2) --> obj2
				StrV(_) =>
					O |- bindProperty(v1, v2) --> obj2
			};
			case e1 of {
				Identifier(id) =>
					case G[id?] of {
						true =>
							readGlobal(id) --> addr;
							setRef(addr, ObjV(obj2)) :: H''' --> H''''
						false =>
							H''' => H''''
					}
				otherwise =>
					H''' => H''''
			}
		
		//Fig.1 E-DELETEFIELD, E-DELETEFIELD-NOTFOUND
		Delete(e1, e2) :: G, H --> ObjV(obj2) :: G, H'''
		where
			e1 :: H --> ObjV(O) :: H';
			e2 :: H' --> StrV(str) :: H'';
			case O[StrV(str)?] of {
				true =>
					O |- removeProperty(StrV(str)) --> obj2		
				false =>
					O => obj2	
			};
			case e1 of {
				Identifier(id) =>
					case G[id?] of {
						true =>
							readGlobal(id) --> addr;
							setRef(addr, ObjV(obj2)) :: H'' --> H'''
						false =>
							H'' => H'''
					}
				otherwise =>
					H'' => H'''
			}
	
		//Fig.1 E-LET
		Let(x, e1, e2) --> v2
  		where
  			e1 --> v1;
  			bindVar(x, v1) --> E2;
			E E2|- e2 --> v2
			
		//Fig.1 E-APP
		E |- App(e, exps) --> v
		where
			e --> ClosV(args, ret, E2);
			E {E, E2} |- bindFuncArgs(args, exps) --> E3;
			E3 |- ret --> v
	
		//Fig.2 E-SETREF
		Assign(id, exp) :: G, H --> v :: G', H {addr |--> v, H'}
		where
			case G[id?] of {
				true =>
					readGlobal(id) :: G --> addr;
					G => G'	
				false =>
					fresh => addr;
					bindGlobal(id, addr) :: G --> G'
			};
			exp :: H --> v :: H'
		
		//Fig.2 E-REF
		Ref(exp) :: H --> LocV(addr) :: H {addr |--> ObjV(o), H'}
		where
			exp :: H --> ObjV(o) :: H';
			fresh => addr
		
		//Fig.2 E-DEREF
		Deref(exp) :: H --> v :: H'
		where
			exp :: H --> LocV(addr) :: H';
			H'[addr] => v