From ba61ed50e7b2fdc78690de92d734a3747029f903 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Wed, 8 Jun 2022 12:32:14 +0200 Subject: read globals from LLBC JSON into functions --- src/Pure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index 5834b87f..05f78e35 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -1,5 +1,6 @@ open Identifiers open Names +open FunIdentifier module T = Types module V = Values module E = Expressions @@ -10,7 +11,6 @@ module RegionGroupId = T.RegionGroupId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId -module FunDeclId = A.FunDeclId module SynthPhaseId = IdGen () (** We give an identifier to every phase of the synthesis (forward, backward -- cgit v1.2.3 From 414769e0c9a1d370d3ab906b710e2e8adfe25e5e Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 13 Jun 2022 17:10:43 +0200 Subject: crude generation working - missing unit tests & special constants handling --- src/Pure.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index 05f78e35..256a872a 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -305,6 +305,7 @@ type qualif_id = | Func of fun_id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) + (* TODO | Global of GlobalDeclId.id*) [@@deriving show] type qualif = { id : qualif_id; type_args : ty list } [@@deriving show] -- cgit v1.2.3 From 7703c4ca86a390303d0a120f8811c8fd704c5168 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Tue, 21 Jun 2022 11:41:09 +0200 Subject: concrete & symbolic evaluation work with new LLBC format --- src/Pure.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index 256a872a..42f56fed 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -1,6 +1,5 @@ open Identifiers open Names -open FunIdentifier module T = Types module V = Values module E = Expressions @@ -567,7 +566,7 @@ type fun_body = { } type fun_decl = { - def_id : FunDeclId.id; + def_id : A.FunDeclId.id; back_id : T.RegionGroupId.id option; basename : fun_name; (** The "base" name of the function. -- cgit v1.2.3 From 47691de8fe3dc32a29663d4d8343eb415ce1d81e Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Thu, 30 Jun 2022 12:22:14 +0200 Subject: Traduct globals body separately (WIP) --- src/Pure.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index 42f56fed..b3be2040 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -302,9 +302,9 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] type qualif_id = | Func of fun_id + | Global of A.GlobalDeclId.id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) - (* TODO | Global of GlobalDeclId.id*) [@@deriving show] type qualif = { id : qualif_id; type_args : ty list } [@@deriving show] @@ -575,5 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; + is_global : bool; body : fun_body option; } -- cgit v1.2.3 From f9b324be57708e9496ca6e9ac0b7e68ffd9e7108 Mon Sep 17 00:00:00 2001 From: Sidney Congard Date: Mon, 18 Jul 2022 16:27:00 +0200 Subject: Address much stuff of the PR, throw exceptions at remaining places --- src/Pure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index b3be2040..5244b0bc 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -575,6 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; - is_global : bool; + is_global_body : bool; body : fun_body option; } -- cgit v1.2.3 From c8ccd864e1fa6de3241d9dba184cf8ee4101e421 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 17:52:27 +0200 Subject: Make minor cleanup --- src/Pure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index 5244b0bc..ced56c6a 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -575,6 +575,6 @@ type fun_decl = { (to identify the forward/backward functions) later. *) signature : fun_sig; - is_global_body : bool; + is_global_decl_body : bool; body : fun_body option; } -- cgit v1.2.3 From e1b9c968752946e36aeaed1f01272f8481b1a6f1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 22 Sep 2022 18:40:08 +0200 Subject: Make minor cleanup --- src/Pure.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'src/Pure.ml') diff --git a/src/Pure.ml b/src/Pure.ml index ced56c6a..afda2caa 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -10,6 +10,8 @@ module RegionGroupId = T.RegionGroupId module VariantId = T.VariantId module FieldId = T.FieldId module SymbolicValueId = V.SymbolicValueId +module FunDeclId = A.FunDeclId +module GlobalDeclId = A.GlobalDeclId module SynthPhaseId = IdGen () (** We give an identifier to every phase of the synthesis (forward, backward @@ -302,7 +304,7 @@ type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show] type qualif_id = | Func of fun_id - | Global of A.GlobalDeclId.id + | Global of GlobalDeclId.id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) [@@deriving show] @@ -566,7 +568,7 @@ type fun_body = { } type fun_decl = { - def_id : A.FunDeclId.id; + def_id : FunDeclId.id; back_id : T.RegionGroupId.id option; basename : fun_name; (** The "base" name of the function. -- cgit v1.2.3