search

metaborg / dynsem

DynSem
Apache License 2.0
12 stars 4 forks source link

Error in DynSem core: (Variable _lifted_L_Int_M121 cannot be resolved) #134

Closed milosonator closed 7 years ago

milosonator commented 7 years ago

There are static errors in my explicated DynSem core, It's very hard to make a small example to replicate the problem on a small scale.

Runtime error is: Exception in thread "main" org.metaborg.meta.lang.dynsem.interpreter.nodes.rules.ReductionFailure: Accessed null value for slot _lifted_L_Int_O141

The problem has to do with the case switch inside the rule ObjectL(inherit, [ ], code) . It makes up some variables for semantic components that don't point anywhere. I thought the 'lifted_...' was something of the past.

Please look into this.

module semantics/trans/semantics_varschemes_typeannos_noaliases_factorized_explimpl_factorized_explicated2_copyprop_unfactorized_unfactorized

imports 

signature
    sorts
      call__Meta
      addMember__Meta
      addMembers__Meta
      createLocals__Meta
      wrapValues__Meta
      Program
      Statement
      Assignment
      VarInit
      Declaration
      Use
      MethodName
      Prefix
      Identifier
      Annotations
      Annotation
      Params
      Param
      MethodBody
      Exp
      Part
      CallArgs
      OperatorCF
      Inherit
      Alias
      Exclude
      Boolean
      Lineup
      Block
      BlockParams
      Declaration
      Assignment
      Exp
      V
      O
      M
      Unit
      Table
      readObject__Meta
      allocateObject__Meta
      writeObject__Meta
      readMethod__Meta
      allocateMethod__Meta
      writeMethod__Meta
      writeLocal__Meta
      readLocal__Meta
      lookup__Meta
      lookupInOuter__Meta
      memberTable__Meta
      Context
      Self
      Outer
      Phase
    constructors
      call : M * List(V) -> call__Meta {meta-function}
      addMember : String * List(String) * List(Statement) -> addMember__Meta {meta-function}
      addMembers : List(String) * List(List(Statement)) -> addMembers__Meta {meta-function}
      createLocals : List(String) * List(List(Statement)) -> createLocals__Meta {meta-function}
      wrapValues : List(V) -> wrapValues__Meta {meta-function}
      WrappedP : Phase -> V 
      Program : List(Statement) * String -> Program 
      Dialect : String -> Statement 
      Import : String * String -> Statement 
      Assignment : Assignment -> Statement 
      Declaration : Declaration -> Statement 
      Expression : Exp -> Statement 
      Assignment : String * Exp -> Assignment 
      VarInit : Exp -> VarInit 
      NoVarInit : VarInit 
      Constant : String * Annotations * Exp -> Declaration 
      Variable : String * Annotations * VarInit -> Declaration 
      MethodDecl : Prefix * List(MethodName) * Annotations * MethodBody -> Declaration 
      ClassDecl : List(MethodName) * Inherit * List(Use) * List(Statement) -> Declaration 
      TraitDecl : List(MethodName) * MethodBody -> Declaration 
      Use : Exp * Alias * Exclude -> Use 
      MethodID : Identifier * Params -> MethodName 
      MethodOp : OperatorCF * Params -> MethodName 
      Prefix : Prefix 
      NoPrefix : Prefix 
      ID : String -> Identifier 
      Annotations : List(Annotation) -> Annotations 
      NoAnnotations : Annotations 
      Public : Annotation 
      Readable : Annotation 
      Writeable : Annotation 
      Confidential : Annotation 
      Manifest : Annotation 
      Overrides : Annotation 
      Params : List(Param) -> Params 
      NoParams : Params 
      Param : String -> Param 
      MethodBody : List(Statement) -> MethodBody 
      ObjectDecl : Inherit * List(Use) * List(Statement) -> Exp 
      Number : String -> Exp 
      String : String -> Exp 
      Boolean : Boolean -> Exp 
      Self : Exp 
      Outer : Exp 
      PlaceHolder : Exp 
      MCallOpEx : Exp * OperatorCF * Exp -> Exp 
      MCallWDot : Exp * List(Part) -> Exp 
      MCallImpl : List(Part) -> Exp 
      MCallPrefixOp : OperatorCF * CallArgs -> Exp 
      MCallPrefixOpExp : OperatorCF * Exp -> Exp 
      LineupExp : Lineup -> Exp 
      Ellipsis : Exp 
      BlockExp : Block -> Exp 
      Return : Exp -> Exp 
      Part : Identifier * CallArgs -> Part 
      ArgsParen : List(Exp) -> CallArgs 
      NoArgs : CallArgs 
      ArgBlock : Block -> CallArgs 
      ArgNumber : String -> CallArgs 
      ArgString : String -> CallArgs 
      ArgLineup : Lineup -> CallArgs 
      ArgBoolean : Boolean -> CallArgs 
      OperatorCF : String -> OperatorCF 
      Inherit : Exp * Alias * Exclude -> Inherit 
      NoInherit : Inherit 
      Alias : String * String -> Alias 
      NoAlias : Alias 
      Exclude : List(String) -> Exclude 
      NoExclude : Exclude 
      True : Boolean 
      False : Boolean 
      Lineup : List(Exp) -> Lineup 
      Block : List(Statement) -> Block 
      BlockWParams : BlockParams * List(Statement) -> Block 
      BlockParams : List(Param) -> BlockParams 
      MCallL : String * List(Exp) -> Exp 
      MCallRecvL : Exp * String * List(Exp) -> Exp 
      ObjectL : Inherit * List(Use) * List(Statement) -> Exp 
      MethodL : String * Annotations * List(String) * List(Statement) -> Declaration 
      ConstantL : String * Annotations * Exp -> Declaration 
      VariableL : String * Annotations -> Declaration 
      TraitL : String * List(String) * List(Statement) -> Declaration 
      AssignmentL : String * Exp -> Assignment 
      NumL : String -> Exp 
      NumV : Int -> V 
      StringV : String -> V 
      BoolV : Bool -> V 
      ObjectRef : Int -> V 
      Done : V 
      Error : V 
      Uninitialized : V 
      Object : Int * Map(String,Int) -> O 
      Method : List(String) * List(Statement) * Int -> M 
      Code : V -> Statement 
      Unit : Unit 
      NoObject : O 
      NoMethod : String -> M 
      NoMethodAndStop : String -> M 
      WrappedO : O -> V 
      WrappedM : M -> V 
      WrappedLS : List(Statement) -> V 
      WrappedLCS : List(List(Statement)) -> V 
      WrappedMembers : Map(String,Int) -> V 
      Stored : O -> V 
      readObject : Int -> readObject__Meta {meta-function}
      allocateObject : O -> allocateObject__Meta {meta-function}
      writeObject : Int * O -> writeObject__Meta {meta-function}
      readMethod : Int -> readMethod__Meta {meta-function}
      allocateMethod : M -> allocateMethod__Meta {meta-function}
      writeMethod : Int * M -> writeMethod__Meta {meta-function}
      writeLocal : String * V -> writeLocal__Meta {meta-function}
      readLocal : String -> readLocal__Meta {meta-function}
      WrappedL : Map(String,V) -> V 
      WrappedOHeap : Map(Int,O) -> V 
      WrappedMHeap : Map(Int,M) -> V 
      lookup : String -> lookup__Meta {meta-function}
      lookupInOuter : String -> lookupInOuter__Meta {meta-function}
      memberTable : Int -> memberTable__Meta {meta-function}
      ObjectC : Context 
      MethodC : Context 
      BlockC : Context 
      Self : Int -> Self 
      Exec : Phase 
      Build : Phase 
      Init : Phase 
    native constructors
    native operators
      nativeIBinOp : String * Int * Int -> Int
      nativePrint : V -> V
      nativeEq : V * V -> Bool
      nativeMinus : V * V -> Int
      nativePlus : V * V -> Int
      nativeLte : V * V -> Bool
      parseNumber : String -> Int
      print : V -> V
      error : String -> String
      error : String * String -> String
      error : String * String * String -> String
      debug : String -> String
      debug : String * String -> String
      debug : String * String * String -> String
    arrows
       Program  -init-> V 
      S, P, C |- Program :: OH, MH, L -default-> V :: OH, MH, L
      S, P, C |- List(Statement) :: OH, MH, L -default-> V :: OH, MH, L
       List(Statement)  -selectDecls-> List(Statement) 
       List(Statement)  -selectStmts-> List(Statement) 
      S, P, C |- Exp :: OH, MH, L -default-> V :: OH, MH, L
      S, P, C |- Statement :: OH, MH, L -default-> V :: OH, MH, L
      S, P, C |- Declaration :: OH, MH, L -default-> V :: OH, MH, L
      S, P, C |- Assignment :: OH, MH, L -default-> V :: OH, MH, L
      S, P, C |- Inherit :: OH, MH, L -default-> Int :: OH, MH, L
      S, P, C |- List(Exp) :: OH, MH, L -ea-> List(V) :: OH, MH, L
      S, P, C |- call__Meta :: OH, MH, L -default-> V :: OH, MH, L
      S |- addMember__Meta :: OH, MH -default-> Unit :: OH, MH
      S |- addMembers__Meta :: OH, MH -default-> Unit :: OH, MH
      S, P, C |- createLocals__Meta :: OH, MH, L -default-> Unit :: OH, MH, L
       wrapValues__Meta  -default-> List(List(Statement)) 
       readObject__Meta :: OH -default-> O :: OH
       allocateObject__Meta :: OH -default-> Int :: OH
       writeObject__Meta :: OH -default-> O :: OH
       readMethod__Meta :: MH -default-> M :: MH
       allocateMethod__Meta :: MH -default-> Int :: MH
       writeMethod__Meta :: MH -default-> M :: MH
       writeLocal__Meta :: L -default-> V :: L
       readLocal__Meta :: L -default-> V :: L
      S, C |- lookup__Meta :: OH, MH, L -default-> M :: OH, MH, L
      S |- lookupInOuter__Meta :: OH, MH -default-> M :: OH, MH
       memberTable__Meta :: OH -default-> Map(String,Int) :: OH
    native datatypes
    components
      OH : Map(Int,O)
      MH : Map(Int,M)
      L : Map(String,V)
      C : Context
      S : Self
      P : Phase
    variables
      v : V
      vs : List(V)
      o : O
      m : M
      r : Int

rules

  writeObject(addr, o1) :: OH OH1 -default-> o1 :: OH {addr |--> o1} + OH1.

  writeMethod(addr, m1) :: MH MH1 -default-> m1 :: MH {addr |--> m1} + MH1.

  writeLocal(name, v1) :: L L1 -default-> v1 :: L {name |--> v1} + L1.

  wrapValues([  ]) -default-> [  ] : List(List(Statement)).

  wrapValues([ v1 | vs1 ]) -default-> [ [ Code(v1) | [  ] ] | wvs ]
  where
    wrapValues(vs1) -default-> wvs.

  S _, P _, C MethodC() |- VariableL(name, _) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH1, MH MH1, L L2
  where
    writeLocal(name, Uninitialized()) :: L L1 -default-> _ :: L L2.

  S _, P _, C _ |- VariableL(_, _) :: OH OH1, MH MH1, L L1 -default-> Error() :: OH OH1, MH MH1, L L1
  where
    error("Variables outside methods not implemented") => _.

  S _, P _, C _ |- String(s) :: OH OH1, MH MH1, L L1 -default-> StringV(s) :: OH OH1, MH MH1, L L1.

  S Self(self), P _, C _ |- Self() :: OH OH1, MH MH1, L L1 -default-> ObjectRef(self) :: OH OH1, MH MH1, L L1.

  readObject(addr) :: OH OH1 -default-> OH1[addr] :: OH OH1.

  readMethod(addr) :: MH MH1 -default-> MH1[addr] :: MH MH1.

  readLocal(name) :: L L1 -default-> L1[name] :: L L1.

  S _, P P1, C _ |- Program(code, _) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH3, MH MH2, L L2
  where
    allocateObject(NoObject()) :: OH OH1 -default-> noObj :: OH OH2;
    S Self(noObj), P P1, C ObjectC() |- code :: OH OH2, MH MH1, L L1 -default-> v1 :: OH OH3, MH MH2, L L2.

  S Self(self), P _, C _ |- Outer() :: OH OH1, MH MH1, L L1 -default-> ObjectRef(outer) :: OH OH2, MH MH1, L L1
  where
    readObject(self) :: OH OH1 -default-> Object(outer, _) :: OH OH2.

  S Self(selfRef), P Exec(), C _ |- ObjectL(NoInherit(), [  ], code) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(newSelf) :: OH OH4, MH MH3, L L3
  where
    allocateObject(Object(selfRef, {})) :: OH OH1 -default-> newSelf :: OH OH2;
    code -selectDecls-> decls;
    S Self(newSelf), P Build(), C ObjectC() |- decls :: OH OH2, MH MH1, L L1 -default-> _ :: OH OH3, MH MH2, L L2;
    code -selectStmts-> stmts;
    S Self(newSelf), P Exec(), C ObjectC() |- stmts :: OH OH3, MH MH2, L L2 -default-> _ :: OH OH4, MH MH3, L L3.

  S Self(selfRef), P Exec(), C C1 |- ObjectL(inherit, [  ], code) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(newSelf) :: OH OH7, MH MH6, L L6
  where
    allocateObject(Object(selfRef, {})) :: OH OH1 -default-> newSelf :: OH OH2;
    code -selectDecls-> decls;
    S Self(newSelf), P Build(), C ObjectC() |- decls :: OH OH2, MH MH1, L L1 -default-> _ :: OH OH3, MH MH2, L L2;
    case inherit of {
      NoInherit() =>
        OH3 => OH4;
        MH2 => MH3;
        L2 => L3
      i@Inherit(_, _, _) =>
        S Self(newSelf), P Build(), C C1 |- i :: OH OH3, MH MH2, L L2 -default-> _ :: OH OH5, MH MH4, L L4;
        S Self(newSelf), P Init(), C C1 |- i :: OH OH5, MH MH4, L L4 -default-> _ :: OH OH6, MH MH5, L L5
    };
    code -selectStmts-> stmts;
    S Self(newSelf), P Exec(), C ObjectC() |- stmts :: OH _lifted_L_Int_O141, MH _lifted_L_Int_M121, L _lifted_L_String_V102 -default-> _ :: OH OH7, MH MH6, L L6.

  S S1, P Build(), C _ |- ObjectL(NoInherit(), [  ], code) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(selfRef) :: OH OH2, MH MH2, L L2
  where
    S1 => Self(selfRef);
    debug("object constructor in build mode, NoInherit") => _;
    code -selectDecls-> decls;
    S S1, P Build(), C ObjectC() |- decls :: OH OH1, MH MH1, L L1 -default-> _ :: OH OH2, MH MH2, L L2.

  S S1, P P1, C C1 |- ObjectL(inherit, [  ], code) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(selfRef) :: OH OH3, MH MH3, L L3
  where
    S1 => Self(selfRef);
    P1 => Build();
    debug("object constructor in build mode, Inherit") => _;
    S S1, P P1, C C1 |- inherit :: OH OH1, MH MH1, L L1 -default-> _ :: OH OH2, MH MH2, L L2;
    code -selectDecls-> decls;
    S S1, P Build(), C ObjectC() |- decls :: OH OH2, MH MH2, L L2 -default-> _ :: OH OH3, MH MH3, L L3.

  S S1, P Init(), C _ |- ObjectL(NoInherit(), [  ], code) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(selfRef) :: OH OH2, MH MH2, L L2
  where
    S1 => Self(selfRef);
    debug("object constructor in init mode, NoInherit") => _;
    code -selectStmts-> stmts;
    S S1, P Exec(), C ObjectC() |- stmts :: OH OH1, MH MH1, L L1 -default-> _ :: OH OH2, MH MH2, L L2.

  S S1, P P1, C C1 |- ObjectL(inherit, [  ], code) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(selfRef) :: OH OH3, MH MH3, L L3
  where
    S1 => Self(selfRef);
    P1 => Init();
    debug("object constructor in init mode, Inherit") => _;
    S S1, P P1, C C1 |- inherit :: OH OH1, MH MH1, L L1 -default-> _ :: OH OH2, MH MH2, L L2;
    code -selectStmts-> stmts;
    S S1, P Exec(), C ObjectC() |- stmts :: OH OH2, MH MH2, L L2 -default-> _ :: OH OH3, MH MH3, L L3.

  S _, P _, C _ |- ObjectL(_, _, _) :: OH OH1, MH MH1, L L1 -default-> ObjectRef(r1) :: OH OH2, MH MH1, L L1
  where
    error("No valid object constructor.") => _;
    allocateObject(NoObject()) :: OH OH1 -default-> r1 :: OH OH2.

  S _, P _, C _ |- NumL(s) :: OH OH1, MH MH1, L L1 -default-> NumV(parseNumber(s)) :: OH OH1, MH MH1, L L1.

  S _, P _, C _ |- NoInherit() :: OH OH1, MH MH1, L L1 -default-> r1 :: OH OH2, MH MH1, L L1
  where
    allocateObject(NoObject()) :: OH OH1 -default-> r1 :: OH OH2.

  S S1, P _, C ObjectC() |- MethodL(name, _, params, code) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH2, MH MH2, L L1
  where
    S S1 |- addMember(name, params, code) :: OH OH1, MH MH1 -default-> _ :: OH OH2, MH MH2.

  S _, P _, C MethodC() |- MethodL(name, _, _, _) :: OH OH1, MH MH1, L L1 -default-> Error() :: OH OH1, MH MH1, L L1
  where
    error("Error: cannot create method: '", name, "' inside a methodContext") => _.

  memberTable(r1) :: OH OH1 -default-> tbl :: OH OH2
  where
    readObject(r1) :: OH OH1 -default-> Object(_, tbl) :: OH OH2.

  memberTable(r1) :: OH OH1 -default-> {} :: OH OH2
  where
    readObject(r1) :: OH OH1 -default-> NoObject() :: OH OH2;
    debug("this object has no table entries because it does not exist") => _.

  S S1, P P1, C C1 |- MCallRecvL(receiver, name, args) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH5, MH MH5, L L5
  where
    S S1, P P1, C C1 |- receiver :: OH OH1, MH MH1, L L1 -default-> ObjectRef(r1) :: OH OH2, MH MH2, L L2;
    S Self(r1), C C1 |- lookup(name) :: OH OH2, MH MH2, L L2 -default-> m1 :: OH OH3, MH MH3, L L3;
    S S1, P P1, C C1 |- args :: OH OH3, MH MH3, L L3 -ea-> vs1 :: OH OH4, MH MH4, L L4;
    S Self(r1), P P1, C C1 |- call(m1, vs1) :: OH OH4, MH MH4, L L4 -default-> v1 :: OH OH5, MH MH5, L L5.

  S S1, P p, C C1 |- MCallL("print", [ e1 | [  ] ]) :: OH OH1, MH MH1, L L1 -default-> nativePrint(v1) :: OH OH2, MH MH2, L L2
  where
    S S1, P p, C C1 |- e1 :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2;
    S1 => Self(s);
    debug("printing from self: ") => _;
    print(NumV(s)) => _;
    print(WrappedP(p)) => _.

  S S1, P P1, C C1 |- MCallL(name, l1) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH4, MH MH4, L L4
  where
    S S1, P P1, C C1 |- l1 :: OH OH1, MH MH1, L L1 -ea-> vs1 :: OH OH2, MH MH2, L L2;
    debug("generic implicit call of: '", name, "'") => _;
    S S1, C C1 |- lookup(name) :: OH OH2, MH MH2, L L2 -default-> m1 :: OH OH3, MH MH3, L L3;
    S S1, P P1, C C1 |- call(m1, vs1) :: OH OH3, MH MH3, L L3 -default-> v1 :: OH OH4, MH MH4, L L4;
    debug("done generic implicit call of: '", name, "'") => _.

  S Self(self) |- lookupInOuter(name) :: OH OH1, MH MH1 -default-> m :: OH OH4, MH MH2
  where
    debug("looking in outer slots for: '", name, "'") => _;
    print(NumV(self)) => _;
    readObject(self) :: OH OH1 -default-> Object(outer, _) :: OH OH2;
    print(NumV(outer)) => _;
    readObject(outer) :: OH OH2 -default-> Object(_, tbl) :: OH OH3;
    debug("looking in outer (this object has an outer)") => _;
    debug("gotten outer") => _;
    print(NumV(outer)) => _;
    print(WrappedMembers(tbl)) => _;
    case tbl[name?] of {
      true =>
        readMethod(tbl[name]) :: MH MH1 -default-> m : M :: MH MH2;
        OH3 => OH4
      otherwise =>
        S Self(outer) |- lookupInOuter(name) :: OH OH3, MH MH1 -default-> m : M :: OH OH4, MH MH2
    }.

  S _ |- lookupInOuter(name) :: OH OH1, MH MH1 -default-> NoMethod(name) :: OH OH1, MH MH1.

  S Self(self) |- lookupInOuter(name) :: OH OH1, MH MH1 -default-> NoMethod(name) :: OH OH3, MH MH1
  where
    readObject(self) :: OH OH1 -default-> Object(outer, _) :: OH OH2;
    readObject(outer) :: OH OH2 -default-> NoObject() :: OH OH3;
    debug("looking in outer (this object has no outer)") => _.

  S Self(self), C MethodC() |- lookup(name) :: OH OH1, MH MH1, L L -default-> m :: OH OH2, MH MH2, L L1
  where
    debug("lookup in method context for: '", name, "'") => _;
    case L[name?] of {
      true =>
        Method([  ] : List(String), [ Code(L[name]) | [  ] : List(Statement) ], self) => m : M;
        OH1 => OH2;
        MH1 => MH2;
        L => L1
      otherwise =>
        true == false;
        OH1 => OH2;
        MH1 => MH2;
        L => L1
    }.

  S S1, C _ |- lookup(name) :: OH OH1, MH MH1, L L1 -default-> m :: OH OH3, MH MH2, L L2
  where
    S1 => Self(self);
    debug("looking in self slots (non-method context) for: '", name, "'") => _;
    print(NumV(self)) => _;
    memberTable(self) :: OH OH1 -default-> tbl :: OH OH2;
    print(WrappedMembers(tbl)) => _;
    case tbl[name?] of {
      true =>
        readMethod(tbl[name]) :: MH MH1 -default-> m : M :: MH MH2;
        OH2 => OH3;
        L1 => L2
      otherwise =>
        debug("no such method: '", name, "' in this object") => _;
        S S1 |- lookupInOuter(name) :: OH OH2, MH MH1 -default-> m : M :: OH OH3, MH MH2;
        L1 => L2
    }.

  S S1, P P1, C C1 |- Inherit(e, _, _) :: OH OH1, MH MH1, L L1 -default-> r1 :: OH OH2, MH MH2, L L2
  where
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> ObjectRef(r1) :: OH OH2, MH MH2, L L2.

  S S1, P P1, C C1 |- Expression(e) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2
  where
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2.

  S _, P _, C _ |- Ellipsis() :: OH OH1, MH MH1, L L1 -default-> Error() :: OH OH1, MH MH1, L L1
  where
    error("Attempt to evaluate ellipsis (...)") => _.

  S S1, P P1, C C1 |- Declaration(e) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2
  where
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2.

  S S1, P P1, C C1 |- createLocals([ n | ns ], [ code | codes ]) :: OH OH1, MH MH1, L L1 -default-> Unit() :: OH OH3, MH MH3, L L4
  where
    S S1, P P1, C C1 |- code :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2;
    writeLocal(n, v1) :: L L2 -default-> _ :: L L3;
    S S1, P P1, C C1 |- createLocals(ns, codes) :: OH OH2, MH MH2, L L3 -default-> _ :: OH OH3, MH MH3, L L4.

  S _, P _, C _ |- createLocals([  ], [  ]) :: OH OH1, MH MH1, L L1 -default-> Unit() :: OH OH1, MH MH1, L L1.

  S S1, P P1, C C1 |- ConstantL(name, _, e) :: OH OH1, MH MH1, L L -default-> Done() :: OH OH2, MH MH2, L L1
  where
    C1 => MethodC();
    debug("adding local: ", name) => _;
    case L[name?] of {
      true =>
        error("Cannot rebind to constant") => _;
        error("Cannot rebind to constant: '", name, "' ") => _;
        OH1 => OH2;
        MH1 => MH2;
        L => L1
      otherwise =>
        S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L -default-> v : V :: OH OH2, MH MH2, L L2;
        writeLocal(name, v) :: L L2 -default-> _ :: L L1
    }.

  S S1, P P1, C C1 |- ConstantL(name, _, e) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH3, MH MH3, L L2
  where
    C1 => ObjectC();
    debug("adding member: ", name) => _;
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2;
    S S1 |- addMember(name, [  ] : List(String), [ Code(v1) | [  ] : List(Statement) ]) :: OH OH2, MH MH2 -default-> _ :: OH OH3, MH MH3.

  S S1, P Build(), C _ |- ConstantL(name, _, _) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH2, MH MH2, L L1
  where
    debug("__BUILD__adding member: ", name) => _;
    S S1 |- addMember(name, [  ] : List(String), [ Code(Uninitialized()) | [  ] : List(Statement) ]) :: OH OH1, MH MH1 -default-> _ :: OH OH2, MH MH2.

  S S1, P P1, C C1 |- ConstantL(name, _, e) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH3, MH MH3, L L2
  where
    P1 => Init();
    debug("__INIT__ adding member: ", name) => _;
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2;
    S S1 |- addMember(name, [  ] : List(String), [ Code(v1) | [  ] : List(Statement) ]) :: OH OH2, MH MH2 -default-> _ :: OH OH3, MH MH3.

  S _, P _, C _ |- ConstantL(_, _, _) :: OH OH1, MH MH1, L L1 -default-> Error() :: OH OH1, MH MH1, L L1
  where
    error("Error: unknown context for constant") => _.

  S _, P _, C _ |- Code(v1) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH1, MH MH1, L L1.

  S _, P _, C _ |- call(NoMethod(name), _) :: OH OH1, MH MH1, L L1 -default-> Error() :: OH OH1, MH MH1, L L1
  where
    error("Message not understood: '", name, "'") => _.

  S _, P P1, C _ |- call(Method([  ], code, scope), [  ]) :: OH OH1, MH MH1, L L -default-> v1 :: OH OH2, MH MH2, L L
  where
    debug("calling method with no args") => _;
    S Self(scope), P P1, C MethodC() |- code :: OH OH1, MH MH1, L {} -default-> v1 :: OH OH2, MH MH2, L _.

  S S1, P P1, C C1 |- call(Method(l1, code, scope), vs1) :: OH OH1, MH MH1, L L -default-> v1 :: OH OH3, MH MH3, L L
  where
    l1 => [ _ | _ ];
    vs1 => [ _ | _ ];
    debug("calling method with some args") => _;
    wrapValues(vs1) -default-> l2;
    S S1, P P1, C C1 |- createLocals(l1, l2) :: OH OH1, MH MH1, L {} -default-> _ :: OH OH2, MH MH2, L L1;
    S Self(scope), P P1, C MethodC() |- code :: OH OH2, MH MH2, L L1 -default-> v1 :: OH OH3, MH MH3, L _;
    debug("done calling methods with some args") => _.

  S S1, P P1, C C1 |- AssignmentL(name, e) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH2, MH MH2, L L3
  where
    C1 => MethodC();
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2;
    writeLocal(name, v1) :: L L2 -default-> _ :: L L3.

  S _, P _, C _ |- AssignmentL(_, _) :: OH OH1, MH MH1, L L1 -default-> Error() :: OH OH1, MH MH1, L L1
  where
    error("Assignment outside methods not implemented") => _.

  S S1, P P1, C C1 |- Assignment(e) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2
  where
    S S1, P P1, C C1 |- e :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2.

  allocateObject(o1) :: OH OH1 -default-> addr :: OH OH2
  where
    fresh => addr;
    writeObject(addr, o1) :: OH OH1 -default-> _ :: OH OH2.

  allocateMethod(m1) :: MH MH1 -default-> addr :: MH MH2
  where
    fresh => addr;
    writeMethod(addr, m1) :: MH MH1 -default-> _ :: MH MH2.

  S _ |- addMembers([  ], [  ]) :: OH OH1, MH MH1 -default-> Unit() :: OH OH1, MH MH1.

  S S1 |- addMembers([ n | ns ], [ code | codes ]) :: OH OH1, MH MH1 -default-> Unit() :: OH OH3, MH MH3
  where
    S S1 |- addMember(n, [  ] : List(String), code) :: OH OH1, MH MH1 -default-> _ :: OH OH2, MH MH2;
    S S1 |- addMembers(ns, codes) :: OH OH2, MH MH2 -default-> _ :: OH OH3, MH MH3.

  S Self(self) |- addMember(name, params, code) :: OH OH1, MH MH1 -default-> Unit() :: OH OH3, MH MH2
  where
    debug("attempt to write member: '", name, "'") => _;
    allocateMethod(Method(params, code, self)) :: MH MH1 -default-> mRef :: MH MH2;
    readObject(self) :: OH OH1 -default-> Object(enc, tbl) :: OH OH2;
    writeObject(self, Object(enc, {name |--> mRef} + tbl)) :: OH OH2 -default-> _ :: OH OH3;
    debug("added member: '", name, "' successfully") => _;
    print(NumV(self)) => _.

  p@Program(_, _) -init-> v1
  where
    S Self(fresh), P Exec(), C ObjectC() |- p :: OH {}, MH {}, L {} -default-> v1 :: OH _, MH _, L _.

  S _, P _, C _ |- [  ] : List(Statement) :: OH OH1, MH MH1, L L1 -default-> Done() :: OH OH1, MH MH1, L L1.

  S S1, P P1, C C1 |- [ code | [  ] ] : List(Statement) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2
  where
    S S1, P P1, C C1 |- code :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2.

  S S1, P P1, C C1 |- [ code | l1 ] : List(Statement) :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH3, MH MH3, L L3
  where
    l1 => [ _ | _ ];
    S S1, P P1, C C1 |- code :: OH OH1, MH MH1, L L1 -default-> _ :: OH OH2, MH MH2, L L2;
    S S1, P P1, C C1 |- l1 :: OH OH2, MH MH2, L L2 -default-> v1 :: OH OH3, MH MH3, L L3.

  [  ] : List(Statement) -selectDecls-> [  ] : List(Statement).

  [ s1 | ss ] : List(Statement) -selectDecls-> [ s1 | ss' ]
  where
    s1 => Declaration(MethodL(_, _, _, _));
    ss -selectDecls-> ss'.

  [ s1 | ss ] : List(Statement) -selectDecls-> [ s1 | ss' ]
  where
    s1 => Declaration(ConstantL(_, _, _));
    ss -selectDecls-> ss'.

  [ s1 | ss ] : List(Statement) -selectDecls-> [ s1 | ss' ]
  where
    s1 => Declaration(VariableL(_, _));
    ss -selectDecls-> ss'.

  [ _ | ss ] : List(Statement) -selectDecls-> ss'
  where
    ss -selectDecls-> ss'.

  [  ] : List(Statement) -selectStmts-> [  ] : List(Statement).

  [ s1 | ss ] : List(Statement) -selectStmts-> [ s1 | ss' ]
  where
    s1 => Assignment(AssignmentL(_, _));
    ss -selectStmts-> ss'.

  [ s1 | ss ] : List(Statement) -selectStmts-> [ s1 | ss' ]
  where
    s1 => Expression(_);
    ss -selectStmts-> ss'.

  [ _ | ss ] : List(Statement) -selectStmts-> ss'
  where
    ss -selectStmts-> ss'.

  S _, P _, C _ |- [  ] : List(Exp) :: OH OH1, MH MH1, L L1 -ea-> [  ] : List(V) :: OH OH1, MH MH1, L L1.

  S S1, P P1, C C1 |- [ a | [  ] ] : List(Exp) :: OH OH1, MH MH1, L L1 -ea-> [ v1 | [  ] ] :: OH OH2, MH MH2, L L2
  where
    S S1, P P1, C C1 |- a :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2.

  S S1, P P1, C C1 |- [ a | as ] : List(Exp) :: OH OH1, MH MH1, L L1 -ea-> [ v1 | vs ] :: OH OH3, MH MH3, L L3
  where
    S S1, P P1, C C1 |- a :: OH OH1, MH MH1, L L1 -default-> v1 :: OH OH2, MH MH2, L L2;
    S S1, P P1, C C1 |- as :: OH OH2, MH MH2, L L2 -ea-> vs : List(V) :: OH OH3, MH MH3, L L3.
vvergu commented 7 years ago

What i normally do is minimize the problem with a binary search algorithm until i narrow down the problem to the smallest subset of rules which causes the problem.

Once i have that set of rules i create a self-contained module which exhibits the problem. That's typically quite small.

milosonator commented 7 years ago

Minimal example to trigger the error, doesn't make that much sense as a semantics spec but it shows the error:

module semantics/trans/semantics

signature

  sorts
      Exp
    constructors
      Constructor: Exp
    arrows
      List(Exp) :: OH --> Exp :: OH
      Exp --> Exp
    components
      OH : Map(Int,Int)

rules

   Constructor() --> Constructor()
    where
      case true of {
        true => 

        otherwise => 
      };
      [] --> _.

Transform to DynSem Core to see the problem

'Expected result' --> remove case switch and transform to core. Semantic component is properly propagated.

vvergu commented 7 years ago

Thanks. This is something i can work with.

vvergu commented 7 years ago

The problem seems to be related to a (previously unknown) type analysis bug. Take the following specification:

module semantics

signature
  sorts
    Exp
  constructors
    Constructor: Exp
  arrows
    Exp --> Int

rules
   Constructor() --> z
    where
      case true of {
        true =>
          1 => y
      };
      y => z.

The reference to variable y in the last premise is incorrectly marked as unresolved. If however the reference to z is replaced by a reference to y then the incorrect error report no longer happens.

vvergu commented 7 years ago

I believe this is a different symptom of the underlying cause of #36. Hopefully when fixing #36 this issue will just go away like a well behaved bug should.