Web Home

StrictnessAnalysisJFC

Welcome to the StrictnessAnalysisJFC web

Source language

t  := n
   |   x
   |   fun x => t1
   |   t1 t2
   |   let name x = t1 in t2 end
   |   t1 + t2
   |   _|_

Target language

t' := n
   |   x
   |   fun x => t1
   |   t1' t2'
   |   t1' ! t2'
   |   let name x = t1' in t2' end
   |   let value x = t1' in t2' end
   |   t1' + t2'
   |   _|_

Project

Directories

Strictjfc

This is the principal directory, it contains the core of the project.

GaSuTySyBaStrict.ag contains the data type that describes the syntax, either the Source Language and Target Language.

FreeVars.hs contains the functions that returns the set of free variables of a term.

HelperGamma.hs contains some function relates with the managing of Gamma.

Ident.hs describes the Ident type and some functions relates with the managing of it.

ReturnTypes.hs contains the information of the types that rules written SemGASuTySyBaStrict.ag in returns.

SemGaSuTySyBaStrict.ag implements the rules of the Substructural Type System for Backward Strictness Analysis.

SemHelper.hs contains a bunch of helper functions needed for implementation of SemGASuTySyBaStrict.ag.

Subst.hs contains the functions that implements the unify and substitutions for the types.

Tests and examples

Tests:
- Inference Test:
  - Term: 10 Result: Nat. Status: OK
  - Term: fun x => x. Result: t1 -S-> t1 Status: OK
  - Term: (fun x => x) 10. Result: Nat Status: OK
  - Term: 10 + 10 Result: Nat Status: OK
  - Term: 10 + (fun x => x) 10. Result: Nat. Status: OK
  - Term: Let id = fun x => x in id 10. Result: Nat. Status: It fails. The inference system fails.
Examples