From 9c39b5a4d76c6334dcf933c74f59b96b5281dd98 Mon Sep 17 00:00:00 2001 From: Alex Kassil Date: Tue, 15 Aug 2023 20:18:02 -0700 Subject: [PATCH] Remove formal docs Reviewed By: pradeep90 Differential Revision: D48377479 fbshipit-source-id: 13a46c243099e0b7dfc206839a4da40b710cb95b --- documentation/website/docs/formal/.gitignore | 4 - .../docs/formal/python_semantic/.gitignore | 9 - .../docs/formal/python_semantic/Eval.v | 511 ------ .../docs/formal/python_semantic/Expression.v | 90 -- .../docs/formal/python_semantic/Lib/List.v | 23 - .../docs/formal/python_semantic/Lib/String.v | 51 - .../docs/formal/python_semantic/Lvalue.v | 8 - .../docs/formal/python_semantic/Makefile | 40 - .../website/docs/formal/python_semantic/Map.v | 83 - .../docs/formal/python_semantic/README | 8 - .../docs/formal/python_semantic/Semantic.v | 1420 ----------------- .../docs/formal/python_semantic/Statement.v | 37 - .../website/docs/formal/python_semantic/Typ.v | 52 - .../docs/formal/python_semantic/Value.v | 116 -- .../docs/formal/python_semantic/_CoqProject | 12 - .../formal/python_semantic/extra/footer.html | 8 - .../formal/python_semantic/extra/header.html | 27 - .../python_semantic/extra/resources/config.js | 79 - .../extra/resources/coqdoc.css | 208 --- .../extra/resources/coqdocjs.css | 256 --- .../extra/resources/coqdocjs.js | 201 --- .../subtyping_description/DejaVuSansMono.sty | 38 - .../formal/subtyping_description/Makefile | 15 - .../formal/subtyping_description/lstocaml.sty | 60 - .../subtyping_description/mathpartir.sty | 492 ------ .../formal/subtyping_description/pyre_sub.tex | 339 ---- 26 files changed, 4187 deletions(-) delete mode 100644 documentation/website/docs/formal/.gitignore delete mode 100644 documentation/website/docs/formal/python_semantic/.gitignore delete mode 100644 documentation/website/docs/formal/python_semantic/Eval.v delete mode 100644 documentation/website/docs/formal/python_semantic/Expression.v delete mode 100644 documentation/website/docs/formal/python_semantic/Lib/List.v delete mode 100644 documentation/website/docs/formal/python_semantic/Lib/String.v delete mode 100644 documentation/website/docs/formal/python_semantic/Lvalue.v delete mode 100644 documentation/website/docs/formal/python_semantic/Makefile delete mode 100644 documentation/website/docs/formal/python_semantic/Map.v delete mode 100644 documentation/website/docs/formal/python_semantic/README delete mode 100644 documentation/website/docs/formal/python_semantic/Semantic.v delete mode 100644 documentation/website/docs/formal/python_semantic/Statement.v delete mode 100644 documentation/website/docs/formal/python_semantic/Typ.v delete mode 100644 documentation/website/docs/formal/python_semantic/Value.v delete mode 100644 documentation/website/docs/formal/python_semantic/_CoqProject delete mode 100644 documentation/website/docs/formal/python_semantic/extra/footer.html delete mode 100644 documentation/website/docs/formal/python_semantic/extra/header.html delete mode 100644 documentation/website/docs/formal/python_semantic/extra/resources/config.js delete mode 100644 documentation/website/docs/formal/python_semantic/extra/resources/coqdoc.css delete mode 100644 documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.css delete mode 100644 documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.js delete mode 100644 documentation/website/docs/formal/subtyping_description/DejaVuSansMono.sty delete mode 100644 documentation/website/docs/formal/subtyping_description/Makefile delete mode 100644 documentation/website/docs/formal/subtyping_description/lstocaml.sty delete mode 100644 documentation/website/docs/formal/subtyping_description/mathpartir.sty delete mode 100644 documentation/website/docs/formal/subtyping_description/pyre_sub.tex diff --git a/documentation/website/docs/formal/.gitignore b/documentation/website/docs/formal/.gitignore deleted file mode 100644 index 2ec7e4ca94a..00000000000 --- a/documentation/website/docs/formal/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -*.aux -*.log -*.pdf -*.out diff --git a/documentation/website/docs/formal/python_semantic/.gitignore b/documentation/website/docs/formal/python_semantic/.gitignore deleted file mode 100644 index 37646366ea2..00000000000 --- a/documentation/website/docs/formal/python_semantic/.gitignore +++ /dev/null @@ -1,9 +0,0 @@ -Makefile.coq -Makefile.coq.conf -CoqMakefile.conf -*.vo -*.glob -*.aux -.*.swp -.coqdeps.d -html diff --git a/documentation/website/docs/formal/python_semantic/Eval.v b/documentation/website/docs/formal/python_semantic/Eval.v deleted file mode 100644 index 2a5c7f14f49..00000000000 --- a/documentation/website/docs/formal/python_semantic/Eval.v +++ /dev/null @@ -1,511 +0,0 @@ -Require Import String Bool ZArith List. -Require Pyre.Value. -Require Pyre.Lvalue. -Require Pyre.Typ. -Require Pyre.Expression. -Require Pyre.Statement. -Require Import Pyre.Map. - -Import Pyre.Value.ListHelpers. -Import Pyre.Typ.ListHelpers. -Import Pyre.Expression.ListHelpers. - -(* begin hide *) -Definition evaluate_boolean_operator lexpr op rexpr := - match op with - | Expression.And => andb lexpr rexpr - | Expression.Or => orb lexpr rexpr -end. - -(* Helper to evaluate value membership *) -Fixpoint value_in (x lst:Value.t) : bool := - match lst with - | Value.Sequence lst => List.existsb (fun y => Value.eqb x y) lst - | _ => false - end. - -Definition evaluate_int_comparison_operator lexpr op rexpr: bool := - match lexpr, rexpr with - | Value.Integer lexpr, Value.Integer rexpr => - match op with - | Expression.GreaterThan => Z.gtb lexpr rexpr - | Expression.GreaterThanOrEquals => Z.geb lexpr rexpr - | Expression.LessThan => Z.ltb lexpr rexpr - | Expression.LessThanOrEquals => Z.leb lexpr rexpr - | _ => false - end - | _ , _ => false -end. - -Definition evaluate_comparison_operator lexpr op rexpr := - match op with - | Expression.Equals => Value.eqb lexpr rexpr - | Expression.NotEquals => negb (Value.eqb lexpr rexpr) - | Expression.GreaterThan - | Expression.GreaterThanOrEquals - | Expression.LessThan - | Expression.LessThanOrEquals => - evaluate_int_comparison_operator lexpr op rexpr - | Expression.In => value_in lexpr rexpr - | Expression.NotIn => negb (value_in lexpr rexpr) - | _ => (* TODO(T53097965): implement Is/IsNot *) false - end -. - -Definition evaluate_unary_operator op expr : option Value.t := - match op, expr with - | Expression.Not, Value.Boolean b => Some (Value.Boolean (negb b)) - | Expression.Invert, Value.Integer z => Some (Value.Integer (-z -1)%Z) - | Expression.Negative, Value.Integer z => Some (Value.Integer (- z)%Z) - | Expression.Positive, Value.Integer z => Some (Value.Integer z) - | _, _ => None - end. - -Lemma evaluate_unary_int_operator : forall op z, - evaluate_unary_operator op (Value.Integer z) = - match op with - | Expression.Negative => Some (Value.Integer (-z)%Z) - | Expression.Positive => Some (Value.Integer z) - | Expression.Invert => Some (Value.Integer (-z -1)%Z) - | _ => None - end. -Proof. -now destruct op; intros z; simpl. -Qed. -(* end hide *) - -(** Map from identifiers to values. Used during <> evaluation *) -Definition EState := SMap.t Value.t. -Definition Empty : EState := SMap.empty _. - -(** * Evaluation of expressions - Evaluates the expression <> using the state <>. Returns some - <> if everything went ok, or <> otherwise. -*) -Fixpoint eval (now: EState) (expr : Expression.t) : option Value.t := - match expr with - | Expression.BooleanOperator lexpr op rexpr => - match (eval now lexpr, eval now rexpr) with - | (Some (Value.Boolean b0), Some (Value.Boolean b1)) => - Some (Value.Boolean (evaluate_boolean_operator b0 op b1)) - | (_, _) => None - end - | Expression.ComparisonOperator lexpr op rexpr => - match (eval now lexpr, eval now rexpr) with - | (Some vl, Some vr) => - Some (Value.Boolean (evaluate_comparison_operator vl op vr)) - | (_, _) => None - end - | Expression.False_ => Some (Value.Boolean false) - | Expression.Integer z => Some (Value.Integer z) - | Expression.List el => - match eval_list now el with - | Some vl => Some (Value.Sequence vl) - | None => None - end - | Expression.Id id => SMap.find id now - | Expression.None => Some Value.None - | Expression.String s => Some (Value.String s) - | Expression.Ternary target test alternative => - match eval now test with - | Some (Value.Boolean true) => eval now target - | Some (Value.Boolean false) => eval now alternative - | Some _ => None - | None => None - end - | Expression.True_ => Some (Value.Boolean true) - | Expression.Tuple el => - match eval_list now el with - | Some vl => Some (Value.Sequence vl) - | None => None - end - | Expression.UnaryOperator op e => - match eval now e with - | Some v => evaluate_unary_operator op v - | None => None - end - end -with eval_list (now: EState) (elist : Expression.tlist) : - option Value.tlist := - match elist with - | Expression.Nil => Some (Value.Nil) - | Expression.Cons hd tl => - match (eval now hd, eval_list now tl) with - | (Some hd, Some tl) => Some (Value.Cons hd tl) - | (_, _) => None - end - end -. - -Lemma eval_list_length: forall (state: EState) - (l: Expression.tlist) (vl: Value.tlist), - eval_list state l = Some vl -> List.length l = List.length vl. -Proof. -intro now; induction l as [ | e es hi]; intros vs' h; simpl in *. -- now injection h; clear h; intro h; subst. -- case_eq (eval now e); [ intros v | ]; intros hv; rewrite hv in h. - + case_eq (eval_list now es); [ intros vs | ]; intros hvs; rewrite hvs in h. - * injection h; clear h; intro h; subst; simpl. - now rewrite (hi _ hvs). - * discriminate h. - + discriminate h. -Qed. - -(** Global state for the statement operational semantic. It is made of -the state for expression evaluation, along with information about know -functions. *) -Definition State := @Map.State Value.t. -Definition EState_of_State (state : State) : EState := RawState state. -Coercion EState_of_State : State >-> EState. - -(* Creates an empty state, keeping the function information around. It is -used to create the initial state for a sub-function call. *) -Definition reset_local (now: State) : State := - mkState _ Empty (FuncState now). - -Fixpoint prepare_call_state (now: EState) - (arguments: list Value.t) - (parameters: list (string * Typ.t)) : option EState := - match (arguments, parameters) with - | (nil, nil) => Some now - | (v :: arguments, ((name, _) :: parameters)) => - prepare_call_state (SMap.add name v now) arguments parameters - | (_, _) => None -end. - -Lemma prepare_call_state_length: forall now arguments parameters after, - prepare_call_state now arguments parameters = Some after -> - List.length arguments = List.length parameters. -Proof. -intros now arguments; revert now. -induction arguments as [ | arg arguments hi]; - intros now [ | [? name] parameters] - after h; simpl in *; try discriminate; [ reflexivity | ]. -now rewrite (hi _ _ _ h). -Qed. - -Lemma prepare_call_state_same_length: forall now arguments parameters, - List.length arguments = List.length parameters -> - exists after, prepare_call_state now arguments parameters = Some after. -Proof. -intros now arguments; revert now. -induction arguments as [ | arg arguments hi]; intros now [ | [name ?] params] - hlen; simpl in *; try discriminate. -- now exists now. -- injection hlen; intros; subst; clear hlen. - eapply hi in H as [after h]. - now exists after; exact h. -Qed. - -(** * Continuations - -Type of continuation, to deal with the execution flow. -- <> means that there is nothing left to execute. -- <> is the sequence operator. When the current statement is - evaluated, continue the evaluation with <> and then with <>. -- <> means that we are currently evaluating - a while loop. The payload will drive what happens when we reach the end - of the loop or a control operator. Once the loop is done, continue with - <>. -- <> means that we are executing a - sub-routine/function. Before the call, the current state was <>. - Once the call returns, the output value (if any) will be stored in - the <> identifier (if any). - execution then resumes using the <> continuation. -*) -Inductive Cont := - | KStop: Cont - | KSeq: Statement.t -> Cont -> Cont - | KWhile: forall (test: Expression.t) (body orelse: Statement.t) (k: Cont), - Cont - | KCall: forall (call_state: State) - (target: option (Lvalue.t * Typ.t)) - (k: Cont), - Cont -. - -(** * Single Step Semantic - - <> means that in the <> <>, the - statement <> with contiuation <> will - evaluation in the statement <> with continuation <>. As a - result the new evaluation <> is <>. -*) -Inductive sss: State -> Statement.t -> Cont -> - State -> Statement.t -> Cont -> Prop := - | sssAssign: forall (state: State) id annotation value k v, - eval state value = Some v -> - sss state (Statement.Assign (Lvalue.Id id) annotation value) k - (set state id v) Statement.Pass k - (* executing a function call yield a fresh new state (and the current - one is stored in the <> continuation *) - | sssCallFun: forall (state: State) id annotation callee arguments func k - (vargs: Value.tlist) call_state, - get_info state callee = Some func -> - eval_list state (from_list (List.map snd arguments)) = Some vargs -> - prepare_call_state Empty vargs (parameters func) = Some call_state -> - sss - state - (Statement.Call (Some (id, annotation)) (Expression.Id callee) arguments) - k - (mkState _ call_state (FuncState state)) - (body func) - (KCall state (Some (id, return_annotation func)) k) - (* executing a procedure call yield a fresh new state (and the current - one is stored in the <> continuation *) - | sssCallProc: forall (state: State) callee arguments func k - (vargs: Value.tlist) call_state, - get_info state callee = Some func -> - eval_list state (from_list (List.map snd arguments)) = Some vargs -> - prepare_call_state Empty vargs (parameters func) = Some call_state -> - sss - state - (Statement.Call None (Expression.Id callee) arguments) - k - (mkState _ call_state (FuncState state)) - (body func) - (KCall state None k) - | sssReturnFun: forall (state call_state: State) ret id annotation k vret, - eval state ret = Some vret -> - sss state (Statement.Return ret) (KCall call_state (Some (Lvalue.Id id, annotation)) k) - (set call_state id vret) Statement.Pass k - | sssReturnProc: forall (state call_state: State)ret k, - sss state (Statement.Return ret) (KCall call_state None k) - call_state Statement.Pass k - | sssReturnWhile: forall state test body orelse k ret, - sss state (Statement.Return ret) (KWhile test body orelse k) - state (Statement.Return ret) k - | sssReturnSeq: forall state st k ret, - sss state (Statement.Return ret) (KSeq st k) - state (Statement.Return ret) k - (* if some `Return` is spotted at toplevel (outside any function), - we transition to the standard "exit" state: Pass/KStop *) - | sssReturnStop: forall state ret, - sss state (Statement.Return ret) KStop - state Statement.Pass KStop - | sssPassProc: forall (state call_state: State) k, - sss state Statement.Pass (KCall call_state None k) - call_state Statement.Pass k - | sssExpression : forall (state: State) expr v k, - eval state expr = Some v -> - sss state (Statement.Expression expr) k state Statement.Pass k - | sssSeq: forall state st0 st1 k, - sss state (Statement.Seq st0 st1) k state st0 (KSeq st1 k) - | sssPassSeq: forall state st k, - sss state Statement.Pass (KSeq st k) state st k - | sssWhileTrue: forall (state: State) test body orelse k, - eval state test = Some (Value.Boolean true) -> - sss state (Statement.While test body orelse) k - state body (KWhile test body orelse k) - | sssWhileFalse: forall (state: State) test body orelse k, - eval state test = Some (Value.Boolean false) -> - sss state (Statement.While test body orelse) k - state orelse k - | sssPassWhileTrue: forall (state: State) test body orelse k, - eval state test = Some (Value.Boolean true) -> - sss state Statement.Pass (KWhile test body orelse k) - state body (KWhile test body orelse k) - | sssPassWhileFalse: forall (state: State) test body orelse k, - eval state test = Some (Value.Boolean false) -> - sss state Statement.Pass (KWhile test body orelse k) - state orelse k - | sssIfTrue: forall test body orelse (state: State) k, - eval state test = Some (Value.Boolean true) -> - sss state (Statement.If test body orelse) k - state body k - | sssIfFalse: forall test body orelse (state: State) k, - eval state test = Some (Value.Boolean false) -> - sss state (Statement.If test body orelse) k - state orelse k -. - -(** Multi step version of sss *) -Inductive sssn: State -> Statement.t -> Cont -> - State -> Statement.t -> Cont -> Prop := - | sss_refl: forall state st k, sssn state st k state st k - | sss_trans: forall state st k state' st' k' state'' st'' k'', - sss state st k state' st' k' -> - sssn state' st' k' state'' st'' k'' -> - sssn state st k state'' st'' k'' -. - -Hint Constructors sss sssn : core. - -Lemma sssn_step: forall state st k state' st' k', - sss state st k state' st' k' -> - sssn state st k state' st' k'. -Proof. -intros ? ? ? ? ? ? h. -eapply sss_trans; [now apply h | now apply sss_refl ]. -Qed. - -Lemma sssn_trans: forall state st k state' st' k' state'' st'' k'', - sssn state st k state' st' k' -> - sssn state' st' k' state'' st'' k'' -> - sssn state st k state'' st'' k''. -Proof. -intros s st k s' st' k' s'' st'' k'' h; revert s'' st'' k''. -induction h as [ s st k | s st k s' st' k' s'' st'' k'' h hs hi]; - intros z zt l;[ now idtac | ]; intro h''. -eapply sss_trans; [ now apply h | ]. -now apply hi. -Qed. - -(* begin hide *) -Module Test. -(* Toy examples to convince myself that everything is correct *) -Definition XID : Lvalue.t := Lvalue.Id "x"%string. -Definition YID : Lvalue.t := Lvalue.Id "y"%string. -Definition X : Expression.t := Expression.Id "x"%string. -Definition Ret x := Statement.Return x. -(* Identity function, named "int_id", from int to int *) - -Definition int_id_parameters := ((("x"%string), Typ.Integer) :: nil). - -Definition int_id : func := mkFun "int_id"%string - int_id_parameters - Typ.Integer - (Ret X). - -Definition Int z : Expression.t := Expression.Integer z. - -(* Empty value state, with a single function defined: int_id *) -Definition test_state : State := - mkState _ Empty (SMap.add "int_id"%string int_id (SMap.empty _)). -(* Value state has a single binding: y |-> 42. Function information - is the same as test_state *) -Definition final_state : State := set test_state "y"%string (Value.Integer 42). - -(* Function call `y := int_id(42)` *) -Definition Prog := - Statement.Call (Some (YID, Typ.Integer)) - (Expression.Id "int_id"%string) - ((None, Int 42) :: nil). - -(* Proof that the program `Prog` executes correctly and updates the - initial environment `test_state` into `final_state`. *) -Lemma sss_int_id_42: - sssn test_state Prog KStop final_state Statement.Pass KStop. -Proof. -unfold Prog. -eapply sss_trans. - apply sssCallFun with (vargs := (Value.Cons (Value.Integer 42) Value.Nil)). - unfold get_info, test_state; simpl. - apply SMap.find_1. - apply SMap.add_1; reflexivity. - - simpl; now reflexivity. - - simpl; now reflexivity. - -simpl. -eapply sss_trans. - constructor. - simpl. - apply SMap.find_1. - apply SMap.add_1; reflexivity. -now apply sss_refl. -Qed. - -(* Function "expect_int" : int -> void *) -Definition expect_int : func := mkFun "expect_int"%string - int_id_parameters (* we use the same list of parameters *) - Typ.None - Statement.Pass. - -(* New test state: Empty value state and a single function definition: - expect_int *) -Definition test_state2 : State := - mkState _ Empty (SMap.add "expect_int"%string expect_int (SMap.empty _)). - -(* Function call `expect_int(1664)` *) -Definition Prog2 := - Statement.Call None - (Expression.Id "expect_int"%string) - ((None, Int 1664) :: nil). - -(* Proof that the program `Prog2` executes correctly and do not modify its - initial environment `test_state2`. *) -Lemma sss_expect_int: - sssn test_state2 Prog2 KStop test_state2 Statement.Pass KStop. -Proof. -unfold Prog2. -eapply sss_trans. - apply sssCallProc with (vargs := Value.Cons (Value.Integer 1664) Value.Nil). - apply SMap.find_1. - apply SMap.add_1; reflexivity. - - simpl; now reflexivity. - - simpl; now reflexivity. -simpl. -eapply sss_trans. - now constructor. -now apply sss_refl. -Qed. - -Lemma WhileFalse: forall s body orelse k, - sssn s (Statement.While Expression.False_ body orelse) k s orelse k. -Proof. -intros s body orelse k. -eapply sss_trans. -now apply sssWhileFalse. -now apply sss_refl. -Qed. - -End Test. -(* end hide *) - -(** Single Step Semantic is a deterministic relation *) -Lemma sss_determinist: forall s0 st0 k0 s1 st1 k1 s2 st2 k2, - sss s0 st0 k0 s1 st1 k1 -> - sss s0 st0 k0 s2 st2 k2 -> - (s1 = s2 /\ st1 = st2 /\ k1 = k2). -Proof. -intros s0 st0 k0 s1 st1 k1 s2 st2 k2 h; revert s2 st2 k2. -destruct h as [ - s id annotation value k v hvalue - | s id annotation callee arguments func k vargs cstate hf heval hstate - | s callee arguments func k vargs cstate hf heval hstate - | s s' ret id annotation k vret heval - | s s' ret k - | s test body orelse k ret - | s st k ret - | s ret - | s s' k - | s expr v k heval - | s st0 st1 k - | s st k - | s test body orelse k - | s test body orelse k - | s test body orelse k - | s test body orelse k - | test body orelse s k heval - | test body orelse s k -]; intros s2 st2 k2 h; try now inversion h. -- inversion h; subst; clear h. - rewrite hvalue in H7; injection H7; intros; subst. - now split. -- inversion h; subst; clear h. - rewrite hf in H8; injection H8; clear H8; intros; subst. - rewrite heval in H9; injection H9; clear H9; intros; subst. - now rewrite hstate in H10; injection H10; clear H10; intros; subst. -- inversion h; subst; clear h. - rewrite hf in H1; injection H1; clear H1; intros; subst. - rewrite heval in H3; injection H3; clear H3; intros; subst. - now rewrite hstate in H8; injection H8; clear H8; intros; subst. -- inversion h; subst; clear h. - now rewrite heval in H8; injection H8; intros; subst. -- inversion h; subst; clear h; [now idtac | ]. - now rewrite H in H8; discriminate H8. -- inversion h; subst; clear h; [ | now idtac ]. - now rewrite H in H8; discriminate H8. -- inversion h; subst; clear h; [ now idtac | ]. - now rewrite H in H8; injection H8; intros; subst. -- inversion h; subst; clear h; [ | now idtac]. - now rewrite H in H8; injection H8; intros; subst. -- inversion h; subst; clear h; [ now idtac | ]. - now rewrite heval in H7; injection H7; intros; subst. -- inversion h; subst; clear h; [ | now idtac ]. - now rewrite H in H8; injection H8; intros; subst. -Qed. diff --git a/documentation/website/docs/formal/python_semantic/Expression.v b/documentation/website/docs/formal/python_semantic/Expression.v deleted file mode 100644 index 568f6c2daf1..00000000000 --- a/documentation/website/docs/formal/python_semantic/Expression.v +++ /dev/null @@ -1,90 +0,0 @@ -Require Import ZArith List String. - -(** * Operators *) -(** Boolean operators *) -Inductive boolean_operator := - | And - | Or -. - -(** Comparison operators - Currently <> and <> are not supported -*) -Inductive comparison_operator := - | Equals - | GreaterThan - | GreaterThanOrEquals - | In - | Is - | IsNot - | LessThan - | LessThanOrEquals - | NotEquals - | NotIn -. - -(** Unary operators *) -Inductive unary_operator := - | Invert - | Negative - | Not - | Positive. - -(** * Expressions - More will be added later. See - https://github.com/facebook/pyre-check/blob/main/ast/expression.mli#L216 -*) -Inductive t: Set := - | BooleanOperator: forall (left: t) (op: boolean_operator) (right: t), t - | ComparisonOperator: forall (left: t) (op: comparison_operator) (right: t), t - | False_: t - | Integer: Z -> t - | List: tlist -> t - | Id: string -> t - | None: t - | String: string -> t - | Ternary: forall (target: t) (test: t) (alternative: t), t - | True_: t - | Tuple: tlist -> t - | UnaryOperator: unary_operator -> t -> t -with tlist: Set := - | Nil: tlist - | Cons: t -> tlist -> tlist -. - -(* begin hide *) -Hint Constructors t tlist : core. - -Scheme expr_ind' := Induction for t Sort Prop - with expr_list_ind' := Induction for tlist Sort Prop. - -Combined Scheme expression_ind from expr_ind', expr_list_ind'. - -Module ListHelpers. -Fixpoint to_list (l: tlist) : list t := - match l with - | Nil => nil - | Cons hd tl => hd :: to_list tl - end. - -Fixpoint from_list (l: list t) : tlist := - match l with - | nil => Nil - | hd :: tl => Cons hd (from_list tl) - end. - -Lemma to_list_cancel: forall (l: tlist), from_list (to_list l) = l. -Proof. -induction l as [ | hd tl hi]; simpl in *; [ now idtac | ]. -now rewrite hi. -Qed. - -Lemma from_list_cancel: forall (l: list t), to_list (from_list l) = l. -Proof. -induction l as [ | hd tl hi]; simpl in *; [ now idtac | ]. -now rewrite hi. -Qed. - -Coercion to_list: tlist >-> list. -End ListHelpers. -(* end hide *) diff --git a/documentation/website/docs/formal/python_semantic/Lib/List.v b/documentation/website/docs/formal/python_semantic/Lib/List.v deleted file mode 100644 index 606068f6101..00000000000 --- a/documentation/website/docs/formal/python_semantic/Lib/List.v +++ /dev/null @@ -1,23 +0,0 @@ -Require Import List Sorted. -Import ListNotations. - -(** Facts about HdRel and Forall *) -Section HdRelFacts. -Variable A: Type. -Variable R: A -> A -> Prop. -Hypothesis Rtrans : forall x y z, R x y -> R y z -> R x z. - -Lemma HdRel_Forall: forall l x, - Sorted R l -> - HdRel R x l -> Forall (R x) l. -Proof. -induction l as [ | hd tl hi]; intros x hs h; simpl in *; [ now constructor | ]. -apply HdRel_inv in h. -constructor; [ assumption | ]. -apply Sorted_inv in hs as [ h0 h1]. -apply hi; [assumption |]. -destruct tl; [ now constructor | constructor]. -apply HdRel_inv in h1. -now apply (Rtrans x hd a). -Qed. -End HdRelFacts. diff --git a/documentation/website/docs/formal/python_semantic/Lib/String.v b/documentation/website/docs/formal/python_semantic/Lib/String.v deleted file mode 100644 index a73d4609106..00000000000 --- a/documentation/website/docs/formal/python_semantic/Lib/String.v +++ /dev/null @@ -1,51 +0,0 @@ -Require Import String. -Require Import OrderedType OrderedTypeEx. - -(* Wrapper around String_as_OT *) -Module String_facts := OrderedTypeFacts(String_as_OT). - -Definition lt (s1 s2: string) : Prop := String_as_OT.lt s1 s2. - -Definition ltb (s1 s2: string) : bool := - match String_facts.lt_dec s1 s2 with - | left _ => true - | right _ => false -end. - -Lemma ltb_lt: forall s1 s2, lt s1 s2 <-> ltb s1 s2 = true. -Proof. -unfold lt, ltb. -intros s1 s2; split; intro h. -- destruct String_facts.lt_dec as [ hdec | hdec ]; [ reflexivity | ]. - now elim hdec. -- destruct String_facts.lt_dec as [ hdec | hdec ]; [ | discriminate ]. - assumption. -Qed. - -Lemma ltb_nlt: forall s1 s2, (~ lt s1 s2) <-> ltb s1 s2 = false. -Proof. -intros s1 s2; split; intro h. -- destruct (ltb_lt s1 s2) as [h1 h2]. - destruct (ltb s1 s2); [ | reflexivity ]. - now elim (h (h2 refl_equal)). -- destruct (ltb_lt s1 s2) as [h1 h2]. - intro hlt. - apply h1 in hlt. - rewrite h in hlt. - discriminate. -Qed. - -Definition lt_trans := String_as_OT.lt_trans. - -Lemma lt_ge: forall x y:string, ltb x y = false -> ltb y x = true \/ x = y. -Proof. -intros x y hltb. -destruct (String_facts.lt_total x y) as [h | [h | h]]. -- apply ltb_lt in h. - now rewrite h in hltb; discriminate. -- now subst; right. -- apply ltb_lt in h. - now left. -Qed. - -Definition lt_not_eq := String_as_OT.lt_not_eq. diff --git a/documentation/website/docs/formal/python_semantic/Lvalue.v b/documentation/website/docs/formal/python_semantic/Lvalue.v deleted file mode 100644 index 3a24159d6e5..00000000000 --- a/documentation/website/docs/formal/python_semantic/Lvalue.v +++ /dev/null @@ -1,8 +0,0 @@ -Require Import String. - -(** Lvalues - Currently we only support simple variables. -*) -Inductive t : Set := - | Id : string -> t -. diff --git a/documentation/website/docs/formal/python_semantic/Makefile b/documentation/website/docs/formal/python_semantic/Makefile deleted file mode 100644 index bfe56ac8a2e..00000000000 --- a/documentation/website/docs/formal/python_semantic/Makefile +++ /dev/null @@ -1,40 +0,0 @@ -EXTRA_DIR:=extra -COQDOCFLAGS:= \ - --external 'http://ssr2.msr-inria.inria.fr/doc/ssreflect-1.5/' Ssreflect \ - --external 'http://ssr2.msr-inria.inria.fr/doc/mathcomp-1.5/' MathComp \ - --toc --toc-depth 2 --html --interpolate \ - --index indexpage --no-lib-name --parse-comments \ - --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html -export COQDOCFLAGS -COQMAKEFILE:=Makefile.coq -COQ_PROJ:=_CoqProject -VS:=$(wildcard *.v) -VS_IN_PROJ:=$(shell grep .v $(COQ_PROJ)) - -ifeq (,$(VS_IN_PROJ)) -VS_OTHER := $(VS) -else -VS := $(VS_IN_PROJ) -endif - -all: html - -clean: $(COQMAKEFILE) - @$(MAKE) -f $(COQMAKEFILE) $@ - rm -f $(COQMAKEFILE) - rm -f $(COQMAKEFILE).conf - find . -name "*.aux" -delete - -html: $(COQMAKEFILE) $(VS) - rm -fr html - @$(MAKE) -f $(COQMAKEFILE) $@ - cp $(EXTRA_DIR)/resources/* html - -$(COQMAKEFILE): $(COQ_PROJ) $(VS) - coq_makefile -f $(COQ_PROJ) $(VS_OTHER) -o $@ - -%: $(COQMAKEFILE) force - @$(MAKE) -f $(COQMAKEFILE) $@ -force $(COQ_PROJ) $(VS): ; - -.PHONY: clean all force diff --git a/documentation/website/docs/formal/python_semantic/Map.v b/documentation/website/docs/formal/python_semantic/Map.v deleted file mode 100644 index ececb1ab2e6..00000000000 --- a/documentation/website/docs/formal/python_semantic/Map.v +++ /dev/null @@ -1,83 +0,0 @@ -From Coq Require Import Structures.OrderedTypeEx. -From Coq Require Import FMapList. -From Coq Require Import String. -From Pyre Require Typ Statement. - -Module SMap := FMapList.Make(String_as_OT). - -(** * Information about function definitions - -We store in here all relevant information about known functions: -- their <>. -- their signature, as a list of <> and a <>. -- the actual <> statement of the function. -*) -Record func : Set := mkFun { - (* TODO(T53097965): support dotted access for methods *) - name: string; - (* TODO(T53097965): support more parameter kinds *) - parameters: list (string * Typ.t); - (* decorators: Expression.t list; *) - return_annotation: Typ.t; (* no option, set to TNone if need be *) - (* async: bool; *) - (* parent: Reference.t option; (1* The class owning the method. *1) *) - body: Statement.t; -}. - -(** Global state for the statement operational semantic. It is made of -the state for expression evaluation, along with information about know -functions. *) -Record State {A: Set} := mkState { - RawState :> SMap.t A; - FuncState : SMap.t func -}. - -Definition set {A: Set} (state: @State A) (id: string) (v: A) := - mkState _ (SMap.add id v state) (FuncState state). - -Definition remove {A: Set} (state : @State A) (id: string) : @State A := - mkState _ (SMap.remove id state) (FuncState state). - - -Definition get_info {A: Set} (state: @State A) (fun_name: string) : option func := - SMap.find fun_name (FuncState state). - -From Coq Require Import FMapFacts. - -Module SMapFacts := WFacts (SMap). - -Lemma find_add_smap: forall {A: Set} (state : SMap.t A) (x y: string) (v : A), - SMap.find y (SMap.add x v state) = - if (y =? x)%string then Some v else SMap.find y state. -Proof. -intros A state x y v. -case_eq (String.eqb y x); intro hyx. -- apply SMapFacts.add_eq_o. - apply String.eqb_eq in hyx; rewrite hyx; reflexivity. -- apply SMapFacts.add_neq_o. - apply String.eqb_neq in hyx. - firstorder. -Qed. - -Lemma find_add: forall {A: Set} (state : @State A) (x y: string) (v : A), - SMap.find y (set state x v) = - if (y =? x)%string then Some v else SMap.find y state. -Proof. -intros A state x y v. -unfold set; simpl. -rewrite find_add_smap. -reflexivity. -Qed. - -Lemma find_remove_smap: forall {A : Set} (state: @SMap.t A) (x z: string), - SMap.find z (SMap.remove x state) = - if (z =? x)%string then None else SMap.find z state. -Proof. -intros A state x z. -case_eq (String.eqb z x); intro hzx. -- apply SMapFacts.remove_eq_o. - apply String.eqb_eq in hzx; rewrite hzx; reflexivity. -- apply SMapFacts.remove_neq_o. - apply String.eqb_neq in hzx. - firstorder. -Qed. diff --git a/documentation/website/docs/formal/python_semantic/README b/documentation/website/docs/formal/python_semantic/README deleted file mode 100644 index 755a6021471..00000000000 --- a/documentation/website/docs/formal/python_semantic/README +++ /dev/null @@ -1,8 +0,0 @@ -Setup: - -This project is developed using Coq 8.10. -You can install it using `opam2`: -- opam switch create coq ocaml-base-compiler.4.08.1 -- eval $(opam env) -- opam install coq # should be 8.10 as the time of writing -- make diff --git a/documentation/website/docs/formal/python_semantic/Semantic.v b/documentation/website/docs/formal/python_semantic/Semantic.v deleted file mode 100644 index 166ca23f254..00000000000 --- a/documentation/website/docs/formal/python_semantic/Semantic.v +++ /dev/null @@ -1,1420 +0,0 @@ -Require Import List ZArith String. -Require Pyre.Lvalue. -Require Pyre.Value. -Require Pyre.Expression. -Require Import Pyre.Eval. -Require Pyre.Statement. -Require Pyre.Typ. -Require Import Pyre.Map. - -Import Pyre.Value.ListHelpers. -Import Pyre.Typ.ListHelpers. -Import Pyre.Expression.ListHelpers. - -(** * Typing judgements *) - -(** Typing context (Map from identifiers to types). - The bool parameter is only used in the typing of - Statement.t -*) -Definition TContext := SMap.t (bool * Typ.t). -Definition Empty : TContext := SMap.empty _. -Section TypingExpression. - -Import Pyre.Expression. - -(** Typing judgement for expressions *) -Inductive ok : TContext -> Expression.t -> Typ.t -> Prop := - | typFalse: forall context, ok context False_ Typ.Boolean - | typTrue: forall context, ok context True_ Typ.Boolean - | typInteger: forall context z, ok context (Integer z) Typ.Integer - | typString: forall context str, ok context (String str) Typ.String - | typNone: forall context, ok context None Typ.None - | tyBop: forall context b0 b1 op, - ok context b0 Typ.Boolean -> - ok context b1 Typ.Boolean -> - ok context (BooleanOperator b0 op b1) Typ.Boolean - | tyCmp: forall context e0 e1 op, - ok context e0 Typ.Integer -> - ok context e1 Typ.Integer -> - ok context (ComparisonOperator e0 op e1) Typ.Boolean - | TyList: forall context (l: Expression.tlist) ty, - ok_list context l ty -> - ok context (List l) (Typ.List ty) - | TyTuple: forall context (l: Expression.tlist) lty, - ok_tuple context l lty -> - ok context (Tuple l) (Typ.Tuple lty) - | TyNot: forall context expr, - ok context expr Typ.Boolean -> - ok context (UnaryOperator Not expr) Typ.Boolean - | TyUnary: forall context expr op, - op <> Not -> - ok context expr Typ.Integer -> - ok context (UnaryOperator op expr) Typ.Integer - | TyTernary : forall context target test alternative typ, - ok context target typ -> - ok context alternative typ -> - ok context test Typ.Boolean -> - ok context (Ternary target test alternative) typ - | TyId: forall context id b T, - SMap.find id context = Some (b, T) -> - ok context (Id id) T -with ok_list: TContext -> Expression.tlist -> Typ.t -> Prop := - | tyListNil : forall context typ, ok_list context Nil typ - | tyListCons : forall context hd tl typ, - ok context hd typ -> - ok_list context tl typ -> - ok_list context (Cons hd tl) typ -with ok_tuple : TContext -> Expression.tlist -> Typ.tlist -> Prop := - | tyTupleSingl : forall context expr typ, - ok context expr typ -> - ok_tuple context (Cons expr Nil) (Typ.Cons typ Typ.Nil) - | tyTupleCons : forall context expr le typ lt, - ok context expr typ -> - ok_tuple context le lt -> - ok_tuple context (Cons expr le) (Typ.Cons typ lt) -. - -(* begin hide *) -Scheme ok_ind' := Induction for ok Sort Prop - with ok_list_ind' := Induction for ok_list Sort Prop - with ok_tuple_ind' := Induction for ok_tuple Sort Prop. - -Combined Scheme ok_induc from ok_ind', ok_list_ind', ok_tuple_ind'. - -Lemma ok_tuple_len: forall context le lt, - ok_tuple context le lt -> List.length le = List.length lt. -Proof. -intro context. -induction 1; simpl in *; now intuition. -Qed. - -Lemma ok_tuple_len_pos : forall context le lt, - ok_tuple context le lt -> List.length le > 0. -Proof. -intro context. -induction 1; simpl in *; now intuition. -Qed. - -Lemma ok_list_spec: forall context l typ, - ok_list context l typ -> Forall (fun expr => ok context expr typ) l. -Proof. -induction 1 as [ context typ | context hd tl typ h0 h1 hi ]; - [ now apply Forall_nil | ]. -now apply Forall_cons. -Qed. - -Lemma ok_list_forall: forall context (l: Expression.tlist) typ, - Forall (fun expr => ok context expr typ) l -> ok_list context l typ. -Proof. -intro context. -induction l as [ | hd tl hi]; intros typ h; inversion h; subst; clear h. -- now constructor. -- apply hi in H2. - now constructor. -Qed. - -Lemma ok_tuple_spec: forall context l lt, ok_tuple context l lt -> - List.length l > 0 /\ - List.length l = List.length lt /\ - Forall (fun et => ok context (fst et) (snd et)) (List.combine l lt). -Proof. -induction 1 as [context expr typ h | context expr typ es et h hs hi ]. -- intuition. - now apply Forall_cons. -- now simpl; intuition. -Qed. - -Lemma ok_tuple_forall: forall context (l: Expression.tlist) (lt: Typ.tlist), - List.length l > 0 -> - List.length l = List.length lt -> - Forall (fun et => ok context (fst et) (snd et)) (List.combine l lt) -> - ok_tuple context l lt. -Proof. -induction l as [ | hd tl hi]; - intros lt hp hl h; inversion h; subst; clear h; simpl in *. -- now idtac. -- destruct lt as [ | typ typs]; [now idtac | ]. - simpl in H0. - discriminate H0. -- destruct x as [v' t']; simpl in *. - destruct lt as [ | typ typs]; [now idtac | ]. - injection hl; clear hl; intro hl. - simpl in H; injection H; clear H; intros heq0 heq1; subst. - (* special case for list of size 1 *) - case_eq tl. - + intros ? h; subst. - simpl in hl. - destruct typs as [ | ]; [ | now idtac]. - now constructor. - + intros ? ? htl ?; subst. - constructor; [ now idtac | ]. - now apply hi; simpl; intuition. -Qed. - -Lemma ok_tuple_forall2: forall context (l: Expression.tlist) (lt: Typ.tlist), - List.length lt > 0 -> - List.length l = List.length lt -> - Forall (fun et => ok context (fst et) (snd et)) (List.combine l lt) -> - ok_tuple context l lt. -Proof. -intros context l lt h heq hf. -now apply ok_tuple_forall; intuition. -Qed. -(* end hide *) - -End TypingExpression. - -Hint Constructors ok ok_list ok_tuple : core. - -Section TypingValue. - -Import Value. - -(** Typing judgement for values *) -Inductive okv : Value.t -> Typ.t -> Prop := - | TyVBoolean: forall b, okv (Boolean b) Typ.Boolean - | TyVInteger: forall i, okv (Integer i) Typ.Integer - | TyVString: forall str, okv (String str) Typ.String - | TyVList: forall (l: Value.tlist) T, - okv_list l T -> - okv (Sequence l) (Typ.List T) - | TyVTuple: forall (l: Value.tlist) (lt: Typ.tlist), - okv_tuple l lt -> - okv (Sequence l) (Typ.Tuple lt) - | TyNone: okv Value.None Typ.None -with okv_list: Value.tlist -> Typ.t -> Prop := - | TyVNil: forall typ, okv_list Nil typ - | TyVCons: forall hd tl typ, - okv hd typ -> - okv_list tl typ -> - okv_list (Cons hd tl) typ -with okv_tuple: Value.tlist -> Typ.tlist -> Prop := - | TyVSingle: forall expr typ, - okv expr typ -> - okv_tuple (Cons expr Nil) (Typ.Cons typ Typ.Nil) - | TyVTuples: forall expr typ es typs, - okv expr typ -> - okv_tuple es typs -> - okv_tuple (Cons expr es) (Typ.Cons typ typs) -. - -(* begin hide *) -Lemma okv_list_spec: forall lv typ, okv_list lv typ -> - Forall (fun v => okv v typ) lv. -Proof. -induction 1 as [ | hd tl typ h0 h1 hi ]; [ now apply Forall_nil | ]. -now apply Forall_cons. -Qed. - -Lemma okv_list_forall: forall (lv: Value.tlist) typ, - Forall (fun v => okv v typ) lv -> okv_list lv typ. -Proof. -induction lv as [ | hd tl hi]; intros typ h; inversion h; subst; clear h. -- now constructor. -- apply hi in H2. - now constructor. -Qed. - -Lemma okv_tuple_spec: forall lv lt, okv_tuple lv lt -> - List.length lv > 0 /\ - List.length lv = List.length lt /\ - Forall (fun vt => okv (fst vt) (snd vt)) (List.combine lv lt). -Proof. -induction 1 as [ expr typ h | expr typ es et h hs hi ]. -- intuition. - now apply Forall_cons. -- now simpl; intuition. -Qed. - -Lemma okv_tuple_forall: forall (lv: Value.tlist) (lt: Typ.tlist), - List.length lv > 0 -> - List.length lv = List.length lt -> - Forall (fun vt => okv (fst vt) (snd vt)) (List.combine lv lt) -> - okv_tuple lv lt. -Proof. -induction lv as [ | hd tl hi]; - intros lt hp hl h; inversion h; subst; clear h; simpl in *. -- now idtac. -- destruct lt as [ | typ typs]; [now idtac | ]. - simpl in H0. - discriminate H0. -- destruct x as [v' t']; simpl in *. - destruct lt as [ | typ typs]; [now idtac | ]. - injection hl; clear hl; intro hl. - simpl in H; injection H; clear H; intros heq0 heq1; subst. - (* special case for list of size 1 *) - case_eq tl. - + intros ? h; subst. - simpl in hl. - destruct typs as [ | ]; [ | now idtac]. - now constructor. - + intros ? ? htl ?; subst. - constructor; [ now idtac | ]. - now apply hi; simpl; intuition. -Qed. - -Lemma okv_tuple_forall2: forall (lv: Value.tlist) (lt: Typ.tlist), - List.length lt > 0 -> - List.length lv = List.length lt -> - Forall (fun vt => okv (fst vt) (snd vt)) (List.combine lv lt) -> - okv_tuple lv lt. -Proof. -intros lv lt h heq hf. -now apply okv_tuple_forall; intuition. -Qed. -(* end hide *) - -End TypingValue. - -Hint Constructors okv okv_list okv_tuple : core. - -(** Well-formed <> w.r.t. some <>: - for any typed variable in the context, there must be a value of the - right type associated to in the the state. *) -Definition well_formed_estate (state : EState) (context: TContext) : Prop := - (forall k b T, SMap.find k context = Some (b, T) -> - exists v, SMap.find k state = Some v /\ okv v T) -. - -(* begin hide *) -Lemma well_formed_estate_get: forall state context, - well_formed_estate state context -> - forall id b T, SMap.find id context = Some (b, T) -> - exists v, SMap.find id state = Some v /\ okv v T. -Proof. -intros s context hwf k T. -now apply hwf. -Qed. - -Lemma ty_bool_int : forall context expr typ, ok context expr typ -> - forall state, well_formed_estate state context -> - (typ = Typ.Boolean -> exists b, eval state expr = Some (Value.Boolean b)) /\ - (typ = Typ.Integer -> exists z, eval state expr = Some (Value.Integer z)). -Proof. -induction 1 as [ - | context - | context z - | context str - | context - | context left right op hl hil hr hir - | context left right op hl hil hr hir - | context l typ hl - | context l typs hl - | context expr he hie - | context expr op hop he hie - | context target test alterntaive typ htarget hitarget - halt hialt htest hitest - | context id b T h -]; intros state hwf; subst; split; intro heq; subst; - try discriminate; simpl in *. -+ now exists false. -+ now exists true. -+ now exists z. -+ destruct (hil state hwf) as [h0 _]. - destruct (hir state hwf) as [h1 _]. - destruct (h0 refl_equal) as [x0 hx0]. - destruct (h1 refl_equal) as [x1 hx1]. - rewrite hx0, hx1. - now exists (evaluate_boolean_operator x0 op x1). -+ destruct (hil state hwf) as [_ h0]. - destruct (hir state hwf) as [_ h1]. - destruct (h0 refl_equal) as [x0 hx0]. - destruct (h1 refl_equal) as [x1 hx1]. - rewrite hx0, hx1. - now exists (evaluate_comparison_operator (Value.Integer x0) op (Value.Integer x1)). -+ destruct (hie state hwf) as [h0 _]. - destruct (h0 refl_equal) as [ x0 hx0 ]. - rewrite hx0. - now exists (negb x0). -+ destruct (hie state hwf) as [_ h0]. - destruct (h0 refl_equal) as [ x0 hx0 ]. - rewrite hx0; simpl. - rewrite evaluate_unary_int_operator; destruct op; try (now elim hop). - * now exists (-x0 -1)%Z. - * now exists ( - x0 )%Z. - * now exists x0. -+ destruct (hitarget state hwf) as [h0 _]. - destruct (hialt state hwf) as [h1 _]. - destruct (hitest state hwf) as [h2 _]. - destruct (h0 refl_equal) as [x0 hx0]. - destruct (h1 refl_equal) as [x1 hx1]. - destruct (h2 refl_equal) as [x2 hx2]. - rewrite hx2; destruct x2. - * rewrite hx0. - now exists x0. - * rewrite hx1. - now exists x1. -+ destruct (hitarget state hwf) as [_ h0]. - destruct (hialt state hwf) as [_ h1]. - destruct (hitest state hwf) as [h2 _]. - destruct (h0 refl_equal) as [x0 hx0]. - destruct (h1 refl_equal) as [x1 hx1]. - destruct (h2 refl_equal) as [x2 hx2]. - rewrite hx2; destruct x2. - * rewrite hx0. - now exists x0. - * rewrite hx1. - now exists x1. -+ apply well_formed_estate_get with (state := state) in h; [ | now idtac ]. - destruct h as [ v [-> hv]]. - inversion hv; subst; clear hv. - now exists b0. -+ apply well_formed_estate_get with (state := state) in h; [ | now idtac ]. - destruct h as [ v [-> hv]]. - inversion hv; subst; clear hv. - now exists i. -Qed. -(* end hide *) - -(** Every expression typed as <> must be an actual <> *) -Lemma ty_bool : forall context expr, ok context expr Typ.Boolean -> - forall state, well_formed_estate state context -> - exists b, eval state expr = Some (Value.Boolean b). -Proof. -intros context expr h s hwf; eapply ty_bool_int in h as [ h0 _]. -- now apply h0. -- now apply hwf. -Qed. - -(** Every expression typed as <> must be an actual <> *) -Lemma ty_int : forall context expr, ok context expr Typ.Integer -> - forall state, well_formed_estate state context -> - exists z, eval state expr = Some (Value.Integer z). -Proof. -intros context expr h s hwf; eapply ty_bool_int in h as [ _ h0]. -- now apply h0. -- now apply hwf. -Qed. - -(* begin hide *) -Lemma ty_string_ : forall context expr typ, ok context expr typ -> - typ = Typ.String -> - forall state, well_formed_estate state context -> - exists str, eval state expr = Some (Value.String str). -Proof. -induction 1 as [ - | context - | context z - | context str - | context - | context left right op hl hil hr hir - | context left right op hl hil hr hir - | context l typ hl - | context l typs hl - | context expr he hie - | context expr op hop he hie - | context target test alterntaive typ htarget hitarget - halt hialt htest hitest - | context id b T h -] ; intros heq state hwf; subst; try discriminate; simpl in *. -- now exists str. -- apply ty_bool with (state := state) in htest as [ b hb ];[ | now idtac ]. - rewrite hb. - destruct (hitarget refl_equal state hwf) as [s1 hs1]. - destruct (hialt refl_equal state hwf) as [s2 hs2]. - rewrite hs1, hs2. - destruct b. - + now exists s1. - + now exists s2. -- apply well_formed_estate_get with (state := state) in h; [ | now idtac]. - destruct h as [v [-> hv]]. - inversion hv; subst; clear hv. - now exists str. -Qed. -(* end hide *) - -(** Every expression typed as <> must be an actual <> *) -Lemma ty_string : forall context expr, ok context expr Typ.String -> - forall state, well_formed_estate state context -> - exists str, eval state expr = Some (Value.String str). -Proof. -intros context expr h state hwf. -now apply ty_string_ with (context := context) (state := state) in h. -Qed. - -(* begin hide *) -Lemma ty_none_: forall context expr typ, ok context expr typ -> - typ = Typ.None -> forall state, well_formed_estate state context -> - eval state expr = Some Value.None. -Proof. -induction 1 as [ - | context - | context z - | context str - | context - | context left right op hl hil hr hir - | context left right op hl hil hr hir - | context l typ hl - | context l typs hl - | context expr he hie - | context expr op hop he hie - | context target test alterntaive typ htarget hitarget - halt hialt htest hitest - | context id b T h -] ; intros heq state hwf; subst; try discriminate; simpl in *. -- reflexivity. -- apply ty_bool with (state := state) in htest as [ b hb ];[ | now idtac ]. - rewrite hb. - rewrite (hitarget refl_equal state hwf). - rewrite (hialt refl_equal state hwf). - now destruct b. -- apply well_formed_estate_get with (state := state) in h; [ | now idtac]. - destruct h as [v [-> hv]]. - inversion hv; subst; clear hv. - reflexivity. -Qed. -(* end hide *) - -(** Every expression typed as <> must be <> *) -Lemma ty_none: forall context expr, ok context expr Typ.None -> - forall state, well_formed_estate state context -> - eval state expr = Some Value.None. -Proof. -intros context expr h state hwf. -now apply ty_none_ with (context := context) (state := state) in h. -Qed. - -Definition is_sequence (typ : Typ.t) : option Typ.t := - match typ with - | Typ.List T => Some T - | _ => None - end. - -Definition is_tuple (typ : Typ.t) : list Typ.t := - match typ with - | Typ.Tuple l => l - | _ => nil -end. - -Section TypingStatement. - -Import Pyre.Statement. - -(* TODO(T53097965): - use the strings in a correct way. For the moment they are totally - discarded and I consider that the order of arguments matches the - the order of parameters: we only consider positional arguments. - *) - -(** Takes a list of arguments and a list of function parameter definitions - and (pairwise) checks that expressions are typed with the corresponding type, - in context <>. *) -Fixpoint check_arguments context (arguments: list (option string * Expression.t)) - (parameters: list (string * Typ.t)) : Prop := - match (arguments, parameters) with - | ((_, arg) :: arguments, (_, ty) :: parameters) => - ok context arg ty /\ check_arguments context arguments parameters - | (nil, nil) => True - | _ => False - end. - -Lemma check_arguments_length: forall context arguments parameters, - check_arguments context arguments parameters -> - List.length arguments = List.length parameters. -Proof. -intro context; induction arguments as [| [ ? arg] arguments hi]; - intros [| [name ?] parameters] h; simpl in *; try now elim h. -destruct h as [hok hc]. -now rewrite (hi _ hc). -Qed. - -(** Helper to prepare the typing context of sub-routine/function calls *) -Fixpoint prepare_call_context (now: TContext) - (parameters: list (string * Typ.t)) : TContext := - match parameters with - | nil => now - | (name, ty) :: parameters => - prepare_call_context (SMap.add name (true, ty) now) parameters -end. - -(** General context for type checking statements: it is made of an expression - typing context and some information about declared function *) -Definition Context := @Map.State (bool * Typ.t). -Definition TContext_of_Context (context : Context) : TContext := RawState context. -Coercion TContext_of_Context : Context >-> TContext. - -Definition mkContext context info : Context := - mkState _ context info. - -(** Typing judgement for statements - - <> means that in the typing context <>, evaluating the - statement <> will generate the context <>. - <> is the current expected return type (or None in case of procedure / - global statement). -*) -Inductive typ : Context -> Typ.t -> Statement.t -> Context -> Prop := - | typAssignIdNone: forall (context: Context) return_type id value T, - SMap.find id context = None -> - ok context value T -> - typ context return_type - (Assign (Lvalue.Id id) None value) (set context id (false, T)) - | typAssignIdNoneWeak: forall (context: Context) return_type id value T Tid, - SMap.find id context = Some (false, Tid) -> - ok context value T -> - typ context return_type - (Assign (Lvalue.Id id) None value) (set context id (false, T)) - | typAssignIdNoneStrong: forall (context: Context) return_type id value T, - SMap.find id context = Some (true, T) -> - ok context value T -> - typ context return_type - (Assign (Lvalue.Id id) None value) (set context id (true, T)) - | typAssignIdAnnot: forall (context: Context) return_type id value T, - ok context value T -> - typ context return_type - (Assign (Lvalue.Id id) (Some T) value) (set context id (true, T)) - | typExpression: forall (context: Context) return_type expr T, - ok context expr T -> - typ context return_type (Expression expr) context - | typIf: forall (context context': Context) return_type test body orelse, - ok context test Typ.Boolean -> - typ context return_type body context' -> - typ context return_type orelse context' -> - typ context return_type (If test body orelse) context' - | tyPass: forall (context: Context) return_type, - typ context return_type Pass context - | tySeq: forall (context context' context'': Context) return_type st next, - typ context return_type st context' -> - typ context' return_type next context'' -> - typ context return_type (Seq st next) context'' - | typWhile: forall (context context': Context) return_type test body orelse, - ok context test Typ.Boolean -> - typ context return_type body context -> - typ context return_type orelse context' -> - typ context return_type (While test body orelse) context' - | typCallFun: forall (context: Context) return_type target annotation - function_name arguments function_def, - get_info context function_name = Some function_def -> - return_annotation function_def = annotation -> - check_arguments context arguments (parameters function_def) -> - typ - context - return_type - (Call (Some (Lvalue.Id target, annotation)) (Expression.Id function_name) arguments) - (set context target (true, return_annotation function_def)) - | typCallProc: forall (context: Context) return_type function_name arguments - function_def, - get_info context function_name = Some function_def -> - return_annotation function_def = Typ.None -> - check_arguments context arguments (parameters function_def) -> - typ context return_type (Call None (Expression.Id function_name) arguments) context - | typReturn: forall (context context': Context) ret T, - ok context ret T -> - typ context T (Return ret) context' -. - -(** Well-formed conditions for function definition: <> is a - set of defined functions. In this context, a function <> is - well-formed if its body is correctly typed w.r.t. its arguments types - and return annotation. *) -Definition well_formed_function function_info (f: func) : Prop := - (exists return_context, - typ (mkContext (prepare_call_context Empty (parameters f)) function_info) - (return_annotation f) - (body f) return_context) -. - -(** General well-formed statement for State/Context: - - The underlying evaluation state / typing context must be well-formed. - - They must store the same information about function definitions. - - Every function definition recorded so far must be well-formed. -*) -Definition well_formed (state: Eval.State) (context: Context) : Prop := - (* underlying states are coherent *) - well_formed_estate state context /\ - (* same function definitions in both context *) - (FuncState state = FuncState context) /\ - (* functions are correctly typed *) - (forall function_name function_def, - get_info context function_name = Some function_def -> - well_formed_function (FuncState context) function_def) -. - -(* begin hide *) -Lemma well_formed_get: forall state context, well_formed state context -> - forall id b T, SMap.find id context = Some (b, T) -> - exists v, SMap.find id state = Some v /\ okv v T. -Proof. -intros [s ?] [context ?] [hwf ?] k T h; simpl in *. -now apply hwf. -Qed. - -Lemma well_formed_info_eq: forall state context, well_formed state context -> - FuncState state = FuncState context. -Proof. -intros s context h; now apply h. -Qed. - -Lemma well_formed_function_get: forall state context, - well_formed state context -> - forall function_name function_def, - get_info context function_name = Some function_def -> - well_formed_function (FuncState context) function_def. -Proof. -intros s context h f func hg; now apply h in hg. -Qed. - -Lemma well_formed_get_info: forall state context, - well_formed state context -> - forall function_name, - get_info context function_name = get_info state function_name. -Proof. -intros s context [? [h ?]] f; unfold get_info. -now rewrite h. -Qed. - -Lemma well_formed_function_get_alt: forall state context, - well_formed state context -> - forall function_name function_def, - get_info state function_name = Some function_def -> - well_formed_function (FuncState state) function_def. -Proof. -intros s context h f func hg. -rewrite (well_formed_info_eq _ _ h). -apply well_formed_function_get with s f; intuition. -now rewrite well_formed_get_info with (state := s). -Qed. -(* end hide *) - -(** Typing judgement for continuations - - <> encodes the fact that continuation <> will correctly - execute under the context <>. The type <> is the current return - type, or Typ.None if a procedure or a global statement is involved. -*) -Inductive ktyp : Context -> Typ.t -> Cont -> Prop := - | ktypKStop : forall context return_type, - ktyp context return_type KStop - | ktypSeq: forall context context' return_type st k, - typ context return_type st context' -> - ktyp context' return_type k -> - ktyp context return_type (KSeq st k) - | ktypKWhile: forall (context context': Context) return_type test - body orelse k, - ok context test Typ.Boolean -> - typ context return_type body context -> - typ context return_type orelse context' -> - ktyp context' return_type k -> - ktyp context return_type (KWhile test body orelse k) - | ktypKCallProc: forall context call_context return_type saved_state k, - well_formed saved_state call_context -> - ktyp call_context return_type k -> - ktyp context Typ.None (KCall saved_state None k) - | ktypKCallFun: forall context call_context return_type saved_state target - annotation k, - well_formed saved_state (remove call_context target) -> - SMap.find target call_context = Some (true, annotation) -> - ktyp call_context return_type k -> - ktyp context annotation (KCall saved_state (Some (Lvalue.Id target, annotation)) k) -. - -End TypingStatement. - -Hint Constructors typ ktyp : core. - -(** * Type soundness - - Proof that a correctly typed expression always evaluate to a value, - and this value has the same type as the input expression. -*) - -Lemma eval_ok_ : - (forall context expr typ, ok context expr typ -> - forall state, well_formed_estate state context -> - exists v, eval state expr = Some v /\ okv v typ) /\ - (forall context le typ, ok_list context le typ -> - forall state, well_formed_estate state context -> - exists lv, eval_list state le = Some lv /\ - okv_list lv typ) /\ - (forall context le lt, ok_tuple context le lt -> - forall state, well_formed_estate state context -> - exists lv, eval_list state le = Some lv /\ okv_tuple lv lt). -Proof. -apply ok_induc. -(* ok *) -- intros context state hwf; subst; exists (Value.Boolean false); now split. -- intros context state hwf; subst; exists (Value.Boolean true); now split. -- intros context z state hwf; subst; exists (Value.Integer z); now split. -- intros context str state hwf; subst; exists (Value.String str); now split. -- intros context state hwf; subst; exists Value.None; now split. -- intros context b0 b1 op h0 ? h1 ? state hwf; simpl; subst. - apply ty_bool with (state := state) in h0; [ | now idtac]. - destruct h0 as [vb0 ->]. - apply ty_bool with (state := state) in h1; [ | now idtac ]. - destruct h1 as [vb1 ->]. - now eexists; split; [ reflexivity | idtac]. -- intros context e0 e1 op h0 ? h1 ? state hwf; simpl; subst. - apply ty_int with (state := state) in h0; [ | now idtac ]. - destruct h0 as [v0 ->]. - apply ty_int with (state := state) in h1; [ | now idtac ]. - destruct h1 as [v1 ->]. - now eexists; split; [ reflexivity | idtac]. -- intros context l ty h hi state hwf; simpl. - destruct (hi _ hwf) as [vl [-> h0]]. - now eexists; split; [reflexivity | constructor ]. -- intros context l ty h hi state hwf; simpl. - destruct (hi _ hwf) as [vl [-> h0]]. - now eexists; split; [reflexivity | constructor ]. -- intros context expr h hi state hwf; simpl. - apply ty_bool with (state := state) in h as [v ->]; [ | now idtac ]. - now eexists; split; [reflexivity | ]. -- intros context expr op hop h hi state hwf; simpl. - apply ty_int with (state := state) in h as [v ->]; [ | now idtac ]. - rewrite evaluate_unary_int_operator. - destruct op; try (now elim hop); now eexists; split; [reflexivity | ]. -- intros context target test alt typ htarget hitarget halt hialt htest hitest - state hwf; simpl. - apply ty_bool with (state := state) in htest as [b ->]; [ | now idtac ]. - destruct (hitarget _ hwf) as [vt [-> hvt]]. - destruct (hialt _ hwf) as [va [-> hva]]. - now destruct b; eexists; split; [ reflexivity | | reflexivity | ]. -- intros context id b typ hg state hwf; simpl. - now apply well_formed_estate_get with (context := context) (b := b); - [ now apply hwf | ]. -(* ok_list *) -- intros context typ state hwf; simpl. - now exists Value.Nil; intuition. -- intros context hd tl typ h0 hi0 h1 hi1 state hwf; simpl. - destruct (hi0 _ hwf) as [vhd [-> hv]]. - destruct (hi1 _ hwf) as [vtl [-> ht]]. - now exists (Value.Cons vhd vtl); intuition. -(* ok_tuple *) -- intros context expr typ h hi state hwf; simpl. - destruct (hi _ hwf) as [v [-> ?]]. - now exists (Value.Cons v Value.Nil); intuition. -- intros context expr el typ tl h0 hi0 h1 hi1 state hwf; simpl. - destruct (hi0 _ hwf) as [vhd [-> ?]]. - destruct (hi1 _ hwf) as [vtl [-> ?]]. - now exists (Value.Cons vhd vtl); intuition. -Qed. - -Lemma eval_ok: forall context expr typ, ok context expr typ -> - forall state, well_formed_estate state context -> - exists v, eval state expr = Some v /\ okv v typ. -Proof. -intros. -now eapply eval_ok_; eauto. -Qed. - -Lemma eval_list_ok: forall context le typ, ok_list context le typ -> - forall state, well_formed_estate state context -> - exists lv, eval_list state le = Some lv /\ okv_list lv typ. -Proof. -intros. -now eapply eval_ok_; eauto. -Qed. - -Lemma eval_tuple_ok: forall context le lt, ok_tuple context le lt -> - forall state, well_formed_estate state context -> - exists lv, eval_list state le = Some lv /\ okv_tuple lv lt. -Proof. -intros. -now eapply eval_ok_; eauto. -Qed. - -Lemma ok_sequence : forall context expr T, ok context expr T -> - forall T', is_sequence T = Some T' -> - forall state, well_formed_estate state context -> - exists lv, eval state expr = Some (Value.Sequence lv). -Proof. -induction 1 as [ - | context - | context z - | context str - | context - | context left right op hl hr - | context left right op hl hr - | context l typ hl - | context l typs hl - | context expr he - | context expr op hop he - | context target test alterntaive typ htarget hit halt hia htest hitest - | context id b T h -]; intros T' hT state hwf; simpl; subst; - try (unfold is_sequence in hT; simpl in hT; discriminate). -- apply eval_list_ok with (state := state) in hl as [lv [-> ?]]; [ | now idtac ]. - now exists lv. -- destruct (hit T' hT state hwf) as [l1 ->]. - destruct (hia T' hT state hwf) as [l2 ->]. - apply ty_bool with (state := state) in htest as [b ->]; [ | now idtac ]. - now destruct b; eexists; reflexivity. -- apply well_formed_estate_get with (state := state) in h as [v [-> h1]]; - [ | now idtac ]. - inversion h1; subst; clear h1; try discriminate; now eexists; reflexivity. -Qed. - -Lemma ty_list: forall context expr T, ok context expr (Typ.List T) -> - forall state, well_formed_estate state context -> - exists lv, eval state expr = Some (Value.Sequence lv) /\ - okv (Value.Sequence lv) (Typ.List T). -Proof. -intros context expr T hok state hwf. -apply eval_ok with (state := state) in hok; [ | now idtac]. -destruct hok as [v [-> hv]]. -inversion hv; subst; clear hv. -exists l; split; [ now idtac | ]. -now constructor. -Qed. - -(* begin hide *) -Lemma well_formed_estate_add: forall state context, - well_formed_estate state context -> - forall id b v T, okv v T -> - well_formed_estate (SMap.add id v state) (SMap.add id (b, T) context). -Proof. -intros state context hwf id b v T hok. -intros k b' S. -rewrite !find_add_smap. -destruct String.eqb. -- intro h; injection h; clear h; intros; subst. - exists v; split; [ | assumption ]. - reflexivity. -- now apply hwf. -Qed. - -Lemma well_formed_set: forall state context, - well_formed state context -> - forall id b v T, okv v T -> - well_formed (set state id v) (set context id (b, T)). -Proof. -intros state context hwf id b v T hok; split; [| split]. -- now destruct hwf; apply well_formed_estate_add. -- now apply hwf. -- intros f func; simpl. - now apply hwf. -Qed. - -(* Helper lemma to build valid context and state for prepare_call_*: - In a well_formed global context/state, if some arguments are correctly - typed, then calling prepare_call_* on a well formed context/state pair leads - to a new well formed context/state pair. - - We'll then use this function with the trival "empty" pair to build - the context/state we need for function calls *) -Lemma well_formed_estate_prepare_: - (* current context/state is well formed *) - forall current_context current_state, - well_formed_estate current_state current_context -> - (* arguments are typed by parameters *) - forall arguments parameters, - check_arguments current_context arguments parameters -> - forall value_arguments, - eval_list current_state (from_list (map snd arguments)) = Some value_arguments -> - (* updating a well formed pair leads to a new well formed pair *) - forall state context new_state, - well_formed_estate state context -> - prepare_call_state state value_arguments parameters = Some new_state -> - well_formed_estate new_state (prepare_call_context context parameters). -Proof. -intros current_context current_state hwf_current. -induction arguments as [ | [? expr] arguments hi]; - intros parameters hcheck value_arguments heval state context new_state hwf hprep; - simpl in *. -- destruct parameters as []; [ | now elim hcheck ]; simpl. - injection heval; intro; subst; clear heval; simpl in hprep. - now injection hprep; intro; subst; clear hprep. -- destruct parameters as [ | [ ? ty] parameters ]; [now elim hcheck | ]; simpl. - case_eq (eval current_state expr); - [intros v hv | intro hn; rewrite hn in heval; discriminate heval ]. - rewrite hv in heval. - case_eq (eval_list current_state (from_list (map snd arguments))); - [intros vargs hvs | intro hn; rewrite hn in heval; discriminate heval ]. - rewrite hvs in heval; injection heval; clear heval; intro hvargs; - subst; simpl. - destruct hcheck as [hok hcheck]. - simpl in hprep. - apply (hi _ hcheck _ hvs (SMap.add s v state) _); [ | assumption ]. - apply well_formed_estate_add; [ now idtac | ]. - apply eval_ok with (state := current_state) in hok; [ | now idtac ]. - destruct hok as [w [h1 h2]]. - now rewrite hv in h1; injection h1; clear h1; intro h1; subst. -Qed. - -Lemma well_formed_estate_prepare: - forall context state arguments parameters value_arguments, - well_formed_estate state context -> - check_arguments context arguments parameters -> - eval_list state (from_list (map snd arguments)) = Some value_arguments -> - forall new_state, - prepare_call_state Eval.Empty value_arguments parameters = Some new_state -> - well_formed_estate new_state (prepare_call_context Empty parameters). -Proof. -intros context state arguments parameters value_arguments hwf hcheck heval - new_state hprep. -eapply well_formed_estate_prepare_. -- now apply hwf. -- now apply hcheck. -- now apply heval. -- intros k b T h; discriminate h. -- now apply hprep. -Qed. - -Lemma well_formed_estate_add_remove: forall state context, - well_formed_estate state context -> - forall id b T, - well_formed_estate state (SMap.remove id (SMap.add id (b, T) context)). -Proof. -intros s ctx hwf id b T id' b' T'; simpl. -rewrite find_remove_smap. -case_eq (id' =? id)%string; intros heq; [ intro; discriminate | ]. -rewrite find_add_smap, heq; intro hg. -now apply hwf in hg. -Qed. -(* end hide *) - -(** * Type Preservation - - Under a well-formed context/state, if a statement and a continuation - are correctly typed, then any operational step leads to new correctly - typed statement and resolution, and the resulting states are still - well-formed. -*) -Lemma sss_preservation: forall context context' state state' stmt stmt' - k k' return_type, - typ context return_type stmt context' -> - ktyp context' return_type k -> - well_formed state context -> - sss state stmt k state' stmt' k' -> - exists ocontext ocontext' return_type', - typ ocontext return_type' stmt' ocontext' /\ - ktyp ocontext' return_type' k' /\ - well_formed state' ocontext. -Proof. -intros context context' state state' stmt stmt' k k' return_type h; - revert state state' stmt' k k'; -destruct h as [ - context return_type id expr T hget okvalue - | context return_type id expr T Tid hget okvalue - | context return_type id expr T hget okvalue - | context return_type id expr T okvalue - | context return_type expr T h - | context context' return_type test body orelse oktest hbody horlese - | context return_type - | context context' context'' return_type stmt next hst hnext - | context context' return_type test body orlelse hok hbody horelse - | context return_type target annotation f arguments func hg hret hcheck - | context return_type f arguments func hg hret hcheck - | context context' ret T hok -]; intros s s' stmt' k k' hk hwf hs. -(* Assign *) -- destruct (eval_ok _ _ _ okvalue s (proj1 hwf)) as [v [hv0 hv1]]. - inversion hs; subst; clear hs. - exists (set context id (false, T)); exists (set context id (false, T)); - exists return_type; intuition. - rewrite hv0 in H7; injection H7; clear H7; intros ?; subst. - now apply well_formed_set. -- destruct (eval_ok _ _ _ okvalue s (proj1 hwf)) as [v [hv0 hv1]]. - inversion hs; subst; clear hs. - exists (set context id (false, T)); exists (set context id (false, T)); - exists return_type; intuition. - rewrite hv0 in H7; injection H7; clear H7; intros ?; subst. - now apply well_formed_set. -- destruct (eval_ok _ _ _ okvalue s (proj1 hwf)) as [v [hv0 hv1]]. - inversion hs; subst; clear hs. - exists (set context id (true, T)); exists (set context id (true, T)); - exists return_type; intuition. - rewrite hv0 in H7; injection H7; clear H7; intros ?; subst. - now apply well_formed_set. -- destruct (eval_ok _ _ _ okvalue s (proj1 hwf)) as [v [hv0 hv1]]. - inversion hs; subst; clear hs. - exists (set context id (true, T)); exists (set context id (true, T)); - exists return_type; intuition. - rewrite hv0 in H7; injection H7; clear H7; intros ?; subst. - now apply well_formed_set. -(* Expression *) -- inversion hs; subst; clear hs. - exists context; exists context; exists return_type; now split. -(* If *) -- inversion hs; subst; clear hs. - + exists context; exists context'; exists return_type; now split. - + exists context; exists context'; exists return_type; now split. -(* Pass *) -- inversion hs; subst; clear hs. - + inversion hk; subst; clear hk. - exists call_context; exists call_context; exists return_type0; now split. - + inversion hk; subst; clear hk. - exists context; exists context'; exists return_type; now split. - + inversion hk; subst; clear hk. - exists context; exists context; exists return_type; intuition. - now apply ktypKWhile with (context' := context') (return_type := return_type). - + inversion hk; subst; clear hk. - exists context; exists context'; exists return_type; now split. -(* Seq *) -- inversion hs; subst; clear hs. - exists context; exists context'; exists return_type; intuition. - now apply ktypSeq with (context' := context'') (return_type := return_type). -(* While *) -- inversion hs; subst; clear hs. - + exists context; exists context; exists return_type; intuition. - now apply ktypKWhile with (context' := context') (return_type := return_type). - + exists context; exists context'; exists return_type; now split. -(* Call *) -- inversion hs; subst; clear hs. - unfold get_info in H8; unfold get_info in hg. - rewrite (well_formed_info_eq _ _ hwf), hg in H8; injection H8; intros; - subst; clear H8. - apply well_formed_function_get with (state := s) in hg as [fctx hf]; [| now idtac]. - exists (mkContext (prepare_call_context Empty (parameters func0)) - (FuncState context)). - exists fctx; exists (return_annotation func0); split; [ assumption | split ]. - + apply ktypKCallFun with - (call_context := set context target (true, return_annotation func0)) - (return_type := return_type); intuition. - * split; [ now apply well_formed_estate_add_remove; apply hwf | ]. - split; [ now apply hwf | ]. - intros f' func'; simpl. - now apply hwf. - * now rewrite find_add, String.eqb_refl. - + split; [ | split ]. - * eapply well_formed_estate_prepare; - [now apply hwf | now apply hcheck | now apply H9| assumption]. - * now apply hwf. - * intros f' func'; simpl. - now apply hwf. -- inversion hs; subst; clear hs. - unfold get_info in H1; unfold get_info in hg. - rewrite (well_formed_info_eq _ _ hwf), hg in H1; injection H1; intros; subst; clear H1. - apply well_formed_function_get with (state := s) in hg as [ fctx hf ]; [ | now idtac ]. - exists (mkContext (prepare_call_context Empty (parameters func0)) (FuncState context)). - rewrite hret in hf. - exists fctx; exists Typ.None; split; [ assumption | split ]. - + now apply ktypKCallProc with (call_context := context) (return_type := return_type). - + split; [ | split ]. - * eapply well_formed_estate_prepare; - [now apply hwf | now apply hcheck | now apply H3| assumption ]. - * now apply hwf. - * intros f' func'; simpl. - now apply hwf. -(* Return *) -- inversion hs; subst; clear hs. - + inversion hk; subst; clear hk. - exists call_context; exists call_context; exists return_type; - split; [now constructor | ]. - split; [assumption | ]. - destruct H5 as [hewf h]. - split; [ | now apply h]. - intros x bx Tx hx. - unfold get in H7. - generalize (hewf x bx Tx). - simpl. - rewrite find_remove_smap, find_add_smap. - case_eq (x =? id)%string; intro heq. - * intros _. - apply String.eqb_eq in heq; subst. - unfold TContext_of_Context in hx. - rewrite hx in H7; injection H7; clear H7; intro; subst. - apply eval_ok with (state := RawState s) in hok; [ | now apply hwf ]. - destruct hok as [w [hw ?]]. - unfold EState_of_State in H1. - rewrite hw in H1; injection H1; clear H1; intro; subst. - now exists vret. - * intro hg; apply hg in hx as [v [hv hv2]]. - now exists v. - + inversion hk; subst; clear hk. - exists call_context; exists call_context; exists return_type; - split; [now constructor | now split ]. - + inversion hk; subst; clear hk. - exists context; exists context'0; exists T; - split; [ now constructor | now split ]. - + inversion hk; subst; clear hk. - exists context; exists context'0; exists T; - split; [ now constructor | now split ]. - + inversion hk; subst; clear hk. - exists context; exists context; exists Typ.None; - split; [ now constructor | now split ]. -Qed. - -(** If some <> are correctly typed by some <> then - evaluating the <> leads to a list of values. *) -Lemma check_arguments_eval: forall (arguments : list (option string * Expression.t)) - state context parameters, - well_formed_estate state context -> - check_arguments context arguments parameters -> - exists value_arguments, - eval_list state (from_list (map snd arguments)) = Some value_arguments. -Proof. -induction arguments as [ | [? arg] arguments hi]; - intros state context parameters hwf hcheck; simpl in *. -- destruct parameters; [| now elim hcheck]. - now exists Value.Nil. -- destruct parameters as [ | [? ty] parameters]; [ now elim hcheck | ]; simpl in *. - destruct hcheck as [ha has]. - apply eval_ok with (state := state) in ha as [ v [-> hv]]; [ | now idtac]. - destruct (hi _ _ _ hwf has) as [vs ->]. - now exists (Value.Cons v vs). -Qed. - -(** A <> pair of statement and continuation is a situation where - there is no further possible reduction, and is considered a normal - final situation. - For the moment, we consider: - - statement == Pass and continuation == KStop: the "genuine" final state. - - statement == Pass and continuation == KCall: this one can only happen - when a return statement is missing. We can't rule it out using - typing only. We should make sure that all programs we check - have the relevant 'return' invocation in all functions. -*) -Definition done st k := - match st with - | Statement.Pass => - match k with - | KStop - | KCall _ _ _ => True - | _ => False - end - | _ => False -end. - -(** In this system, a correctly typed triple <> is either a - final (<>) configuration, or can be reduced at least one step - using the operational semantic. - - With preservation and determinism, we have the main correctness tools - for our system. *) -Lemma progress: forall context context' return_type stmt k, - typ context return_type stmt context' -> - ktyp context' return_type k -> - forall state, well_formed state context -> - (done stmt k) \/ (exists state' stmt' k', sss state stmt k state' stmt' k'). -Proof. -destruct 1 as [ - context return_type id expr T hget okvalue - | context return_type id expr T Tid hget okvalue - | context return_type id expr T hget okvalue - | context return_type id expr T okvalue - | context return_type expr T h - | context context' return_type test body orelse oktest hbody horlese - | context return_type - | context context' context'' return_type st next hst hnext - | context context' return_type test body orlelse hok hbody horelse - | context return_type target annotation function_name arguments function_def - hg hret hcheck - | context return_type function_name arguments function_def hg hret hcheck - | context context' ret T hok -]; intros hk state hwf. -- apply eval_ok with (state := RawState state) in okvalue; [ | now apply hwf ]. - destruct okvalue as [v hv]. - now right; repeat eexists; econstructor; apply hv. -- apply eval_ok with (state := RawState state) in okvalue; [ | now apply hwf ]. - destruct okvalue as [v hv]. - now right; repeat eexists; econstructor; apply hv. -- apply eval_ok with (state := RawState state) in okvalue; [ | now apply hwf ]. - destruct okvalue as [v hv]. - now right; repeat eexists; econstructor; apply hv. -- apply eval_ok with (state := RawState state) in okvalue; [ | now apply hwf ]. - destruct okvalue as [v hv]. - now right; repeat eexists; econstructor; apply hv. -- apply eval_ok with (state := RawState state) in h; [ | now apply hwf ]. - destruct h as [v hv]. - now right; repeat eexists; econstructor; apply hv. -- right. - apply ty_bool with (state := RawState state) in oktest; [ | now apply hwf]. - destruct oktest as [[] hb]; - repeat eexists; econstructor; exact hb. -- inversion hk; subst; clear hk. - + now left; split; firstorder. - + now right; repeat eexists; econstructor. - + right. - apply ty_bool with (state := RawState state) in H; [ | now apply hwf ]. - destruct H as [[] hb]; - repeat eexists; econstructor; exact hb. - + now right; repeat eexists; econstructor. - + now left; split; firstorder. -- now right; repeat eexists; econstructor. -- right. - apply ty_bool with (state := RawState state) in hok; [ | now apply hwf ]. - destruct hok as [[] hb]; now repeat eexists; econstructor. -- right. - assert (hlen: List.length arguments = List.length (parameters function_def)) - by now apply check_arguments_length in hcheck. - apply check_arguments_eval with (state := RawState state) in hcheck; [ | now apply hwf]. - destruct hcheck as [vs hvs]. - assert (hlen2: List.length arguments = List.length vs) by - now apply eval_list_length in hvs; - rewrite <- hvs, Expression.ListHelpers.from_list_cancel, map_length. - destruct (prepare_call_state_same_length Eval.Empty vs (parameters function_def)) - as [ after hafter ]; [now rewrite hlen2 in hlen | ]. - repeat eexists. - econstructor; [| now apply hvs| now apply hafter]. - apply well_formed_get_info with (function_name := function_name) in hwf; - rewrite <- hwf. - now apply hg. -- right. - assert (hlen: List.length arguments = List.length (parameters function_def)) - by now apply check_arguments_length in hcheck. - apply check_arguments_eval with (state := RawState state) in hcheck; [ | now apply hwf]. - destruct hcheck as [vs hvs]. - assert (hlen2: List.length arguments = List.length vs) by - now apply eval_list_length in hvs; - rewrite <- hvs, Expression.ListHelpers.from_list_cancel, map_length. - destruct (prepare_call_state_same_length Eval.Empty vs (parameters function_def)) - as [ after hafter ]; [ now rewrite hlen2 in hlen | ]. - repeat eexists. - econstructor; [| now apply hvs| now apply hafter]. - apply well_formed_get_info with (function_name := function_name) in hwf; - rewrite <- hwf. - now apply hg. -- inversion hk; subst; clear hk. - + right; repeat eexists. - now constructor. - + right; repeat eexists. - now econstructor. - + right; repeat eexists. - now econstructor. - + right; repeat eexists. - now econstructor. - + apply eval_ok with (state := RawState state) in hok as [v [hv1 hv2]]; - [ | now apply hwf ]. - right; exists (set saved_state target v); exists Statement.Pass; exists k0. - now constructor. -Qed. - -(* begin hide *) -Module Test. - -(* Creating a test context with no type information on variable, and -the same function information that Eval.Test.test_state *) -Definition test_context: Context := - mkState _ (SMap.empty _) (FuncState Eval.Test.test_state). - -(* Final typing context, with y:int as only type information *) -Definition final_context : Context := - set test_context "y"%string (true, Typ.Integer). - -(* We show here that in the context `test_context`, and under any return type, - type checking the program Eval.Test.Prog only introduces y:int in the - context *) -Lemma Typing_Prog: forall return_type, - typ test_context return_type Eval.Test.Prog final_context. -Proof. -intro return_type. -unfold Test.Prog, final_context, Test.YID. -apply typCallFun with (function_def := Test.int_id). -- apply SMap.find_1; apply SMap.add_1. - reflexivity. -- reflexivity. -- simpl; split; [| exact I]. - now constructor. -Qed. - -Definition test_context2 : Context := - mkState _ (SMap.empty _) (FuncState Eval.Test.test_state2). - -Lemma Typing_Prog2: forall return_type, - typ test_context2 return_type Eval.Test.Prog2 test_context2. -Proof. -intro return_type. -apply typCallProc with (function_def := Test.expect_int). -- apply SMap.find_1; apply SMap.add_1. - reflexivity. -- reflexivity. -- simpl; split; [| exact I]. - now constructor. -Qed. - -(* Some well-formed proofs *) -Lemma well_formed_int_id : well_formed_function (FuncState test_context) Test.int_id. -Proof. -unfold well_formed_function. -exists (mkContext (prepare_call_context Empty (parameters Test.int_id)) - (FuncState test_context)). -constructor. -econstructor. -simpl. -apply SMap.find_1; apply SMap.add_1. -reflexivity. -Qed. - -Lemma well_formed_test: well_formed Test.test_state test_context. -Proof. -split; [| split; [ reflexivity | intros fname fdef ]]. -- intros id T. - unfold test_context; simpl. - intros b h; discriminate h. -- unfold get_info; simpl. - rewrite find_add_smap. - case_eq (fname =? "int_id")%string; intro heq. - + intro h; injection h; clear h; intro h; subst. - exact well_formed_int_id. - + intro h; discriminate h. -Qed. - -(* Successive valid assignement mixing weak and strong update *) -Definition Prog_Assign_good := - Statement.to_seq - (Statement.Assign Eval.Test.XID None (Eval.Test.Int 42) :: - Statement.Assign Eval.Test.XID None Expression.True_ :: - Statement.Assign Eval.Test.XID (Some Typ.Integer) (Eval.Test.Int 42) :: - Statement.Assign Eval.Test.XID None (Eval.Test.Int 42) :: - Statement.Assign Eval.Test.XID (Some Typ.Boolean) Expression.False_ :: - nil). - -Definition EmptyContext : Context := - mkState _ (SMap.empty _) (SMap.empty _). - -Lemma Prog_Assign_good_typed: forall return_type, - typ EmptyContext return_type Prog_Assign_good - (* resulting context. It's content is not really relevant *) - (set (set (set (set - (set EmptyContext "x" (false, Typ.Integer)) - "x" (false, Typ.Boolean)) - "x" (true, Typ.Integer)) - "x" (true, Typ.Integer)) - "x" (true, Typ.Boolean)). -Proof. -unfold EmptyContext. -intros return_type. -econstructor; [ | econstructor; [ | econstructor; [ | econstructor ]]]. -- apply typAssignIdNone; [ reflexivity | ]. - now constructor. -- unfold set; simpl. - apply typAssignIdNoneWeak with (Tid := Typ.Integer); [ | now constructor ]. - apply SMap.find_1; apply SMap.add_1. - reflexivity. -- apply typAssignIdAnnot. - now constructor. -- apply typAssignIdNoneStrong; [ | now constructor ]. - apply SMap.find_1; apply SMap.add_1. - reflexivity. -- apply typAssignIdAnnot. - now constructor. -Qed. - -(* Invalid assignement *) -Definition Prog_Assign_wrong1 := - Statement.Assign Eval.Test.XID (Some Typ.Integer) Expression.True_. - -(* Invalid assignement after user annotation *) -Definition Prog_Assign_wrong2 := - Statement.to_seq - (Statement.Assign Eval.Test.XID (Some Typ.Integer) (Eval.Test.Int 42) :: - Statement.Assign Eval.Test.XID None Expression.True_ :: - nil). - -Lemma Prog_Assign_wrong1_untypable: forall context return_type return_context, - typ context return_type Prog_Assign_wrong1 return_context -> False. -Proof. -intros context return_type return_context h. -inversion h; subst; clear h. -now inversion H5. -Qed. - -Lemma Prog_Assign_wrong2_untypable: forall context return_type return_context, - typ context return_type Prog_Assign_wrong2 return_context -> False. -Proof. -intros context return_type return_context h. -inversion h; subst; clear h. -inversion H3; subst; clear H3. -inversion H5; subst; clear H5. -- now rewrite find_add, String.eqb_refl in H3. -- rewrite find_add, String.eqb_refl in H3. - now injection H3. -- rewrite find_add, String.eqb_refl in H3. - injection H3; clear H3; intro hT. - rewrite <- hT in H6. - now inversion H6. -Qed. - -End Test. -(* end hide *) diff --git a/documentation/website/docs/formal/python_semantic/Statement.v b/documentation/website/docs/formal/python_semantic/Statement.v deleted file mode 100644 index c3fa17d6e2f..00000000000 --- a/documentation/website/docs/formal/python_semantic/Statement.v +++ /dev/null @@ -1,37 +0,0 @@ -Require Import List String. -Require Pyre.Expression. -Require Pyre.Lvalue. -Require Pyre.Typ. - -(** * Statements - - More will be added later on. See - https://github.com/facebook/pyre-check/blob/main/ast/statement.mli#L331 -*) -Inductive t : Set := - | Assign: forall (target: Lvalue.t) - (annotation: option Typ.t) - (value: Expression.t), - t - | Call: forall (target: option (Lvalue.t * Typ.t)) - (callee: Expression.t) - (arguments: list ((option string) * Expression.t)), - t - | Expression: Expression.t -> t - | Delete: Expression.t -> t - | For: forall (target: Lvalue.t) (iterator: Expression.t) (body orelse: t), t - | Global: list string -> t - | If: forall (test: Expression.t) (body orelse: t), t - | Nonlocal: list string -> t - | Pass: t - | While: forall (test: Expression.t) (body orelse: t), t - | Seq : forall (st next : t), t - | Return: forall (ret: Expression.t), t -. - -Fixpoint to_seq (statements: list t) : t := - match statements with - | nil => Pass - | hd :: nil => hd - | hd :: tl => Seq hd (to_seq tl) - end. diff --git a/documentation/website/docs/formal/python_semantic/Typ.v b/documentation/website/docs/formal/python_semantic/Typ.v deleted file mode 100644 index 8956df6bb8b..00000000000 --- a/documentation/website/docs/formal/python_semantic/Typ.v +++ /dev/null @@ -1,52 +0,0 @@ -Require Import List ZArith String. - -(** Types *) -Inductive t: Set := - | Integer: t - | Boolean: t - | String: t - | List: t -> t - | Tuple: tlist -> t - | None: t -with tlist: Set := - | Nil: tlist - | Cons: t -> tlist -> tlist -. - -Hint Constructors t tlist : core. - -Scheme typ_ind' := Induction for t Sort Prop - with typ_list_ind' := Induction for tlist Sort Prop. - -Combined Scheme typ_ind from typ_ind', typ_list_ind'. - -Require Import List. - -Module ListHelpers. - -Fixpoint to_list (l: tlist) : list t := - match l with - | Nil => nil - | Cons hd tl => hd :: to_list tl - end. - -Fixpoint from_list (l: list t) : tlist := - match l with - | nil => Nil - | hd :: tl => Cons hd (from_list tl) - end. - -Lemma to_list_cancel: forall l, from_list (to_list l) = l. -Proof. -induction l as [ | hd tl hi]; simpl in *; [ now idtac | ]. -now rewrite hi. -Qed. - -Lemma from_list_cancel: forall l, to_list (from_list l) = l. -Proof. -induction l as [ | hd tl hi]; simpl in *; [ now idtac | ]. -now rewrite hi. -Qed. - -Coercion to_list: tlist >-> list. -End ListHelpers. diff --git a/documentation/website/docs/formal/python_semantic/Value.v b/documentation/website/docs/formal/python_semantic/Value.v deleted file mode 100644 index 1b515fb11c8..00000000000 --- a/documentation/website/docs/formal/python_semantic/Value.v +++ /dev/null @@ -1,116 +0,0 @@ -Require Import String Bool ZArith List. - -(** * Values *) -Inductive t : Set := - | Boolean: bool -> t - | Integer: Z -> t - | String: string -> t - | Sequence: tlist -> t - | None: t -with tlist : Set := - | Nil: tlist - | Cons: t -> tlist -> tlist -. - -Hint Constructors t tlist : core. - -Scheme value_ind' := Induction for t Sort Prop - with value_list_ind' := Induction for tlist Sort Prop. - -Combined Scheme value_ind from value_ind', value_list_ind'. - -(** Boolean equality for values and list of values *) -Fixpoint eqb (l r: t) { struct l } : bool := - match l, r with - | Boolean b0, Boolean b1 => Bool.eqb b0 b1 - | Integer z0, Integer z1 => Z.eqb z0 z1 - | String s0, String s1 => String.eqb s0 s1 - | Sequence l1, Sequence l2 => eqb_list l1 l2 - | None, None => true - | _ ,_ => false - end -with eqb_list (l1 l2: tlist) : bool := - match l1, l2 with - | Nil, Nil => true - | (Cons hd1 tl1), (Cons hd2 tl2) => - andb (eqb hd1 hd2) (eqb_list tl1 tl2) - | _, _ => false - end. - -Lemma eqb_true_ : (forall v0 v1, eqb v0 v1 = true -> v0 = v1) - /\ (forall l0 l1, eqb_list l0 l1 = true -> l0 = l1). -Proof. -apply value_ind. -- intros b [] h; simpl in *; try discriminate. - now apply Bool.eqb_prop in h; subst. -- intros z [] h; simpl in *; try discriminate. - now apply Z.eqb_eq in h; subst. -- intros str [] h; simpl in *; try discriminate. - now apply String.eqb_eq in h; subst. -- intros l0 hi [ | | | l1 | ] h; simpl in *; try discriminate. - now apply hi in h; subst. -- now intros [ ]; try discriminate. -- now intros [ ]; try discriminate. -- intros v hiv l0 hi [ | hd tl ] h; simpl in *; try discriminate. - apply andb_prop in h as [h0 h1]. - apply hiv in h0 as ->. - now apply hi in h1 as ->. -Qed. - -Lemma eqb_eq: forall v0 v1, eqb v0 v1 = true -> v0 = v1. -Proof. - now apply eqb_true_. -Qed. - -Lemma eqb_list_eq: forall l0 l1, eqb_list l0 l1 = true -> l0 = l1. -Proof. - now apply eqb_true_. -Qed. - -Lemma eqb_refl_: (forall v, eqb v v = true) /\ (forall lv, eqb_list lv lv = true). -Proof. -apply value_ind; try (now intros). -- now intros []. -- intro z; simpl. - now rewrite Z.eqb_refl. -- intro s; simpl. - now rewrite String.eqb_refl. -- intros v hv lv hlv; simpl. - now rewrite hv, hlv. -Qed. - -Lemma eqb_refl: forall v, eqb v v = true. -Proof. -now apply eqb_refl_. -Qed. - -Require Import List. - -Module ListHelpers. - -Fixpoint to_list (l: tlist) : list t := - match l with - | Nil => nil - | Cons hd tl => hd :: to_list tl - end. - -Fixpoint from_list (l: list t) : tlist := - match l with - | nil => Nil - | hd :: tl => Cons hd (from_list tl) - end. - -Lemma to_list_cancel: forall l, from_list (to_list l) = l. -Proof. -induction l as [ | hd tl hi]; simpl in *; [ now idtac | ]. -now rewrite hi. -Qed. - -Lemma from_list_cancel: forall l, to_list (from_list l) = l. -Proof. -induction l as [ | hd tl hi]; simpl in *; [ now idtac | ]. -now rewrite hi. -Qed. - -Coercion to_list: tlist >-> list. -End ListHelpers. diff --git a/documentation/website/docs/formal/python_semantic/_CoqProject b/documentation/website/docs/formal/python_semantic/_CoqProject deleted file mode 100644 index ef245a4370f..00000000000 --- a/documentation/website/docs/formal/python_semantic/_CoqProject +++ /dev/null @@ -1,12 +0,0 @@ --Q . Pyre - -Lib/String.v -Lib/List.v -Map.v -Value.v -Lvalue.v -Typ.v -Expression.v -Statement.v -Eval.v -Semantic.v diff --git a/documentation/website/docs/formal/python_semantic/extra/footer.html b/documentation/website/docs/formal/python_semantic/extra/footer.html deleted file mode 100644 index d0f79a884f0..00000000000 --- a/documentation/website/docs/formal/python_semantic/extra/footer.html +++ /dev/null @@ -1,8 +0,0 @@ - - - - - - diff --git a/documentation/website/docs/formal/python_semantic/extra/header.html b/documentation/website/docs/formal/python_semantic/extra/header.html deleted file mode 100644 index cc81721b491..00000000000 --- a/documentation/website/docs/formal/python_semantic/extra/header.html +++ /dev/null @@ -1,27 +0,0 @@ - - - - - - - - - - - - - -
-
diff --git a/documentation/website/docs/formal/python_semantic/extra/resources/config.js b/documentation/website/docs/formal/python_semantic/extra/resources/config.js deleted file mode 100644 index 1888f4ea9c0..00000000000 --- a/documentation/website/docs/formal/python_semantic/extra/resources/config.js +++ /dev/null @@ -1,79 +0,0 @@ -/** - * Copyright (c) Meta Platforms, Inc. and affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ - -var coqdocjs = coqdocjs || {}; - -coqdocjs.repl = { - "forall": "\u{2200}", - "exists": "\u{2203}", - "~": "\u{00AC}", - "/\\": "\u{2227}", - "\\/": "\u{2228}", - "->": "\u{2192}", - "<-": "\u{2190}", - "<->": "\u{2194}", - "=>": "\u{21D2}", - "<>": "\u{2260}", - "<=": "\u{2264}", - ">=": "\u{2265}", - "el": "\u{2208}", - "nel": "\u{2209}", - "<<=": "\u{2286}", - "|-": "\u{22A2}", - ">>": "\u{00BB}", - "<<": "\u{2286}", - "++": "\u{29FA}", - "===": "\u{2261}", - "=/=": "\u{2262}", - "=~=": "\u{2245}", - "==>": "\u{27F9}", - "lhd": "\u{22B2}", - "rhd": "\u{22B3}", - "nat": "\u{2115}", - "alpha": "\u{03B1}", - "beta": "\u{03B2}", - "gamma": "\u{03B3}", - "delta": "\u{03B4}", - "epsilon": "\u{03B5}", - "eta": "\u{03B7}", - "iota": "\u{03B9}", - "kappa": "\u{03BA}", - "lambda": "\u{03BB}", - "mu": "\u{03BC}", - "nu": "\u{03BD}", - "omega": "\u{03C9}", - "phi": "\u{03D5}", - "pi": "\u{03C0}", - "psi": "\u{03C8}", - "rho": "\u{03C1}", - "sigma": "\u{03C3}", - "tau": "\u{03C4}", - "theta": "\u{03B8}", - "xi": "\u{03BE}", - "zeta": "\u{03B6}", - "Delta": "\u{0394}", - "Gamma": "\u{0393}", - "Pi": "\u{03A0}", - "Sigma": "\u{03A3}", - "Omega": "\u{03A9}", - "Xi": "\u{039E}" -}; - -coqdocjs.subscr = { - "0" : "\u{2080}", - "1" : "\u{2081}", - "2" : "\u{2082}", - "3" : "\u{2083}", - "4" : "\u{2084}", - "5" : "\u{2085}", - "6" : "\u{2086}", - "7" : "\u{2087}", - "8" : "\u{2088}", - "9" : "\u{2089}", -}; - -coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/documentation/website/docs/formal/python_semantic/extra/resources/coqdoc.css b/documentation/website/docs/formal/python_semantic/extra/resources/coqdoc.css deleted file mode 100644 index b79a2891ab0..00000000000 --- a/documentation/website/docs/formal/python_semantic/extra/resources/coqdoc.css +++ /dev/null @@ -1,208 +0,0 @@ -/** - * Copyright (c) Meta Platforms, Inc. and affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ - -@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700); - -body{ - font-family: 'Open Sans', sans-serif; - font-size: 14px; - color: #2D2D2D -} - -a { - text-decoration: none; - border-radius: 3px; - padding-left: 3px; - padding-right: 3px; - margin-left: -3px; - margin-right: -3px; - color: inherit; - font-weight: bold; -} - -#main .code a, #main .inlinecode a, #toc a { - font-weight: inherit; -} - -a[href]:hover, [clickable]:hover{ - background-color: rgba(0,0,0,0.1); - cursor: pointer; -} - -h, h1, h2, h3, h4, h5 { - line-height: 1; - color: black; - text-rendering: optimizeLegibility; - font-weight: normal; - letter-spacing: 0.1em; - text-align: left; -} - -div + br { - display: none; -} - -div:empty{ display: none;} - -#main h1 { - font-size: 2em; -} - -#main h2 { - font-size: 1.667rem; -} - -#main h3 { - font-size: 1.333em; -} - -#main h4, #main h5, #main h6 { - font-size: 1em; -} - -#toc h2 { - padding-bottom: 0; -} - -#main .doc { - margin: 0; - text-align: justify; -} - -.inlinecode, .code, #main pre { - font-family: monospace; -} - -.code > br:first-child { - display: none; -} - -.doc + .code{ - margin-top:0.5em; -} - -.block{ - display: block; - margin-top: 5px; - margin-bottom: 5px; - padding: 10px; - text-align: center; -} - -.block img{ - margin: 15px; -} - -table.infrule { - border: 0px; - margin-left: 50px; - margin-top: 10px; - margin-bottom: 10px; -} - -td.infrule { - font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace; - text-align: center; - padding: 0; - line-height: 1; -} - -tr.infrulemiddle hr { - margin: 1px 0 1px 0; -} - -.infrulenamecol { - color: rgb(60%,60%,60%); - padding-left: 1em; - padding-bottom: 0.1em -} - -.id[type="constructor"], .id[type="projection"], .id[type="method"], -.id[title="constructor"], .id[title="projection"], .id[title="method"] { - color: #A30E16; -} - -.id[type="var"], .id[type="variable"], -.id[title="var"], .id[title="variable"] { - color: inherit; -} - -.id[type="definition"], .id[type="record"], .id[type="class"], -.id[type="instance"], .id[type="inductive"], .id[type="library"], -.id[title="definition"], .id[title="record"], .id[title="class"], -.id[title="instance"], .id[title="inductive"], .id[title="library"] { - color: #A6650F; -} - -.id[type="lemma"], -.id[title="lemma"]{ - color: #188B0C; -} - -.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"], -.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{ - color : #2874AE; -} - -.comment { - color: #808080; -} - -/* TOC */ - -#toc h2{ - letter-spacing: 0; - font-size: 1.333em; -} - -/* Index */ - -#index { - margin: 0; - padding: 0; - width: 100%; -} - -#index #frontispiece { - margin: 1em auto; - padding: 1em; - width: 60%; -} - -.booktitle { font-size : 140% } -.authors { - font-size : 90%; - line-height: 115%; -} -.moreauthors { font-size : 60% } - -#index #entrance { - text-align: center; -} - -#index #entrance .spacer { - margin: 0 30px 0 30px; -} - -ul.doclist { - margin-top: 0em; - margin-bottom: 0em; -} - -#toc > * { - clear: both; -} - -#toc > a { - display: block; - float: left; - margin-top: 1em; -} - -#toc a h2{ - display: inline; -} diff --git a/documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.css b/documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.css deleted file mode 100644 index 4c296662dbf..00000000000 --- a/documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.css +++ /dev/null @@ -1,256 +0,0 @@ -/** - * Copyright (c) Meta Platforms, Inc. and affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ - -/* replace unicode */ - -.id[repl] .hidden { - font-size: 0; -} - -.id[repl]:before{ - content: attr(repl); -} - -/* folding proofs */ - -@keyframes show-proof { - 0% { - max-height: 1.2em; - opacity: 1; - } - 99% { - max-height: 1000em; - } - 100%{ - } -} - -@keyframes hide-proof { - from { - visibility: visible; - max-height: 10em; - opacity: 1; - } - to { - max-height: 1.2em; - } -} - -.proof { - cursor: pointer; -} -.proof * { - cursor: pointer; -} - -.proof { - overflow: hidden; - position: relative; - display: inline-block; -} - -.proof[show="false"] { - max-height: 1.2em; - visibility: visible; - opacity: 0.5; -} - -.proof[show="false"][animate] { - animation-name: hide-proof; - animation-duration: 0.25s; -} - -.proof[show=true] { - animation-name: show-proof; - animation-duration: 10s; -} - -.proof[show="false"]:before { - position: absolute; - visibility: visible; - width: 100%; - height: 100%; - display: block; - opacity: 0; - content: "M"; -} -.proof[show="false"]:hover:before { - content: ""; -} - -.proof[show="false"] + br + br { - display: none; -} - -.proof[show="false"]:hover { - visibility: visible; - opacity: 0.5; -} - -#toggle-proofs[proof-status="no-proofs"] { - display: none; -} - -#toggle-proofs[proof-status="some-hidden"]:before { - content: "Show Proofs"; -} - -#toggle-proofs[proof-status="all-shown"]:before { - content: "Hide Proofs"; -} - - -/* page layout */ - -html, body { - height: 100%; - margin:0; - padding:0; -} - -@media only screen { -/* no div with internal scrolling to allow printing of whole content */ - body { - display: flex; - flex-direction: column - } - - #content { - flex: 1; - overflow: auto; - display: flex; - flex-direction: column; - } -} - -#content:focus { - outline: none; /* prevent glow in OS X */ -} - -#main { - display: block; - padding: 16px; - padding-top: 1em; - padding-bottom: 2em; - margin-left: auto; - margin-right: auto; - max-width: 60em; - flex: 1 0 auto; -} - -.libtitle { - display: none; -} - -/* header */ -#header { - width:100%; - padding: 0; - margin: 0; - display: flex; - align-items: center; - background-color: rgb(21,57,105); - color: white; - font-weight: bold; - overflow: hidden; -} - - -.button { - cursor: pointer; -} - -#header * { - text-decoration: none; - vertical-align: middle; - margin-left: 15px; - margin-right: 15px; -} - -#header > .right, #header > .left { - display: flex; - flex: 1; - align-items: center; -} -#header > .left { - text-align: left; -} -#header > .right { - flex-direction: row-reverse; -} - -#header a, #header .button { - color: white; - box-sizing: border-box; -} - -#header a { - border-radius: 0; - padding: 0.2em; -} - -#header .button { - background-color: rgb(63, 103, 156); - border-radius: 1em; - padding-left: 0.5em; - padding-right: 0.5em; - margin: 0.2em; -} - -#header a:hover, #header .button:hover { - background-color: rgb(181, 213, 255); - color: black; -} - -#header h1 { padding: 0; - margin: 0;} - -/* footer */ -#footer { - text-align: center; - opacity: 0.5; - font-size: 75%; -} - -/* hyperlinks */ - -@keyframes highlight { - 50%{ - background-color: black; - } -} - -:target * { - animation-name: highlight; - animation-duration: 1s; -} - -a[name]:empty { - float: right; -} - -/* Proviola */ - -div.code { - width: auto; - float: none; -} - -div.goal { - position: fixed; - left: 75%; - width: 25%; - top: 3em; -} - -div.doc { - clear: both; -} - -span.command:hover { - background-color: inherit; -} diff --git a/documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.js b/documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.js deleted file mode 100644 index 1a36323fc3d..00000000000 --- a/documentation/website/docs/formal/python_semantic/extra/resources/coqdocjs.js +++ /dev/null @@ -1,201 +0,0 @@ -/** - * Copyright (c) Meta Platforms, Inc. and affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ - -var coqdocjs = coqdocjs || {}; -(function(){ - -function replace(s){ - var m; - if (m = s.match(/^(.+)'/)) { - return replace(m[1])+"'"; - } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { - return replace(m[1])+m[2].replace(/\d/g, - function(d){return coqdocjs.subscr[d]}); - } else if (coqdocjs.repl.hasOwnProperty(s)){ - return coqdocjs.repl[s] - } else { - return s; - } -} - -function toArray(nl){ - return Array.prototype.slice.call(nl); -} - -function replInTextNodes() { - coqdocjs.replInText.forEach(function(toReplace){ - toArray(document.getElementsByClassName("code")) - .concat(toArray(document.getElementsByClassName("inlinecode"))) - .forEach(function(elem){ - toArray(elem.childNodes).forEach(function(node){ - if (node.nodeType != Node.TEXT_NODE) return; - var fragments = node.textContent.split(toReplace); - node.textContent = fragments[fragments.length-1]; - for (var k = 0; k < fragments.length - 1; ++k) { - node.parentNode.insertBefore(document - .createTextNode(fragments[k]),node); - var replacement = document.createElement("span"); - replacement.appendChild(document.createTextNode(toReplace)); - replacement.setAttribute("class", "id"); - replacement.setAttribute("type", "keyword"); - node.parentNode.insertBefore(replacement, node); - } - }); - }); - }); -} - -function replNodes() { - toArray(document.getElementsByClassName("id")).forEach(function(node){ - if (["var", "variable", "keyword", "notation", "definition", "inductive"] - .indexOf(node.getAttribute("type"))>=0){ - var text = node.textContent; - var replText = replace(text); - if(text != replText) { - node.setAttribute("repl", replText); - node.setAttribute("title", text); - var hidden = document.createElement("span"); - hidden.setAttribute("class", "hidden"); - while (node.firstChild) { - hidden.appendChild(node.firstChild); - } - node.appendChild(hidden); - } - } - }); -} - -function isVernacStart(l, t){ - t = t.trim(); - for(var s of l){ - if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){ - return true; - } - } - return false; -} - -function isProofStart(s){ - return isVernacStart(["Proof"], s); -} - -function isProofEnd(s){ - return isVernacStart(["Qed", "Admitted", "Defined", "Abort"], s); -} - -function proofStatus(){ - var proofs = toArray(document.getElementsByClassName("proof")); - if(proofs.length) { - for(var proof of proofs) { - if (proof.getAttribute("show") === "false") { - return "some-hidden"; - } - } - return "all-shown"; - } - else { - return "no-proofs"; - } -} - -function updateView(){ - document.getElementById("toggle-proofs").setAttribute("proof-status", - proofStatus()); -} - -function foldProofs() { - var hasCommands = true; - var nodes = document.getElementsByClassName("command"); - if(nodes.length == 0) { - hasCommands = false; - console.log("no command tags found") - nodes = document.getElementsByClassName("id"); - } - toArray(nodes).forEach(function(node){ - if(isProofStart(node.textContent)) { - var proof = document.createElement("span"); - proof.setAttribute("class", "proof"); - - node.parentNode.insertBefore(proof, node); - if(proof.previousSibling.nodeType === Node.TEXT_NODE) - proof.appendChild(proof.previousSibling); - while(node && !isProofEnd(node.textContent)) { - proof.appendChild(node); - node = proof.nextSibling; - } - if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed - if (!hasCommands && proof.nextSibling) - proof.appendChild(proof.nextSibling); // the dot after the Qed - - proof.addEventListener("click", function(proof){return function(e){ - if (e.target.parentNode.tagName.toLowerCase() === "a") - return; - proof.setAttribute("show", - proof.getAttribute("show") === "true" ? "false" : "true"); - proof.setAttribute("animate", ""); - updateView(); - };}(proof)); - proof.setAttribute("show", "false"); - } - }); -} - -function toggleProofs(){ - var someProofsHidden = proofStatus() === "some-hidden"; - toArray(document.getElementsByClassName("proof")).forEach(function(proof){ - proof.setAttribute("show", someProofsHidden); - proof.setAttribute("animate", ""); - }); - updateView(); -} - -function repairDom(){ - // pull whitespace out of command - toArray(document.getElementsByClassName("command")).forEach(function(node){ - while(node.firstChild && node.firstChild.textContent.trim() == ""){ - console.log("try move"); - node.parentNode.insertBefore(node.firstChild, node); - } - }); - toArray(document.getElementsByClassName("id")).forEach(function(node){ - node.setAttribute("type", node.getAttribute("title")); - }); - toArray(document.getElementsByClassName("idref")).forEach(function(ref){ - toArray(ref.childNodes).forEach(function(child){ - if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) - ref.removeAttribute("href"); - }); - }); - -} - -function fixTitle(){ - var url = "/" + window.location.pathname; - var modulename = "." + url.substring(url.lastIndexOf('/')+1, - url.lastIndexOf('.')); - modulename = modulename.substring(modulename.lastIndexOf('.')+1); - if (modulename === "toc") {modulename = "Table of Contents";} - else if (modulename === "indexpage") {modulename = "Index";} - else {modulename = modulename + ".v";}; - document.title = modulename; -} - -function postprocess(){ - repairDom(); - replInTextNodes() - replNodes(); - foldProofs(); - document.getElementById("toggle-proofs").addEventListener("click", - toggleProofs); - updateView(); -} - -fixTitle(); -document.addEventListener('DOMContentLoaded', postprocess); - -coqdocjs.toggleProofs = toggleProofs; -})(); diff --git a/documentation/website/docs/formal/subtyping_description/DejaVuSansMono.sty b/documentation/website/docs/formal/subtyping_description/DejaVuSansMono.sty deleted file mode 100644 index 2b4d6d6a336..00000000000 --- a/documentation/website/docs/formal/subtyping_description/DejaVuSansMono.sty +++ /dev/null @@ -1,38 +0,0 @@ -\ProvidesPackage{DejaVuSansMono} [2011/06/01 Style file for DejaVuSansMono.] -%% -%% Options: -%% [scaled] --> Scale = 0.95 -%% [scaled=0.9] --> Scale = 0.90 -%% -\RequirePackage{keyval} -\define@key{DejaVuSansMono}{scaled}[0.95]{% - \def\DejaVuSansMono@scale{#1}} -\def\ProcessOptionsWithKV#1{% - \let\@tempc\relax - \let\DejaVuSansMono@tempa\@empty - \@for\CurrentOption:=\@classoptionslist\do{% - \@ifundefined{KV@#1@\CurrentOption}% - {}% - {% - \edef\DejaVuSansMono@tempa{\DejaVuSansMono@tempa,\CurrentOption,}% - \@expandtwoargs\@removeelement\CurrentOption - \@unusedoptionlist\@unusedoptionlist - }% - }% - \edef\DejaVuSansMono@tempa{% - \noexpand\setkeys{#1}{% - \DejaVuSansMono@tempa\@ptionlist{\@currname.\@currext}% - }% - }% - \DejaVuSansMono@tempa - \let\CurrentOption\@empty -} -\ProcessOptionsWithKV{DejaVuSansMono} -\AtEndOfPackage{% - \let\@unprocessedoptions\relax -} - - -\renewcommand{\ttdefault}{DejaVuSansMono-TLF} - -\endinput diff --git a/documentation/website/docs/formal/subtyping_description/Makefile b/documentation/website/docs/formal/subtyping_description/Makefile deleted file mode 100644 index 37ef3b212a3..00000000000 --- a/documentation/website/docs/formal/subtyping_description/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -DOC=pyre_sub - -all: $(DOC).pdf - -$(DOC).pdf: $(DOC).tex - rubber -d $^ - -watch: - sh -c "mupdf-gl $(DOC).pdf 2>/dev/null >&2 & jobs -p %1 > .mupdf.pid" - fswatch $(DOC).tex | xargs -n1 sh -c 'make && echo "Refreshing..." && kill -n 1 `cat .mupdf.pid`' - -clean: - rm -f *.aux *.dvi *.log - -.PHONY: watch clean diff --git a/documentation/website/docs/formal/subtyping_description/lstocaml.sty b/documentation/website/docs/formal/subtyping_description/lstocaml.sty deleted file mode 100644 index a0bf0081d47..00000000000 --- a/documentation/website/docs/formal/subtyping_description/lstocaml.sty +++ /dev/null @@ -1,60 +0,0 @@ -%% -% Copyright (c) Meta Platforms, Inc. and affiliates. -% -% This source code is licensed under the MIT license found in the -% LICENSE file in the root directory of this source tree. -%% - -\usepackage{xcolor} -\definecolor{butter}{HTML}{C4A000} -\definecolor{orange}{HTML}{CE5C00} -\definecolor{chocolate}{HTML}{8F5902} -\definecolor{chameleon}{HTML}{4E9A06} -\definecolor{skyblue}{HTML}{204A87} -\definecolor{plum}{HTML}{5C3566} -\definecolor{scarletred}{HTML}{A40000} -\definecolor{lightalu}{HTML}{BABDB6} -\definecolor{darkalu}{HTML}{2E3436} - -\newcommand{\kwstyle}{} - -\usepackage{listings} - -\lstset{ - basicstyle=\footnotesize\ttfamily, - breaklines=true, - aboveskip=10pt, - belowskip=5pt, - xleftmargin=10pt, - commentstyle=\color{orange}, - keywordstyle=\kwstyle, - language=Caml, - stringstyle=\color{plum}, - tabsize=2, - numberstyle=\tiny\color{gray}, - escapeinside={(*@}{*)}, - numbers=left, - numbersep=2pt, - keywordstyle=[1]\kwstyle\color{chameleon}, - keywordstyle=[2]\kwstyle\color{scarletred}, - keywordstyle=[3]\kwstyle\color{skyblue}, - keywordstyle=[4]\kwstyle\color{butter}, - keywordstyle=[5]\kwstyle\color{skyblue}, - keywordstyle=[6]\kwstyle\color{skyblue}, - keywordstyle=[7]\kwstyle\color{chameleon}, - keywordstyle=[8]\kwstyle\color{butter}, - keywordstyle=[9]\kwstyle\color{butter}, - keywords=[1]{let,val,method,in,and,rec,private,virtual,constraint}, - keywords=[2]{type,open,class,module,exception,external}, - keywords=[3]{fun,function,functor,match,try,with}, - keywords=[4]{as,when,of}, - keywords=[5]{if,then,else}, - keywords=[6]{begin,end,object,struct,sig,for,while,do,done,to,downto}, - keywords=[7]{true,false}, - keywords=[8]{include,inherit,initializer}, - keywords=[9]{new,ref,mutable,lazy,assert,raise}, -} - -\lstset{literate= - {`}{{{\lq}}}1 -} diff --git a/documentation/website/docs/formal/subtyping_description/mathpartir.sty b/documentation/website/docs/formal/subtyping_description/mathpartir.sty deleted file mode 100644 index 0e2a71d43bf..00000000000 --- a/documentation/website/docs/formal/subtyping_description/mathpartir.sty +++ /dev/null @@ -1,492 +0,0 @@ -% Mathpartir --- Math Paragraph for Typesetting Inference Rules -% -% Copyright (C) 2001, 2002, 2003, 2004, 2005, 2015 Didier Remy -% -% Author : Didier Remy -% Version : 1.3.1 -% Bug Reports : to author -% Web Site : http://pauillac.inria.fr/~remy/latex/ -% -% Mathpartir 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, or (at your option) -% any later version. -% -% Mathpartir 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 -% (http://pauillac.inria.fr/~remy/license/GPL). -% -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% File mathpartir.sty (LaTeX macros) -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{mathpartir} - [2015/11/06 version 1.3.1 Math Paragraph for Typesetting Inference Rules] - -%% - -%% Identification -%% Preliminary declarations - -\RequirePackage {keyval} - -%% Options -%% More declarations - -%% PART I: Typesetting maths in paragraphe mode - -%% \newdimen \mpr@tmpdim -%% Dimens are a precious ressource. Uses seems to be local. -\let \mpr@tmpdim \@tempdima - -% To ensure hevea \hva compatibility, \hva should expands to nothing -% in mathpar or in inferrule -\let \mpr@hva \empty - -%% normal paragraph parametters, should rather be taken dynamically -\def \mpr@savepar {% - \edef \MathparNormalpar - {\noexpand \lineskiplimit \the\lineskiplimit - \noexpand \lineskip \the\lineskip}% - } - -\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} -\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} -\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} -\let \MathparLineskip \mpr@lineskip -\def \mpr@paroptions {\MathparLineskip} -\let \mpr@prebindings \relax - -\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em - -\def \mpr@goodbreakand - {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} -\def \mpr@and {\hskip \mpr@andskip} -\def \mpr@andcr {\penalty 50\mpr@and} -\def \mpr@cr {\penalty -10000\mpr@and} -%\def \mpr@cr {\penalty -10000\vadjust{\vbox{}}\mpr@and} -\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} - -\def \mpr@bindings {% - \let \and \mpr@andcr - \let \par \mpr@andcr - \let \\\mpr@cr - \let \eqno \mpr@eqno - \let \hva \mpr@hva - } -\let \MathparBindings \mpr@bindings - -% \@ifundefined {ignorespacesafterend} -% {\def \ignorespacesafterend {\aftergroup \ignorespaces} - -\newenvironment{mathpar}[1][] - {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering - \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else - \noindent $\displaystyle\fi - \MathparBindings} - {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} - -\newenvironment{mathparpagebreakable}[1][] - {\begingroup - \par - \mpr@savepar \parskip 0em \hsize \linewidth \centering - \mpr@prebindings \mpr@paroptions #1% - \vskip \abovedisplayskip \vskip -\lineskip% - \ifmmode \else $\displaystyle\fi - \MathparBindings - } - {\unskip - \ifmmode $\fi \par\endgroup - \vskip \belowdisplayskip - \noindent - \ignorespacesafterend} - -% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum -% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi} - -%%% HOV BOXES - -\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip - \vbox \bgroup \tabskip 0em \let \\ \cr - \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup - \egroup} - -\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize - \box0\else \mathvbox {#1}\fi} - - -%% Part II -- operations on lists - -\newtoks \mpr@lista -\newtoks \mpr@listb - -\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter -{#2}\edef #2{\the \mpr@lista \the \mpr@listb}} - -\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter -{#2}\edef #2{\the \mpr@listb\the\mpr@lista}} - -\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb -\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} - -\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} -\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} - -\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} -\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} - -\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}% - \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the - \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty - \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop - \mpr@flatten \mpr@all \mpr@to \mpr@one - \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof - \mpr@all \mpr@stripend - \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi - \ifx 1\mpr@isempty - \repeat -} - -\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty - \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp} - -%% Part III -- Type inference rules - -\newif \if@premisse -\newbox \mpr@hlist -\newbox \mpr@vlist -\newif \ifmpr@center \mpr@centertrue -\def \mpr@vskip {} -\def \mpr@htovlist {% - \setbox \mpr@hlist - \hbox {\strut - \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi - \unhbox \mpr@hlist}% - \setbox \mpr@vlist - \vbox {\if@premisse - \box \mpr@hlist - \ifx \mpr@vskip \empty \else - \hrule height 0em depth \mpr@vskip width 0em - \fi - \unvbox \mpr@vlist - \else - \unvbox \mpr@vlist - \ifx \mpr@vskip \empty \else - \hrule height 0em depth \mpr@vskip width 0em - \fi - \box \mpr@hlist - \fi}% -} -% OLD version -% \def \mpr@htovlist {% -% \setbox \mpr@hlist -% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}% -% \setbox \mpr@vlist -% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist -% \else \unvbox \mpr@vlist \box \mpr@hlist -% \fi}% -% } - -\def \mpr@item #1{$\displaystyle #1$} -\def \mpr@sep{2em} -\def \mpr@blank { } -\def \mpr@hovbox #1#2{\hbox - \bgroup - \ifx #1T\@premissetrue - \else \ifx #1B\@premissefalse - \else - \PackageError{mathpartir} - {Premisse orientation should either be T or B} - {Fatal error in Package}% - \fi \fi - \def \@test {#2}\ifx \@test \mpr@blank\else - \setbox \mpr@hlist \hbox {}% - \setbox \mpr@vlist \vbox {}% - \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi - \let \@hvlist \empty \let \@rev \empty - \mpr@tmpdim 0em - \expandafter \mpr@makelist #2\mpr@to \mpr@flat - \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi - \def \\##1{% - \def \@test {##1}\ifx \@test \empty - \mpr@htovlist - \mpr@tmpdim 0em %%% last bug fix not extensively checked - \else - \setbox0 \hbox{\mpr@item {##1}}\relax - \advance \mpr@tmpdim by \wd0 - %\mpr@tmpdim 1.02\mpr@tmpdim - \ifnum \mpr@tmpdim < \hsize - \ifnum \wd\mpr@hlist > 0 - \if@premisse - \setbox \mpr@hlist - \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}% - \else - \setbox \mpr@hlist - \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}% - \fi - \else - \setbox \mpr@hlist \hbox {\unhbox0}% - \fi - \else - \ifnum \wd \mpr@hlist > 0 - \mpr@htovlist - \mpr@tmpdim \wd0 - \fi - \setbox \mpr@hlist \hbox {\unhbox0}% - \fi - \advance \mpr@tmpdim by \mpr@sep - \fi - }% - \@rev - \mpr@htovlist - \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist - \fi - \egroup -} - -%%% INFERENCE RULES - -\@ifundefined{@@over}{% - \let\@@over\over % fallback if amsmath is not loaded - \let\@@overwithdelims\overwithdelims - \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims - \let\@@above\above \let\@@abovewithdelims\abovewithdelims - }{} - -%% The default - -\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em - $\displaystyle {#1\mpr@over #2}$}} -\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em - $\displaystyle {#1\@@atop #2}$}} - -\let \mpr@fraction \mpr@@fraction - -%% A generic solution to arrow - -\def \mpr@@fractionaboveskip {0ex} -\def \mpr@@fractionbelowskip {0.22ex} - -\def \mpr@make@fraction #1#2#3#4#5{\hbox {% - \def \mpr@tail{#1}% - \def \mpr@body{#2}% - \def \mpr@head{#3}% - \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}% - \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}% - \dimen0\ht3\advance\dimen0 by \dp3\relax - \dimen0 0.5\dimen0\relax - \advance \dimen0 by \mpr@@fractionaboveskip - \setbox1=\hbox {\raise \dimen0 \box1}\relax - \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0 - \advance \dimen0 by \mpr@@fractionbelowskip - \setbox2=\hbox {\lower \dimen0 \box2}\relax - \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}% - \dimen0=\wd0\box0 - \box0 \hskip -\dimen0\relax - \hbox to \dimen0 {$%\color{blue} - \mathrel{\mpr@tail}\joinrel - \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% - $}}} - -%% Old stuff should be removed in next version -\def \mpr@@nothing #1#2 - {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$} -\def \mpr@@reduce #1#2{\hbox - {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} -\def \mpr@@rewrite #1#2#3{\hbox - {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}} -\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} - -\def \mpr@empty {} -\def \mpr@inferrule - {\bgroup - \ifnum \linewidth<\hsize \hsize \linewidth\fi - \mpr@rulelineskip - \let \and \qquad - \let \hva \mpr@hva - \let \@rulename \mpr@empty - \let \@rule@options \mpr@empty - \let \mpr@over \@@over - \mpr@inferrule@} -\newcommand {\mpr@inferrule@}[3][] - {\everymath={\displaystyle}% - \def \@test {#2}\ifx \empty \@test - \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% - \else - \def \@test {#3}\ifx \empty \@test - \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% - \else - \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% - \fi \fi - \def \@test {#1}\ifx \@test\empty \box0 - \else \vbox -%%% Suggestion de Francois pour les etiquettes longues -%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi - {\hbox {\DefTirName {#1}}\box0}\fi - \egroup} - -\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} - -% They are two forms -% \inferrule [label]{[premisses}{conclusions} -% or -% \inferrule* [options]{[premisses}{conclusions} -% -% Premisses and conclusions are lists of elements separated by \\ -% Each \\ produces a break, attempting horizontal breaks if possible, -% and vertical breaks if needed. -% -% An empty element obtained by \\\\ produces a vertical break in all cases. -% -% The former rule is aligned on the fraction bar. -% The optional label appears on top of the rule -% The second form to be used in a derivation tree is aligned on the last -% line of its conclusion -% -% The second form can be parameterized, using the key=val interface. The -% folloiwng keys are recognized: -% -% width set the width of the rule to val -% narrower set the width of the rule to val\hsize -% before execute val at the beginning/left -% lab put a label [Val] on top of the rule -% lskip add negative skip on the right -% left put a left label [Val] -% Left put a left label [Val], ignoring its width -% right put a right label [Val] -% Right put a right label [Val], ignoring its width -% leftskip skip negative space on the left-hand side -% rightskip skip negative space on the right-hand side -% vdots lift the rule by val and fill vertical space with dots -% after execute val at the end/right -% -% Note that most options must come in this order to avoid strange -% typesetting (in particular leftskip must preceed left and Left and -% rightskip must follow Right or right; vdots must come last -% or be only followed by rightskip. -% - -%% Keys that make sence in all kinds of rules -\def \mprset #1{\setkeys{mprset}{#1}} -\define@key {mprset}{andskip}[]{\mpr@andskip=#1} -\define@key {mprset}{lineskip}[]{\lineskip=#1} -\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip} -\define@key {mprset}{flushleft}[]{\mpr@centerfalse} -\define@key {mprset}{center}[]{\mpr@centertrue} -\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} -\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction} -\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} -\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} -% To be documented. -\define@key {mprset}{defaultfraction}[]{\let \mpr@fraction \mpr@@fraction} -\define@key {mprset}{sep}{\def\mpr@sep{#1}} -\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}} -\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}} -\define@key {mprset}{style}[1]{\def\TirNameStyle{#1}def} -\define@key {mprset}{rightstyle}[1]{\def\RightTirNameStyle{#1}} -\define@key {mprset}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} -\define@key {mprset}{vskip}[1]{\def \mpr@vskip{#1}} - -\newbox \mpr@right -\define@key {mpr}{flushleft}[]{\mpr@centerfalse} -\define@key {mpr}{center}[]{\mpr@centertrue} -\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} -\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1} -\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} -\define@key {mpr}{width}{\hsize #1} -\define@key {mpr}{sep}{\def\mpr@sep{#1}} -\define@key {mpr}{before}{#1} -\define@key {mpr}{lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} -\define@key {mpr}{Lab}{\let \DefTirName \LabTirName \def \mpr@rulename {#1}} -\define@key {mpr}{style}[1]{\def\TirNameStyle{#1}def} -\define@key {mpr}{rightstyle}[1]{\def\RightTirNameStyle{#1}} -\define@key {mpr}{leftstyle}[1]{\def\LeftTirNameStyle{#1}} -\define@key {mpr}{vskip}[1]{\def \mpr@vskip{#1}} -\define@key {mpr}{narrower}{\hsize #1\hsize} -\define@key {mpr}{leftskip}{\hskip -#1} -\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} -\define@key {mpr}{rightskip} - {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} -\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax - \advance \hsize by -\wd0\box0} - -\define@key {mpr}{left}{\setbox0 \hbox {$\LeftTirName {#1}\;$}\relax - \advance \hsize by -\wd0\box0} -\define@key {mpr}{Left}{\llap{$\LeftTirName {#1}\;$}} -\define@key {mpr}{right} - {\setbox0 \hbox {$\;\RightTirName {#1}$}\relax \advance \hsize by -\wd0 - \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} -\define@key {mpr}{RIGHT} - {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0 - \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} -\define@key {mpr}{Right} - {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\RightTirName {#1}$}}} -\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} -\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} -\define@key {mpr}{vcenter}[]{\mpr@vcentertrue} - -\newif \ifmpr@vcenter \mpr@vcenterfalse -\newcommand \mpr@inferstar@ [3][]{\begingroup - \setbox0 \hbox - {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax - \setbox \mpr@right \hbox{}% - \setkeys{mpr}{#1}% - $\ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else - \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi - \box \mpr@right \mpr@vdots$ - \ifmpr@vcenter \aftergroup \mpr@vcentertrue \fi} - \ifmpr@vcenter - \box0 - \else - \setbox1 \hbox {\strut} - \@tempdima \dp0 \advance \@tempdima by -\dp1 - \raise \@tempdima \box0 - \fi - \endgroup} - -\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} -\newcommand \mpr@err@skipargs[3][]{} -\def \mpr@inferstar*{\ifmmode - \let \@do \mpr@inferstar@ - \else - \let \@do \mpr@err@skipargs - \PackageError {mathpartir} - {\string\inferrule* can only be used in math mode}{}% - \fi \@do} - - -%%% Exports - -% Envirnonment mathpar - -\let \inferrule \mpr@infer - -% make a short name \infer is not already defined -\@ifundefined {infer}{\let \infer \mpr@infer}{} - -\def \TirNameStyle #1{\small \textsc{#1}} -\def \LeftTirNameStyle #1{\TirNameStyle {#1}} -\def \RightTirNameStyle #1{\TirNameStyle {#1}} - -\def \lefttir@name #1{\hbox {\small \LeftTirNameStyle{#1}}} -\def \righttir@name #1{\hbox {\small \RightTirNameStyle{#1}}} -\let \TirName \lefttir@name -\let \LeftTirName \lefttir@name -\let \DefTirName \lefttir@name -\let \LabTirName \lefttir@name -\let \RightTirName \righttir@name - -%%% Other Exports - -% \let \listcons \mpr@cons -% \let \listsnoc \mpr@snoc -% \let \listhead \mpr@head -% \let \listmake \mpr@makelist - - - - -\endinput diff --git a/documentation/website/docs/formal/subtyping_description/pyre_sub.tex b/documentation/website/docs/formal/subtyping_description/pyre_sub.tex deleted file mode 100644 index c2b9a3dc3ce..00000000000 --- a/documentation/website/docs/formal/subtyping_description/pyre_sub.tex +++ /dev/null @@ -1,339 +0,0 @@ -%% -% Copyright (c) Meta Platforms, Inc. and affiliates. -% -% This source code is licensed under the MIT license found in the -% LICENSE file in the root directory of this source tree. -%% - -\documentclass[a4paper]{article} - -\usepackage[T1]{fontenc} -\usepackage[utf8]{inputenc} -\usepackage[english]{babel} -\usepackage{amsmath,amssymb} -\usepackage{comment} -\usepackage{mathpartir} -\usepackage{listings} -\usepackage{textcomp} -\usepackage[scaled=0.85]{DejaVuSansMono} -\usepackage{hyperref} - -% local ocaml style -\usepackage{lstocaml} - -% bunch of macros to mimic type.ml definitions -\newcounter{pyrule} -\setcounter{pyrule}{1} - -\newcommand{\pyList}[1]{#1_{\ldots}} -\newcommand{\pyTok}[1]{\texttt{#1}} -\newcommand{\ruleName}[1]{\small\textsc{\thepyrule-#1}\stepcounter{pyrule}} - -\newcommand{\pyAny}{\pyTok{Any}} -\newcommand{\pyTop}{\pyTok{Top}} -\newcommand{\pyBottom}{\pyTok{Bottom}} -\newcommand{\pyUndeclared}{\pyTok{Undeclared}} -\newcommand{\pyPrimitive}[1]{\pyTok{Primitive}[\text{``#1''}]} -\newcommand{\pyObject}{\pyPrimitive{object}} -\newcommand{\pyVariable}[1]{\pyTok{Variable}[#1]} -\newcommand{\pyPVC}[1]{\pyTok{ParameterVariadicComponent}[#1]} -\newcommand{\pyAnnotated}[1]{\pyTok{Annotated}[#1]} -\newcommand{\pyOptional}[1]{\pyTok{Optional}[#1]} -\newcommand{\pyTuple}[1]{\pyTok{Tuple}[#1]} -\newcommand{\pyBoundedTuple}[1]{\pyTuple{\pyTok{Bounded} (#1)}} -\newcommand{\pyConcreteTuple}[1]{\pyBoundedTuple{\pyTok{Concrete}[#1]}} -\newcommand{\pyUnboundedTuple}[1]{\pyTuple{#1, \ldots}} -\newcommand{\pyParametric}[2]{\pyTok{Parametric}[\text{``#1''}][#2]} -\newcommand{\pyRawCallable}[3]{\pyTok{Callable}[#1, #2, #3]} -\newcommand{\pyCallable}[1]{\pyTok{Callable}[#1]} -\newcommand{\pyFun}[1]{\pyRawCallable{\pyTok{Named}[\text{``#1''}]}{\_}{\_}} -\newcommand{\pyTypedDictionary}[1]{\pyTok{TypedDictionary}[#1]} -\newcommand{\pyLiteral}[1]{\pyTok{Literal}[#1]} - -\newcommand{\PyreRevision}{a9b640f6953f0d41d8c96c595ae60ea2952bdce5} -\begin{document} - -\title{Pyre subtyping relation} -\date{July 4th, 2019} -\author{Vincent Siles} - -\maketitle - -\section{Forewords} -As Pyre is a fast moving target, this file has been written using the revision -\texttt{\PyreRevision}. This code can be found -at \href{https://github.com/facebook/pyre-check}{Facebook's github repository}. - -\section{Type definitions and helper functions} -All type definitions and helper functions can be found in the -\href{https://github.com/facebook/pyre-check/tree/\PyreRevision/analysis/type.ml}{\texttt{analysis/type.ml}} -file. - -\section{Subtyping algorithm} - -The following algorithm is a description of the typing rules checked by -the \texttt{less\_or\_equal} function (see -\href{https://github.com/facebook/pyre-check/tree/\PyreRevision/analysis/typeOrder.ml}{\texttt{analysis/typeOrder.ml}}). - -The algorithm is performing some sanity checks (types are actually -tracked, expected variance is actually a valid one, \ldots). In case where -these tests are failing, an exception is raised. We won't discuss these -cases here. - -The following rules must be used in the described order. The first rule that -matches must be used. -\\ - -\begin{center} -\begin{tabular}{ccc} - \inferrule{S = T}{S\le T} \\ - \ruleName{struct.eq} \\ \\ - - \inferrule{~}{T \le\pyAny} \\ - \ruleName{any.right} \\ \\ - - \inferrule{\pyUndeclared\notin{} S}{S \le\pyTop} \\ - \ruleName{top.right} \\ \\ - - \inferrule{Top \le{} T}{\bot} \\ - \ruleName{top.left} \\ \\ - - \inferrule{\texttt{Config[any\_is\_bottom]} = true}{\pyAny\le{} T} \\ - \ruleName{any.left} \\ \\ - - \inferrule{~}{\pyBottom\le{} T} \\ - \ruleName{bot.left} \\ \\ - - \inferrule{S \le\pyBottom}{\bot} \\ - \ruleName{bot.right} \\ \\ - - \inferrule{~}{S \le\pyObject} \\ - \ruleName{object.right} \\ \\ - - \inferrule{S \le\pyVariable{T}}{\bot} \\ - \ruleName{Variable.right} \\ \\ - - \inferrule{\pyPVC{\_}\le{} \_}{\bot} \\ - \ruleName{pvc.left} \\ \\ - - \inferrule{\_ \le\pyPVC{\_}}{\bot} \\ - \ruleName{pvc.right} \\ \\ - - \inferrule{S \le{} T}{\pyAnnotated{S} \le{} T} \\ - \ruleName{annotated.left} -\end{tabular} -\end{center} - - - -\begin{center} -\begin{tabular}{ccc} - \inferrule{S \le{} T}{S \le\pyAnnotated{T}} \\ - \ruleName{annotated.right} \\ \\ - - \inferrule{\text{See next section}} - {\pyParametric{S}{\pyList{X}}\le\pyParametric{T}{\pyList{Y}}} \\ - \ruleName{parametric} \\ \\ - - \inferrule{\forall{} i, A_i \le{} B}{\bigcup_i{A_i} \le{} B} \\ - \ruleName{union.left} \\ \\ - - \inferrule{\exists{} k, \pyVariable{S}\le{} B_k~\|~\texttt{upper\_bound} (\pyVariable{S}) \le\bigcup_i{B_i}} - {\pyVariable{S}\le\bigcup_i{B_i}} \\ - \ruleName{variable.union} \\ \\ - - \inferrule{\exists{} k, A \le{} B_k}{A \le\bigcup_i{B_i}} \\ - \ruleName{union.right} \\ \\ - - \inferrule{\pyVariable{S}\le{} T~\|~\texttt{upper\_bound} (\pyVariable{S}) \le\pyOptional{T}} - {\pyVariable{S}\le\pyOptional{T}} \\ - \ruleName{variable.optional} \\ \\ - - \inferrule{S \le{} T}{\pyOptional{S} \le\pyOptional{T}} \\ - \ruleName{optional} \\ \\ - - \inferrule{S \le{} T}{S \le\pyOptional{T}} \\ - \ruleName{optional.right} \\ \\ - - \inferrule{\pyOptional{S} \le{} T}{\bot} \\ - \ruleName{optional.fallback} \\ \\ - - \inferrule{\texttt{upper\_bound} (\pyVariable{S}) \le{} T}{\pyVariable{S}\le{} T} \\ - \ruleName{variable.fallback} \\ \\ - - \inferrule{~}{\pyTuple{\_} \le\pyBoundedTuple{\pyAny}} \\ - \ruleName{tuple.any.right} -\end{tabular} -\end{center} - - - -\begin{center} -\begin{tabular}{ccc} - \inferrule{~}{\pyBoundedTuple{\pyAny}\le\pyTuple{\_}} \\ - \ruleName{tuple.any.left} \\ \\ - - \inferrule{|S| = |T| \\ \forall{} i, S_i \le{} T_i} - {\pyConcreteTuple{\pyList{S}}\le\pyConcreteTuple{\pyList{T}}} \\ - \ruleName{tuple.concrete} \\ \\ - - %% vsiles notes: I don't get this rule. What could be bigger than object ? - \inferrule{\pyUnboundedTuple{\pyObject}\le{} T} - {\pyBoundedTuple{\pyVariable{\_}}\le{} T} \\ - \ruleName{tuple.variable.left} \\ \\ - - \inferrule{S \le\pyBoundedTuple{\pyVariable{\_}}}{\bot} \\ - \ruleName{tuple.variable.right} \\ \\ - - \inferrule{S \le{} T}{\pyUnboundedTuple{S}\le\pyUnboundedTuple{T}} \\ - \ruleName{tuple.unbounded} \\ \\ - - %% vsiles notes: When do we encounter Concrete [] ? Only with explicit () - %% or in some internal routine ? - \inferrule{~}{\pyConcreteTuple{~}\le\pyUnboundedTuple{T}} \\ - \ruleName{tuple.empty.unbounded} \\ \\ - - \inferrule{\pyList{S}\not= [] \\ \texttt{join} (\pyList{S})\le{} T} - {\pyConcreteTuple{\pyList{S}}\le\pyUnboundedTuple{T}} \\ - \ruleName{tuple.concrete.unbounded} \\ \\ - - \inferrule{\pyParametric{tuple}{\texttt{union\_upper\_bound} (S)}\le\pyParametric{name}{args}} - {\pyBoundedTuple{S}\le\pyParametric{name}{args}} \\ - \ruleName{tuple.bounded.parametric} \\ \\ - - \inferrule{\pyParametric{tuple}{[S]}\le\pyParametric{name}{args}} - {\pyUnboundedTuple{S}\le\pyParametric{name}{args}} \\ - \ruleName{tuple.unbounded.parametric} \\ \\ - - \inferrule{\pyParametric{tuple}{[S]}\le\pyPrimitive{T}} - {\pyUnboundedTuple{S}\le\pyPrimitive{T}} \\ - \ruleName{tuple.primitive.unbounded} \\ \\ - - \inferrule{\pyList{S}\not= [] \\ \pyParametric{tuple}{\texttt{join} (\pyList{S})}\le\pyPrimitive{T}} - {\pyConcreteTuple{\pyList{S}}\le\pyPrimitive{T}} \\ - \ruleName{tuple.primitive.concrete} \\ \\ - - \inferrule{~}{\pyPrimitive{tuple}\le\pyTuple{\_}} \\ - \ruleName{primitive.tuple} -\end{tabular} -\end{center} - - - - -\begin{center} -\begin{tabular}{ccc} - \inferrule{\pyTuple{\_}\le{}T}{\bot} \\ - \ruleName{tuple.sink.left} \\ \\ - - \inferrule{S\le\pyTuple{\_}}{\bot} \\ - \ruleName{tuple.sink.right} \\ \\ - - \inferrule{\text{``f''} = \text{``g''}}{\pyFun{f}\le\pyFun{g}} \\ - \ruleName{callable.named} \\ \\ - - \inferrule{F\approx{} implem \\ \forall{}i, F\approx{}overloads_i} - {\pyCallable{F}\le\pyRawCallable{\_}{implem}{\pyList{overloads}}} \\ - \ruleName{callable.compat} \\ \\ - - %% vsiles notes: I have absolutely no clue about that one - \inferrule{\pyTok{is\_meta} (S) \\ |S|.params = 1 \\ S' = \pyTok{constructor} - (\texttt{protocol\_assuptions}, S.params[0]) \\ S'\le\pyCallable{F}} - {S\le\pyCallable{F}} \\ - \ruleName{callable.protocol} \\ \\ - - \inferrule{\pyPrimitive{F}\le\pyPrimitive{G}} - {\pyParametric{F}{\pyList{X}}\le\pyPrimitive{G}} \\ - \ruleName{parametric.primitive} \\ \\ - - \inferrule{\pyParametric{F}{[~]}\le\pyParametric{G}{\pyList{Y}}} - {\pyPrimitive{F}\le\pyParametric{G}{\pyList{Y}}} \\ - \ruleName{primitive.parametric} \\ \\ - - \inferrule{\texttt{join} (\pyParametric{typing.Callable}{[\pyBottom]}, S)= - \pyParametric{typing.Callable}{[S']} \\ S' \le{}\pyCallable{F}} - {S \le\pyCallable{F}} \\ - \ruleName{callable.join} \\ \\ - - \inferrule{\_\le\pyCallable{\_}}{\bot} \\ - \ruleName{callable.sink.right} \\ \\ - - \inferrule{\pyCallable{\_}\le\_}{\bot} \\ - \ruleName{callable.sink.left} \\ \\ - - \inferrule{\pyTypedDictionary{S}.total = \pyTypedDictionary{T}.total \\ - \texttt{same\_fields} (\pyTypedDictionary{S}, \pyTypedDictionary{T})} - {\pyTypedDictionary{S}\le\pyTypedDictionary{T}} \\ - \ruleName{typeddictionary} -\end{tabular} -\end{center} - - - - -\begin{center} -\begin{tabular}{ccc} - \inferrule{\pyPrimitive{TypedDictionary}\le{} T}{\pyTypedDictionary{\_}\le{} T} \\ - \ruleName{typeddictionary.left} \\ \\ - - \inferrule{S \le\pyPrimitive{TypedDictionary}}{S \le\pyTypedDictionary{\_}} \\ - \ruleName{typeddictionary.right} \\ \\ - - \inferrule{S \le\pyLiteral{\_}}{\bot} \\ - \ruleName{literal.right} \\ \\ - - \inferrule{\texttt{weaken\_literal} (\pyLiteral{S})\le{} T}{\pyLiteral{S}\le{} T} \\ - \ruleName{literal.left} -\end{tabular} -\end{center} - - - -If all the above steps fail, the \texttt{Handler} module/struct is used -to look into the type hierarchy and check if the left hand side is a -nominal subtype of the right hand side (as described by \texttt{class} -inheritance). - -\subsection{\textsc{parametric} rule} - -In this section we are trying to test if -$\pyParametric{S}{\pyList{X}}\le\pyParametric{T}{\pyList{Y}}$. -Since the rule is a bit too complex, we'll describe it here with some details. - -\begin{enumerate} - \item An auxiliary function \pyTok{compare\_parameter (S, T, v)} - compares two types \pyTok{S} and \pyTok{T}, taking into account the - variance \pyTok{v} (usually the variance of \pyTok{S}). - \begin{itemize} - \item There are some shady cases that need to be discussed, which forces - the result of $\le$ compared to $\pyTop$ and $\pyBottom$, - disregarding the variance. - \item If \pyTok{v} is \pyTok{Covariant}, we test if - $\pyTok{S}\le\pyTok{T}$. - \item If \pyTok{v} is \pyTok{Contraviant}, we test if - $\pyTok{T}\le\pyTok{S}$. - \item If \pyTok{v} is \pyTok{Invariant}, we test equality - $\pyTok{S}\le\pyTok{T} \wedge \pyTok{T}\le\pyTok{S}$. - \end{itemize} - - - \item \pyTok{S} and \pyTok{T} are checked to be related in the - class hierarchy (implemanted by \texttt{Hander}). If a valid relation - is spotted, their arguments are check by the comparison function: - \begin{itemize} - \item They must have the same length. - \item The variance list must be of the same length then - $\pyList{X}$. - \item Folding \pyTok{compare\_parameter} on all three lists must - succeed - \end{itemize} -\end{enumerate} - - -\subsection{About $\approx$} - -$F \approx Sig$ means that $F$ is compatible (as in could be used as, see -\texttt{simulate\_signature\_select} in \texttt{analysis/type.ml}) with -the specified signature. - -\end{document}