Put dup, drop, and pairs in the base fragment

Makefile

@@ -18,9 +18,6 @@ OTT_FILES_LIST = \
   toplevel_definition.ott \
   arith.ott \
   unit.ott \
-  pair.ott \
-  drop.ott \
-  dup.ott \
   pattern_matching.ott \
   variant.ott \
   option.ott \

ott/base.ott

@@ -11,6 +11,8 @@ grammar
 % We do not distinguish variables from field labels (nor environments from records)
 label, l, var, x :: 'label_' ::= {{coq string}} {{com Label / variable}} 
   | id :: S :: user {{coq [[id]]}} {{ocaml (Aux.explode [[id]])}}
+  | car :: M :: car {{coq "car"%string}} {{ocaml (Aux.explode "car")}} {{com First component of a binary pair}}
+  | cdr :: M :: cdr {{coq "cdr"%string}} {{ocaml (Aux.explode "cdr")}} {{com Second component of a binary pair}}
 
 rty :: 'rty_' ::= {{com Record type}}
   | { l_1 : ty_1 ; .. ; l_n : ty_n } :: :: record
@@ -20,6 +22,7 @@ rty :: 'rty_' ::= {{com Record type}}
 ty, a, b, c :: 'ty_' ::= {{com Type}} {{menhir-start }}
   | rty :: :: rty {{com Record type}}
   | ( ty ) :: S :: paren {{icho ( [[ty]] )}} {{com Parenthesised type}}
+  | ty * ty' :: :: prod {{com Binary product type}}
 
 
 %% Instructions
@@ -28,10 +31,14 @@ instruction, I, ins :: 'instr_' ::= {{com Instruction}}
   | noop :: :: noop {{com No operation}}
   | instruction_1 ; instruction_2 :: :: seq {{com Sequencing}}
   | lhs = rhs :: :: assign {{com Assignment}}
+  | drop var :: :: drop {{com Resource dropping}}
 
 lhs :: 'lhs_' ::= {{com Left-hand side of assignement}}
   | var :: :: var
   | { l_1 = var_1 ; .. ; l_n = var_n } :: :: record
+  | ( var_1 , var_2 ) :: S :: pair
+  {{coq lhs_record (("car", [[var_1]])::("cdr", [[var_2]])::nil)}}
+  {{ocaml Lhs_record [((Aux.explode "car"), [[var_1]]);((Aux.explode "cdr"), [[var_2]])]}}
 
 rhs :: 'rhs_' ::= {{com Right-hand side of assignments}}
   | arg :: :: arg
@@ -40,6 +47,7 @@ rhs :: 'rhs_' ::= {{com Right-hand side of assignments}}
   | { var with l_1 = var_1 ; ... ; l_n = var_n } :: :: update
 
 f :: 'fun_' ::= {{com Function symbol}}
+  | dup :: :: dup
 
 arg :: 'arg_' ::= {{com Function argument}}
   | var :: :: var
@@ -150,6 +158,9 @@ defns
     % ------------ :: record_join
     % g |- { l_1 : ty_1 ; .. ; l_n : ty_n } @ { l'_1 : ty'_1 ; .. ; l'_m : ty'_m } == { l_1 : ty_1 ; .. ; l_n : ty_n ; l'_1 : ty'_1 ; .. ; l'_m : ty'_m }
 
+    ----------------------------------------------- :: pair
+    g |- ty_1 * ty_2 == { car : ty_1 ; cdr : ty_2 }
+
   defn
     g |- ty :: :: ty_well_formed :: twf_ {{com Type well-formedness}} by
 
@@ -160,6 +171,12 @@ defns
     g |- { l_1 : ty_1 ; .. ; l_n : ty_n }
 
 
+    g |- ty
+    g |- ty'
+    ------------- :: pair
+    g |- ty * ty'
+
+
     % TO PROVE: if (g |- ty) and (g |- ty == ty') then (g |- ty')
 
   defn
@@ -178,6 +195,11 @@ by
     ------------------------------------------------- :: record
     tvar not free in { l_1 : ty_1 ; .. ; l_n : ty_n }
 
+    tvar not free in ty
+    tvar not free in ty'
+    ------------------------- :: pair
+    tvar not free in ty * ty'
+
   defn
     g |- instruction : ty => ty' :: :: instr :: T_ {{ com Instruction typing }} by
 
@@ -212,6 +234,9 @@ by
     g |- lhs = rhs : a => c
 
 
+    ---------------------------------- :: drop
+    g |- drop var : {var : ty} => {}
+
     % TO PROVE: if (g |- instruction : ty => ty') then (g |- ty) and (g |- ty')
 
   defn
@@ -262,6 +287,10 @@ by
     g |- f : ty => ty' :: :: f :: Tf_ {{com Function symbol typing}} by
 
 
+    ---------------------------------------- :: dup
+    g |- dup : ty => { car : ty ; cdr : ty }
+
+
   defn
     g |- value : ty :: :: val :: Tval_ {{com Value typing}} by
 
@@ -283,6 +312,7 @@ defns
     ------------------------------------------------------------------------------------------------------------------ :: record
     E |- { l_1 = x_1 ; .. ; l_n = x_n } / { l_1 = val_1 ; .. ; l_n = val_n } -> { x_1 = val_1 ; .. ; x_n = val_n }
 
+
   defn
     E |- arg /a val -> val' :: :: arg :: arg_ {{com Argument evaluation}} by
 
@@ -298,6 +328,11 @@ defns
   defn
     E |- f / val -> val' :: :: f :: f_ {{com Function symbol evaluation}} by
 
+
+    -------------------------------------------- :: dup
+    E |- dup / val -> { car = val; cdr = val }
+
+
   defn
     E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
 
@@ -339,4 +374,8 @@ defns
     E |- rhs / val -> val'
     E |- lhs / val' -> val''
     ------------------------------------------------------ :: assign
-    E |- lhs = rhs / val -> val''
\ No newline at end of file
+    E |- lhs = rhs / val -> val''
+
+
+    ------------------------------------------------ :: drop
+    E |- drop var / { var = val } -> :val_rval: {}

ott/drop.ott

-grammar
-
-instruction, I :: 'instr_' ::= {{com Instruction}}
-  | drop var :: :: drop {{com Resource dropping}}
-
-
-defns
-  Jtype :: 'typing_' ::=
-
-  defn
-    g |- instruction : ty => ty' :: :: instr :: T_ {{ com Instruction typing }} by
-
-
-    ---------------------------------- :: drop
-    g |- drop var : {var : ty} => unit
-
-defns
-  Jeval :: 'eval_' ::=
-
-  defn
-    E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
-
-    ------------------------------------------------ :: drop
-    E |- drop var / { var = val } -> :val_rval: {}

ott/dup.ott

-grammar
-
-f :: 'fun_' ::= {{com Function symbol}}
-  | dup :: :: dup
-
-
-defns
-  Jtype :: 'typing_' ::=
-
-  defn
-    g |- f : ty => ty' :: :: f :: Tf_ {{com Function symbol typing}} by
-
-    ------------------------ :: dup
-    g |- dup : ty => ty * ty
-
-defns
-  Jeval :: 'eval_' ::=
-
-  defn
-    E |- f / val -> val' :: :: f :: f_ {{com Function symbol evaluation}} by
-
-    -------------------------------------------- :: dup
-    E |- dup / val -> { car = val; cdr = val }
\ No newline at end of file

ott/pair.ott

-
-grammar
-
-label, l, var, x :: 'label_' ::= {{ coq-equality }}
-  | car :: M :: car {{coq "car"%string}} {{ocaml (Aux.explode "car")}} {{com First component of a binary pair}}
-  | cdr :: M :: cdr {{coq "cdr"%string}} {{ocaml (Aux.explode "cdr")}} {{com Second component of a binary pair}}
-
-ty, a, b, c :: 'ty_' ::=
-  | ty * ty' :: :: prod {{com Binary product type}}
-
-lhs :: 'lhs_' ::=
-  | ( var_1 , var_2 ) :: S :: pair
-  {{coq lhs_record (("car", [[var_1]])::("cdr", [[var_2]])::nil)}}
-  {{ocaml Lhs_record [((Aux.explode "car"), [[var_1]]);((Aux.explode "cdr"), [[var_2]])]}}
-defns
-  Jtype :: 'typing_' ::=
-
-  defn
-    g |- ty_1 == ty_2 :: :: type_eq :: Teq_ {{com Type equality}} by
-
-    % Definition of the pair type is axiomatized because I did not find a way to define it directly in Ott
-    ----------------------------------------------- :: pair
-    g |- ty_1 * ty_2 == { car : ty_1 ; cdr : ty_2 }
-
-  defn
-    g |- ty :: :: ty_well_formed :: twf_ {{com Type well-formedness}} by
-
-    g |- ty
-    g |- ty'
-    ------------- :: pair
-    g |- ty * ty'
-
-  defn
-    tvar not free in ty :: :: fresh_tvar :: Tfresh_tvar {{com Type variable freshness}} by
-
-    tvar not free in ty
-    tvar not free in ty'
-    ------------------------- :: pair
-    tvar not free in ty * ty'