*  The Action Semantics of microSpecimen  *
        

--	**  Semantic Entities  **

	needs Standard .


--	***  Bindings  ***
	
	needs 		Data , Storage , Abstractions .

(1)	token = symbol .
(2)	bindable(T:token) = integer ! function ! cell .


--	***  Storage  ***

(1) 	storable(C:cell) = integer .


--	***  Abstractions  ***

 	introduces 	function , fun-argument , fun-result .
	needs 		Data , Storage .

(1) 	function = abstraction .
(2) 	fun-argument = integer .
(3) 	fun-result = integer .



--	**  Semantic Functions  ** 

	needs AbstractSyntax , SemanticEntities . 


--	***  Programs  ***

	introduces 	run [[ _ ]] .
	needs 		Declarations , Commands .

(1)	run [[ _ ]] :: Program -> act .

(2) 	run [[ PROGRAM I:Identifier D:Declaration C:Command ]] = 
		| elaborate D  
		hence 
		| execute C .


--	***  Declarations  ***

	introduces 	elaborate [[ _ ]] .
	needs 		Commands , Expressions .


--	****  Elaborating Declarations  ****

(1)	elaborate [[ _ ]] :: Declaration -> act .

(2)	elaborate [[ CONST I:Identifier T:Type E:Expression ]] =
		| evaluate E
		then
		| bind tokenOf I to the integer .

(3)	elaborate [[ VAR I:Identifier T:Type E:Expression ]] =
		| | evaluate E then give the integer label #1
	   	| and 
	   	| | allocate a cell then give it label #2 
		then 
		| | bind tokenOf I to the cell#2 
	   	| and 
	   	| | store the integer#1 in the cell#2 . 

(5)	elaborate [[ FUN I1:Identifier I2:Identifier T1:Type T2:Type
                         E:Expression ]] = 
		recursively 
		| bind tokenOf I1 to
		| | closure abstraction  
		| |         | | | rebind 
	      	| |	    | | moreover 
	      	| |	    | | | bind tokenOf I2 to the integer
	        | |	    | hence 
           	| |         | | evaluate E then give the integer . 
	 
(6)	elaborate [[ DECLSEQ D1:Declaration D2:Declaration ]] =
		| elaborate D1
		before 
		| elaborate D2 .


--	***  Commands  ***

	introduces 	execute [[ _ ]] .
	needs 		Declarations , Expressions , Literals .


--	****  Executing Commands  ****
 
(1)	execute [[ _ ]] :: Command -> act . 

(2)	execute [[ ASSIGN I:Identifier E:Expression ]] = 
	   	| evaluate E
		then 
		| store the integer in the cell bound to tokenOf I . 

(3)     execute [[ WHILE E:Expression C:Command ]] = 
		unfolding 
		| | evaluate E
		| then 
		| | | check (it is 1) and then execute C and then unfold
	   	| | or 
	   	| | | check not (it is 1) . 
 
(4)	execute [[ LOCAL D:Declaration C:Command ]] = 
        	| rebind moreover elaborate D 
        	hence 
        	| execute C . 

(5)  	execute [[ COMSEQ C1:Command C2:Command ]] = 
		execute C1 and then execute C2 .


--	***  Expressions  ***

	introduces	evaluate [[ _ ]] , applyOperator [[ _ ]] . 
	needs 		Literals .


--	****  Evaluating Expressions  ****

(1)	evaluate [[ _ ]] :: Expression -> act . 

(2)   	evaluate [[ NUMERAL N:Integer ]] = give valuationOf N . 

(3)  	evaluate [[ IDENTIFIER I:Identifier ]] = 
		| give the integer bound to tokenOf I
		or
		| give the integer stored in (the cell bound to tokenOf I) .

(4)   	evaluate [[ IFEXP E:Expression E1:Expression E2:Expression ]] = 
        	| evaluate E
        	then 
        	| | check (it is 1) and then evaluate E1 
           	| or 
           	| | check (it is 0) and then evaluate E2 . 

(5)   	evaluate [[ APL I:Identifier E:Expression ]] =
		| evaluate E
        	then 
        	| enact (the abstraction bound to tokenOf I with the integer) .

(6)   	evaluate [[ BOP E1:Expression O:Operator E2:Expression ]] = 
        	| | evaluate E1 then give the integer label #1 
           	| and 
           	| | evaluate E2 then give the integer label #2  
        	then 
        	| applyOperator O . 

(7)   	evaluate [[ MOP O:Operator E:Expression ]] = 
        	| evaluate E then give the value
        	then 
        	| applyOperator O . 


--	****  Evaluating Operators  ****

(1)	applyOperator [[ _ ]]  :: Operator -> act .

(2) 	applyOperator [[ PLUS ]] = 
		give sum (the integer#1, the integer#2) . 

(3) 	applyOperator [[ MINUS ]] = 
		give difference (the integer#1, the integer#2) .

(4) 	applyOperator [[ TIMES ]] = 
		give product (the integer#1, the integer#2) .

(5) 	applyOperator [[ DIV ]] = 
		give quotient (the integer#1, the integer#2) .

(6) 	applyOperator [[ EQUAL ]] = 
		| check (the value#1 is the value#2) and then give 1
		or
		| check not(the value#1 is the value#2) and then give 0 .

(6) 	applyOperator [[ LESS ]] = 
		| check isLessThan(the value#1,the value#2) and then give 1
		or
		| check not(isLessThan(the value#1,the value#2)) and then give 0 .


--	**  Lexical Syntax  **

--	introduces	tokenOf [[ _ ]] , valuationOf  [[ _ ]] .

--	identifier =  letter  
--	           |  identifier letter  
--		   |  identifier digit .

--	numeral = digit  
--	        | numeral digit . 

--	digit = 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 .

--	letter  = A | B | ... | Z | a | ... | z .


--	***  Identifiers  ***

--	(1)	tokenOf [[ _ ]] :: Identifier -> token .

--	(2) 	tokenOf [[ I ]] = symbol I .


--	***  Numerals  ***

--	(1)	valuationOf [[ _ ]] :: Numeral -> integer .

--	(2) 	valuationOf [[ 0 ]] = 0 . 

--	...

--	(11) 	valuationOf [[ 9 ]] = 9 .

--	(12) 	valuationOf [[ N D ]] = 
--			sum (product (valuationOf N, 10), valuationOf D) .