(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006, Adam Chlipala
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
 *)

(* Evaluation of expressions until only externs are around *)

structure Reduce :> REDUCE = struct

open Ast Print Env

structure SM = StringMap

fun freeIn x (b, _) =
    case b of
	EInt _ => false
      | EString _ => false
      | EList es => List.exists (freeIn x) es

      | ELam (x', _, b') => x <> x' andalso freeIn x b'
      | EVar x' => x = x'
      | EApp (e1, e2) => freeIn x e1 orelse freeIn x e2

      | ESkip => false
      | ESet (_, e) => freeIn x e
      | EGet (x', _, _, b') => x <> x' andalso freeIn x b'
      | ESeq es => List.exists (freeIn x) es
      | ELocal (e1, e2) => freeIn x e1 orelse freeIn x e2
      | EWith (e1, e2) => freeIn x e1 orelse freeIn x e2
      | EALam (x', _, b') => x <> x' andalso freeIn x b'

      | EIf (e1, e2, e3) => freeIn x e1 orelse freeIn x e2 orelse freeIn x e3

local
    val freshCount = ref 0
in
fun freshVar () =
    let
	val v = !freshCount
    in
	freshCount := v + 1;
	Int.toString v ^ "v"
    end
end

fun subst x e (bAll as (b, loc)) =
    case b of
	EInt _ => bAll
      | EString _ => bAll
      | EList es => (EList (map (subst x e) es), loc)

      | ELam (x', to, b') =>
	if x = x' then
	    bAll
	else if freeIn x' e then
	    let
		val x'' = freshVar ()
	    in
		(ELam (x'', to, subst x e (subst x' (EVar x'', loc) b')), loc)
	    end
	else
	    (ELam (x', to, subst x e b'), loc)
      | EVar x' =>
	if x = x' then
	    e
	else
	    bAll
      | EApp (b1, b2) => (EApp (subst x e b1, subst x e b2), loc)

      | ESkip => bAll
      | ESet (v, b) => (ESet (v, subst x e b), loc)
      | EGet (x', topt, v, b') =>
	if x = x' then
	    bAll
	else if freeIn x' e then
	    let
		val x'' = freshVar ()
	    in
		(EGet (x'', topt, v, subst x e (subst x' (EVar x'', loc) b')), loc)
	    end
	else
	    (EGet (x', topt, v, subst x e b'), loc)
      | ESeq es => (ESeq (map (subst x e) es), loc)
      | ELocal (b1, b2) => (ELocal (subst x e b1, subst x e b2), loc)
      | EWith (b1, b2) => (EWith (subst x e b1, subst x e b2), loc)
      | EALam (x', p, b') =>
	if x = x' then
	    bAll
	else if freeIn x' e then
	    let
		val x'' = freshVar ()
	    in
		(EALam (x'', p, subst x e (subst x' (EVar x'', loc) b')), loc)
	    end
	else
	    (EALam (x', p, subst x e b'), loc)

      | EIf (b1, b2, b3) => (EIf (subst x e b1, subst x e b2, subst x e b3), loc)

fun findPrim (e, _) =
    case e of
	EApp (f, x) =>
	(case findPrim f of
	     NONE => NONE
	   | SOME (f, xs) => SOME (f, xs @ [x]))
      | EVar x => SOME (x, [])
      | _ => NONE

fun reduceExp G (eAll as (e, loc)) =
    case e of
	EInt _ => eAll
      | EString _ => eAll
      | EList es => (EList (map (reduceExp G) es), loc)

      | ELam (x, to, e) =>
	let
	    val to' = case to of
			  NONE => (Tycheck.newUnif (), loc)
			| SOME to => to

	    val G' = bindVal G (x, to', NONE)
	in
	    (ELam (x, to, reduceExp G' e), loc)
	end
      | EVar x =>
	(case lookupEquation G x of
	     NONE =>
	     (case function x of
		  NONE => eAll
		| SOME f => case f [] of
				NONE => eAll
			      | SOME e' => reduceExp G e')
	   | SOME (e, G') => reduceExp G' e)
      | EApp (e1, e2) =>
	let
	    val e1' = reduceExp G e1
	    val e2' = reduceExp G e2
	in
	    case e1' of
		(ELam (x, _, b), _) => reduceExp G (subst x e2' b)
	      | _ =>
		case findPrim eAll of
		    NONE => (EApp (e1', e2'), loc)
		  | SOME (f, args) =>
		    case function f of
			NONE => (EApp (e1', e2'), loc)
		      | SOME f => case f (map (reduceExp G) args) of
				      NONE => (EApp (e1', e2'), loc)
				    | SOME e' => reduceExp G e'
	end

      | ESkip => eAll
      | ESet (v, b) => (ESet (v, reduceExp G b), loc)
      | EGet (x, topt, v, b) => (EGet (x, topt, v, reduceExp G b), loc)
      | ESeq es => (ESeq (map (reduceExp G) es), loc)
      | ELocal (e1, e2) => (ELocal (reduceExp G e1, reduceExp G e2), loc)
      | EWith (e1, e2) =>
	let
	    val e1' = reduceExp G e1
	    val e2' = reduceExp G e2
	in
	    case e1' of
		(EALam (x, _, b), _) => reduceExp G (subst x e2' b)
	      | _ => (EWith (e1', e2'), loc)
	end
      | EALam (x, p, e) =>
	let
	    val G' = bindVal G (x, (TAction (p, SM.empty, SM.empty), loc), NONE)
	in
	    (EALam (x, p, reduceExp G' e), loc)
	end

      | EIf (e1, e2, e3) =>
	let
	    val e1' = reduceExp G e1
	    fun e2' () = reduceExp G e2
	    fun e3' () = reduceExp G e3
	in
	    case e1' of
		(EVar "true", _) => e2' ()
	      | (EVar "false", _) => e3' ()
	      | _ => (EIf (e1', e2' (), e3' ()), loc)
	end

end