Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Separate flags for explicit/implicit parameters and inductive/non-inductive variables #255

Merged
merged 4 commits into from
May 31, 2022
Merged

Separate flags for explicit/implicit parameters and inductive/non-inductive variables #255

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
94e722d
Introduce `Plicity` module
MartyO256 May 30, 2022
1fcbcf8
Introduce `Inductivity` module
MartyO256 May 30, 2022
6742e1a
Add `{Plicity,Inductivity}.equal`
MartyO256 May 30, 2022
21a7e9d
Split `LF.depend` flags into `Plicity.t` and `Inductivity.t`
MartyO256 May 30, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
186 changes: 93 additions & 93 deletions src/core/abstract.ml
View file
Open in desktop

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions src/core/abstract.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,14 @@ type error =

type sort =
| LFTyp of LF.typ
| MetaTyp of LF.ctyp * LF.depend
| MetaTyp of LF.ctyp * Plicity.t * Inductivity.t
type marker =
| Pure of sort
| Impure

type free_var =
| FDecl of kind * marker
| CtxV of (Id.name * Id.cid_schema * LF.depend)
| CtxV of (Id.name * Id.cid_schema * Plicity.t * Inductivity.t)

type fctx = free_var LF.ctx

Expand Down
44 changes: 22 additions & 22 deletions src/core/apxnorm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,15 +43,15 @@ let lengthApxMCtx = Context.length
(* EtaExpansion of approximate terms *)
let rec shiftApxTerm k =
function
| Apx.LF.Lam (loc, x, m') -> Apx.LF.Lam(loc, x, shiftApxTerm (k+1) m')
| Apx.LF.Lam (loc, x, m') -> Apx.LF.Lam(loc, x, shiftApxTerm (k + 1) m')
| Apx.LF.Root (loc, h , spine) ->
let h' = shiftApxHead k h in
let spine' = shiftApxSpine k spine in
Apx.LF.Root(loc, h', spine')

and shiftApxHead k =
function
| Apx.LF.BVar x -> Apx.LF.BVar (x+k)
| Apx.LF.BVar x -> Apx.LF.BVar (x + k)
| Apx.LF.FMVar (u, s) ->
Apx.LF.FMVar (u, Option.(s $> fun s -> shiftApxSub k s))
| Apx.LF.FPVar (p, s) ->
Expand Down Expand Up @@ -230,10 +230,10 @@ let rec cnormApxTyp cD delta a (cD'', t) =
| Apx.LF.Atom (loc, c, spine) ->
Apx.LF.Atom (loc, c, cnormApxSpine cD delta spine (cD'', t))

| Apx.LF.PiTyp ((t_decl, dep), a) ->
| Apx.LF.PiTyp ((t_decl, plicity), a) ->
let t_decl' = cnormApxTypDecl cD delta t_decl (cD'', t) in
let a' = cnormApxTyp cD delta a (cD'', t) in
Apx.LF.PiTyp ((t_decl', dep), a')
Apx.LF.PiTyp ((t_decl', plicity), a')

| Apx.LF.Sigma typ_rec ->
let typ_rec' = cnormApxTypRec cD delta typ_rec (cD'', t) in
Expand Down Expand Up @@ -295,7 +295,7 @@ let rec cnormApxExp cD delta e (cD'', t) =
dprint (fun () -> "cnormApxExp -- MLam (or could be PLam)");
let e' =
cnormApxExp cD (Apx.LF.Dec(delta, Apx.LF.DeclOpt u)) e
(Int.LF.Dec (cD'', Int.LF.DeclOpt (u, `explicit)), Whnf.mvar_dot1 t)
(Int.LF.Dec (cD'', Int.LF.DeclOpt (u, Plicity.explicit)), Whnf.mvar_dot1 t)
in
Apx.Comp.MLam (loc, u, e')

Expand All @@ -304,10 +304,10 @@ let rec cnormApxExp cD delta e (cD'', t) =
let e2' = cnormApxExp cD delta e2 (cD'', t) in
Apx.Comp.Pair (loc, e1', e2')

| Apx.Comp.LetPair (loc, i, (x,y, e)) ->
| Apx.Comp.LetPair (loc, i, (x, y, e)) ->
let i' = cnormApxExp' cD delta i (cD'', t) in
let e' = cnormApxExp cD delta e (cD'', t) in
Apx.Comp.LetPair (loc, i', (x,y, e'))
Apx.Comp.LetPair (loc, i', (x, y, e'))

| Apx.Comp.Let (loc, i, (x, e)) ->
let i' = cnormApxExp' cD delta i (cD'', t) in
Expand Down Expand Up @@ -364,7 +364,7 @@ and cnormApxExp' cD delta i cDt =
let mobj' = cnormApxMetaObj cD delta mobj cDt in
Apx.Comp.BoxVal (loc, mobj')

and cnormApxMetaObj cD delta (loc,mobj) cDt =
and cnormApxMetaObj cD delta (loc, mobj) cDt =
( loc
, match mobj with
| Apx.Comp.ClObj (psi, sigma) ->
Expand Down Expand Up @@ -397,9 +397,9 @@ and cnormApxBranch cD delta b (cD'', t) =
let rec append_mctx cD'' =
function
| Apx.LF.Empty -> cD''
| Apx.LF.Dec (delta2', Apx.LF.Decl(x, _, dep)) ->
| Apx.LF.Dec (delta2', Apx.LF.Decl (x, _, plicity)) ->
let cD1'' = append_mctx cD'' delta2' in
Int.LF.Dec (cD1'', Int.LF.DeclOpt (x, Int.LF.Depend.to_plicity dep))
Int.LF.Dec (cD1'', Int.LF.DeclOpt (x, plicity))
in

match b with
Expand Down Expand Up @@ -482,10 +482,10 @@ and collectApxSub fMVs =
| Apx.LF.Dot (Apx.LF.Obj m, s) ->
let fMVs' = collectApxTerm fMVs m in
collectApxSub fMVs' s
| Apx.LF.SVar (i,s) ->
| Apx.LF.SVar (i, s) ->
collectApxSubOpt fMVs s
| Apx.LF.FSVar (n,s) ->
collectApxSubOpt (n::fMVs) s
| Apx.LF.FSVar (n, s) ->
collectApxSubOpt (n :: fMVs) s

and collectApxSpine fMVs =
function
Expand Down Expand Up @@ -566,7 +566,7 @@ let rec collectApxTyp fMVd =
function
| Apx.LF.Atom (loc, c, tS) ->
collectApxSpine fMVd tS
| Apx.LF.PiTyp ((Apx.LF.TypDecl (x, tA),_ ), tB) ->
| Apx.LF.PiTyp ((Apx.LF.TypDecl (x, tA), _ ), tB) ->
let fMVd1 = collectApxTyp fMVd tA in
collectApxTyp fMVd1 tB
| Apx.LF.Sigma trec ->
Expand All @@ -588,7 +588,7 @@ let collectApxCDecl fMVd =
| Apx.LF.Decl(_, Apx.LF.ClTyp (Apx.LF.PTyp tA, cPsi), _) ->
let fMVd1 = collectApxDCtx fMVd cPsi in
collectApxTyp fMVd1 tA
| Apx.LF.Decl (_,Apx.LF.CTyp _,_) -> fMVd
| Apx.LF.Decl (_, Apx.LF.CTyp _, _) -> fMVd

let rec collectApxCompTyp fMVd =
function
Expand All @@ -601,11 +601,11 @@ let rec collectApxCompTyp fMVd =
| Apx.Comp.TypPiBox (_, cdecl, tau) ->
let fMVd1 = collectApxCDecl fMVd cdecl in
collectApxCompTyp fMVd1 tau
| Apx.Comp.TypBox (loc, (loc',Apx.LF.ClTyp(Apx.LF.MTyp tA, cPsi)))
| Apx.Comp.TypBox (loc, (loc',Apx.LF.ClTyp(Apx.LF.PTyp tA, cPsi))) ->
| Apx.Comp.TypBox (loc, (loc', Apx.LF.ClTyp(Apx.LF.MTyp tA, cPsi)))
| Apx.Comp.TypBox (loc, (loc', Apx.LF.ClTyp(Apx.LF.PTyp tA, cPsi))) ->
let fMVd1 = collectApxDCtx fMVd cPsi in
collectApxTyp fMVd1 tA
| Apx.Comp.TypBox (loc, (loc',Apx.LF.ClTyp(Apx.LF.STyp (_ , cPhi), cPsi))) ->
| Apx.Comp.TypBox (loc, (loc', Apx.LF.ClTyp(Apx.LF.STyp (_ , cPhi), cPsi))) ->
let fMVd1 = collectApxDCtx fMVd cPsi in
collectApxDCtx fMVd1 cPhi
| Apx.Comp.TypBase (_loc, _c, mS) ->
Expand Down Expand Up @@ -764,10 +764,10 @@ let rec fmvApxTyp fMVs cD d_param =
| Apx.LF.Atom (loc, c, spine) ->
Apx.LF.Atom (loc, c, fmvApxSpine fMVs cD d_param spine)

| Apx.LF.PiTyp ((t_decl, dep), a) ->
| Apx.LF.PiTyp ((t_decl, plicity), a) ->
let t_decl' = fmvApxTypDecl fMVs cD d_param t_decl in
let a' = fmvApxTyp fMVs cD d_param a in
Apx.LF.PiTyp ((t_decl', dep), a')
Apx.LF.PiTyp ((t_decl', plicity), a')

| Apx.LF.Sigma typ_rec ->
let typ_rec' = fmvApxTypRec fMVs cD d_param typ_rec in
Expand Down Expand Up @@ -853,10 +853,10 @@ let rec fmvApxExp fMVs cD ((l_cd1, l_delta, k) as d_param) =
let e1' = fmvApxExp fMVs cD d_param e1 in
let e2' = fmvApxExp fMVs cD d_param e2 in
Apx.Comp.Pair (loc, e1', e2')
| Apx.Comp.LetPair (loc, i, (x,y, e)) ->
| Apx.Comp.LetPair (loc, i, (x, y, e)) ->
let i' = fmvApxExp' fMVs cD d_param i in
let e' = fmvApxExp fMVs cD d_param e in
Apx.Comp.LetPair (loc, i', (x,y, e'))
Apx.Comp.LetPair (loc, i', (x, y, e'))
| Apx.Comp.Let (loc, i, (x, e)) ->
let i' = fmvApxExp' fMVs cD d_param i in
let e' = fmvApxExp fMVs cD d_param e in
Expand Down
Loading