<commit_before>﻿// Learn more about F# at http://fsharp.net
// See the 'F# Tutorial' project for more help.
#light "off"
module Microsoft.FStar.Backends.ML.ExtractTyp
open Prims
open Microsoft.FStar.Absyn
open Microsoft.FStar.Backends.ML.Syntax
open Microsoft.FStar.Util
open Microsoft.FStar.Tc.Env
open Microsoft.FStar.Absyn.Syntax
open Microsoft.FStar
open Microsoft.FStar.Tc.Normalize
open Microsoft.FStar.Absyn.Print
open Microsoft.FStar.Backends.ML.Env

let binderIsExp (bn:binder): bool = is_inr (fst bn)

let rec argsIsExp (k:knd') (typeName : string) : list<bool> =
match k with
| Kind_type -> []
| Kind_arrow (bs,r) -> List.append (List.map binderIsExp bs) (argsIsExp r.n typeName)
| Kind_delayed (k, _ ,_) -> failwith "extraction.numIndices : expected a compressed argument"
| _ -> failwith ("unexpected signature of inductive type" ^ typeName) 

let  numIndices (k:knd') (typeName : string) : int = List.length (argsIsExp k typeName)

let mlty_of_isExp (b:bool) : mlty =
    if b then erasedContent else unknownType


(*copied from ocaml-strtrans.fs*)
let prependTick (x,n) = if Util.starts_with x "'" then (x,n) else ("'"^x,n)

let translate_eff g l = 
    if lid_equals l Const.effect_PURE_lid 
    then MayErase 
    else Keep

(*generates inp_1 -> inp_2 -> ... inp_n -> out *)
let rec curry (inp: (list<mlty>)) (out: mlty) =
  match inp with
  | [] -> out
  | h::tl -> MLTY_Fun (h, Keep, curry tl out) //TODO: Fix the e_tag

(*
  Below, "the thesis" refers to:
  <NAME>. “Programmation Fonctionnelle Certifiée – L’extraction de Programmes Dans L’assistant Coq.” Université Paris-Sud, 2004.
  http://www.pps.univ-paris-diderot.fr/~letouzey/download/these_letouzey_English.ps.gz
*)

(*\box type in the thesis, to be used to denote the result of erasure of logical (computationally irrelevant) content.
  The actual definiton is a bit complicated, because we need for any x, \box x to be convertible to \box.
*)


let convRange (r:Range.range) : int = 0 (*FIX!!*)
let convIdent (id:ident) : mlident = (id.idText ,(convRange id.idRange))
    
type argTransform = arg -> Tot<option<arg>> (*none indicates that this argument should be deleted*)
type nthArgTransform = int -> Tot<argTransform> (* f n is the argtransform for the nth argument (of a type constant)*)
let idArgTransform :argTransform = fun a -> Some a
type nthArgTransforms = lident (*name of a constant*) -> Tot<nthArgTransform>
 

type context = env

(*
let tyVarKind (bv : bvvar) : knd = {n=Kind_type; tk=None; pos= bv.p; fvs =None; uvs = None}
let bvvar2btvar (bv : bvvar) : btvar = {v=bv.v; sort = Kind_type ; p=bv.p} *)


(* vars in tyVars will have type Type, irrespective of that types they had in F*. This is to match the limitations of  OCaml*)


let btvar2mlident (btv: btvar) : mlident =  (prependTick (convIdent btv.v.ppname)) 


let extendContextWithRepAsTyVar (b : either<btvar,bvvar> * either<btvar,bvvar>) (c:context): context = 
match b with
| (Inl bt, Inl btr) -> 
           //printfn "mapping from %A\n" btr.v.realname;
           //printfn "to %A\n" bt.v.realname;
   extend_ty c btr (Some ((MLTY_Var (btvar2mlident bt))))
| (Inr bv, Inr _ ) -> extend_bv c bv ([], erasedContent)
| _ -> failwith "Impossible case"


let extendContextWithRepAsTyVars (b : list< (either<btvar,bvvar> * either<btvar,bvvar>) > ) (c:context): context = 
   List.fold_right (extendContextWithRepAsTyVar) b c (*TODO: is the fold in the right direction? check *)

let extendContextAsTyvar (availableInML : bool) (b : either<btvar,bvvar>) (c:context): context = 
match b with
| (Inl bt) -> extend_ty c bt (Some (if availableInML then (MLTY_Var (btvar2mlident bt)) else unknownType))
//if availableInML then (extend_ty c bt (Some ( (MLTY_Var (btvar2mlident bt))))) else (extend_hidden_ty c bt unknownType)
| (Inr bv) -> extend_bv c bv ([], erasedContent)

let extendContext (c:context) (tyVars : list<either<btvar,bvvar>>) : context = 
   List.fold_right (extendContextAsTyvar true) (tyVars) c (*TODO: is the fold in the right direction? check *)


let deltaUnfold (i : lident) (c: context) : (option<typ>) = None (*TODO: FIX!!*)

(*The thesis defines a type scheme as "something that becomes a type when enough arguments (possibly none?) are applied to it" ,  e.g. vector, list.
    I guess in F*, these include Inductive types and type abbreviations.
    Formal definition is @ Definition 8, Sec. 1.2.3
      *)
let isTypeScheme (i : lident) (c: context) : bool = true  (*TODO: FIX!! *)


let lident2mlpath (l:lident) : mlpath =
  ( (* List.map (fun x -> x.idText) l.ns *) [], l.ident.idText)



let extractTyVar (c:context) (btv : btvar) = (lookup_ty c (Inl btv))

(* (if (contains c btv) then MLTY_Var (btvar2mlident btv) else unknownType) *)


let rec extractType' (c:context) (ft:typ') : mlty = 
(*the \hat{\epsilon} function in the thesis (Sec. 3.3.5) *)
(* First \beta, \iota and \zeta reduce ft. Do require the caller to do so.
    Since F* does not have SN, one has to be more careful for the termination argument.
    Because OCaml does not support computations in Type, unknownType is supposed to be used if they are really unaviodable.
    The classic example is the type : T b \def if b then nat else bool. If we dont compute, T true will extract to unknownType.
    Why not \delta? I guess the reason is that unfolding definitions will make the resultant OCaml code less readable.
    However in the Typ_app case,  \delta reduction is done as the second-last resort, just before giving up and returing unknownType;
        a bloated type is atleast as good as unknownType?
    An an F* specific example, unless we unfold Mem x pre post to StState x wp wlp, we have no idea that it should be translated to x
*)
match ft with // assume ft is compressed. is there a compresser for typ'?
  | Typ_btvar btv -> extractTyVar c btv
  (*it is not clear whether description in the thesis covers type applications with 0 args. However, this case is needed to translate types like nnat, and so far seems to work as expected*)
  | Typ_const ftv ->  extractTyConstApp c ftv []
  | Typ_fun (bs, codomain) -> 
        let (bts, newC) = extractBindersTypes c bs in
        (let codomainML = (extractComp  newC codomain) in 
        if  (codomainML = erasedContent) 
        then erasedContent (*perhaps this is not needed*)
        else  (curry bts codomainML))

  | Typ_refine (bv (*var and unrefined type*) , _ (*refinement condition*)) -> extractTyp c bv.sort

  (*can this be a partial type application? , i.e can the result of this application be something like Type -> Type, or nat -> Type? : Yes *)
  (* should we try to apply additional arguments here? if not, where? FIX!! *)
  | Typ_app (ty, arrgs) ->
    (match (Util.compress_typ ty).n with
        | Typ_btvar btv ->  extractTyVar c btv
            (*the args are thrown away, because in OCaml, type variables have type Type and not something like -> .. -> .. Type *)
        | Typ_const ftv -> extractTyConstApp c ftv arrgs            
        | Typ_app (tyin, argsin) -> extractType' c (Typ_app (tyin,(List.append argsin arrgs)))
        | _ -> unknownType)

  | Typ_lam  _ -> unknownType
  | Typ_ascribed _  -> unknownType
  | Typ_meta _ -> unknownType
  | Typ_uvar _ -> unknownType
  | Typ_delayed _  -> failwith "expected the argument to be compressed"
  |   _ -> unknownType
and getTypeFromArg (c:context) (a:arg) : mlty =
match (fst a) with
| Inl ty -> extractTyp c ty
| Inr _ -> erasedContent 
and extractTyConstApp (c:context) (ftv:ftvar) (ags : args) =
            match  (isTypeScheme ftv.v c)  with
             | true -> 
                 let mlargs = List.map (getTypeFromArg c) ags in
                 let k = ftv.sort in
                 let ar =  argsIsExp k.n ftv.v.str in
                 //assert (List.length ar >= List.length mlargs);
                 let (_, missingArgs) = Util.first_N (List.length mlargs) ar in
                 let argCompletion =  List.map mlty_of_isExp missingArgs in
                    (MLTY_Named (List.append mlargs argCompletion,(lident2mlpath ftv.v)))
             | false -> 
                 (match  (deltaUnfold ftv.v c) with
                 | Some tyu ->  extractTyp c tyu
                 | None -> unknownType
                 )

(* Return the new context, where this binder IS in scope. Because we wish to call the F* normalizer, the context should always be up-to-date*)
and extractBinderType  (c:context) (bn : binder): mlty * context = 
match bn with
| (Inl btv,_) -> (extractKind c (btv.sort), (extendContextAsTyvar false (Inl btv) c))
| (Inr bvv,_) -> (extractTyp c (bvv.sort), (extendContextAsTyvar false (Inr bvv) c))

and extractBindersTypes  (c:context) (bs : list<binder>): list<mlty> * context =
    (fun (x,c) -> (List.rev x,c)) (List.fold_left (fun (lt,cp) b -> let (nt, nc)= extractBinderType cp b in ((nt::lt),nc))  ([],c) bs)

and extractTyp  (c:context) (ft:typ) : mlty = extractType' c (Util.compress_typ ft).n
and extractKind (c:context) (ft:knd) : mlty = erasedContent
and extractComp  (c:context) (ft:comp) : mlty = extractComp' c (ft.n) 
and extractComp'  (c:context) (ft:comp') : mlty =
match  ft with
  | Total ty -> extractTyp c ty
  | Comp cm -> extractTyp c (cm.result_typ)<commit_msg>integrated translation of effects.<commit_after>﻿// Learn more about F# at http://fsharp.net
// See the 'F# Tutorial' project for more help.
#light "off"
module Microsoft.FStar.Backends.ML.ExtractTyp
open Prims
open Microsoft.FStar.Absyn
open Microsoft.FStar.Backends.ML.Syntax
open Microsoft.FStar.Util
open Microsoft.FStar.Tc.Env
open Microsoft.FStar.Absyn.Syntax
open Microsoft.FStar
open Microsoft.FStar.Tc.Normalize
open Microsoft.FStar.Absyn.Print
open Microsoft.FStar.Backends.ML.Env

let binderIsExp (bn:binder): bool = is_inr (fst bn)

let rec argsIsExp (k:knd') (typeName : string) : list<bool> =
match k with
| Kind_type -> []
| Kind_arrow (bs,r) -> List.append (List.map binderIsExp bs) (argsIsExp r.n typeName)
| Kind_delayed (k, _ ,_) -> failwith "extraction.numIndices : expected a compressed argument"
| _ -> failwith ("unexpected signature of inductive type" ^ typeName) 

let  numIndices (k:knd') (typeName : string) : int = List.length (argsIsExp k typeName)

let mlty_of_isExp (b:bool) : mlty =
    if b then erasedContent else unknownType


(*copied from ocaml-strtrans.fs*)
let prependTick (x,n) = if Util.starts_with x "'" then (x,n) else ("'"^x,n)

let translate_eff g l : e_tag = 
    if lid_equals l Const.effect_PURE_lid //TODO : what about effect abbreviations?
    then MayErase 
    else Keep

(*generates inp_1 -> inp_2 -> ... inp_n -> out *)
let rec curry (inp: (list<mlty>)) (erase : e_tag) (out: mlty) =
  match inp with
  | [] -> out
  | h::tl -> MLTY_Fun (h, erase, curry tl erase out) //TODO: Fix the e_tag

(*
  Below, "the thesis" refers to:
  <NAME>. “Programmation Fonctionnelle Certifiée – L’extraction de Programmes Dans L’assistant Coq.” Université Paris-Sud, 2004.
  http://www.pps.univ-paris-diderot.fr/~letouzey/download/these_letouzey_English.ps.gz
*)

(*\box type in the thesis, to be used to denote the result of erasure of logical (computationally irrelevant) content.
  The actual definiton is a bit complicated, because we need for any x, \box x to be convertible to \box.
*)


let convRange (r:Range.range) : int = 0 (*FIX!!*)
let convIdent (id:ident) : mlident = (id.idText ,(convRange id.idRange))
    
type argTransform = arg -> Tot<option<arg>> (*none indicates that this argument should be deleted*)
type nthArgTransform = int -> Tot<argTransform> (* f n is the argtransform for the nth argument (of a type constant)*)
let idArgTransform :argTransform = fun a -> Some a
type nthArgTransforms = lident (*name of a constant*) -> Tot<nthArgTransform>
 

type context = env

(*
let tyVarKind (bv : bvvar) : knd = {n=Kind_type; tk=None; pos= bv.p; fvs =None; uvs = None}
let bvvar2btvar (bv : bvvar) : btvar = {v=bv.v; sort = Kind_type ; p=bv.p} *)


(* vars in tyVars will have type Type, irrespective of that types they had in F*. This is to match the limitations of  OCaml*)


let btvar2mlident (btv: btvar) : mlident =  (prependTick (convIdent btv.v.ppname)) 


let extendContextWithRepAsTyVar (b : either<btvar,bvvar> * either<btvar,bvvar>) (c:context): context = 
match b with
| (Inl bt, Inl btr) -> 
           //printfn "mapping from %A\n" btr.v.realname;
           //printfn "to %A\n" bt.v.realname;
   extend_ty c btr (Some ((MLTY_Var (btvar2mlident bt))))
| (Inr bv, Inr _ ) -> extend_bv c bv ([], erasedContent)
| _ -> failwith "Impossible case"


let extendContextWithRepAsTyVars (b : list< (either<btvar,bvvar> * either<btvar,bvvar>) > ) (c:context): context = 
   List.fold_right (extendContextWithRepAsTyVar) b c (*TODO: is the fold in the right direction? check *)

let extendContextAsTyvar (availableInML : bool) (b : either<btvar,bvvar>) (c:context): context = 
match b with
| (Inl bt) -> extend_ty c bt (Some (if availableInML then (MLTY_Var (btvar2mlident bt)) else unknownType))
//if availableInML then (extend_ty c bt (Some ( (MLTY_Var (btvar2mlident bt))))) else (extend_hidden_ty c bt unknownType)
| (Inr bv) -> extend_bv c bv ([], erasedContent)

let extendContext (c:context) (tyVars : list<either<btvar,bvvar>>) : context = 
   List.fold_right (extendContextAsTyvar true) (tyVars) c (*TODO: is the fold in the right direction? check *)


let deltaUnfold (i : lident) (c: context) : (option<typ>) = None (*TODO: FIX!!*)

(*The thesis defines a type scheme as "something that becomes a type when enough arguments (possibly none?) are applied to it" ,  e.g. vector, list.
    I guess in F*, these include Inductive types and type abbreviations.
    Formal definition is @ Definition 8, Sec. 1.2.3
      *)
let isTypeScheme (i : lident) (c: context) : bool = true  (*TODO: FIX!! *)


let lident2mlpath (l:lident) : mlpath =
  ( (* List.map (fun x -> x.idText) l.ns *) [], l.ident.idText)



let extractTyVar (c:context) (btv : btvar) = (lookup_ty c (Inl btv))

(* (if (contains c btv) then MLTY_Var (btvar2mlident btv) else unknownType) *)


let rec extractType' (c:context) (ft:typ') : mlty = 
(*the \hat{\epsilon} function in the thesis (Sec. 3.3.5) *)
(* First \beta, \iota and \zeta reduce ft. Do require the caller to do so.
    Since F* does not have SN, one has to be more careful for the termination argument.
    Because OCaml does not support computations in Type, unknownType is supposed to be used if they are really unaviodable.
    The classic example is the type : T b \def if b then nat else bool. If we dont compute, T true will extract to unknownType.
    Why not \delta? I guess the reason is that unfolding definitions will make the resultant OCaml code less readable.
    However in the Typ_app case,  \delta reduction is done as the second-last resort, just before giving up and returing unknownType;
        a bloated type is atleast as good as unknownType?
    An an F* specific example, unless we unfold Mem x pre post to StState x wp wlp, we have no idea that it should be translated to x
*)
match ft with // assume ft is compressed. is there a compresser for typ'?
  | Typ_btvar btv -> extractTyVar c btv
  (*it is not clear whether description in the thesis covers type applications with 0 args. However, this case is needed to translate types like nnat, and so far seems to work as expected*)
  | Typ_const ftv ->  extractTyConstApp c ftv []
  | Typ_fun (bs, codomain) -> 
        let (bts, newC) = extractBindersTypes c bs in
        (let codomainML, erase = (extractComp  newC codomain) in 
        if  (codomainML = erasedContent) 
        then erasedContent (*perhaps this is not needed, or should be done in a later phase*)
        else  (curry bts erase codomainML))

  | Typ_refine (bv (*var and unrefined type*) , _ (*refinement condition*)) -> extractTyp c bv.sort

  (*can this be a partial type application? , i.e can the result of this application be something like Type -> Type, or nat -> Type? : Yes *)
  (* should we try to apply additional arguments here? if not, where? FIX!! *)
  | Typ_app (ty, arrgs) ->
    (match (Util.compress_typ ty).n with
        | Typ_btvar btv ->  extractTyVar c btv
            (*the args are thrown away, because in OCaml, type variables have type Type and not something like -> .. -> .. Type *)
        | Typ_const ftv -> extractTyConstApp c ftv arrgs            
        | Typ_app (tyin, argsin) -> extractType' c (Typ_app (tyin,(List.append argsin arrgs)))
        | _ -> unknownType)

  | Typ_lam  _ -> unknownType
  | Typ_ascribed _  -> unknownType
  | Typ_meta _ -> unknownType
  | Typ_uvar _ -> unknownType
  | Typ_delayed _  -> failwith "expected the argument to be compressed"
  |   _ -> unknownType
and getTypeFromArg (c:context) (a:arg) : mlty =
match (fst a) with
| Inl ty -> extractTyp c ty
| Inr _ -> erasedContent 
and extractTyConstApp (c:context) (ftv:ftvar) (ags : args) =
            match  (isTypeScheme ftv.v c)  with
             | true -> 
                 let mlargs = List.map (getTypeFromArg c) ags in
                 let k = ftv.sort in
                 let ar =  argsIsExp k.n ftv.v.str in
                 //assert (List.length ar >= List.length mlargs);
                 let (_, missingArgs) = Util.first_N (List.length mlargs) ar in
                 let argCompletion =  List.map mlty_of_isExp missingArgs in
                    (MLTY_Named (List.append mlargs argCompletion,(lident2mlpath ftv.v)))
             | false -> 
                 (match  (deltaUnfold ftv.v c) with
                 | Some tyu ->  extractTyp c tyu
                 | None -> unknownType
                 )

(* Return the new context, where this binder IS in scope. Because we wish to call the F* normalizer, the context should always be up-to-date*)
and extractBinderType  (c:context) (bn : binder): mlty * context = 
match bn with
| (Inl btv,_) -> (extractKind c (btv.sort), (extendContextAsTyvar false (Inl btv) c))
| (Inr bvv,_) -> (extractTyp c (bvv.sort), (extendContextAsTyvar false (Inr bvv) c))

and extractBindersTypes  (c:context) (bs : list<binder>): list<mlty> * context =
    (fun (x,c) -> (List.rev x,c)) (List.fold_left (fun (lt,cp) b -> let (nt, nc)= extractBinderType cp b in ((nt::lt),nc))  ([],c) bs)

and extractTyp  (c:context) (ft:typ) : mlty = extractType' c (Util.compress_typ ft).n
and extractKind (c:context) (ft:knd) : mlty = erasedContent
and extractComp  (c:context) (ft:comp) : mlty * e_tag = extractComp' c (ft.n) 
and extractComp'  (c:context) (ft:comp') : mlty * e_tag =
match  ft with
  | Total ty -> (extractTyp c ty, MayErase)
  | Comp cm -> (extractTyp c (cm.result_typ), translate_eff c cm.effect_name )
{'fraction_non_alphanumeric': 0.11492769983336021, 'fraction_numerical': 0.0024727194538515292, 'mean_word_length': 3.3467289719626168, 'pattern_counts': {'":': 0, '<': 39, '<?xml version=': 0, '>': 141, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1174674', 'n_tokens_mistral': 6309, 'n_tokens_neox': 6120, 'n_words': 2233}