Skip to content

Commit 7b14ff9

Browse files
TDiazTTDiazT
committed
[refactor] Reorder and extract some dummy vars and aux functs
1 parent 1c1eeb4 commit 7b14ff9

File tree

1 file changed

+31
-27
lines changed

1 file changed

+31
-27
lines changed

‎template-rocq/src/quoter.ml‎

Lines changed: 31 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -482,9 +482,26 @@ struct
482482
let (fn,_) = quote_term_remember (fun _ () -> ()) (fun _ _ () -> ()) in
483483
fst (fn () env sigma trm)
484484

485+
let dummy_qint = Q.quote_int 9999
486+
let dummy_quniv = Q.quote_univ_instance Univ.Instance.empty
487+
let dummy_qevar = Q.mkEvar dummy_qint [||]
488+
let dummy_qind =
489+
let open Names in
490+
let dummy_kername = KerName.make (ModPath.MPfile DirPath.empty) (Label.make "dummy") in
491+
Q.quote_inductive (Q.quote_kn dummy_kername, dummy_qint)
492+
485493
let quote_untyped_term_remember
486494
(add_constant : KerName.t -> 'a -> 'a)
487495
(add_inductive : Names.inductive -> Declarations.mutual_inductive_body -> 'a -> 'a) =
496+
let mkLambda (id, bkind, ty) body =
497+
Glob_term.GLambda (id, bkind, ty, body)
498+
in
499+
let mkProd (id, bkind, ty) body =
500+
Glob_term.GProd (id, bkind, ty, body)
501+
in
502+
let mkLetIn (id, ty, letinfo) body =
503+
Glob_term.GLetIn (id, ty, letinfo, body)
504+
in
488505
let rec quote_term (acc : 'a) env sigma trm =
489506
let aux acc env trm =
490507
match trm with
@@ -494,14 +511,14 @@ struct
494511
| GlobRef.VarRef var -> (Q.mkVar (Q.quote_ident var), acc)
495512
| GlobRef.ConstRef c ->
496513
let kn = Constant.canonical c in
497-
(Q.mkConst (Q.quote_kn kn) dummy_univ, add_constant kn acc)
514+
(Q.mkConst (Q.quote_kn kn) dummy_quniv, add_constant kn acc)
498515
| GlobRef.IndRef mind ->
499-
(Q.mkInd (quote_inductive' mind) dummy_univ,
516+
(Q.mkInd (quote_inductive' mind) dummy_quniv,
500517
let mib = Environ.lookup_mind (fst mind) (snd env) in
501518
add_inductive mind mib acc)
502519
| GlobRef.ConstructRef (mind, c) ->
503520
let mib = Environ.lookup_mind (fst mind) (snd env) in
504-
(Q.mkConstruct (quote_inductive' mind, Q.quote_int (c - 1)) dummy_univ,
521+
(Q.mkConstruct (quote_inductive' mind, Q.quote_int (c - 1)) dummy_quniv,
505522
add_inductive mind mib acc)
506523
)
507524

@@ -514,15 +531,15 @@ struct
514531

515532
(* NOTE: Relevance set to Relevant always *)
516533
| Glob_term.GLambda (n, _, t, b) ->
517-
let binder = Context.make_annot n Sorts.Relevant in
534+
let binder = Context.annotR n in
518535
let (t',acc) = quote_term acc env sigma t in
519536
(* let (b',acc) = quote_term acc (push_rel (toDecl (n, None, t)) env) sigma b in *)
520537
let (b',acc) = quote_term acc env sigma b in
521538
(Q.mkLambda (Q.quote_aname binder) t' b', acc)
522539

523540
(* NOTE: Relevance set to Relevant always *)
524541
| Glob_term.GProd (n, _, t, b) ->
525-
let binder = Context.make_annot n Sorts.Relevant in
542+
let binder = Context.annotR n in
526543
let (t',acc) = quote_term acc env sigma t in
527544
(* let env = push_rel (toDecl (n, None, t)) env in *)
528545
let (b',acc) = quote_term acc env sigma b in
@@ -532,7 +549,7 @@ struct
532549
(
533550
match ty with
534551
| Some ty' ->
535-
let binder = Context.make_annot name Sorts.Relevant in
552+
let binder = Context.annotR name in
536553
let (exp',acc) = quote_term acc env sigma exp in
537554
(* What to do if missing type annotation ? *)
538555
let (ty',acc) = quote_term acc env sigma ty' in
@@ -543,7 +560,7 @@ struct
543560
)
544561

545562
| Glob_term.GCases (case_style, type_info, discrs, branches) ->
546-
let qpred, acc = if Option.is_empty type_info then dummy_evar, acc else quote_term acc env sigma (Option.get type_info) in
563+
let qpred, acc = if Option.is_empty type_info then dummy_qevar, acc else quote_term acc env sigma (Option.get type_info) in
547564
(match case_style with
548565
| Constr.RegularStyle ->
549566
(
@@ -563,18 +580,18 @@ struct
563580

564581
(* Function to process a discriminator and get its parameters *)
565582
let process_discriminator (discr, (as_info, pred_patt)) env sigma =
566-
let as_binder = mkAnnot as_info in
583+
let as_binder = Context.annotR as_info in
567584
let (ind, npar, qu, q_pars) =
568585
if Option.is_empty pred_patt then
569-
(dummy_ind, Q.quote_int 9999, dummy_univ, [||])
586+
(dummy_qind, dummy_qint, dummy_quniv, [||])
570587
else
571588
let ((mind, idx), _) = (Option.get pred_patt).CAst.v in
572589
let mib = Environ.lookup_mind mind (snd env) in
573590
let ind = Q.quote_inductive (Q.quote_kn (Names.MutInd.canonical mind),
574591
Q.quote_int idx) in
575592
let npar = Q.quote_int mib.mind_nparams in
576593
let qu = Q.quote_univ_instance mib.mind_univ_hyps in
577-
let q_pars = Array.make mib.mind_nparams dummy_evar in
594+
let q_pars = Array.make mib.mind_nparams dummy_qevar in
578595
(ind, npar, qu, q_pars)
579596
in
580597
let (qdiscr, acc) = quote_term acc env sigma discr in
@@ -610,7 +627,7 @@ struct
610627
| Glob_term.PatCstr (_, ctor_pats, _) -> ctor_pat_names ctor_pats
611628
)
612629
) pats [] in
613-
let pat_binders = Array.of_list (List.map mkAnnot pat_names) in
630+
let pat_binders = Array.of_list (List.map Context.annotR pat_names) in
614631
let qpat_binders = quote_name_annots pat_binders in
615632
let qbody, acc = quote_term acc env sigma body in
616633
((qpat_binders, qbody) :: brs, acc)
@@ -629,7 +646,7 @@ struct
629646
| Glob_term.GFix (rec_idxs, idx) ->
630647
(* FIXME : What to do with undefined indices *)
631648
let rec_idxs_norm = Array.map (Option.default 0) rec_idxs in
632-
let fn_names = Array.map (fun name -> Context.make_annot (Name name) Sorts.Relevant) fn_names in
649+
let fn_names = Array.map (fun fname -> Context.annotR (Name fname)) fn_names in
633650
(* Wraps body in as many lambdas, prod or letIn as binders are passed *)
634651
let wrapBody mkWrapper =
635652
let mkAbsOrLetIn (id, binfo, letinfo, ty) body =
@@ -663,7 +680,7 @@ struct
663680
| GLocalUniv _ -> failwith "GLocalUniv not supported by TemplateCoq"
664681
| _ -> failwith "not supported by TemplateCoq"
665682
)
666-
(* NOTE : Probably a better option ? *)
683+
(* NOTE : There is probably a better option ? *)
667684
| UAnonymous rigid -> Sorts.type1
668685
) in
669686
(Q.mkSort (Q.quote_sort sort), acc)
@@ -681,24 +698,11 @@ struct
681698
| Glob_term.GLetTuple _ -> failwith "GLetTuple not supported by TemplateCoq"
682699
| Glob_term.GIf _ -> failwith "GIf not supported by TemplateCoq"
683700
(* FIXME: Do a proper thing *)
684-
| Glob_term.GHole _ -> dummy_evar, acc
701+
| Glob_term.GHole _ -> dummy_qevar, acc
685702
| Glob_term.GProj _ -> failwith "GProj not supported by TemplateCoq"
686703
| Glob_term.GArray _ -> failwith "GArray not supported by TemplateCoq"
687704
in
688705
aux acc env (DAst.get trm)
689-
and dummy_univ = Q.quote_univ_instance Univ.Instance.empty
690-
and dummy_evar = Q.mkEvar (Q.quote_int 9999) [||]
691-
and dummy_ind =
692-
let open Names in
693-
let dummy_kername = KerName.make (ModPath.MPfile DirPath.empty) (Label.make "dummy") in
694-
Q.quote_inductive (Q.quote_kn dummy_kername, (Q.quote_int 9999))
695-
and mkAnnot n = Context.make_annot n Sorts.Relevant
696-
and mkLambda (id, bkind, ty) body =
697-
Glob_term.GLambda (id, bkind, ty, body)
698-
and mkProd (id, bkind, ty) body =
699-
Glob_term.GProd (id, bkind, ty, body)
700-
and mkLetIn (id, ty, letinfo) body =
701-
Glob_term.GLetIn (id, ty, letinfo, body)
702706
and quote_recdecl (acc : 'a) env sigma b (ns,ts,ds) =
703707
(* let ctxt = *)
704708
(* CArray.map2_i (fun i na t -> (Context.Rel.Declaration.LocalAssum (na, Vars.lift i t))) ns ts in *)

0 commit comments

Comments
 (0)