Skip to content

Commit

Permalink
Cleanup + add DV module in gen files
Browse files Browse the repository at this point in the history
  • Loading branch information
hanxic committed Jul 13, 2023
1 parent 65ab2b4 commit 6783d73
Showing 1 changed file with 13 additions and 11 deletions.
24 changes: 13 additions & 11 deletions src/fix-extraction.sh
Original file line number Diff line number Diff line change
Expand Up @@ -67,24 +67,28 @@ done

for f in "${GENMLIFILES[@]}"
do
sed -i "1s/^/open DynamicValues\n/" $EXTRACT_DIR/$f
sed -i "1s/^/open EitherMonad\n/" $EXTRACT_DIR/$f
sed -i "/module Int/,/end/d" $EXTRACT_DIR/$f
sed -i "/module Int1/,/end/d" $EXTRACT_DIR/$f
sed -i "/module Int8/,/end/d" $EXTRACT_DIR/$f
sed -i "/module Int32/,/end/d" $EXTRACT_DIR/$f
sed -i "/module Coq_Int64/,/end/d" $EXTRACT_DIR/$f
sed -i "/type \(\w\+\) = \1$/d" $EXTRACT_DIR/$f
replace "s/Int.int/int/g" $f
replace "s/Int1.int/int/g" $f
replace "s/Int8.int/int/g" $f
replace "s/Int32.int/int/g" $f
replace "s/Coq_Int64.int/int/g" $f
replace "s/Int64.int/int/g" $f
replace "s/Int1.int/DynamicValues.int1/g" $f
replace "s/Int8.int/DynamicValues.int8/g" $f
replace "s/Int32.int/DynamicValues.int32/g" $f
replace "s/Coq_Int64.int/DynamicValues.int64/g" $f
replace "s/Int64.int/DynamicValues.int64/g" $f
sed -i "/val succ : int -> int/d" $EXTRACT_DIR/$f
replace "s/coq_VMemintptr/coq_VMemInt_intptr/g" $f
done

for f in "${GENFILES[@]}"
do
sed -i "1s/^/open DynamicValues\n/" $EXTRACT_DIR/$f
sed -i "1s/^/open EitherMonad\n/" $EXTRACT_DIR/$f
replace "s/Pervasives.succ/succ/g" $f
replace "s/Pervasives.max/max/g" $f
replace "s/Pervasives.pred/pred/g" $f
Expand All @@ -94,12 +98,10 @@ do
replace "s/Coq_Z.max/max/g" $f
replace "s/Coq_Z.min/min/g" $f
replace "s/Coq_Z.pred/pred/g" $f
replace "s/Int1.int/int/g" $f
replace "s/Int8.int/int/g" $f
replace "s/Int32.int/int/g" $f
replace "s/Coq_Int64.int/int/g" $f
sed -i "1s/^/open EitherMonad\n/" $EXTRACT_DIR/$f
# replace "s/Coq_Pos.succ/succ/g" $f
replace "s/Int1.int/DynamicValues.int1/g" $f
replace "s/Int8.int/DynamicValues.int8/g" $f
replace "s/Int32.int/DynamicValues.int32/g" $f
replace "s/Coq_Int64.int/DynamicValues.int64/g" $f
done

# This feels risky. These two are very similar, and only differ because of some newlines in the extraction...
Expand Down

0 comments on commit 6783d73

Please sign in to comment.