diff options
Diffstat (limited to 'Jennisys/Jennisys/MethodUnifier.fs')
| -rw-r--r-- | Jennisys/Jennisys/MethodUnifier.fs | 107 |
1 files changed, 0 insertions, 107 deletions
diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs deleted file mode 100644 index d2b1db68..00000000 --- a/Jennisys/Jennisys/MethodUnifier.fs +++ /dev/null @@ -1,107 +0,0 @@ -module MethodUnifier
-
-open Ast
-open Getters
-open AstUtils
-open FixpointSolver
-open PrintUtils
-open Resolver
-open Utils
-
-let TryUnify targetMthd candMethod =
- let targetPre,targetPost = GetMethodPrePost targetMthd
- let targetPre = BinaryAnd targetPre (GetMethodGhostPrecondition targetMthd)
- let candPre,candPost = GetMethodPrePost candMethod
- let candPre = BinaryAnd candPre (GetMethodGhostPrecondition candMethod)
- let builder = new CascadingBuilder<_>(None)
- builder {
- let! unifs1 = UnifyImplies targetPre candPre RTL Map.empty
- let! unifs2 = UnifyImplies candPost targetPost LTR unifs1
- return Some(unifs2)
- }
-
-let rec TryFindAMatch targetMthd candidateMethods =
- let targetMthdName = GetMethodName targetMthd
- match candidateMethods with
- | candMthd :: rest ->
- if GetMethodName candMthd = targetMthdName then
- // skip if it is the same method
- TryFindAMatch targetMthd rest
- else
- match TryUnify targetMthd candMthd with
- | Some(unifs) -> Some(candMthd,unifs)
- | None -> TryFindAMatch targetMthd rest
- | [] -> None
-
-let TryFindExistingOpt comp targetMthd =
- TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers)
-
-let TryFindExisting comp targetMthd =
- match TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with
- | Some(m,unifs) -> m,unifs
- | None -> targetMthd, Map.empty
-
-let ApplyMethodUnifs receiver (c,m) unifs =
- let __Apply args = args |> List.map (fun var ->
- let name = GetExtVarName var
- match Map.tryFind name unifs with
- | Some(e) -> e
- | None -> VarLiteral(name))
- let ins = GetMethodInArgs m |> __Apply
- let outs = GetMethodOutArgs m |> __Apply
-
- let retVars, asgs = outs |> List.fold (fun (acc1,acc2) e ->
- let vname = SymGen.NewSymFake e
- let v = Var(vname, None, false)
- let acc1' = acc1 @ [v]
- let acc2' = acc2 @ [ArbitraryStatement(Assign(VarLiteral(vname), e))]
- acc1', acc2'
- ) ([],[])
- let mcallExpr = MethodCall(receiver, GetComponentName c, GetMethodName m, ins)
- match retVars, outs with
- | [], [] -> [ArbitraryStatement(ExprStmt(mcallExpr))]
- | [_], [VarLiteral(vn2)] -> [ArbitraryStatement(Assign(VarDeclExpr([Var(vn2, None, false)], false), mcallExpr))]
- | _ ->
- let mcall = ArbitraryStatement(Assign(VarDeclExpr(retVars, true), mcallExpr))
- mcall :: asgs
-
-// ====================================================
-///
-// ====================================================
-let TryFindExistingAndConvertToSolution indent comp m cond callGraph =
- let __Calls caller callee =
- let keyOpt = callGraph |> Map.tryFindKey (fun (cc,mm) mset -> CheckSameMethods (comp,caller) (cc,mm))
- match keyOpt with
- | Some(k) -> callGraph |> Map.find k |> Set.contains ((GetComponentName comp),(GetMethodName callee))
- | None -> false
- (* --- function body starts here --- *)
- if not Options.CONFIG.genMod then
- None
- else
- let idt = Indent indent
- let candidateMethods = GetMembers comp |> List.filter (fun cm ->
- match cm with
- | Method(mname,_,_,_,_) when not (__Calls cm m) -> true
- | _ -> false)
- match TryFindAMatch m candidateMethods with
- | Some(m',unifs) ->
- Logger.InfoLine (idt + " - substitution method found:")
- Logger.InfoLine (Printer.PrintMethodSignFull (indent+6) comp m')
- Logger.DebugLine (idt + " Unifications: ")
- let idtt = idt + " "
- unifs |> Map.fold (fun acc k v -> acc + (sprintf "%s%s -> %s%s" idtt k (Printer.PrintExpr 0 v) newline)) "" |> Logger.Debug
- let obj = { name = "this"; objType = GetClassType comp }
- let modObjs = if IsModifiableObj obj (comp,m) then Set.singleton obj else Set.empty
- let body = ApplyMethodUnifs ThisLiteral (comp,m') unifs
- let hInst = { objs = Utils.MapSingleton obj.name obj;
- modifiableObjs = modObjs;
- assignments = body;
- concreteValues = body;
- methodArgs = Map.empty;
- methodRetVals = Map.empty;
- concreteMethodRetVals = Map.empty;
- globals = Map.empty }
- Some(Map.empty |> Map.add (comp,m) [cond, hInst]
- |> Map.add (comp,m') [])
- | None -> None
-
|