Section coqPassCoreToCore.
Context
+ (do_flatten : bool)
+ (do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
(hetmet_flatten : CoreVar)
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
(addErrorMessage ("HaskStrong...")
- (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
- hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
- in (* insert HaskProof-to-HaskProof manipulations here *)
- OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
- >>= fun e' =>
- (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
- mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
- (projT2 e'') INil
- >>= fun q =>
- OK (weakExprToCoreExpr q)
- )))))))))).
+ (if do_skolemize
+ then
+ (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten'
+ hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e)
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
+ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ >>= fun e' => (snd e') >>= fun e'' =>
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e'') INil
+ >>= fun q => OK (weakExprToCoreExpr q))
+ else (if do_flatten
+ then
+ (let haskProof := flatten_proof (*hetmet_flatten' hetmet_unflatten'
+ hetmet_flattened_id' my_ga*) (@expr2proof _ _ _ _ _ _ _ e)
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ τ nil _
+ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ >>= fun e' => (snd e') >>= fun e'' =>
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e'') INil
+ >>= fun q => OK (weakExprToCoreExpr q))
+ else
+ (let haskProof := @expr2proof _ _ _ _ _ _ _ e
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ τ nil _
+ (fun _ => Prelude_error "unbound unique") _ haskProof) O)
+ >>= fun e' => (snd e') >>= fun e'' =>
+ strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e'') INil
+ >>= fun q => OK (weakExprToCoreExpr q))))
+ ))))))))).
Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) :=
match coreToCoreExpr' ce with
End coqPassCoreToCore.
Definition coqPassCoreToCore
+ (do_flatten : bool)
+ (do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
(hetmet_flatten : CoreVar)
(hetmet_pga_curryl : CoreVar)
(hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) :=
coqPassCoreToCore'
+ do_flatten
+ do_skolemize
hetmet_brak
hetmet_esc
hetmet_flatten
reflexivity.
Qed.
- Definition flatten_proof :
+ Definition flatten_skolemized_proof :
forall {h}{c},
ND SRule h c ->
ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
Defined.
+ Definition flatten_proof :
+ forall {h}{c},
+ ND Rule h c ->
+ ND Rule h c.
+ apply (Prelude_error "sorry, non-skolemized flattening isn't implemented").
+ Defined.
+
Definition skolemize_and_flatten_proof :
forall {h}{c},
ND Rule h c ->
intros.
rewrite mapOptionTree_compose.
rewrite mapOptionTree_compose.
- apply flatten_proof.
+ apply flatten_skolemized_proof.
apply skolemize_proof.
apply X.
Defined.