Skip to content

Commit

Permalink
prepare for 0.3.1
Browse files Browse the repository at this point in the history
  • Loading branch information
@c-cube
c-cube committed Nov 24, 2016
2 parents e08f8df + 7526cae commit 6857df8
Show file tree
Hide file tree
Showing 503 changed files with 68,179 additions and 445 deletions.
4 changes: 4 additions & 0 deletions README.adoc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,10 @@ used for reporting bugs.

To build Nunchaku, there are several ways.

== Documentation

the API documentation can be found at https://nunchaku-inria.github.io/nunchaku/.

=== Released versions

Releases can be found on https://gforge.inria.fr/projects/nunchaku .
Expand Down
4 changes: 2 additions & 2 deletions _oasis
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: nunchaku
Version: 0.3
Version: 0.3.1
Homepage: https://github.com/nunchaku/nunchaku
Authors: Simon Cruanes, Jasmin Blanchette
License: BSD-2-clause
Expand All @@ -25,7 +25,7 @@ Library nunchaku_core
Pack: true
Modules: ID, Var, MetaVar, Location, Intf, Utils, Transform,
UntypedAST, Model, TypeUnify, Problem, FO, Reduce,
Env, Signature, Statement, FO_tptp, FO_rel, Cardinality,
Env, Statement, FO_tptp, FO_rel, Cardinality,
Scheduling, Polarity, Traversal, ProblemMetadata,
AnalyzeType, Prelude, TypeCheck, Lazy_list,
Sexp_lib, Sexp_lex,
Expand Down
3 changes: 1 addition & 2 deletions _tags
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
# OASIS_START
# DO NOT EDIT (digest: a6a4cf1c163937710a2666320f41a739)
# DO NOT EDIT (digest: 0b0218c6de70ee6a72e00f7814fcc531)
# Ignore VCS directories, you can use the same kind of rule outside
# OASIS_START/STOP if you want to exclude directories that contains
# useless stuff for the build process
Expand Down Expand Up @@ -30,7 +30,6 @@ true: annot, bin_annot
"src/core/FO.cmx": for-pack(Nunchaku_core)
"src/core/Reduce.cmx": for-pack(Nunchaku_core)
"src/core/Env.cmx": for-pack(Nunchaku_core)
"src/core/Signature.cmx": for-pack(Nunchaku_core)
"src/core/Statement.cmx": for-pack(Nunchaku_core)
"src/core/FO_tptp.cmx": for-pack(Nunchaku_core)
"src/core/FO_rel.cmx": for-pack(Nunchaku_core)
Expand Down
1 change: 0 additions & 1 deletion doc/intro.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,6 @@ ProblemMetadata
Reduce
Scheduling
Sexp_lib
Signature
Statement
TermInner
TermMono
Expand Down
161 changes: 161 additions & 0 deletions docs/0.3/AnalyzeType.Make.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,161 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<link rel="stylesheet" href="style.css" type="text/css">
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
<link rel="Start" href="index.html">
<link rel="Up" href="AnalyzeType.html">
<link title="Index of types" rel=Appendix href="index_types.html">
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
<link title="Index of values" rel=Appendix href="index_values.html">
<link title="Index of modules" rel=Appendix href="index_modules.html">
<link title="Index of module types" rel=Appendix href="index_module_types.html">
<link title="ID" rel="Chapter" href="ID.html">
<link title="Var" rel="Chapter" href="Var.html">
<link title="MetaVar" rel="Chapter" href="MetaVar.html">
<link title="Location" rel="Chapter" href="Location.html">
<link title="Intf" rel="Chapter" href="Intf.html">
<link title="Utils" rel="Chapter" href="Utils.html">
<link title="Transform" rel="Chapter" href="Transform.html">
<link title="UntypedAST" rel="Chapter" href="UntypedAST.html">
<link title="Model" rel="Chapter" href="Model.html">
<link title="TypeUnify" rel="Chapter" href="TypeUnify.html">
<link title="Problem" rel="Chapter" href="Problem.html">
<link title="FO" rel="Chapter" href="FO.html">
<link title="Reduce" rel="Chapter" href="Reduce.html">
<link title="Env" rel="Chapter" href="Env.html">
<link title="Signature" rel="Chapter" href="Signature.html">
<link title="Statement" rel="Chapter" href="Statement.html">
<link title="FO_tptp" rel="Chapter" href="FO_tptp.html">
<link title="FO_rel" rel="Chapter" href="FO_rel.html">
<link title="Cardinality" rel="Chapter" href="Cardinality.html">
<link title="Scheduling" rel="Chapter" href="Scheduling.html">
<link title="Polarity" rel="Chapter" href="Polarity.html">
<link title="Traversal" rel="Chapter" href="Traversal.html">
<link title="ProblemMetadata" rel="Chapter" href="ProblemMetadata.html">
<link title="AnalyzeType" rel="Chapter" href="AnalyzeType.html">
<link title="Prelude" rel="Chapter" href="Prelude.html">
<link title="TypeCheck" rel="Chapter" href="TypeCheck.html">
<link title="Lazy_list" rel="Chapter" href="Lazy_list.html">
<link title="Sexp_lib" rel="Chapter" href="Sexp_lib.html">
<link title="Sexp_lex" rel="Chapter" href="Sexp_lex.html">
<link title="TermInner" rel="Chapter" href="TermInner.html">
<link title="TermTyped" rel="Chapter" href="TermTyped.html">
<link title="TermMono" rel="Chapter" href="TermMono.html">
<link title="Pattern" rel="Chapter" href="Pattern.html">
<link title="TypePoly" rel="Chapter" href="TypePoly.html">
<link title="TypeMono" rel="Chapter" href="TypeMono.html">
<link title="Parsing_utils" rel="Chapter" href="Parsing_utils.html">
<link title="Lexer" rel="Chapter" href="Lexer.html">
<link title="Parser" rel="Chapter" href="Parser.html">
<link title="TPTP_print" rel="Chapter" href="TPTP_print.html">
<link title="TPTP_lexer" rel="Chapter" href="TPTP_lexer.html">
<link title="TPTP_parser" rel="Chapter" href="TPTP_parser.html">
<link title="TPTP_preprocess" rel="Chapter" href="TPTP_preprocess.html">
<link title="TPTP_model_ast" rel="Chapter" href="TPTP_model_ast.html">
<link title="TPTP_model_lexer" rel="Chapter" href="TPTP_model_lexer.html">
<link title="TPTP_model_parser" rel="Chapter" href="TPTP_model_parser.html">
<link title="Ast_kodkod" rel="Chapter" href="Ast_kodkod.html">
<link title="Lex_kodkod" rel="Chapter" href="Lex_kodkod.html">
<link title="Parse_kodkod" rel="Chapter" href="Parse_kodkod.html">
<link title="Tip_ast" rel="Chapter" href="Tip_ast.html">
<link title="Tip_parser" rel="Chapter" href="Tip_parser.html">
<link title="Tip_lexer" rel="Chapter" href="Tip_lexer.html">
<link title="Parse_tip" rel="Chapter" href="Parse_tip.html">
<link title="Skolem" rel="Chapter" href="Skolem.html">
<link title="TypeInference" rel="Chapter" href="TypeInference.html">
<link title="ElimPatternMatch" rel="Chapter" href="ElimPatternMatch.html">
<link title="Monomorphization" rel="Chapter" href="Monomorphization.html">
<link title="Specialize" rel="Chapter" href="Specialize.html">
<link title="LambdaLift" rel="Chapter" href="LambdaLift.html">
<link title="Elim_HOF" rel="Chapter" href="Elim_HOF.html">
<link title="ElimRecursion" rel="Chapter" href="ElimRecursion.html">
<link title="ElimMultipleEqns" rel="Chapter" href="ElimMultipleEqns.html">
<link title="ElimIndPreds" rel="Chapter" href="ElimIndPreds.html">
<link title="ElimCopy" rel="Chapter" href="ElimCopy.html">
<link title="Polarize" rel="Chapter" href="Polarize.html">
<link title="Unroll" rel="Chapter" href="Unroll.html">
<link title="IntroGuards" rel="Chapter" href="IntroGuards.html">
<link title="Model_clean" rel="Chapter" href="Model_clean.html">
<link title="ElimData" rel="Chapter" href="ElimData.html">
<link title="ElimTypes" rel="Chapter" href="ElimTypes.html">
<link title="Elim_prop_args" rel="Chapter" href="Elim_prop_args.html">
<link title="Elim_ite" rel="Chapter" href="Elim_ite.html">
<link title="Elim_infinite" rel="Chapter" href="Elim_infinite.html">
<link title="FoToRelational" rel="Chapter" href="FoToRelational.html"><title>Nunchaku documentation : AnalyzeType.Make</title>
</head>
<body>
<div class="navbar">&nbsp;<a class="up" href="AnalyzeType.html" title="AnalyzeType">Up</a>
&nbsp;</div>
<h1>Functor <a href="type_AnalyzeType.Make.html">AnalyzeType.Make</a></h1>

<pre><span class="keyword">module</span> Make <code class="code">(</code><code class="code"><span class="constructor">T</span></code><code class="code"> : </code><code class="type"><a href="TermInner.S.html">TermInner.S</a></code><code class="code">) </code>: <code class="code"><span class="keyword">sig</span></code> <a href="AnalyzeType.Make.html">..</a> <code class="code"><span class="keyword">end</span></code></pre><table border="0" cellpadding="3" width="100%">
<tr>
<td align="left" valign="top" width="1%%"><b>Parameters: </b></td>
<td>
<table class="paramstable">
<tr>
<td align="center" valign="top" width="15%">
<code>T</code></td>
<td align="center" valign="top">:</td>
<td><code class="type"><a href="TermInner.S.html">TermInner.S</a></code>
</table>
</td>
</tr>
</table>
<hr width="100%">

<pre><span id="TYPEty"><span class="keyword">type</span> <code class="type"></code>ty</span> = <code class="type">T.t</code> </pre>


<pre><span id="TYPEenv"><span class="keyword">type</span> <code class="type">'a</code> env</span> = <code class="type">('a, <a href="AnalyzeType.Make.html#TYPEty">ty</a>) <a href="Env.html#TYPEt">Env.t</a></code> </pre>
<div class="info ">
We only consider monomorphic types<br>
</div>


<pre><span id="TYPEcache"><span class="keyword">type</span> <code class="type"></code>cache</span> </pre>
<div class="info ">
Cache for memoizing cardinality computations<br>
</div>


<pre><span id="VALcreate_cache"><span class="keyword">val</span> create_cache</span> : <code class="type">?default_card:int -> unit -> <a href="AnalyzeType.Make.html#TYPEcache">cache</a></code></pre><div class="info ">
</div>
<div class="param_info"><code class="code">default_card</code> : if provided, the uninterpreted types we
know nothing about will be considered as having this card</div>

<pre><span id="VALcardinality_ty"><span class="keyword">val</span> cardinality_ty</span> : <code class="type">?cache:<a href="AnalyzeType.Make.html#TYPEcache">cache</a> -><br> 'a <a href="AnalyzeType.Make.html#TYPEenv">env</a> -> <a href="AnalyzeType.Make.html#TYPEty">ty</a> -> <a href="Cardinality.html#TYPEt">Cardinality.t</a></code></pre><div class="info ">
<code class="code">cardinality_ty ty</code> computes the cardinality of the type <code class="code">ty</code>, which
must be monomorphic.<br>
<b>Raises</b><ul><li><code>EmptyData</code> if there is some ill-defined data in <code class="code">env</code></li>
<li><code>Polymorphic</code> if the type is polymorphic,
or depends on polymorphic types</li>
</ul>
</div>

<pre><span id="VALcardinality_ty_id"><span class="keyword">val</span> cardinality_ty_id</span> : <code class="type">?cache:<a href="AnalyzeType.Make.html#TYPEcache">cache</a> -><br> 'a <a href="AnalyzeType.Make.html#TYPEenv">env</a> -> <a href="ID.html#TYPEt">ID.t</a> -> <a href="Cardinality.html#TYPEt">Cardinality.t</a></code></pre><div class="info ">
<code class="code">cardinality id</code> computes the cardinality of the type
named <code class="code">id</code>.<br>
<b>Raises</b><ul><li><code>EmptyData</code> if there is some ill-defined data in <code class="code">env</code></li>
<li><code>Error</code> if <code class="code">id</code> is not a valid type in <code class="code">env</code></li>
<li><code>Polymorphic</code> if the type is polymorphic,
or depends on polymorphic types</li>
</ul>
</div>

<pre><span id="VALcheck_non_zero"><span class="keyword">val</span> check_non_zero</span> : <code class="type">?cache:<a href="AnalyzeType.Make.html#TYPEcache">cache</a> -><br> 'a <a href="AnalyzeType.Make.html#TYPEenv">env</a> -> ('a, <a href="AnalyzeType.Make.html#TYPEty">ty</a>) <a href="Statement.html#TYPEt">Statement.t</a> -> unit</code></pre><div class="info ">
<code class="code">check_non_zero env stmt</code> checks that <code class="code">stmt</code> is not a definition of
an empty datatype<br>
</div>

<pre><span id="VALis_incomplete"><span class="keyword">val</span> is_incomplete</span> : <code class="type">'a <a href="AnalyzeType.Make.html#TYPEenv">env</a> -> <a href="AnalyzeType.Make.html#TYPEty">ty</a> -> bool</code></pre><div class="info ">
Is the type incomplete, that is, some values from the input type
are not present in this encoding?<br>
</div>

<pre><span id="VALis_abstract"><span class="keyword">val</span> is_abstract</span> : <code class="type">'a <a href="AnalyzeType.Make.html#TYPEenv">env</a> -> <a href="AnalyzeType.Make.html#TYPEty">ty</a> -> bool</code></pre><div class="info ">
Is the type a quotient over the input types (i.e. several distinct
values of the input types are encoded as one value)?<br>
</div>
</body></html>
107 changes: 107 additions & 0 deletions docs/0.3/AnalyzeType.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<link rel="stylesheet" href="style.css" type="text/css">
<meta content="text/html; charset=utf-8" http-equiv="Content-Type">
<link rel="Start" href="index.html">
<link rel="previous" href="ProblemMetadata.html">
<link rel="next" href="Prelude.html">
<link rel="Up" href="index.html">
<link title="Index of types" rel=Appendix href="index_types.html">
<link title="Index of exceptions" rel=Appendix href="index_exceptions.html">
<link title="Index of values" rel=Appendix href="index_values.html">
<link title="Index of modules" rel=Appendix href="index_modules.html">
<link title="Index of module types" rel=Appendix href="index_module_types.html">
<link title="ID" rel="Chapter" href="ID.html">
<link title="Var" rel="Chapter" href="Var.html">
<link title="MetaVar" rel="Chapter" href="MetaVar.html">
<link title="Location" rel="Chapter" href="Location.html">
<link title="Intf" rel="Chapter" href="Intf.html">
<link title="Utils" rel="Chapter" href="Utils.html">
<link title="Transform" rel="Chapter" href="Transform.html">
<link title="UntypedAST" rel="Chapter" href="UntypedAST.html">
<link title="Model" rel="Chapter" href="Model.html">
<link title="TypeUnify" rel="Chapter" href="TypeUnify.html">
<link title="Problem" rel="Chapter" href="Problem.html">
<link title="FO" rel="Chapter" href="FO.html">
<link title="Reduce" rel="Chapter" href="Reduce.html">
<link title="Env" rel="Chapter" href="Env.html">
<link title="Signature" rel="Chapter" href="Signature.html">
<link title="Statement" rel="Chapter" href="Statement.html">
<link title="FO_tptp" rel="Chapter" href="FO_tptp.html">
<link title="FO_rel" rel="Chapter" href="FO_rel.html">
<link title="Cardinality" rel="Chapter" href="Cardinality.html">
<link title="Scheduling" rel="Chapter" href="Scheduling.html">
<link title="Polarity" rel="Chapter" href="Polarity.html">
<link title="Traversal" rel="Chapter" href="Traversal.html">
<link title="ProblemMetadata" rel="Chapter" href="ProblemMetadata.html">
<link title="AnalyzeType" rel="Chapter" href="AnalyzeType.html">
<link title="Prelude" rel="Chapter" href="Prelude.html">
<link title="TypeCheck" rel="Chapter" href="TypeCheck.html">
<link title="Lazy_list" rel="Chapter" href="Lazy_list.html">
<link title="Sexp_lib" rel="Chapter" href="Sexp_lib.html">
<link title="Sexp_lex" rel="Chapter" href="Sexp_lex.html">
<link title="TermInner" rel="Chapter" href="TermInner.html">
<link title="TermTyped" rel="Chapter" href="TermTyped.html">
<link title="TermMono" rel="Chapter" href="TermMono.html">
<link title="Pattern" rel="Chapter" href="Pattern.html">
<link title="TypePoly" rel="Chapter" href="TypePoly.html">
<link title="TypeMono" rel="Chapter" href="TypeMono.html">
<link title="Parsing_utils" rel="Chapter" href="Parsing_utils.html">
<link title="Lexer" rel="Chapter" href="Lexer.html">
<link title="Parser" rel="Chapter" href="Parser.html">
<link title="TPTP_print" rel="Chapter" href="TPTP_print.html">
<link title="TPTP_lexer" rel="Chapter" href="TPTP_lexer.html">
<link title="TPTP_parser" rel="Chapter" href="TPTP_parser.html">
<link title="TPTP_preprocess" rel="Chapter" href="TPTP_preprocess.html">
<link title="TPTP_model_ast" rel="Chapter" href="TPTP_model_ast.html">
<link title="TPTP_model_lexer" rel="Chapter" href="TPTP_model_lexer.html">
<link title="TPTP_model_parser" rel="Chapter" href="TPTP_model_parser.html">
<link title="Ast_kodkod" rel="Chapter" href="Ast_kodkod.html">
<link title="Lex_kodkod" rel="Chapter" href="Lex_kodkod.html">
<link title="Parse_kodkod" rel="Chapter" href="Parse_kodkod.html">
<link title="Tip_ast" rel="Chapter" href="Tip_ast.html">
<link title="Tip_parser" rel="Chapter" href="Tip_parser.html">
<link title="Tip_lexer" rel="Chapter" href="Tip_lexer.html">
<link title="Parse_tip" rel="Chapter" href="Parse_tip.html">
<link title="Skolem" rel="Chapter" href="Skolem.html">
<link title="TypeInference" rel="Chapter" href="TypeInference.html">
<link title="ElimPatternMatch" rel="Chapter" href="ElimPatternMatch.html">
<link title="Monomorphization" rel="Chapter" href="Monomorphization.html">
<link title="Specialize" rel="Chapter" href="Specialize.html">
<link title="LambdaLift" rel="Chapter" href="LambdaLift.html">
<link title="Elim_HOF" rel="Chapter" href="Elim_HOF.html">
<link title="ElimRecursion" rel="Chapter" href="ElimRecursion.html">
<link title="ElimMultipleEqns" rel="Chapter" href="ElimMultipleEqns.html">
<link title="ElimIndPreds" rel="Chapter" href="ElimIndPreds.html">
<link title="ElimCopy" rel="Chapter" href="ElimCopy.html">
<link title="Polarize" rel="Chapter" href="Polarize.html">
<link title="Unroll" rel="Chapter" href="Unroll.html">
<link title="IntroGuards" rel="Chapter" href="IntroGuards.html">
<link title="Model_clean" rel="Chapter" href="Model_clean.html">
<link title="ElimData" rel="Chapter" href="ElimData.html">
<link title="ElimTypes" rel="Chapter" href="ElimTypes.html">
<link title="Elim_prop_args" rel="Chapter" href="Elim_prop_args.html">
<link title="Elim_ite" rel="Chapter" href="Elim_ite.html">
<link title="Elim_infinite" rel="Chapter" href="Elim_infinite.html">
<link title="FoToRelational" rel="Chapter" href="FoToRelational.html"><title>Nunchaku documentation : AnalyzeType</title>
</head>
<body>
<div class="navbar"><a class="pre" href="ProblemMetadata.html" title="ProblemMetadata">Previous</a>
&nbsp;<a class="up" href="index.html" title="Index">Up</a>
&nbsp;<a class="post" href="Prelude.html" title="Prelude">Next</a>
</div>
<h1>Module <a href="type_AnalyzeType.html">AnalyzeType</a></h1>

<pre><span class="keyword">module</span> AnalyzeType: <code class="code"><span class="keyword">sig</span></code> <a href="AnalyzeType.html">..</a> <code class="code"><span class="keyword">end</span></code></pre><div class="info module top">
<h1 id="1_AnalyzeTypesCardinalitiesAbstractIncomplete">Analyze Types : Cardinalities, Abstract, Incomplete</h1><br>
</div>
<hr width="100%">

<pre><span id="EXCEPTIONError"><span class="keyword">exception</span> Error</span> <span class="keyword">of</span> <code class="type">string</code></pre>

<pre><span id="EXCEPTIONPolymorphic"><span class="keyword">exception</span> Polymorphic</span></pre>

<pre><span id="EXCEPTIONEmptyData"><span class="keyword">exception</span> EmptyData</span> <span class="keyword">of</span> <code class="type"><a href="ID.html#TYPEt">ID.t</a></code></pre>

<pre><span class="keyword">module</span> <a href="AnalyzeType.Make.html">Make</a> <code class="code">(</code><code class="code"><span class="constructor">T</span></code><code class="code"> : </code><code class="type"><a href="TermInner.S.html">TermInner.S</a></code><code class="code">) </code>: <code class="code"><span class="keyword">sig</span></code> <a href="AnalyzeType.Make.html">..</a> <code class="code"><span class="keyword">end</span></code></pre></body></html>
Loading

0 comments on commit 6857df8

Please sign in to comment.