aboutsummaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/extraction/Extraction.v7
-rw-r--r--src/hls/DeadBlocksproof.v2
-rw-r--r--src/hls/HTLgenproof.v2
-rw-r--r--src/hls/HashTree.v4
-rw-r--r--src/hls/PipelineOp.v2
-rw-r--r--src/hls/Sat.v104
6 files changed, 9 insertions, 112 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index aba2fe7..6357531 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -178,7 +178,6 @@ Extraction Blacklist List String Int.
Extract Inlined Constant Defs.F2R => "fun _ -> assert false".
Extract Inlined Constant Binary.FF2R => "fun _ -> assert false".
Extract Inlined Constant Binary.B2R => "fun _ -> assert false".
-Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
(*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*)
@@ -187,7 +186,7 @@ Extract Constant GiblePargen.schedule => "Schedule.schedule_fn".
(* Loop normalization *)
Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
-Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".
+(*Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".*)
(* Needed in Coq 8.4 to avoid problems with Function definitions. *)
Set Extraction AccessOpaque.
@@ -204,7 +203,8 @@ Separate Extraction
Compiler.transf_c_program Compiler.transf_cminor_program
Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
- Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
+ Ctypes.merge_attributes Ctypes.remove_attributes
+ Ctypes.build_composite_env Ctypes.layout_struct
Initializers.transl_init Initializers.constval
Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection
Ctyping.typecheck_program
@@ -216,6 +216,7 @@ Separate Extraction
Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs
Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs
Conventions1.dummy_int_reg Conventions1.dummy_float_reg
+ Conventions1.allocatable_registers
RTL.instr_defs RTL.instr_uses
Machregs.mregs_for_operation Machregs.mregs_for_builtin
Machregs.two_address_op Machregs.is_stack_reg
diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v
index 7f1da9c..107e206 100644
--- a/src/hls/DeadBlocksproof.v
+++ b/src/hls/DeadBlocksproof.v
@@ -544,7 +544,7 @@ Proof.
elim H.
intros.
- elim not_seen_sons_prop6 with (1:=TT) (i0:=i); auto with datatypes.
+ eelim not_seen_sons_prop6 with (1:=TT) (i:=i); auto with datatypes.
rewrite PTree.gsspec; destruct peq; subst; intros; auto with datatypes.
rewrite PTree.gempty in H0; congruence.
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 1089356..4fc00bc 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -140,7 +140,7 @@ Definition match_prog (p: RTL.program) (tp: HTL.program) :=
Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
main_is_internal p = true.
-Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
+#[global] Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2).
Proof.
red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v
index 7387401..a088a54 100644
--- a/src/hls/HashTree.v
+++ b/src/hls/HashTree.v
@@ -498,14 +498,14 @@ Module HashTree(H: Hashable).
forall x, match_one x x.
Proof. unfold match_one; auto. Qed.
- Instance match_one_Reflexive : Reflexive match_one.
+ #[global] Instance match_one_Reflexive : Reflexive match_one.
Proof. unfold Reflexive. auto using match_one_refl. Qed.
Lemma match_one_trans :
forall x y z, match_one x y -> match_one y z -> match_one x z.
Proof. unfold match_one; auto. Qed.
- Instance match_one_Transitive : Transitive match_one.
+ #[global] Instance match_one_Transitive : Transitive match_one.
Proof. unfold Transitive. eauto using match_one_trans. Qed.
Lemma hash_value_gt :
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index 90ccea0..76634a6 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -34,7 +34,7 @@ Require Import vericert.hls.FunctionalUnits.
Require Import vericert.common.Monad.
Module OptionExtra := MonadExtra(Option).
-Import OptionExtra.MonadNotation.
+(*Import OptionExtra.MonadNotation.*)
Local Open Scope positive.
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 3924ce7..b5970da 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -372,110 +372,6 @@ Fixpoint interp_alist (al : alist) : asgn :=
| l :: al' => upd (interp_alist al') l
end.
-(** Here's the final definition!
-
- This implementation isn't #<i>#quite#</i># what you would expect, since it
- takes an extra parameter expressing a search tree depth. Writing the function
- without that parameter would be trickier when it came to proving termination.
- In practice, you can just seed the bound with one plus the number of variables
- in the input, but the function's return type still indicates a possibility for
- a "time-out" by returning [None].
- *)
-Definition boundedSat: forall (bound : nat) (fm : formula),
- option ({al : alist | satFormula fm (interp_alist al)}
- + {forall a, ~satFormula fm a}).
- refine (fix boundedSat (bound : nat) (fm : formula) {struct bound}
- : option ({al : alist | satFormula fm (interp_alist al)}
- + {forall a, ~satFormula fm a}) :=
- match bound with
- | O => None
- | S bound' =>
- if isNil fm
- then Some (inleft _ (exist _ nil _))
- else match unitPropagate fm with
- | Some (inleft (existT _ fm' (exist _ l _))) =>
- match boundedSat bound' fm' with
- | None => None
- | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
- | Some (inright _) => Some (inright _ _)
- end
- | Some (inright _) => Some (inright _ _)
- | None =>
- let l := chooseSplit fm in
- match setFormula fm l with
- | inleft (exist _ fm' _) =>
- match boundedSat bound' fm' with
- | None => None
- | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
- | Some (inright _) =>
- match setFormula fm (negate l) with
- | inleft (exist _ fm' _) =>
- match boundedSat bound' fm' with
- | None => None
- | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
- | Some (inright _) => Some (inright _ _)
- end
- | inright _ => Some (inright _ _)
- end
- end
- | inright _ =>
- match setFormula fm (negate l) with
- | inleft (exist _ fm' _) =>
- match boundedSat bound' fm' with
- | None => None
- | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
- | Some (inright _) => Some (inright _ _)
- end
- | inright _ => Some (inright _ _)
- end
- end
- end
- end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al).
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- assert (satFormula fm (upd a0 l)); firstorder.
- assert (satFormula fm (upd a0 l)); firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- firstorder.
- destruct (satLit_dec l a);
- [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
- destruct (satLit_dec l a);
- [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
- destruct (satLit_dec l a);
- [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
- destruct (satLit_dec l a);
- [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
- destruct (satLit_dec l a); intuition eauto;
- assert (satFormula fm (upd a l)); firstorder.
- destruct (satLit_dec l a); intuition eauto;
- assert (satFormula fm (upd a l)); firstorder.
- firstorder.
- firstorder.
- destruct (satLit_dec l a); intuition eauto;
- assert (satFormula fm (upd a (negate l))); firstorder.
- destruct (satLit_dec l a); intuition eauto;
- assert (satFormula fm (upd a (negate l))); firstorder.
- destruct (satLit_dec l a);
- [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
-Defined.
-
-Definition boundedSatSimple (bound : nat) (fm : formula) :=
- match boundedSat bound fm with
- | None => None
- | Some (inleft (exist _ a _)) => Some (Some a)
- | Some (inright _) => Some None
- end.
-
(*Eval compute in boundedSatSimple 100 nil.
Eval compute in boundedSatSimple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: nil).
generated by cgit (git 2.34.1) at 2024-06-28 15:13:45 +0000