left with machineries, future work, appendices, biblio, style

final-report-new/._wordcount_selection.tex

@@ -1 +1,2 @@
-cmd
+
+\section{Tactics and Proof Machineries}

final-report-new/05-modular.tex

@@ -65,31 +65,69 @@ \section{The Modular Environment}
 \newcommand{\pcuicc}[3]{\inputminted[firstline={#1},lastline={#2},linenos]{Coq}{
   code/v2/pcuic/theories/#3}}
 
-It would be beneficial to unify these two with the same structure: modules. The
-list of global declarations itself can be seen as an anonymous, ambient,
-top-level module, thus just a special case of a module. Under this
+It would be beneficial to unify modules and environments into a single structure
+- modules. The list of global declarations itself can be seen as an anonymous,
+ambient, top-level module, thus just a special case of a module. Under this
 generalization, any well-formedness properties or well-typedness properties
 about environments should be subsumed under that of modules, and thus giving us
 a good sense in defining the typing rules for modules.
 
+\subsection{Definition of the Data Structure}
 Let us begin by defining modules, then specialize into global declarations:
 
-\tcc{325}{336}{Environment.v}
+\tcc{325}{338}{Environment.v}
 
 Structure field now subsumes global declaration, and we note that structure body
 is just a convenient name for the list of structure fields indexed by its name -
 an identifier. The possible nested structure body inside structure fields are
 what gives the tree structure of modules.
 
-\tcc{405}{408}{Environment.v}
+\tcc{409}{412}{Environment.v}
 
 Similarly, we define module types to be structure bodies, and a module to be a
 module type with an implementation. Since global environments are anonymous
 modules, they do not have a possibility of reuse and thus signature is
 insignificant here - it is of the same structure of a structure body.
 
+So, how do we tell apart a global environment? One way to do it is to
+differentiate it by the directory path to the file.
 
+\tcc{478}{482}{Environment.v}
 
+\subsection{Definition of Typing Rules}
+This section of typing rules are not yet finalized, and are still experimental.
+However, they illustrate a possible set of rules that can implemented and then
+verified against various properties.
+
+\tcc{1271}{1282}{EnvironmentTyping.v}
+\tcc{1292}{1298}{EnvironmentTyping.v}
+
+Structure fields and module implementations are typed accordingly: constants and
+inductives are typed as-if, while modules and module types are typed
+recursively. Module implementation checks relevant definitions except for the
+case of an algebraic expression (in our case an alias to a defined module),
+requires a proof that such a aliased target exists.
+
+The interesting part that is different from the previous implementation is the
+combination of the information when typing a structure body:
+
+\tcc{1284}{1290}{EnvironmentTyping.v}
+
+This time, the typing rules for structure body includes typical checks as in the
+global environment. If we focus on the \verb|on_sb_cons| constructor for the
+inductive case, the checks include
+\begin{enumerate}
+  \item the correctness of the prefix structure body against the environment,
+  \item the freshness of identifier \verb|i| against the prefix structure body
+  and the environment,
+  \item the universe declaration of the structure field,
+  \item and the recursive check to the structure field itself.
+\end{enumerate} 
+
+We define naturally the below:
+
+\tcc{1301}{1302}{EnvironmentTyping.v}
+\tcc{1312}{1312}{EnvironmentTyping.v}
 
 \section{Tactics and Proof Machineries}
 \begin{itemize}

final-report-new/code/v2/template-coq/theories/._wordcount_selection.tex

@@ -0,0 +1 @@
+    (* Record on_structure_field_data (on_structure_field : global_env_ext -> structure_field -> Type)

final-report-new/code/v2/template-coq/theories/Environment.v

@@ -325,12 +325,16 @@ Module Environment (T : Term).
   Inductive structure_field :=
   | ConstantDecl : constant_body -> structure_field
   | InductiveDecl : mutual_inductive_body -> structure_field
-  | ModuleDecl : module_implementation -> list (ident × structure_field) -> structure_field
+  | ModuleDecl :
+      module_implementation
+      -> list (ident × structure_field)
+      -> structure_field
   | ModuleTypeDecl : list (ident × structure_field) -> structure_field
   with module_implementation :=
   | mi_abstract : module_implementation (** Declare Module M: T. *)
   | mi_algebraic : kername -> module_implementation (** Module M [:T] := N. *)
-  | mi_struct : list (ident × structure_field) -> module_implementation (** Module M:T. ... End M.*)
+  | mi_struct : (** Module M:T. ... End M.*)
+      list (ident × structure_field) -> module_implementation 
   | mi_fullstruct : module_implementation (** Module M. ... End M.*).
 
   Notation structure_body := (list (ident × structure_field))%type.

final-report-new/code/v2/template-coq/theories/EnvironmentTyping.v

@@ -1230,75 +1230,73 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT
     Definition fresh_structure_body (i: ident) (sb: structure_body) :=
       All (fun '(i', _) => i <> i') sb.
 
-    (* Record on_structure_field_data (on_structure_field : global_env_ext -> structure_field -> Type)
-      univs sb retro path (udecl: universes_decl) i sf :=
-      {
-          ident_fresh :  fresh_structure_body i sb ;
-          udecl := universes_decl_of_decl sf ;
-          on_udecl_udecl : on_udecl univs udecl ;
-          on_global_decl_d : on_structure_field (mk_global_env univs sb retro path, udecl) sf
-      }. *)
+Record on_structure_field_data
+(on_structure_field : global_env_ext -> structure_field -> Type)
+univs sb retro path (udecl: universes_decl) i sf :=
+  {
+    ident_fresh :  fresh_structure_body i sb ;
+    udecl := universes_decl_of_decl sf ;
+    on_udecl_udecl : on_udecl univs udecl ;
+    on_global_decl_d : on_structure_field (mk_global_env univs sb retro path, udecl) sf
+  }.
 
     Record on_structure_field_data Σ sb i sf :=
       {
           ident_fresh : fresh_structure_body i sb ;
           udecl := universes_decl_of_decl sf ;
           on_udecl_udecl : on_udecl univs udecl ;
-
           on_structure_field_sb : on_structure_field  sf
       }.
 
-    (* Inductive on_structure_body on_structure_field : structure_body -> Type :=
-      | on_sb_nil : on_structure_body on_structure_field nil
-      | on_sb_cons univs sb retro path udecl i sf :
-          on_structure_body on_structure_field sb ->
-          on_structure_field_data on_structure_field univs sb retro path udecl i sf ->
-          on_structure_body on_structure_field (sb ,, (i, sf)). *)
-
-    Inductive on_structure_field Σ : structure_field -> Type :=
-      | on_ConstantDecl c :
-          on_constant_body Σ c -> on_structure_field Σ (ConstantDecl c)
-      | on_InductiveDecl kn inds :
-          on_inductive Σ kn inds -> on_structure_field Σ (InductiveDecl inds)
-      | on_ModuleDecl mi mt :
-          on_module_impl Σ mi ->
-          on_structure_body on_structure_field mt -> (* module type must be correct wrt Σ. *)
-          on_structure_field Σ (ModuleDecl mi mt)
-      | on_ModuleTypeDecl mtd :
-        on_structure_body Σ mtd ->
-        on_structure_field Σ (ModuleTypeDecl mtd)
-    with on_module_impl Σ : module_implementation -> Type :=
-      | on_mi_abstract : on_module_impl Σ mi_abstract
-      | on_mi_algebraic kn : (exists mi mt, lookup_env Σ kn = Some (ModuleDecl mi mt))
-                              -> on_module_impl Σ (mi_algebraic kn)
-      | on_mi_struct sb : on_structure_body Σ sb -> on_module_impl Σ (mi_struct sb)
-      | on_mi_fullstruct : on_module_impl Σ mi_fullstruct.
-
-    Inductive on_structure_field Σ : structure_field -> Type :=
-      | on_ConstantDecl c :
-          on_constant_body Σ c -> on_structure_field Σ (ConstantDecl c)
-      | on_InductiveDecl kn inds :
-          on_inductive Σ kn inds -> on_structure_field Σ (InductiveDecl inds)
-      | on_ModuleDecl mi mt :
-          on_module_impl Σ mi ->
-          on_structure_body on_structure_field mt -> (* module type must be correct wrt Σ. *)
-          on_structure_field Σ (ModuleDecl mi mt)
-      | on_ModuleTypeDecl mtd :
-        on_structure_body Σ mtd ->
-        on_structure_field Σ (ModuleTypeDecl mtd)
-    with on_structure_body (Σ: global_env_ext) : structure_body -> Type :=
-      | on_sb_nil : on_structure_body Σ nil
-      | on_sb_cons Σ sb i sf :
-          on_structure_body Σ sb ->
-          on_structure_field_data on_structure_field univs sb retro path udecl i sf ->
-          on_structure_body on_structure_field (sb ,, (i, sf)).
-
-    with on_module_impl Σ : module_implementation -> Type :=
-      | on_mi_abstract : on_module_impl Σ mi_abstract
-      | on_mi_algebraic kn : (exists mi mt, lookup_env Σ kn = Some (ModuleDecl mi mt))
-                              -> on_module_impl Σ (mi_algebraic kn)
-      | on_mi_struct sb : on_structure_body Σ sb -> on_module_impl Σ (mi_struct sb)
-      | on_mi_fullstruct : on_module_impl Σ mi_fullstruct.
+Inductive on_structure_field Σ : structure_field -> Type :=
+  | on_ConstantDecl c :
+      on_constant_body Σ c -> on_structure_field Σ (ConstantDecl c)
+  | on_InductiveDecl kn inds :
+      on_inductive Σ kn inds -> on_structure_field Σ (InductiveDecl inds)
+  | on_ModuleDecl mi mt :
+      on_module_impl Σ mi
+      -> on_structure_body on_structure_field mt
+      -> on_structure_field Σ (ModuleDecl mi mt)
+  | on_ModuleTypeDecl mtd :
+    on_structure_body Σ mtd
+    -> on_structure_field Σ (ModuleTypeDecl mtd)
+with on_module_impl Σ : module_implementation -> Type :=
+  | on_mi_abstract : on_module_impl Σ mi_abstract
+  | on_mi_algebraic kn :
+      (exists mi mt, lookup_env Σ kn = Some (ModuleDecl mi mt))
+      -> on_module_impl Σ (mi_algebraic kn)
+  | on_mi_struct sb : on_structure_body Σ sb -> on_module_impl Σ (mi_struct sb)
+  | on_mi_fullstruct : on_module_impl Σ mi_fullstruct.
+
+Inductive on_structure_field Σ : structure_field -> Type :=
+  | on_ConstantDecl c :
+      on_constant_body Σ c -> on_structure_field Σ (ConstantDecl c)
+  | on_InductiveDecl kn inds :
+      on_inductive Σ kn inds -> on_structure_field Σ (InductiveDecl inds)
+  | on_ModuleDecl mi mt :
+      on_module_impl Σ mi ->
+      on_structure_body on_structure_field mt ->
+      on_structure_field Σ (ModuleDecl mi mt)
+  | on_ModuleTypeDecl mtd :
+      on_structure_body Σ mtd ->
+      on_structure_field Σ (ModuleTypeDecl mtd)
+
+with on_structure_body (Σ: global_env_ext) : structure_body -> Type :=
+  | on_sb_nil : on_structure_body Σ nil
+  | on_sb_cons Σ sb i sf :
+      on_structure_body Σ sb ->
+      fresh_structure_body Σ i sb ->
+      on_udecl Σ (universes_decl_of_decl sf) ->
+      on_structure_field Σ sf ->
+      on_structure_body Σ (sb ,, (i, sf))
+
+with on_module_impl Σ : module_implementation -> Type :=
+  | on_mi_abstract : on_module_impl Σ mi_abstract
+  | on_mi_algebraic kn :
+      (exists mi mt, lookup_env Σ kn = Some (ModuleDecl mi mt)) ->
+      on_module_impl Σ (mi_algebraic kn)
+  | on_mi_struct sb : on_structure_body Σ sb -> on_module_impl Σ (mi_struct sb)
+  | on_mi_fullstruct : on_module_impl Σ mi_fullstruct.
 
     Definition on_module_type_decl := on_structure_body.
     Definition on_module_decl Σ m := on_module_impl Σ m.1 × on_module_type_decl Σ m.2.