Merge pull request #531 from MetaCoq/primitive-int-float

Primitive integers and floats

Author: mattam82

.gitignore

@@ -416,3 +416,5 @@ erasure/src/pCUICErrors.ml
 erasure/src/pCUICErrors.mli
 erasure/src/pCUICTypeChecker.ml
 erasure/src/pCUICTypeChecker.mli
+erasure/src/pCUICPrimitive.ml
+erasure/src/pCUICPrimitive.mli

checker/theories/Checker.v

@@ -447,7 +447,8 @@ Inductive type_error :=
 | IllFormedFix (m : mfixpoint term) (i : nat)
 | UnsatisfiedConstraints (c : ConstraintSet.t)
 | UnsatisfiableConstraints (c : ConstraintSet.t)
-| NotEnoughFuel (n : nat).
+| NotEnoughFuel (n : nat)
+| NotSupported (s : string).
 
 Definition string_of_type_error (e : type_error) : string :=
   match e with
@@ -468,6 +469,7 @@ Definition string_of_type_error (e : type_error) : string :=
   | UnsatisfiedConstraints c => "Unsatisfied constraints"
   | UnsatisfiableConstraints c => "Unsatisfiable constraints"
   | NotEnoughFuel n => "Not enough fuel"
+  | NotSupported s => s ^ " are not supported"
   end.
 
 Inductive typing_result (A : Type) :=
@@ -769,6 +771,8 @@ Section Typecheck2.
       | Some f => ret f.(dtype)
       | None => raise (IllFormedFix mfix n)
       end
+
+    | tInt _ | tFloat _ => raise (NotSupported "primitive types")
     end.
 
   Definition check (Γ : context) (t : term) (ty : term) : typing_result unit :=

checker/theories/Retyping.v

@@ -99,6 +99,8 @@ Section TypeOf.
       | Some f => ret f.(dtype)
       | None => raise (IllFormedFix mfix n)
       end
+
+    | tInt _ | tFloat _ => raise (NotSupported "primitive types")
     end.
 
   Definition sort_of (Γ : context) (t : term) : typing_result Universe.t :=

configure.sh

@@ -16,8 +16,7 @@ if command -v coqc >/dev/null 2>&1
 then
     COQLIB=`coqc -where`
 
-    if [ "$1" == "local" ]
-    then
+    if [ "$1" = "local" ]; then
         echo "Building MetaCoq locally"
         CHECKER_DEPS="-R ../template-coq/theories MetaCoq.Template -I ../template-coq/build"
         PCUIC_MLDEPS="-I ../checker/src"

erasure/_PluginProject.in

@@ -31,6 +31,8 @@ src/kernames.ml
 # src/typing0.ml
 
 # From PCUIC
+src/pCUICPrimitive.mli
+src/pCUICPrimitive.ml
 src/pCUICAst.ml
 src/pCUICAst.mli
 src/pCUICAstUtils.ml

erasure/src/metacoq_erasure_plugin.mlpack

@@ -14,6 +14,7 @@ Classes0
 Logic1
 Relation
 Relation_Properties
+PCUICPrimitive
 PCUICAst
 PCUICAstUtils
 PCUICUnivSubst

erasure/theories/EAst.v

@@ -1,6 +1,6 @@
 (* Distributed under the terms of the MIT license. *)
 From MetaCoq.Template Require Export utils BasicAst Universes.
-
+From MetaCoq.PCUIC Require Import PCUICPrimitive.
 (** * Extracted terms
 
   These are the terms produced by extraction: compared to kernel terms,
@@ -37,7 +37,8 @@ Inductive term : Set :=
                term (* discriminee *) -> list (nat * term) (* branches *) -> term
 | tProj      : projection -> term -> term
 | tFix       : mfixpoint term -> nat -> term
-| tCoFix     : mfixpoint term -> nat -> term.
+| tCoFix     : mfixpoint term -> nat -> term
+| tPrim      : prim_val term -> term.
 
 Fixpoint mkApps t us :=
   match us with

erasure/theories/EAstUtils.v

@@ -1,6 +1,7 @@
 (* Distributed under the terms of the MIT license. *)
 From MetaCoq.Template Require Import utils Kernames.
 From MetaCoq.Erasure Require Import EAst.
+From MetaCoq.PCUIC Require PCUICPrimitive.
 Require Import ssreflect ssrbool.
 
 
@@ -267,6 +268,7 @@ Fixpoint string_of_term (t : term) : string :=
             ^ string_of_term c ^ ")"
   | tFix l n => "Fix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
   | tCoFix l n => "CoFix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
+  | tPrim p => "Prim(" ^ PCUICPrimitive.string_of_prim string_of_term p ^ ")"
   end.
 
 (** Compute all the global environment dependencies of the term *)

erasure/theories/EInduction.v

@@ -28,6 +28,7 @@ Lemma term_forall_list_ind :
     (forall (s : projection) (t : term), P t -> P (tProj s t)) ->
     (forall (m : mfixpoint term) (n : nat), All (fun x => P (dbody x)) m -> P (tFix m n)) ->
     (forall (m : mfixpoint term) (n : nat), All (fun x => P (dbody x)) m -> P (tCoFix m n)) ->
+    (forall p, P (tPrim p)) ->
     forall t : term, P t.
 Proof.
   intros until t. revert t.

erasure/theories/ELiftSubst.v

@@ -32,9 +32,9 @@ Fixpoint lift n k t : term :=
   | tVar _ => t
   | tConst _ => t
   | tConstruct _ _ => t
+  | tPrim _ => t
   end.
 
-
 Notation lift0 n := (lift n 0).
 Definition up := lift 1 0.