From 5a9c2aa62fa3296f429995f727c5890f1e92865d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 12 Jul 2021 17:11:31 +0200 Subject: [PATCH] Add a PCUICPHOAS file implementing a PHOAS variant of the syntax --- pcuic/_CoqProject.in | 1 + pcuic/theories/PCUICPHOAS.v | 135 +++++++++++++++++++++++++++++++ template-coq/theories/BasicAst.v | 3 + 3 files changed, 139 insertions(+) create mode 100644 pcuic/theories/PCUICPHOAS.v diff --git a/pcuic/_CoqProject.in b/pcuic/_CoqProject.in index 87ecee475..2f6251f12 100644 --- a/pcuic/_CoqProject.in +++ b/pcuic/_CoqProject.in @@ -109,6 +109,7 @@ theories/Bidirectional/BDStrengthening.v theories/PCUICWeakeningEnv.v +theories/PCUICPHOAS.v # theories/All.v # To do separate extraction of the files, not working currently diff --git a/pcuic/theories/PCUICPHOAS.v b/pcuic/theories/PCUICPHOAS.v new file mode 100644 index 000000000..bf6190396 --- /dev/null +++ b/pcuic/theories/PCUICPHOAS.v @@ -0,0 +1,135 @@ +From Coq Require Import String List ZArith. +From MetaCoq.Template Require config utils All. +From MetaCoq.Template Require Import BasicAst TemplateMonad monad_utils. +From MetaCoq.PCUIC Require Import TemplateToPCUIC. +Import MCMonadNotation. +Local Open Scope string_scope. +Import ListNotations. + +(* From MetaCoq.PCUIC Require Import PCUICAst PCUICReduction PCUICCumulativity PCUICTyping PCUICSafeLemmata. *) + +From MetaCoq.Template Require Import Universes. +Declare Custom Entry term. +Module LevelsToIndices. +Import Ast. + +(* Conversion from de Bruijn levels to indices *) +Fixpoint toDB k (t : term) : term := + match t with + | tRel n => Ast.tRel (k - n) + | tVar id => Ast.tVar id + | tEvar ev args => Ast.tEvar ev (List.map (toDB k) args) + | tSort s => Ast.tSort s + | tCast t ck u => Ast.tCast (toDB k t) ck (toDB k u) + | tProd na ty body => Ast.tProd na (toDB k ty) (toDB (S k) body) + | tLambda na ty body => Ast.tLambda na (toDB k ty) (toDB (S k) body) + | tApp f args => Ast.tApp (toDB k f) (List.map (toDB k) args) + | tConst c u => Ast.tConst c u + | tInd c u => Ast.tInd c u + | tConstruct c k u => Ast.tConstruct c k u + | _ => Ast.tInt (Int63.of_Z 0%Z) + end. +End LevelsToIndices. + +Module PHOAS. +Inductive term {var : Type} | : Type := +| tRel (n : var) +| tVar (id : ident) (* For free variables (e.g. in a goal) *) +| tEvar (ev : nat) (args : list term) +| tSort (s : Universe.t) +| tCast (t : term) (kind : cast_kind) (v : term) +| tProd (na : aname) (ty : term) (body : var -> term) +| tLambda (na : aname) (ty : term) (body : var -> term) +| tLetIn (na : aname) (def : term) (def_ty : term) (body : var -> term) +| tApp (f : term) (args : list term) +| tConst (c : kername) (u : Instance.t) +| tInd (ind : inductive) (u : Instance.t) +| tConstruct (ind : inductive) (idx : nat) (u : Instance.t) +| tCase (ind_nbparams_relevance: inductive*nat*relevance) (type_info:term) + (discr:term) (branches : list (nat * term)) +| tProj (proj : projection) (t : term) +| tFix (mfix : mfixpoint term) (idx : nat) +| tCoFix (mfix : mfixpoint term) (idx : nat) +| tInt (i : Int63.int) +| tFloat (f : PrimFloat.float). +Arguments term : clear implicits. + +(* To de Bruijn indices *) +Fixpoint toDB k (t : term nat) : Ast.term := + match t with + | tRel n => Ast.tRel (k - S n) + | tVar id => Ast.tVar id + | tEvar ev args => Ast.tEvar ev (List.map (toDB k) args) + | tSort s => Ast.tSort s + | tCast t ck u => Ast.tCast (toDB k t) ck (toDB k u) + | tProd na ty body => Ast.tProd na (toDB k ty) (toDB (S k) (body k)) + | tLambda na ty body => Ast.tLambda na (toDB k ty) (toDB (S k) (body k)) + | tLetIn na ty b body => Ast.tLetIn na (toDB k ty) (toDB k b) (toDB (S k) (body k)) + | tApp f args => Ast.tApp (toDB k f) (List.map (toDB k) args) + | tConst c u => Ast.tConst c u + | tInd c u => Ast.tInd c u + | tConstruct c k u => Ast.tConstruct c k u + | tCase i t d brs => + Ast.tCase i (toDB k t) (toDB k d) (List.map (fun '(x, y) => (x, toDB k y)) brs) + | tProj p t => Ast.tProj p (toDB k t) + | tFix mfix idx => + let mfix' := List.map (map_def (toDB k) (toDB (k + length mfix))) mfix in + Ast.tFix mfix' idx + | tCoFix mfix idx => + let mfix' := List.map (map_def (toDB k) (toDB (k + length mfix))) mfix in + Ast.tCoFix mfix' idx + | tInt i => Ast.tInt i + | tFloat f => Ast.tFloat f + end. + + Definition tImpl {var} (A B : term var) := tProd bAnon A (fun _ => B). +End PHOAS. +Definition term := forall var, PHOAS.term var. + +(* Definition of_phoas {A} (t : term A) : term := *) + +Definition myterm := PHOAS.term nat. +Definition nat_rel : nat -> myterm := PHOAS.tRel. + +Notation "[! e ]" := (e : myterm) (e custom term at level 200). +Notation "( e )" := e (e custom term, in custom term). +Notation "t1 t2" := (PHOAS.tApp t1 [t2]) (in custom term at level 4, left associativity). + +Notation "'Type' u" := (PHOAS.tSort u) (u constr, in custom term at level 0). +Notation "'Type0'" := (PHOAS.tSort Universe.type0) (in custom term at level 0). +Notation "'Type1'" := (PHOAS.tSort Universe.type1) (in custom term at level 0). +Notation "'Π' x @ ( na , A ) , B" := (PHOAS.tProd (bNamed na) A (fun x => B)) + (in custom term at level 4, right associativity, + x binder, + na constr, + A custom term at level 4, + B custom term at level 4). +Notation "A → B" := (PHOAS.tImpl A B) + (in custom term at level 4, right associativity, + A custom term, + B custom term at level 4). + +Notation "'λ' x @ ( na , A ) , B" := (PHOAS.tLambda (bNamed na) A (fun x : _ => B)) + (in custom term at level 4, right associativity, + x binder, + na constr, + A custom term at level 4, + B custom term at level 4). + +Notation "' x" := (PHOAS.tRel x) (in custom term at level 0, x constr at level 2, format "' x"). +Notation "{ x }" := x (x constr, in custom term). + +Definition of_phoas (t : myterm) : PCUICAst.term := + TemplateToPCUIC.trans (PHOAS.toDB 0 t). + +Coercion of_phoas : myterm >-> PCUICAst.term. + +Coercion nat_rel : nat >-> myterm. + +(* Definition tnat {var} : PHOAS.term var := PHOAS.tInd + {| + inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat"); + inductive_ind := 0 + |} []. *) + +(* Type [! λ x @ ("x", { tnat }), λ x' @ ("x", { tnat }), λ y @ ("y", Type0), 'y 'x]. *) diff --git a/template-coq/theories/BasicAst.v b/template-coq/theories/BasicAst.v index bd9849a0e..17965d9d9 100644 --- a/template-coq/theories/BasicAst.v +++ b/template-coq/theories/BasicAst.v @@ -21,6 +21,9 @@ Arguments mkBindAnn {_}. Arguments binder_name {_}. Arguments binder_relevance {_}. +Definition bAnon := {| binder_name := nAnon; binder_relevance := Relevant |}. +Definition bNamed s := {| binder_name := nNamed s; binder_relevance := Relevant |}. + Derive NoConfusion for binder_annot. #[global] Instance eqdec_binder_annot (A : Type) (e : Classes.EqDec A) : Classes.EqDec (binder_annot A).