<commit_before>﻿#light "off"
module FStar.TypeChecker.NBE
open FStar.All
open FStar
open FStar.TypeChecker
open FStar.Syntax.Syntax

module S = FStar.Syntax.Syntax
module SS = FStar.Syntax.Subst
module Range = FStar.Range
module U = FStar.Syntax.Util
module P = FStar.Syntax.Print
module BU = FStar.Util

(* Utils *)

let map_rev (f : 'a -> 'b) (l : list<'a>) : list<'b> =
  let rec aux (l:list<'a>) (acc:list<'b>) = //NS: weird, this needs an annotation to type-check in F*; cf issue #
   match l with 
   | [] -> acc 
   | x :: xs -> aux xs (f x :: acc)
   in  aux l []

let debug_term (t : term) =
  BU.print1 "%s\n" (P.term_to_string t)

type var = bv
type sort = int

//IN F*: type atom : Type0 =
type atom = //JUST FSHARP
  | Var of var
  | Sort of sort (* for full CiC -- not used right now *)
  | Prod of t * t (* for full CiC -- not used right now *)
  | Match of list<branch> * (* the original branches -- used for readback initially then I realized it is not needed *)
             t * (* the scutinee *)
             (t -> t) (* the closure that pattern matches the scrutiny *) 
  (* keep original branches for readback -- 
     only used to find the original patterns *)
  | Fix of (t -> t) * 
            t * (**)
            int (* the recursive argument *)
  (* Fix is used to represent fixpoints whose evaluation 
       is stuck because the recursive argument is not a contructor. *)
  (* Zoe: I'm not sure how to use this in our setting since F*'s ast does not
     mark the recursive argument and therefore I'm not sure how to prevent 
     infinite fixpoint unrolling *) 
  | FiX of (t -> t) (* Danel: This is a unary rec. def. that will not be unfolded any more *)
//IN F*: and t : Type0 =
and t = //JUST FSHARP
  | Lam of (t -> t)
  | Accu of atom * list<t>
  (* For simplicity represent constructors with fv as in F* *)
  | Construct of fv * list<t>
  | Unit
  | Bool of bool
  | Rec of term * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
type head = t
type annot = option<t> 

let mkConstruct i ts = Construct(i,ts)

let mkAccuVar (v:var) = Accu(Var v, [])
let mkAccuMatch (b : list<branch>) (s : t) (c : t -> t) = Accu(Match (b, s, c), [])

let rec pickBranch (c : fv) (branches : list<branch>) : term = 
  match branches with
  | [] -> failwith "Branch not found"
  | ({v = Pat_cons (c', args)}, _, e) :: bs when (fv_eq c c') ->
    e
  | b :: bs -> pickBranch c bs

(* XXX unused *)
let rec mkBranches branches cont = 
  match branches with 
  | ({ v = (Pat_cons (fv, pats))}, _, _) :: branches' -> 
    (* a new binder for each argument *)
    let (args, binders) = 
      List.fold_right
        (fun (p : pat * bool) ((args:list<t>), (bs:list<(pat * bool)>)) ->
           let x = S.new_bv None S.tun in 
           (mkAccuVar x :: args, (S.withinfo (Pat_var x) Range.dummyRange, snd p) :: bs)
        ) pats ([], []) in
    let value = Construct (fv, args) in
    let pat = S.withinfo (Pat_cons (fv, binders)) Range.dummyRange  in
    let branch = (pat, None, cont value) in
    branch :: mkBranches branches' cont
  | _ -> failwith "Unexpected pattern" 

(* We are not targeting tagless normalization at this point *)
(* Danel: app is now defined simultaneously with translate to accommodate analysing rec. defs. *)
let rec app (f:t) (x:t) =
  match f with
  | Lam f -> f x
  | Accu (a, ts) -> Accu (a, x::ts)
  | Construct (i, ts) -> Construct (i, x::ts)
  | Rec (y, ts) -> (match x with
                    | Construct (i, ts') -> app (translate (Rec (y, ts)::ts) y) x
                                            (* Danel: if a rec. def. is applied to 
                                               a constructor, then we unfold it *)
                    | _ -> Accu (FiX (fun (z:t) -> translate (z::ts) y),[x]))
                                                   (* Danel: if a rec. def. is applied 
                                                      to a non-constructor, turn it into 
                                                      an accumulator *)
  | Unit
  | Bool _ -> failwith "Ill-typed application"<commit_msg>Replaced constructor check with accumulator check<commit_after>﻿#light "off"
module FStar.TypeChecker.NBE
open FStar.All
open FStar
open FStar.TypeChecker
open FStar.Syntax.Syntax

module S = FStar.Syntax.Syntax
module SS = FStar.Syntax.Subst
module Range = FStar.Range
module U = FStar.Syntax.Util
module P = FStar.Syntax.Print
module BU = FStar.Util

(* Utils *)

let map_rev (f : 'a -> 'b) (l : list<'a>) : list<'b> =
  let rec aux (l:list<'a>) (acc:list<'b>) = //NS: weird, this needs an annotation to type-check in F*; cf issue #
   match l with 
   | [] -> acc 
   | x :: xs -> aux xs (f x :: acc)
   in  aux l []

let debug_term (t : term) =
  BU.print1 "%s\n" (P.term_to_string t)

type var = bv
type sort = int

//IN F*: type atom : Type0 =
type atom = //JUST FSHARP
  | Var of var
  | Sort of sort (* for full CiC -- not used right now *)
  | Prod of t * t (* for full CiC -- not used right now *)
  | Match of list<branch> * (* the original branches -- used for readback initially then I realized it is not needed *)
             t * (* the scutinee *)
             (t -> t) (* the closure that pattern matches the scrutiny *) 
  (* keep original branches for readback -- 
     only used to find the original patterns *)
  | Fix of (t -> t) * 
            t * (**)
            int (* the recursive argument *)
  (* Fix is used to represent fixpoints whose evaluation 
       is stuck because the recursive argument is not a contructor. *)
  (* Zoe: I'm not sure how to use this in our setting since F*'s ast does not
     mark the recursive argument and therefore I'm not sure how to prevent 
     infinite fixpoint unrolling *) 
  | FiX of (t -> t) (* Danel: This is a unary rec. def. that will not be unfolded any more *)
//IN F*: and t : Type0 =
and t = //JUST FSHARP
  | Lam of (t -> t)
  | Accu of atom * list<t>
  (* For simplicity represent constructors with fv as in F* *)
  | Construct of fv * list<t>
  | Unit
  | Bool of bool
  | Rec of term * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
type head = t
type annot = option<t> 

let mkConstruct i ts = Construct(i,ts)

let mkAccuVar (v:var) = Accu(Var v, [])
let mkAccuMatch (b : list<branch>) (s : t) (c : t -> t) = Accu(Match (b, s, c), [])

let rec pickBranch (c : fv) (branches : list<branch>) : term = 
  match branches with
  | [] -> failwith "Branch not found"
  | ({v = Pat_cons (c', args)}, _, e) :: bs when (fv_eq c c') ->
    e
  | b :: bs -> pickBranch c bs

(* XXX unused *)
let rec mkBranches branches cont = 
  match branches with 
  | ({ v = (Pat_cons (fv, pats))}, _, _) :: branches' -> 
    (* a new binder for each argument *)
    let (args, binders) = 
      List.fold_right
        (fun (p : pat * bool) ((args:list<t>), (bs:list<(pat * bool)>)) ->
           let x = S.new_bv None S.tun in 
           (mkAccuVar x :: args, (S.withinfo (Pat_var x) Range.dummyRange, snd p) :: bs)
        ) pats ([], []) in
    let value = Construct (fv, args) in
    let pat = S.withinfo (Pat_cons (fv, binders)) Range.dummyRange  in
    let branch = (pat, None, cont value) in
    branch :: mkBranches branches' cont
  | _ -> failwith "Unexpected pattern" 

(* We are not targeting tagless normalization at this point *)
(* Danel: app is now defined simultaneously with translate to accommodate analysing rec. defs. *)
let rec app (f:t) (x:t) =
  match f with
  | Lam f -> f x
  | Accu (a, ts) -> Accu (a, x::ts)
  | Construct (i, ts) -> Construct (i, x::ts)
  | Rec (y, ts) -> (match x with
                    | Accu _ -> Accu (FiX (fun (z:t) -> translate (z::ts) y),[x]))
                                                   (* Danel: if a rec. def. is applied 
                                                      to an accumulator, do not unfold 
                                                      it further *)
                    | _ -> app (translate (Rec (y, ts)::ts) y) x
                                            (* Danel: if a rec. def. is applied to 
                                               a non-accumulator, then we unfold it *)
  | Unit
  | Bool _ -> failwith "Ill-typed application"
{'fraction_non_alphanumeric': 0.12993661628473915, 'fraction_numerical': 0.0007313505607020966, 'mean_word_length': 2.1114903299203642, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 73, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 22, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3861706', 'n_tokens_mistral': 2689, 'n_tokens_neox': 2597, 'n_words': 1054}