<commit_before>#light "off"
module FStar.Reflection.Basic

open FStar
open FStar.All
open FStar.Reflection.Data
open FStar.Syntax.Syntax
open FStar.Order
open FStar.Errors

module S = FStar.Syntax.Syntax // TODO: remove, it's open

module C = FStar.Const
module PC = FStar.Parser.Const
module SS = FStar.Syntax.Subst
module BU = FStar.Util
module Range = FStar.Range
module U = FStar.Syntax.Util
module UF = FStar.Syntax.Unionfind
module Print = FStar.Syntax.Print
module Ident = FStar.Ident
module Env = FStar.TypeChecker.Env
module Err = FStar.Errors
module Z = FStar.BigInt

open FStar.Dyn

(* This file provides implementation for reflection primitives in F*.
 *
 * Users can be exposed to (mostly) raw syntax of terms when working in
 * a metaprogramming effect (such as TAC). These effects are irrelevant
 * for runtime and cannot, of course, be used for proof (where syntax
 * inspection would be completely inconsistent
 *)

 (*
  * Most of this file is tedious and repetitive.
  * We should really allow for some metaprogramming in F*. Oh wait....
  *)

let env_hook = BU.mk_ref None

(* private *)
let inspect_aqual (aq : aqual) : aqualv =
    match aq with
    | Some (Implicit _) -> Data.Q_Implicit
    | Some (Meta t) -> Data.Q_Meta t
    | Some Equality
    | None -> Data.Q_Explicit

(* private *)
let pack_aqual (aqv : aqualv) : aqual =
    match aqv with
    | Data.Q_Explicit -> None
    | Data.Q_Implicit -> Some (Implicit false)
    | Data.Q_Meta t   -> Some (Meta t)

let inspect_fv (fv:fv) : list<string> =
    Ident.path_of_lid (lid_of_fv fv)

let pack_fv (ns:list<string>) : fv =
    let lid = PC.p2l ns in
    let attr =
        if Ident.lid_equals lid PC.cons_lid then Some Data_ctor else
        if Ident.lid_equals lid PC.nil_lid  then Some Data_ctor else
        if Ident.lid_equals lid PC.some_lid then Some Data_ctor else
        if Ident.lid_equals lid PC.none_lid then Some Data_ctor else
        None
    in
    // FIXME: Get a proper delta depth
    lid_as_fv (PC.p2l ns) (Delta_constant_at_level 999) attr

// TODO: move to library?
let rec last (l:list<'a>) : 'a =
    match l with
    | [] -> failwith "last: empty list"<commit_msg>reflection: getting proper fv qualifiers<commit_after>#light "off"
module FStar.Reflection.Basic

open FStar
open FStar.All
open FStar.Reflection.Data
open FStar.Syntax.Syntax
open FStar.Order
open FStar.Errors

module S = FStar.Syntax.Syntax // TODO: remove, it's open

module C = FStar.Const
module PC = FStar.Parser.Const
module SS = FStar.Syntax.Subst
module BU = FStar.Util
module Range = FStar.Range
module U = FStar.Syntax.Util
module UF = FStar.Syntax.Unionfind
module Print = FStar.Syntax.Print
module Ident = FStar.Ident
module Env = FStar.TypeChecker.Env
module Err = FStar.Errors
module Z = FStar.BigInt
module DsEnv = FStar.Syntax.DsEnv

open FStar.Dyn

(* This file provides implementation for reflection primitives in F*.
 *
 * Users can be exposed to (mostly) raw syntax of terms when working in
 * a metaprogramming effect (such as TAC). These effects are irrelevant
 * for runtime and cannot, of course, be used for proof (where syntax
 * inspection would be completely inconsistent
 *)

 (*
  * Most of this file is tedious and repetitive.
  * We should really allow for some metaprogramming in F*. Oh wait....
  *)

let env_hook = BU.mk_ref None

(* private *)
let inspect_aqual (aq : aqual) : aqualv =
    match aq with
    | Some (Implicit _) -> Data.Q_Implicit
    | Some (Meta t) -> Data.Q_Meta t
    | Some Equality
    | None -> Data.Q_Explicit

(* private *)
let pack_aqual (aqv : aqualv) : aqual =
    match aqv with
    | Data.Q_Explicit -> None
    | Data.Q_Implicit -> Some (Implicit false)
    | Data.Q_Meta t   -> Some (Meta t)

let inspect_fv (fv:fv) : list<string> =
    Ident.path_of_lid (lid_of_fv fv)

let pack_fv (ns:list<string>) : fv =
    let lid = PC.p2l ns in
    let fallback () =
        let quals =
            if Ident.lid_equals lid PC.cons_lid then Some Data_ctor else
            if Ident.lid_equals lid PC.nil_lid  then Some Data_ctor else
            if Ident.lid_equals lid PC.some_lid then Some Data_ctor else
            if Ident.lid_equals lid PC.none_lid then Some Data_ctor else
            None
        in
        // FIXME: Get a proper delta depth
        lid_as_fv (PC.p2l ns) (Delta_constant_at_level 999) quals
    in
    match !env_hook with
    | None -> fallback ()
    | Some env ->
     let qninfo = Env.lookup_qname env lid in
     match qninfo with
     | Some (BU.Inr (se, _us), _rng) ->
         let quals = DsEnv.fv_qual_of_se se in
         // FIXME: Get a proper delta depth
         lid_as_fv (PC.p2l ns) (Delta_constant_at_level 999) quals
     | _ ->
         fallback ()

// TODO: move to library?
let rec last (l:list<'a>) : 'a =
    match l with
    | [] -> failwith "last: empty list"
{'fraction_non_alphanumeric': 0.08993177589414926, 'fraction_numerical': 0.002894356005788712, 'mean_word_length': 2.923763179237632, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 27, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, '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': '6875396', 'n_tokens_mistral': 1653, 'n_tokens_neox': 1614, 'n_words': 558}