From bd3124483b558dfad02aa6d634ccbed56900307d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Wed, 26 Jul 2023 15:49:25 +0200 Subject: [PATCH] Fix dead links and compilation warnings in sphinx doc --- .../Input_file_formats/Native/00_summary.md | 6 +++--- .../Native/02_types/02_01_builtin.md | 1 + .../Native/03_declaration_of_axioms.md | 14 +++++++------- .../Input_file_formats/Native/04_setting_goals.md | 6 +++--- .../Input_file_formats/Native/05_theories.md | 2 +- .../Input_file_formats/Native/06_control_flow.md | 12 ++++++------ 6 files changed, 21 insertions(+), 20 deletions(-) diff --git a/docs/sphinx_docs/Input_file_formats/Native/00_summary.md b/docs/sphinx_docs/Input_file_formats/Native/00_summary.md index 66486bf9c..993d23239 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/00_summary.md +++ b/docs/sphinx_docs/Input_file_formats/Native/00_summary.md @@ -23,13 +23,13 @@ Reserved keywords are the following. * To add new uninterpreted symbols (variables or functions) to the signature: [`logic`](01_declaration_of_symbols.md#logic-uninterpreted-symbols) and the [`ac` modifier](01_declaration_of_symbols.md#ac-modifier-associative-and-commutative-symbols) for associative and commutative symbols. * Interpreted functions: [`function`](01_declaration_of_symbols.md#function-user-defined-functions) and [`predicate`](01_declaration_of_symbols.md#predicate-propositional-valued-functions). -* Built-in types: [`int`](02_types/02_01_builtin.md#numbers-int-real-and-floats), [`real`](02_types/02_01_builtin.md#numbers-int-real-and-floats), [`bool`](02_types/02_01_builtin.md#bool-and-prop), [`prop`](02_types/02_01_builtin.md#bool-and-prop), [`unit`](02_types/02_01_builtin.md#unit), [`bitv`](02_types/02_01_builtin.md#bitvectors-bitv), [`farray`](02_types/02_01_builtin.md#functional-polymorphic-arrays-farray). +* Built-in types: [`int`](02_types/02_01_builtin.md#numeric-types), [`real`](02_types/02_01_builtin.md#numeric-types), [`bool`](02_types/02_01_builtin.md#boolean-types), [`prop`](02_types/02_01_builtin.md#boolean-types), [`unit`](02_types/02_01_builtin.md#unit-type), [`bitv`](02_types/02_01_builtin.md#bitvectors), [`farray`](02_types/02_01_builtin.md#polymorphic-functional-arrays). * Constant and operators for propositions are available: `and`, `or`, `xor`, `not`, `true`, `false`. The construct `distinct` is available for all types. Quantifiers `forall` and `exists` can be used. * To create new types: [`type`](02_types/index). They keyword `of` is useful when dealing with structured datatypes, which include [records](02_types/02_02_user_defined.md#records), [enums](02_types/02_02_user_defined.md#enums-and-algebraic-datatypes) and [algebraic datatypes](02_types/02_02_user_defined.md#enums-and-algebraic-datatypes). * To declare new axioms: [`axiom`](03_declaration_of_axioms.md#axiom), and the special case [`rewriting`](03_declaration_of_axioms.md#rewriting). * To define goals that must be proven valid: [`goal`](04_setting_goals.md#goal). [`cut`](04_setting_goals.md#intermediate-goals-cut-and-check) and [`check`](04_setting_goals.md#intermediate-goals-cut-and-check) can create intermediate goals that won't interact with other goals through [triggers](03_declaration_of_axioms.md#triggers). -* New theories may be defined using [theory](05_theories.md#theory-extends-end) (and the keywords `extends` and `end`). Inside theories, [`axiom`](05_theories.md#axiom) can be used with [additional triggers](05_theories.md#semantic-triggers). The construct [`case_split`](05_theories.md#case-split) is also available. -* Other useful constructs are [`let` [...] `in`](06_control_flow.md#let-in), [`match` [...] `with` [...] `end`](06_control_flow.md#match-with) and [`if` [...] `then` [...] `else` [...]](06_control_flow.md#if-then-else). +* New theories may be defined using [theory](05_theories.md#user-defined-extensions-of-theories) (and the keywords `extends` and `end`). Inside theories, [`axiom`](03_declaration_of_axioms.md#axiom) can be used with [additional triggers](05_theories.md#semantic-triggers). The construct [`case_split`](05_theories.md#case_split) is also available. +* Other useful constructs are [`let` [...] `in`](06_control_flow.md#let--in), [`match` [...] `with` [...] `end`](06_control_flow.md#match--with) and [`if` [...] `then` [...] `else` [...]](06_control_flow.md#if--then--else). The list of all reserved keywords, in alphabetical order, is: ``` diff --git a/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md b/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md index 9f809d208..bd95d8d64 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md +++ b/docs/sphinx_docs/Input_file_formats/Native/02_types/02_01_builtin.md @@ -53,6 +53,7 @@ Creation and manipulation of values having those types are covered in [built-in For all those operators, `bool` and `prop` are fully interchangeable. +(the-bool-prop-conflict)= #### The `bool`/`prop` conflict Prior to Alt-Ergo 2.3.0, Alt-Ergo's native language handled differently boolean variables `bool` and propositional variables `prop`. diff --git a/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md b/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md index 2cea18941..de0c8ea39 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md +++ b/docs/sphinx_docs/Input_file_formats/Native/03_declaration_of_axioms.md @@ -11,13 +11,13 @@ The heuristic for choosing new instances is based on *triggers*. By default, tri In order to declare an axiom, the user can use the following construct. Note that axioms must always be named. -#### Syntax +### Syntax ``` ::= 'axiom' ':' ``` Here, `` is an expression which may contain quantifiers, and where user-specified triggers may be added to universal quantifiers. -#### Example +### Example ``` (* Axioms can be used without quantifiers *) @@ -56,7 +56,7 @@ Interval triggers further restrict instantiation of axioms, and check that varia Multiple patterns can be used in syntactic triggers. They are separated by `|` which means 'or' and by `,` which means 'and'. `|` has an higher precedence than `,`. -#### Syntax +### Syntax ``` ::= ':' ? ? '.' ::= 'exists' | 'forall' @@ -75,9 +75,9 @@ Interval triggers also exists. [TODO: add more explanations] ::= '<' | '<=' ``` -[Semantic triggers](05_theories.html#semantic-triggers) are only available in theories +[Semantic triggers](05_theories.md#semantic-triggers) are only available in theories -#### Examples +### Examples ``` (* P(x) used as the only trigger *) logic P,Q,R: int -> prop @@ -110,7 +110,7 @@ To add a new axiom directly in the form of a rewriting technique, the keyword `r [TODO: complete] -#### Syntax +### Syntax ``` ::= 'rewriting' ':' ::= (';' ? )? @@ -118,5 +118,5 @@ To add a new axiom directly in the form of a rewriting technique, the keyword `r ::= | ``` -#### Example +### Example [TODO: find relevant examples] diff --git a/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md b/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md index 68a43f7fa..bc178c3e0 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md +++ b/docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md @@ -9,13 +9,13 @@ Alt-Ergo will answer `Valid` if it can prove that the formula of the goal is tru To declare goals, the user can use the following construct. Note that goals must always be named. -#### Syntax +### Syntax ``` ::= 'goal' ':' ``` Here, `` is an expression which may contain quantifiers. -#### Examples +### Examples ``` logic h, g, f: int, int -> int logic a, b:int @@ -44,7 +44,7 @@ In other word, `cut` and `check` allow to test if intermediate goals can be prov [WIP: complete] -#### Syntax +### Syntax ``` ::= 'check' ::= 'cut' diff --git a/docs/sphinx_docs/Input_file_formats/Native/05_theories.md b/docs/sphinx_docs/Input_file_formats/Native/05_theories.md index fe7220023..4354becad 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/05_theories.md +++ b/docs/sphinx_docs/Input_file_formats/Native/05_theories.md @@ -54,7 +54,7 @@ More information on this strategy and the language extension can be found in [th ### Semantic triggers -In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in [section Axioms](03_declaration_of_axioms.md), additional triggers are available inside theories. +In addition to syntactic triggers (or triggers) and interval triggers (or filters) defined in [axioms](03_declaration_of_axioms.md), additional triggers are available inside theories. Those additional triggers are called semantic triggers. They correspond to the following constructs. diff --git a/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md b/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md index 578a124e9..d544a2010 100644 --- a/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md +++ b/docs/sphinx_docs/Input_file_formats/Native/06_control_flow.md @@ -7,13 +7,13 @@ Like in OCaml, let expressions are available. They allow for named local expressions, which are written `let name = expression in [...]`. Name defined like this only have local scope. -#### Syntax +### Syntax ``` ::= 'let' 'in' ::= '=' ( ',' '=' )* ``` -#### Example +### Example ``` function average(a:real, b:real):real = let sum = a+b in @@ -27,7 +27,7 @@ Pattern matching, a [Really Cool Feature](https://ocaml.org/learn/tutorials/data Warning: the only patterns that can be matched are constructors of algebraic datatypes. Moreover, constructors can't be nested in a pattern. -#### Syntax +### Syntax ``` ::= 'match' 'with' 'end' ::= '|'? '->' ( '|' '->' )* @@ -35,7 +35,7 @@ Moreover, constructors can't be nested in a pattern. ::= ( "," )* ``` -#### Example +### Example ``` type 'a tree = NIL | Node of { left:'a tree; val:'a; right:'a tree } @@ -53,7 +53,7 @@ function height(t: 'a tree):int = The simple construct `if then else` for conditional expressions is available in Alt-Ergo's native language. -#### Syntax +### Syntax ``` ::= 'if' 'then' 'else' (* Note that must have type bool - or prop *) @@ -63,7 +63,7 @@ The simple construct `if then else` for conditional expressions is available in ::= ``` -#### Example +### Example ``` function max(a:int, b:int):int = if a>b then a else b