FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Moving FStar->FStarC #237

Closed mtzguido closed 1 month ago

mtzguido commented 1 month ago

Fixes for F* PR https://github.com/FStarLang/FStar/pull/3557. This scripts gets us most of the way to this PR:

#!/bin/bash

s () {
    # Update fstar files
    L=$1
    R=$2
    M=$3
    find . \( -name '*.fst'  -o -name '*.fsti' \) -exec sed -i "s/\<${L}\.${M}/${R}.${M}/g" {} \+
    # Update OCaml files
    MM=${M//./_}
    find . \( -name '*.ml'   -o -name '*.mly'  \) -exec sed -i "s/\<${L}_${MM}/${R}_${MM}/g" {} \+
}

r () {
    s FStar FStarC "$1"
}

l () {
    s FStarC FStar "$1"
}

r BaseTypes
r Common
r Compiler
r Const
r Dyn
r Errors
r Extraction
r GenSym
r Ident
r Options
r Parser
r Pprint
r Reflection_Types
r Sedlexing
r Syntax
r ToSyntax
r TypeChecker

r Class
l Classical # :^)
l Class_Printable

r Tactics_Result
r Tactics_V1_Builtins
r Tactics_V2_Builtins
r Tactics_V1_Basic
r Tactics_V2_Basic
r Tactics_Types
r Tactics_Native
r Reflection_V1_Builtins
r Reflection_V2_Builtins
r Reflection_V1_Data
r Reflection_V2_Data

sed -i 's/FStar_Parser/FStarC_Parser/g' src/Makefile