Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
00e86f25 by Jonathan Graveline at 2018-05-17T00:31:38Z
Use of predefined function `shift`
- - - - -
1 changed file:
- src/elab.ml
Changes:
=====================================
src/elab.ml
=====================================
--- a/src/elab.ml
+++ b/src/elab.ml
@@ -1531,7 +1531,7 @@ let sform_load usr_elctx loc sargs ot =
sxps (Some ";") in
let _, elctx = lexp_p_decls nods elctx
in elctx in
-
+
(* read file as elab_context *)
let ld_elctx = match sargs with
| [String (_,file_name)] -> read_file file_name !_sform_default_ectx
@@ -1548,7 +1548,8 @@ let sform_load usr_elctx loc sargs ot =
(* create a tuple from context and shift it to user context *)
let tuple = OL.ctx2tup dflt_lctx ld_lctx in
- let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(usr_len - dflt_len))) in
+ let tuple' = Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) in
+
(tuple',Lazy)
(* Register special forms. *)
View it on GitLab: https://gitlab.com/monnier/typer/commit/00e86f25ab7fc396f779e5e9aed995deb41…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/00e86f25ab7fc396f779e5e9aed995deb41…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
f0d1072f by Jonathan Graveline at 2018-05-14T22:15:06Z
First draft
- - - - -
1 changed file:
- + samples/myers.typer
Changes:
=====================================
samples/myers.typer
=====================================
--- /dev/null
+++ b/samples/myers.typer
@@ -0,0 +1,183 @@
+%
+% Adaptation of Myers list from ocaml file `myers.ml`
+%
+% since 2018-05-14
+%
+
+Myers : Type -> Type;
+type Myers (a : Type)
+ | mnil
+ | mcons (data : a) (link1 : (Myers a)) (i : Int) (link2 : (Myers a));
+
+% client shouldn't use next two definition
+
+type _MyersPatternHelper (a : Type)
+ | _pat1 (idx : Int) (data : a) (link1 : Myers a) (i : Int) (link2 : Myers a)
+ | _pat2 (idx : Int);
+
+_pattern_helper : (a : Type) ≡> Int -> Myers a -> _MyersPatternHelper a;
+_pattern_helper n l = case l
+ | mnil => _pat2 n
+ | mcons a l1 i l2 => _pat1 n a l1 i l2;
+
+% Contrary to Myers's presentation, we index from the top of the stack,
+% and we don't store the total length but the "skip distance" instead.
+% This makes `cons' slightly faster, and better matches our use for
+% debruijn environments.
+
+Myers_cons : (a : Type) ≡> a -> Myers a -> Myers a;
+Myers_cons x l = case l
+ | mcons _ _ s1 l1 => ( case l1
+ | mcons _ _ s2 l2 => ( case (Int_>= s1 s2)
+ | true => mcons x l (s1 + s2 + 1) l2
+ | false => mcons x l 1 l
+ )
+ | _ => mcons x l 1 l
+ )
+ | _ => mcons x l 1 l;
+
+Myers_car : (a : Type) ≡> Myers a -> Option a;
+Myers_car l = case l
+ | mnil => none
+ | mcons x _ _ _ => some x;
+
+Myers_cdr : (a : Type) ≡> Myers a -> Myers a;
+Myers_cdr l = case l
+ | mnil => mnil
+ | mcons _ l _ _ => l;
+
+Myers_case : (a : Type) ≡> (b : Type) ≡> Myers a -> b -> (a -> Myers a -> b) -> b;
+Myers_case l n c = case l
+ | mnil => n
+ | mcons x l _ _ => c x l;
+
+Myers_empty : (a : Type) ≡> Myers a -> Bool;
+Myers_empty l = case l
+ | mnil => true
+ | _ => false;
+
+Myers_nthcdr : (a : Type) ≡> Int -> Myers a -> Myers a;
+Myers_nthcdr n l = if_then_else_ (Int_eq n 0) l
+ ( case l
+ | mnil => mnil
+ | mcons _ l1 s l2 => ( case (Int_>= n s)
+ | true => Myers_nthcdr (n - s) l2
+ | false => Myers_nthcdr (n - 1) l1
+ )
+ );
+
+Myers_nth : (a : Type) ≡> Int -> Myers a -> Option a;
+Myers_nth n l = Myers_car (Myers_nthcdr n l);
+
+% While `nth` is O(log N), `set_nth` is O(N)! :-(
+
+Myers_set_nth : (a : Type) ≡> Int -> a -> Myers a -> Myers a;
+Myers_set_nth n v l = case (_pattern_helper n l)
+
+ | _pat1 n vp cdr s tail => if_then_else_ (Int_eq n 0)
+ ( mcons v cdr s tail )
+ ( Myers_cons vp (Myers_set_nth (n - 1) v cdr) )
+
+ % We can't set_nth past the end in general because we'd need to
+ % magically fill the intermediate entries with something of the right type.
+ % But we *can* set_nth just past the end.
+
+ | _pat2 n => if_then_else_ (Int_eq n 0)
+ ( mcons v mnil 1 mnil )
+ ( l ); % should throw an error here!
+
+% This operation would be more efficient using Myers's choice of keeping
+% the length (instead of the skip-distance) in each node.
+
+Myers_length : (a : Type) ≡> Myers a -> Int;
+Myers_length l = let
+
+ lengthp : Myers a -> Int -> Int;
+ lengthp l n = case l
+ | mnil => n
+ | mcons _ _ s l => lengthp l (s + n);
+
+in lengthp l 0;
+
+% Find the first element for which the predicate `p' is true.
+% "Binary" search, assuming the list is "sorted" (i.e. all elements after
+% this one also return true).
+
+Myers_find : (a : Type) ≡> (a -> Bool) -> Myers a -> Option a;
+Myers_find p l = let
+
+ find1 : Myers a -> Option a;
+ find2 : Myers a -> Myers a -> Option a;
+
+ find2 l1 l2 = case l2
+ | mcons x l1 _ l2 => ( case (p x)
+ | false => find2 l1 l2
+ | true => find1 l
+ )
+ | _ => find1 l;
+
+ find1 l = case l
+ | mnil => none
+ | mcons x l1 _ l2 => ( case (p x)
+ | true => some x
+ | false => find2 l1 l2
+ );
+
+in find1 l;
+
+% Find the last node for which the predicate `p' is false.
+% "Binary" search, assuming the list is "sorted" (i.e. all elements after
+% this one also return true).
+
+Myers_findcdr : (a : Type) ≡> (a -> Bool) -> Myers a -> Myers a;
+Myers_findcdr p l = let
+
+ maybev : Option (Myers a) -> Myers a;
+ maybev ov = case ov
+ | none => mnil
+ | some l => l;
+
+ findcdr1 : Option (Myers a) -> Myers a -> Myers a;
+ findcdr2 : Option (Myers a) -> Myers a -> Myers a -> Myers a;
+
+ findcdr2 last l1 l2 = case l2
+ | mcons x l1p _ l2p => ( case (p x)
+ | false => findcdr2 (some l2) l1p l2p
+ | true => findcdr1 last l1
+ )
+ | _ => findcdr1 last l1;
+
+ findcdr1 last l = case l
+ | mnil => maybev last
+ | mcons x l1 _ l2 => ( case (p x)
+ | true => maybev last
+ | false => findcdr2 (some l) l1 l2
+ );
+
+in findcdr1 none l;
+
+Myers_fold_left : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> Myers a -> b;
+Myers_fold_left f i l = case l
+ | mnil => i
+ | mcons x l _ _ => Myers_fold_left f (f i x) l;
+
+Myers_fold_right : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> Myers a -> b -> b;
+Myers_fold_right f l i = case l
+ | mnil => i
+ | mcons x l _ _ => f x (Myers_fold_right f l i);
+
+Myers_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> Myers a -> Myers b;
+Myers_map f l = let
+
+ fp : a -> Myers b -> Myers b;
+ fp x lp = Myers_cons (f x) lp;
+
+in Myers_fold_right fp l mnil;
+
+Myers_iteri : (a : Type) ≡> (Int -> a -> Unit) -> Myers a -> Int;
+Myers_iteri f l = let
+
+ fp : (Int -> a -> Int);
+ fp i x = let _ = (f i x); in i + 1;
+
+in Myers_fold_left fp 0 l;
View it on GitLab: https://gitlab.com/monnier/typer/commit/f0d1072fcad40af573207eb09c999ace99b…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/f0d1072fcad40af573207eb09c999ace99b…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
83f93ecc by Jonathan Graveline at 2018-05-14T22:13:28Z
First draft
- - - - -
1 changed file:
- + samples/list.typer
Changes:
=====================================
samples/list.typer
=====================================
--- /dev/null
+++ b/samples/list.typer
@@ -0,0 +1,144 @@
+%
+% Sorted List as a data structure
+%
+% since 2018-05-14
+%
+% (*function prefixed with `s` take sorted list as argument)
+%
+
+% Some more generic first (not only for sorted list)
+
+List_remove : (a : Type) ≡> (a -> Bool) -> List a -> List a;
+List_remove f l = case l
+ | nil => nil
+ | cons x xs => ( case (f x)
+ | true => List_remove f xs
+ | false => cons x (List_remove f xs)
+ );
+
+List_nth : Int -> List ?a -> ?a -> ?a;
+List_nth = lambda n -> lambda xs -> lambda d -> case xs
+ | nil => d
+ | cons x xs
+ => case Int_<= n 0
+ | true => x
+ | false => List_nth (n - 1) xs d;
+
+%% take a function for ordering
+
+List_sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a;
+List_sort o l = let
+
+ sortp : Option a -> List a -> List a -> List a -> List a;
+ sortp p lt gt l = case p
+ | none => nil
+ | some (pp) => ( case l
+ | nil => ( let
+ ltp : List a; ltp = sortp (List_head1 lt) nil nil (List_tail lt);
+ gtp : List a; gtp = sortp (List_head1 gt) nil nil (List_tail gt);
+ in List_concat ltp (cons pp gtp)
+ )
+ | cons x xs => ( case (o x pp)
+ | true => sortp p lt (cons x gt) xs
+ | false => sortp p (cons x lt) gt xs
+ )
+ );
+
+in sortp (List_head1 l) nil nil (List_tail l);
+
+%% Some algo on sorted list
+
+sList_find : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a;
+sList_find o f a l = case l
+ | nil => none
+ | cons x xs => ( case (f x)
+ | true => some x
+ | false => ( case (o x a)
+ | false => sList_find o f a xs
+ | true => none
+ )
+ );
+
+sList_all : (a : Type) ≡> (a -> Bool) -> List a -> List a;
+sList_all f l = case l
+ | nil => nil
+ | cons x xs => ( case (f x)
+ | true => cons x (sList_all f xs)
+ | false => sList_all f xs
+ );
+
+sList_exist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool;
+sList_exist o f a l = case (sList_find o f a l)
+ | none => false
+ | some _ => true;
+
+sList_insert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a;
+sList_insert o a l = case l
+ | nil => cons a l
+ | cons x xs => ( case (o x a)
+ | true => cons a l
+ | false => cons x (sList_insert o a xs)
+ );
+
+sList_up : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a;
+sList_up o a l = case l
+ | nil => nil
+ | cons x xs => ( case (o x a)
+ | true => l
+ | false => sList_up o a xs
+ );
+
+sList_low : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a;
+sList_low o a l = case l
+ | nil => nil
+ | cons x xs => ( case (o x a)
+ | true => nil
+ | false => cons x (sList_low o a xs)
+ );
+
+%
+% Some predef for built-in type
+%
+
+% sorted list for Int
+
+sInt_order : Int -> Int -> Bool;
+sInt_order m n = Int_> m n;
+
+sInt_eq : Int -> Int -> Bool;
+sInt_eq m n = Int_eq m n;
+
+Int_sort = List_sort sInt_order;
+
+sInt_find n = sList_find sInt_order (sInt_eq n);
+
+sInt_exist n = sList_exist sInt_order (sInt_eq n);
+
+sInt_insert n = sList_insert sInt_order n;
+
+sInt_up n = sList_up sInt_order n;
+
+sInt_low n = sList_low sInt_order n;
+
+% sorted list for Float
+
+sFloat_order : Float -> Float -> Bool;
+sFloat_order m n = Float_> m n;
+
+sFloat_eq : Float -> Float -> Bool;
+sFloat_eq m n = Float_eq m n;
+
+Float_sort = List_sort sFloat_order;
+
+sFloat_find n = sList_find sFloat_order (sFloat_eq n);
+
+sFloat_exist n = sList_exist sFloat_order (sFloat_eq n);
+
+sFloat_insert n = sList_insert sFloat_order n;
+
+sFloat_up n = sList_up sFloat_order n;
+
+sFloat_low n = sList_low sFloat_order n;
+
+% test_list : List Float;
+% test_list = cons 9.0 (cons 1.0 (cons 8.0 (cons 2.0 (cons 7.0 (cons 3.0 (cons 6.0 (cons 4.0 (cons 5.0 nil))))))));
View it on GitLab: https://gitlab.com/monnier/typer/commit/83f93ecc58be52d7d1c449326f033fb3558…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/83f93ecc58be52d7d1c449326f033fb3558…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
34d24f66 by Jonathan Graveline at 2018-05-10T15:20:01Z
Correction in 'sform_load' and removed unused '_sform_default_rctx'
- - - - -
1 changed file:
- src/elab.ml
Changes:
=====================================
src/elab.ml
=====================================
--- a/src/elab.ml
+++ b/src/elab.ml
@@ -114,14 +114,11 @@ let get_special_form name =
added before default context's function
WARNING :
With this setup you can't use special form "load_" within
- builtins.typer and pervasive.typer!!!
+ builtins.typer and pervasive.typer!
*)
let _sform_default_ectx = ref empty_elab_context
-let _sform_default_rctx = ref make_runtime_ctx
let _set_default_ectx ectx =
_sform_default_ectx := ectx
-let _set_default_rctx rctx =
- _sform_default_rctx := rctx
(* The prefix `elab_check_` is used for functions which do internal checking
* (i.e. errors signalled here correspond to internal errors rather than
@@ -1519,8 +1516,13 @@ let lexp_print_var_info ctx =
print_string "\n")
done
-(* sform_load current elab_context, loc of load, string argument, output type *)
-let sform_load user_elctx loc sargs ot =
+(* arguments :
+ elab_context from where load is called,
+ loc is location of load call,
+ sargs should be an array of one file name,
+ ot is the expected type of output tuple.
+*)
+let sform_load usr_elctx loc sargs ot =
let read_file file_name elctx =
let pres = prelex_file file_name in
@@ -1529,26 +1531,24 @@ let sform_load user_elctx loc sargs ot =
sxps (Some ";") in
let _, elctx = lexp_p_decls nods elctx
in elctx in
-
- let loaded_elctx = match sargs with
- | [String (_,path); ] -> read_file path !_sform_default_ectx
- | _ -> (error loc "argument to load should be one file path (String)"; !_sform_default_ectx) in
- let (_,(user_len,var_map),user_lctx,_) = user_elctx in
- let (_,(_,_),loaded_lctx,_) = loaded_elctx in
- let (_,(def_len,_),def_lctx,_) = !_sform_default_ectx in
+ (* read file as elab_context *)
+ let ld_elctx = match sargs with
+ | [String (_,file_name)] -> read_file file_name !_sform_default_ectx
+ | _ -> (error loc "argument to load should be one file name (String)"; !_sform_default_ectx) in
+
+ (* get lexp_context *)
+ let usr_lctx = ectx_to_lctx usr_elctx in
+ let ld_lctx = ectx_to_lctx ld_elctx in
+ let dflt_lctx = ectx_to_lctx !_sform_default_ectx in
- let tuple = OL.ctx2tup def_lctx loaded_lctx in
- let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(user_len - def_len))) in
+ (* length of some lexp_context *)
+ let usr_len = M.length usr_lctx in
+ let dflt_len = M.length dflt_lctx in
- (*
- print_string "\nHere's unmodified tuple : \n";
- lexp_print tuple;
- print_string "\nHere's modified tuple : \n";
- lexp_print tuple';
- (*sform_dummy_ret user_elctx loc*)
- (tuple', Lazy)
- *)
+ (* create a tuple from context and shift it to user context *)
+ let tuple = OL.ctx2tup dflt_lctx ld_lctx in
+ let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(usr_len - dflt_len))) in
(tuple',Lazy)
(* Register special forms. *)
@@ -1641,7 +1641,6 @@ let default_ectx
let default_rctx =
let rctx = EV.from_ectx default_ectx in
- let _ = _set_default_rctx rctx in
rctx
(* String Parsing
View it on GitLab: https://gitlab.com/monnier/typer/commit/34d24f66d0bbe6c30a29862da7c576694a8…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/34d24f66d0bbe6c30a29862da7c576694a8…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
fc0bf4fa by Jonathan Graveline at 2018-05-10T15:15:35Z
Removed 'reset_intra_ref'
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -926,63 +926,13 @@ and clean_map cases =
(** Turning a set of declarations into an object. **)
-let shift n lexp = Lexp.mkSusp lexp (S.Shift (S.Identity,n))
-
-(* arguments are : *)
-(* len is the length of the tuple, 'n value' as in nth value of the tuple *)
-let rec reset_intra_ref len n value =
-
- let rec reset_intra_ref' scope value =
-
- let reset' = reset_intra_ref' scope in
- let nscope nv = reset_intra_ref' (scope + nv) in
-
- match value with
-
- (* the real thing is with Var, all other pattern are for sub expression *)
- (* We want to reset variable from inside the tuple so their idx aren't modified *)
- | Var (v,idx) -> if (idx <= len && idx > scope) then Var (v, (idx + n)) else Var (v,idx)
-
- (* now just check sub expression *)
- | Susp (l,s) -> Susp (reset' l,s)
-
- | Let (loc,defs,l) ->
- let reset'' (v,l,t) = (v,reset' l,reset' t) in
- Let (loc, List.map reset'' defs, nscope (List.length defs) l)
-
- | Arrow (k,ov,t,loc,l) -> Arrow (k,ov,reset' t,loc,nscope 1 l)
-
- | Lambda (k,v,t,l) -> Lambda (k,v,reset' t,nscope 1 l)
-
- | Call (l,args) ->
- let reset'' (k,l) = (k,reset' l) in
- Call (nscope (List.length args) l, List.map reset'' args)
-
- | Inductive (loc,label,args,ctors) ->
- let reset'' (k,vo,t) = (k,vo,reset' t) in
- let ctors' = SMap.map (fun ctor -> List.map reset'' ctor) ctors in
- Inductive (loc,label,List.map reset'' args,ctors')
-
- | Cons (l,s) -> Cons (reset' l,s)
-
- | Case (loc,l,t,brc,dflt) ->
- let reset'' (loc2,vs,l2) = (loc2,vs,nscope 1 l2) in
- let brc' = SMap.map reset'' brc in
- let dflt' = match dflt with
- | None -> None
- | Some (vo,l) -> Some (vo,nscope 1 l) in
- Case (loc,reset' l,reset' t,brc',dflt')
-
- | _ -> value
- in reset_intra_ref' 0 value
-
let mktup types vals =
let loc = DB.dloc in
let cons_name = "cons" in
let cons_label = (loc, cons_name) in
let type_label = (loc, "record") in
- let reset' n (k,l) = (k,reset_intra_ref (List.length vals) n l) in
+ let shift n lexp = Lexp.mkSusp lexp (S.Shift (S.Identity,n)) in
Call (Cons (Inductive (loc, type_label, [],
SMap.add cons_name
@@ -991,8 +941,8 @@ let mktup types vals =
types)
SMap.empty),
cons_label),
- List.mapi reset'
- (List.mapi (fun n v -> (P.Aimplicit, shift (- n) v)) vals))
+ (* shift could be done in sform_load but it is easy to put it here *)
+ List.mapi (fun n v -> (P.Aimplicit, shift (- n) v)) vals)
(* does not seem to let previous global declaration be used by next global declaration *)
let ctx2tup ctx nctx =
View it on GitLab: https://gitlab.com/monnier/typer/commit/fc0bf4fa5b30297aeb3f2827792bff011d7…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/fc0bf4fa5b30297aeb3f2827792bff011d7…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
905fc6f0 by Jonathan Graveline at 2018-05-10T01:08:36Z
Modification and use of susp within sform_load
- - - - -
1 changed file:
- src/elab.ml
Changes:
=====================================
src/elab.ml
=====================================
--- a/src/elab.ml
+++ b/src/elab.ml
@@ -50,6 +50,7 @@ open Lexp
open Env
open Debruijn
module DB = Debruijn
+module M = Myers
module EV = Eval
open Grammar
@@ -1518,160 +1519,37 @@ let lexp_print_var_info ctx =
print_string "\n")
done
-(* load a whole file as a string (there may be a limit on string size) *)
-let _load_whole_file file =
- let fin = open_in file in
- let n = in_channel_length fin in
- let rawstr = Bytes.create n in
- really_input fin rawstr 0 n;
- close_in fin;
- (Bytes.to_string rawstr)
-
-let rec init_tup (tup : Lexp.lexp) : Lexp.lexp = init_tup' (0,SMap.empty) tup
-
-and init_tup' (depth, var_map) lexp =
- let redecl _ = Some (depth) in
- let s_ctx = (depth + 1, var_map) in
- let init' = init_tup' (depth,var_map) in
- match lexp with
-
- | Var ((loc, name), _) -> (
- match (SMap.find_opt name var_map) with
- | Some (idx) -> Var ((loc, name), (depth - idx - 1))
- | None -> (error loc ("undefined variable '"^name^"'"); Var ((loc,name),0))
- )
-
- | Metavar (_, subst, (loc, name)) -> (
- match (SMap.find_opt name var_map) with
- | Some (idx) -> Metavar ((depth - idx - 1),subst, (loc,name))
- | None -> (error loc ("undefined variable '"^name^"'"); Metavar (0,subst,(loc,name)))
- )
-
- | Susp (e, s) -> Susp ((init' e), s)
-
- | Let (loc, decls, body) ->
- let f ((d,vmap),lexps) ((loc,name),l,t) =
- let vmap' = (SMap.update name redecl vmap) in
- (d+1,vmap'), ((loc,name),(init_tup' (d,vmap') l),(init_tup' (d,vmap') t)) :: lexps in
- let (senv',decls') = List.fold_left f ((depth,var_map),[]) decls in
- Let (loc, (List.rev decls'), (init_tup' senv' body))
-
- | Arrow(k, v, tp, loc2, expr) -> (
- match v with
- | Some (loc,name) ->
- let vmap' = (SMap.update name redecl var_map) in
- Arrow (k, v, (init_tup' (depth,vmap') tp), loc2, (init_tup' (depth + 1,vmap') expr))
- | None -> Arrow(k,v,(init_tup' (depth,var_map) tp),loc2,(init_tup' (depth + 1,var_map) expr))
- )
-
- | Lambda(k, (loc, name), ltype, lbody) ->
- let vmap' = (SMap.update name redecl var_map) in
- Lambda (k, (loc, name), (init_tup' (depth,vmap') ltype), (init_tup' (depth+1,vmap')lbody))
-
- | Cons(t, (l,v)) ->
- let vmap' = (SMap.update v redecl var_map) in
- Cons ((init_tup' (depth,vmap') t), (l,v))
-
- | Call(a, args) ->
- let f ((depth,vmap),lexps) (k,l) =
- (depth+1,vmap), (k,(init_tup' (depth,vmap) l)) :: lexps in
- let (senv',args') = List.fold_left f ((depth,var_map),[]) args in
- Call ((init' a),(List.rev args'))
-
- | Inductive (a, (b, name), args, ctors) ->
- let vmap'' = (SMap.update name redecl var_map) in
- (* args *)
- let f1 ((depth,vmap),lexps) (k,(l,v),t) =
- let vmap' = (SMap.update v redecl vmap) in
- (depth+1,vmap'), (k,(l,v),(init_tup' (depth,vmap) t)) :: lexps in
- (* ctors sub list fold function *)
- let f2 ((depth,vmap),lexps) (k,v,t) =
- (depth+1,vmap), (k,v,(init_tup' (depth,vmap) t)) :: lexps in
- (* ctors map fold function *)
- let f3 key ll ((depth,vmap),lexps) =
- let vmap' = (SMap.update key redecl vmap) in
- let ((depth,vmap''),ll') = List.fold_left f2 ((depth,vmap'),[]) ll in
- (depth+1,vmap''), (key,(List.rev ll')) :: lexps in
- (* list key*a to map when called with fold *)
- let f4 ctors_map (key,ll) = (SMap.add key ll ctors_map) in
- (* calling all fold function *)
- let (senv',args') = List.fold_left f1 ((depth,vmap''),[]) args in
- let (senv'',ctors_list) = SMap.fold f3 ctors (senv',[]) in
- let ctors' = List.fold_left f4 SMap.empty (List.rev ctors_list) in
- Inductive (a,(b,name),(List.rev args'),ctors')
-
- | Case (a, target, ret, map, dflt) ->
- let mf (loc,k,l) = (loc,k,(init' l)) in
- let map' = SMap.map mf map in (
- match dflt with
- | None -> Case (a, (init' target), (init' ret), map', None)
- | Some (v, df) -> Case (a, target, ret, map', Some (v, (init' df)))
- )
- (* not handling Builtin... is it needed? *)
- (* sounds like not builtin anymore if redefined *)
- | Sort (a, Stype l) -> Sort (a, Stype (init' l))
- | SortLevel (SLsucc e) -> SortLevel (SLsucc (init' e))
- | SortLevel (SLlub (e1, e2)) -> SortLevel (SLlub ((init' e1), (init' e2)))
- | _ -> (lexp_print lexp; lexp)
-
(* sform_load current elab_context, loc of load, string argument, output type *)
-let sform_load ctx loc sargs ot =
-
- (* COPY PASTE *) (* see end of file for origin *)
- let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) =
- let sdecls = _sexp_parse_str str tenv grm limit in
- lexp_p_decls sdecls ctx in
-
- let lexp_decl_str str ctx =
- _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx in
-
- let eval_decl_str str lctx rctx =
- let lxps, lctx = lexp_decl_str str lctx in
- let elxps = (List.map OL.clean_decls lxps) in
- (EV.eval_decls_toplevel elxps rctx), lctx in
- (* END OF COPY PASTE *)
-
- (* get the whole file as string *)
- let fstr = match sargs with
- | [String (_,file_str)] -> _load_whole_file file_str
- | _ -> "load_error" in
-
- (* get all runtime_env and elab_context *)
- let rctx, elctx = eval_decl_str fstr !_sform_default_ectx !_sform_default_rctx in
-
- (* Things we want : new elab_context, tuple, new grammar, DB.senv_type ... *)
-
- let lctx = DB.ectx_to_lctx !_sform_default_ectx in
- let nlctx = DB.ectx_to_lctx elctx in
- let modtup = OL.ctx2tup lctx nlctx in
+let sform_load user_elctx loc sargs ot =
+
+ let read_file file_name elctx =
+ let pres = prelex_file file_name in
+ let sxps = lex default_stt pres in
+ let nods = sexp_parse_all_to_list (ectx_get_grammar elctx)
+ sxps (Some ";") in
+ let _, elctx = lexp_p_decls nods elctx
+ in elctx in
- let grm = DB.ectx_get_grammar elctx in
- let mergefun (str: SMap.key) (a: 't option) (b: 't option) =
- match a, b with
- | (Some aa, None) -> Some aa
- | (None, Some bb) -> Some bb
- (* Keep the grammar created by the load call *)
- | (Some aa, Some bb) -> Some aa
- | (None, None) -> None in
- let grm' = SMap.merge mergefun grm (ectx_get_grammar ctx) in
-
- (* need to append tuple to lexp_ctx' and modify senv_type *)
- (* ??? assuming meta_scope isn't changed, just adding a tuple in the current scope ??? *)
- let (g,d,l,m) = ctx in
-
- let modtup' = init_tup' d modtup in
+ let loaded_elctx = match sargs with
+ | [String (_,path); ] -> read_file path !_sform_default_ectx
+ | _ -> (error loc "argument to load should be one file path (String)"; !_sform_default_ectx) in
+
+ let (_,(user_len,var_map),user_lctx,_) = user_elctx in
+ let (_,(_,_),loaded_lctx,_) = loaded_elctx in
+ let (_,(def_len,_),def_lctx,_) = !_sform_default_ectx in
- (* lets get a base for DeBruijn index *)
- (*let tup_setype = *)
+ let tuple = OL.ctx2tup def_lctx loaded_lctx in
+ let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(user_len - def_len))) in
- (*sform_dummy_ret modtup loc*)
- (
- print_string "\nhere's unmodified tuple : \n\n";
- lexp_print modtup;
- print_string "\n\nhere's modified tuple : \n\n";
- lexp_print modtup';
- sform_dummy_ret (grm',d,l,m) loc
- )
+ (*
+ print_string "\nHere's unmodified tuple : \n";
+ lexp_print tuple;
+ print_string "\nHere's modified tuple : \n";
+ lexp_print tuple';
+ (*sform_dummy_ret user_elctx loc*)
+ (tuple', Lazy)
+ *)
+ (tuple',Lazy)
(* Register special forms. *)
let register_special_forms () =
View it on GitLab: https://gitlab.com/monnier/typer/commit/905fc6f078077666c408459718b161e7ad4…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/905fc6f078077666c408459718b161e7ad4…
You're receiving this email because of your account on gitlab.com.
Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
5aa903a9 by Jonathan Graveline at 2018-05-10T01:12:36Z
Modification of mktup and new function used in mktup
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -926,11 +926,64 @@ and clean_map cases =
(** Turning a set of declarations into an object. **)
+let shift n lexp = Lexp.mkSusp lexp (S.Shift (S.Identity,n))
+
+(* arguments are : *)
+(* len is the length of the tuple, 'n value' as in nth value of the tuple *)
+let rec reset_intra_ref len n value =
+
+ let rec reset_intra_ref' scope value =
+
+ let reset' = reset_intra_ref' scope in
+ let nscope nv = reset_intra_ref' (scope + nv) in
+
+ match value with
+
+ (* the real thing is with Var, all other pattern are for sub expression *)
+ (* We want to reset variable from inside the tuple so their idx aren't modified *)
+ | Var (v,idx) -> if (idx <= len && idx > scope) then Var (v, (idx + n)) else Var (v,idx)
+
+ (* now just check sub expression *)
+ | Susp (l,s) -> Susp (reset' l,s)
+
+ | Let (loc,defs,l) ->
+ let reset'' (v,l,t) = (v,reset' l,reset' t) in
+ Let (loc, List.map reset'' defs, nscope (List.length defs) l)
+
+ | Arrow (k,ov,t,loc,l) -> Arrow (k,ov,reset' t,loc,nscope 1 l)
+
+ | Lambda (k,v,t,l) -> Lambda (k,v,reset' t,nscope 1 l)
+
+ | Call (l,args) ->
+ let reset'' (k,l) = (k,reset' l) in
+ Call (nscope (List.length args) l, List.map reset'' args)
+
+ | Inductive (loc,label,args,ctors) ->
+ let reset'' (k,vo,t) = (k,vo,reset' t) in
+ let ctors' = SMap.map (fun ctor -> List.map reset'' ctor) ctors in
+ Inductive (loc,label,List.map reset'' args,ctors')
+
+ | Cons (l,s) -> Cons (reset' l,s)
+
+ | Case (loc,l,t,brc,dflt) ->
+ let reset'' (loc2,vs,l2) = (loc2,vs,nscope 1 l2) in
+ let brc' = SMap.map reset'' brc in
+ let dflt' = match dflt with
+ | None -> None
+ | Some (vo,l) -> Some (vo,nscope 1 l) in
+ Case (loc,reset' l,reset' t,brc',dflt')
+
+ | _ -> value
+ in reset_intra_ref' 0 value
+
let mktup types vals =
let loc = DB.dloc in
let cons_name = "cons" in
let cons_label = (loc, cons_name) in
let type_label = (loc, "record") in
+
+ let reset' n (k,l) = (k,reset_intra_ref (List.length vals) n l) in
+
Call (Cons (Inductive (loc, type_label, [],
SMap.add cons_name
(List.map (fun (oname, t)
@@ -938,8 +991,10 @@ let mktup types vals =
types)
SMap.empty),
cons_label),
- List.map (fun v -> (P.Aimplicit, v)) vals)
+ List.mapi reset'
+ (List.mapi (fun n v -> (P.Aimplicit, shift (- n) v)) vals))
+(* does not seem to let previous global declaration be used by next global declaration *)
let ctx2tup ctx nctx =
assert (M.length nctx >= M.length ctx
&& ctx == M.nthcdr (M.length nctx - M.length ctx) nctx);
View it on GitLab: https://gitlab.com/monnier/typer/commit/5aa903a940ea1793a50ed3ba26633eb99b0…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/5aa903a940ea1793a50ed3ba26633eb99b0…
You're receiving this email because of your account on gitlab.com.