(* need this or the Haskell extraction fails *)
Set Printing Width 1300000.
-Require Import Coq.Lists.List.
Require Import Coq.Strings.Ascii.
Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
Require Import Preamble.
Require Import General.
Require Import HaskCoreToWeak.
Require Import HaskWeakToStrong.
Require Import HaskStrongToProof.
-(*Require Import HaskProofToStrong.*)
+Require Import HaskProofToStrong.
Require Import HaskProofToLatex.
Require Import HaskStrongToWeak.
Require Import HaskWeakToCore.
Open Scope string_scope.
Extraction Language Haskell.
+(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
+(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
+(*Extract Inlined Constant map => "Prelude.map".*)
+
(* I try to reuse Haskell types mostly to get the "deriving Show" aspect *)
Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
Extract Inductive list => "([])" [ "([])" "(:)" ].
-(*Extract Inductive vec => "([])" [ "([])" "(:)" ].*)
-(*Extract Inductive Tree => "([])" [ "([])" "(:)" ].*)
-Extract Inlined Constant map => "Prelude.map".
-Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
+Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
Extract Inductive prod => "(,)" [ "(,)" ].
Extract Inductive sum => "Prelude.Either" [ "Prelude.Left" "Prelude.Right" ].
Extract Inductive sumbool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
Extract Inductive unit => "()" [ "()" ].
Extract Inlined Constant string_dec => "(==)".
Extract Inlined Constant ascii_dec => "(==)".
-Extract Inductive string => "Prelude.String" [ "[]" "(:)" ].
(* adapted from ExtrOcamlString.v *)
-Extract Inductive ascii => "Prelude.Char" [ "bin2ascii" ] "bin2ascii'".
+Extract Inductive ascii => "Char" [ "bin2ascii" ] "bin2ascii'".
Extract Constant zero => "'\000'".
Extract Constant one => "'\001'".
Extract Constant shift => "shiftAscii".
Unset Extraction Optimize.
Unset Extraction AutoInline.
-
Variable Name : Type. Extract Inlined Constant Name => "Name.Name".
Variable mkSystemName : Unique -> string -> nat -> Name.
- Extract Inlined Constant mkSystemName => "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
+ Extract Inlined Constant mkSystemName =>
+ "(\u s d -> Name.mkSystemName u (OccName.mkOccName (OccName.varNameDepth (nat2int d)) s))".
Variable mkTyVar : Name -> Kind -> CoreVar.
Extract Inlined Constant mkTyVar => "(\n k -> Var.mkTyVar n (kindToCoreKind k))".
Variable mkCoVar : Name -> CoreType -> CoreType -> CoreVar.
eol+++"\end{document}"+++
eol.
+
Definition coreToStringExpr' (ce:@CoreExpr CoreVar) : ???string :=
addErrorMessage ("input CoreSyn: " +++ ce)
(addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
Context (hetmet_esc : WeakExprVar).
Context (uniqueSupply : UniqSupply).
+ Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
+ match ut with
+ uniqM f =>
+ f uniqueSupply >>= fun x => OK (snd x)
+ end.
+
+ Definition larger : forall ln:list nat, { n:nat & forall n', In n' ln -> gt n n' }.
+ intros.
+ induction ln.
+ exists O.
+ intros.
+ inversion H.
+ destruct IHln as [n pf].
+ exists (plus (S n) a).
+ intros.
+ destruct H.
+ omega.
+ fold (@In _ n' ln) in H.
+ set (pf n' H) as q.
+ omega.
+ Defined.
+
+ Definition FreshNat : @FreshMonad nat.
+ refine {| FMT := fun T => nat -> prod nat T
+ ; FMT_fresh := _
+ |}.
+ Focus 2.
+ intros.
+ refine ((S H),_).
+ set (larger tl) as q.
+ destruct q as [n' pf].
+ exists n'.
+ intros.
+ set (pf _ H0) as qq.
+ omega.
+
+ refine {| returnM := fun a (v:a) => _ |}.
+ intro n. exact (n,v).
+ intros.
+ set (X H) as q.
+ destruct q as [n' v].
+ set (X0 v n') as q'.
+ exact q'.
+ Defined.
+
+ Definition unFresh {T} : @FreshM _ FreshNat T -> T.
+ intros.
+ destruct X.
+ exact O.
+ apply t.
+ Defined.
+
+ Definition env := ★::nil.
+ Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
+ Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
+ eapply nd_comp.
+ eapply nd_comp.
+ eapply nd_rule.
+ apply RVar.
+ eapply nd_rule.
+ eapply (RURule _ _ _ _ (RuCanL _ _)) .
+ eapply nd_rule.
+ eapply RLam.
+ Defined.
+(*
+ Definition TInt : HaskType nil ★.
+ assert (tyConKind' intPrimTyCon = ★).
+ admit.
+ rewrite <- H.
+ unfold HaskType; intros.
+ apply TCon.
+ Defined.
+
+ Definition idproof1 : ND Rule [] [nil > nil > [TInt @@ nil] |- [TInt @@ nil]].
+ apply nd_rule.
+ apply RVar.
+ Defined.
+
+ Definition idtype :=
+ HaskTAll(Γ:=nil) ★ (fun TV ite tv => (TApp (TApp TArrow (TVar tv)) (TVar tv))).
+
+ Definition idproof : ND Rule [] [nil > nil > [] |- [idtype @@ nil]].
+ eapply nd_comp; [ idtac | eapply nd_rule ; eapply RAbsT ].
+ apply idproof0.
+ Defined.
+*)
+(*
+ Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
+ addErrorMessage ("input CoreSyn: " +++ ce)
+ (addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
+ coreExprToWeakExpr ce >>= fun we =>
+ addErrorMessage ("WeakExpr: " +++ we)
+ ((addErrorMessage ("CoreType of WeakExpr: " +++ coreTypeOfCoreExpr (weakExprToCoreExpr we))
+ ((weakTypeOfWeakExpr we) >>= fun t =>
+ (addErrorMessage ("WeakType: " +++ t)
+ ((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
+ addErrorMessage ("HaskType: " +++ τ)
+ ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
+ (let haskProof := @expr2proof _ _ _ _ _ _ e
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ (unFresh (@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof))
+ >>= fun e' => Error (@toString _ (ExprToString _ _ _ _) (projT2 e'))
+(*
+ >>= fun e' =>
+ Prelude_error (@toString _ (@ExprToString nat _ _ _ _ _ _) (projT2 e'))
+ *)
+)
+)))))))).
+(* Error "X").*)
+(*
+ strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
+ (projT2 e')
+ INil
+ >>= fun q => Error (toString q)
+ ))))))))).
+*)
+*)
+
Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ ce)
(addErrorMessage ("input CoreType: " +++ coreTypeOfCoreExpr ce) (
((weakTypeToTypeOfKind φ t ★) >>= fun τ =>
((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e =>
- (* insert HaskStrong-to-HaskStrong manipulations here *)
- strongExprToWeakExpr hetmet_brak hetmet_esc mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply e INil
- >>= fun q => OK (weakExprToCoreExpr q)
-(*
- OK (weakExprToCoreExpr we)
-*)
- )))))))).
+
+ (addErrorMessage ("HaskStrong...")
+ (let haskProof := @expr2proof _ _ _ _ _ _ e
+ in (* insert HaskProof-to-HaskProof manipulations here *)
+ OK ((@proof2expr nat _ FreshNat _ _ _ _ (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.
End core2proof.
-
+(*Set Extraction Optimize.*)
+(*Set Extraction AutoInline.*)
Extraction "Extraction.hs" coqPassCoreToString coqPassCoreToCore.
projects / coq-hetmet.git / blobdiff