<commit_before>﻿(*
   Copyright 2008-2015 <NAME>, <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"
module FStar.Extraction.ML.UEnv
open FStar.ST
open FStar.All
open FStar
open FStar.Util
open FStar.Ident
open FStar.Extraction.ML.Syntax
open FStar.Syntax
open FStar.Syntax.Syntax
open FStar.TypeChecker

module U  = FStar.Syntax.Util
module BU = FStar.Util
module Const = FStar.Parser.Const

// JP: my understanding of this is: we either bind a type (left injection) or a
// term variable (right injection). In the latter case, the variable may need to
// be coerced, hence the [mlexpr] (instead of the [mlident]). In order to avoid
// shadowing (which may occur, as the F* normalization potentially breaks the
// original lexical structure of the F* term), we ALSO keep the [mlsymbol], but
// only for the purpose of resolving name collisions.
// The boolean tells whether this is a recursive binding or not.
type ty_binding = {
    ty_b_name: mlident;
    ty_b_ty: mlty
}

type exp_binding = {
    exp_b_name: mlident;
    exp_b_expr: mlexpr;
    exp_b_tscheme: mltyscheme;
    exp_b_inst_ok: bool
}

type ty_or_exp_b = either<ty_binding, exp_binding>

type binding =
    | Bv  of bv * ty_or_exp_b
    | Fv  of fv * exp_binding

type tydef = {
    tydef_fv:fv;
    tydef_mlmodule_name:list<mlsymbol>;
    tydef_name:mlsymbol;
    tydef_mangled_name:option<mlsymbol>;
    tydef_def:mltyscheme
}

type uenv = {
    env_tcenv: TypeChecker.Env.env;
    env_bindings:list<binding>;
    tydefs:list<tydef>;
    type_names:list<fv>;
    currentModule: mlpath // needed to properly translate the definitions in the current file
}

let debug g f =
    let c = string_of_mlpath g.currentModule in
    if Options.debug_at_level c (Options.Other "Extraction")
    then f ()

// TODO delete
let mkFvvar (l: lident) (t:typ) : fv = lid_as_fv l delta_constant None

(* MLTY_Tuple [] extracts to (), and is an alternate choice.
    However, it represets both the unit type and the unit value. Ocaml gets confused sometimes*)
let erasedContent : mlty = MLTY_Erased

let erasableTypeNoDelta (t:mlty) =
    if t = ml_unit_ty then true
    else match t with
        | MLTY_Named (_, (["FStar"; "Ghost"], "erased")) -> true
        (* erase tactic terms, unless extracting for tactic compilation *)
        | MLTY_Named (_, (["FStar"; "Tactics"; "Effect"], "tactic")) -> Options.codegen () <> Some Options.Plugin
        | _ -> false // this function is used by another function which does delta unfolding

(* \mathbb{T} type in the thesis, to be used when OCaml is not expressive enough for the source type *)
let unknownType : mlty =  MLTY_Top

(*copied from ocaml-strtrans.fs*)
let prependTick x = if BU.starts_with x "'" then x else "'A"^x ///the addition of the space is intentional; it's apparently valid syntax of tvars
let removeTick x = if BU.starts_with x "'" then BU.substring_from x 1 else x

let convRange (r:Range.range) : int = 0 (*FIX!!*)
let convIdent (id:ident) : mlident = id.idText

(* TODO : need to make sure that the result of this name change does not collide with a variable already in the context. That might cause a change in semantics.
   E.g. , consider the following in F*
   let mkPair (a:Type) ('a:Type) (ta : a) (ta' : a') = (ta, ta')

   Perhaps this function also needs to look at env.Gamma*)

(* TODO : if there is a single quote in the name of the type variable, the
 * additional tick in the beginning causes issues with the lexer/parser of OCaml
 * (syntax error).
  Perhaps the type variable is interpreted as a string literal.  For an example,
  see
  https://github.com/FStarLang/FStar/blob/f53844512c76bd67b21b4cf68d774393391eac75/lib/FStar.Heap.fst#L49

   Coq seems to add a space after the tick in such cases. Always adding a space for now
  *)

let bv_as_ml_tyvar x = prependTick (bv_as_mlident x)
let bv_as_ml_termvar x =  removeTick (bv_as_mlident x)

let rec lookup_ty_local (gamma:list<binding>) (b:bv) : mlty =
    match gamma with
        | (Bv (b', Inl ty_b)) :: tl -> if (bv_eq b b') then ty_b.ty_b_ty else lookup_ty_local tl b
        | (Bv (b', Inr _)) :: tl -> if (bv_eq b b') then failwith ("Type/Expr clash: "^(b.ppname.idText)) else lookup_ty_local tl b
        | _::tl -> lookup_ty_local tl b
        | [] -> failwith ("extraction: unbound type var "^(b.ppname.idText))

let tyscheme_of_td (_, _, _, vars, _, body_opt) : option<mltyscheme> =
    match body_opt with
    | Some (MLTD_Abbrev t) -> Some (vars, t)
    | _ -> None

//TODO: this two-level search is pretty inefficient: we should optimize it
let lookup_ty_const (env:uenv) ((module_name, ty_name):mlpath) : option<mltyscheme> =
    BU.find_map env.tydefs  (fun tydef ->
        if module_name = tydef.tydef_mlmodule_name
        && ty_name = tydef.tydef_name
        then Some tydef.tydef_def
        else None)

let module_name_of_fv fv = fv.fv_name.v.ns |> List.map (fun (i:ident) -> i.idText)

let maybe_mangle_type_projector (env:uenv) (fv:fv) : option<mlpath> =
    let mname = module_name_of_fv fv in
    let ty_name = fv.fv_name.v.ident.idText in
    BU.find_map env.tydefs  (fun tydef ->
        if tydef.tydef_mlmodule_name = mname
        && tydef.tydef_name = ty_name
        then match tydef.tydef_mangled_name with
             | None -> Some (mname, ty_name)
             | Some mangled -> Some (mname, mangled)
        else None)

let lookup_tyvar (g:uenv) (bt:bv) : mlty = lookup_ty_local g.env_bindings bt

let lookup_fv_by_lid (g:uenv) (lid:lident) : ty_or_exp_b =
    let x = BU.find_map g.env_bindings (function
        | Fv (fv', x) when fv_eq_lid fv' lid -> Some x
        | _ -> None) in
    match x with<commit_msg>Tweak the equality test shortcut order for lookup_ty_const and maybe_mangle_type_projector in Extraction.Ml.UEnv<commit_after>﻿(*
   Copyright 2008-2015 <NAME>, <NAME> and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
#light "off"
module FStar.Extraction.ML.UEnv
open FStar.ST
open FStar.All
open FStar
open FStar.Util
open FStar.Ident
open FStar.Extraction.ML.Syntax
open FStar.Syntax
open FStar.Syntax.Syntax
open FStar.TypeChecker

module U  = FStar.Syntax.Util
module BU = FStar.Util
module Const = FStar.Parser.Const

// JP: my understanding of this is: we either bind a type (left injection) or a
// term variable (right injection). In the latter case, the variable may need to
// be coerced, hence the [mlexpr] (instead of the [mlident]). In order to avoid
// shadowing (which may occur, as the F* normalization potentially breaks the
// original lexical structure of the F* term), we ALSO keep the [mlsymbol], but
// only for the purpose of resolving name collisions.
// The boolean tells whether this is a recursive binding or not.
type ty_binding = {
    ty_b_name: mlident;
    ty_b_ty: mlty
}

type exp_binding = {
    exp_b_name: mlident;
    exp_b_expr: mlexpr;
    exp_b_tscheme: mltyscheme;
    exp_b_inst_ok: bool
}

type ty_or_exp_b = either<ty_binding, exp_binding>

type binding =
    | Bv  of bv * ty_or_exp_b
    | Fv  of fv * exp_binding

type tydef = {
    tydef_fv:fv;
    tydef_mlmodule_name:list<mlsymbol>;
    tydef_name:mlsymbol;
    tydef_mangled_name:option<mlsymbol>;
    tydef_def:mltyscheme
}

type uenv = {
    env_tcenv: TypeChecker.Env.env;
    env_bindings:list<binding>;
    tydefs:list<tydef>;
    type_names:list<fv>;
    currentModule: mlpath // needed to properly translate the definitions in the current file
}

let debug g f =
    let c = string_of_mlpath g.currentModule in
    if Options.debug_at_level c (Options.Other "Extraction")
    then f ()

// TODO delete
let mkFvvar (l: lident) (t:typ) : fv = lid_as_fv l delta_constant None

(* MLTY_Tuple [] extracts to (), and is an alternate choice.
    However, it represets both the unit type and the unit value. Ocaml gets confused sometimes*)
let erasedContent : mlty = MLTY_Erased

let erasableTypeNoDelta (t:mlty) =
    if t = ml_unit_ty then true
    else match t with
        | MLTY_Named (_, (["FStar"; "Ghost"], "erased")) -> true
        (* erase tactic terms, unless extracting for tactic compilation *)
        | MLTY_Named (_, (["FStar"; "Tactics"; "Effect"], "tactic")) -> Options.codegen () <> Some Options.Plugin
        | _ -> false // this function is used by another function which does delta unfolding

(* \mathbb{T} type in the thesis, to be used when OCaml is not expressive enough for the source type *)
let unknownType : mlty =  MLTY_Top

(*copied from ocaml-strtrans.fs*)
let prependTick x = if BU.starts_with x "'" then x else "'A"^x ///the addition of the space is intentional; it's apparently valid syntax of tvars
let removeTick x = if BU.starts_with x "'" then BU.substring_from x 1 else x

let convRange (r:Range.range) : int = 0 (*FIX!!*)
let convIdent (id:ident) : mlident = id.idText

(* TODO : need to make sure that the result of this name change does not collide with a variable already in the context. That might cause a change in semantics.
   E.g. , consider the following in F*
   let mkPair (a:Type) ('a:Type) (ta : a) (ta' : a') = (ta, ta')

   Perhaps this function also needs to look at env.Gamma*)

(* TODO : if there is a single quote in the name of the type variable, the
 * additional tick in the beginning causes issues with the lexer/parser of OCaml
 * (syntax error).
  Perhaps the type variable is interpreted as a string literal.  For an example,
  see
  https://github.com/FStarLang/FStar/blob/f53844512c76bd67b21b4cf68d774393391eac75/lib/FStar.Heap.fst#L49

   Coq seems to add a space after the tick in such cases. Always adding a space for now
  *)

let bv_as_ml_tyvar x = prependTick (bv_as_mlident x)
let bv_as_ml_termvar x =  removeTick (bv_as_mlident x)

let rec lookup_ty_local (gamma:list<binding>) (b:bv) : mlty =
    match gamma with
        | (Bv (b', Inl ty_b)) :: tl -> if (bv_eq b b') then ty_b.ty_b_ty else lookup_ty_local tl b
        | (Bv (b', Inr _)) :: tl -> if (bv_eq b b') then failwith ("Type/Expr clash: "^(b.ppname.idText)) else lookup_ty_local tl b
        | _::tl -> lookup_ty_local tl b
        | [] -> failwith ("extraction: unbound type var "^(b.ppname.idText))

let tyscheme_of_td (_, _, _, vars, _, body_opt) : option<mltyscheme> =
    match body_opt with
    | Some (MLTD_Abbrev t) -> Some (vars, t)
    | _ -> None

//TODO: this two-level search is pretty inefficient: we should optimize it
let lookup_ty_const (env:uenv) ((module_name, ty_name):mlpath) : option<mltyscheme> =
    BU.find_map env.tydefs  (fun tydef ->
        if ty_name = tydef.tydef_name
        && module_name = tydef.tydef_mlmodule_name
        then Some tydef.tydef_def
        else None)

let module_name_of_fv fv = fv.fv_name.v.ns |> List.map (fun (i:ident) -> i.idText)

let maybe_mangle_type_projector (env:uenv) (fv:fv) : option<mlpath> =
    let mname = module_name_of_fv fv in
    let ty_name = fv.fv_name.v.ident.idText in
    BU.find_map env.tydefs  (fun tydef ->
        if tydef.tydef_name = ty_name
        && tydef.tydef_mlmodule_name = mname
        then match tydef.tydef_mangled_name with
             | None -> Some (mname, ty_name)
             | Some mangled -> Some (mname, mangled)
        else None)

let lookup_tyvar (g:uenv) (bt:bv) : mlty = lookup_ty_local g.env_bindings bt

let lookup_fv_by_lid (g:uenv) (lid:lident) : ty_or_exp_b =
    let x = BU.find_map g.env_bindings (function
        | Fv (fv', x) when fv_eq_lid fv' lid -> Some x
        | _ -> None) in
    match x with
{'fraction_non_alphanumeric': 0.095360205144643, 'fraction_numerical': 0.007051847103133264, 'mean_word_length': 3.403669724770642, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 63, 'https://': 2, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4429768', 'n_tokens_mistral': 4340, 'n_tokens_neox': 4171, 'n_words': 1472}