[POC] run Elpi code in lambdapi #418

gares · 2020-06-09T15:39:18Z

do not merge this is a POC to be discussed at a seminar on the 18th

TODO (hopefully for the 18th):

support Terms.Meta in the HOAS encoding using Elpi's unification variables
from Terms.term Conversion.t to (Terms.term,Env.t,_) ContextualConversion.t
bind Typing.infer(_constr) and Eval.eq_modulo

fblanqui · 2020-06-09T18:22:02Z

Ouah. That's great @gares . Thank you for digging into the code of Lambdapi !

gares · 2020-06-10T16:13:01Z

CI seems to be failing because of "sanity_check" but it does not seem to have much to do with my code (locally it prints messages about files I did not touch). Is it expected?

fblanqui · 2020-06-10T16:41:37Z

Yes:

18:39 ~/lambdapi (elpi) make sanity_check
In src/core/ctxt.ml, line 12 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 53 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 95 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 99 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 175 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 259 more than 78 characters...
In src/core/elpi_lambdapi.ml, line 263 more than 78 characters...

Please run tools/git_hook_helper.sh to have the following pre-commit hook:

#!/bin/sh
if [ ! -z "$(make sanity_check)" ]; then
    echo "Sanity check failed."
    exit 1
fi

gares · 2020-06-10T16:44:56Z

I did set it up, but then I could not commit anything. If I run the script locally I get

gares@ollypat:~/work-area/lambdapi$ make sanity_check 
In src/cli/lambdapi.ml, line 30 more than 78 characters...
In src/core/basics.ml, line 30 more than 78 characters...
In src/core/builtin.ml, line 10 more than 78 characters...
... many other files, including mine, ....

here line 30 of src/cli/lambdapi.ml has 79 chars according to my editor.

Anyway, I'll fix my file, I did not spot it in the sea of errors it prints here

fblanqui · 2020-06-10T16:49:45Z

Well, 79>78 indeed ;-) But that's strange we do not get the same files! Do you use gawk? I have GNU Awk 4.1.4. Could you please give the complete result of make sanity_check too?

gares · 2020-06-10T16:53:44Z

Well spotted, I've no idea why my ubuntu has this variant of awk (by default)

gares@ollypat:~/work-area/lambdapi$ dpkg -l | grep awk
ii  mawk                                       1.3.3-17ubuntu3                                  amd64        a pattern scanning and text processing language

I've installed gawk, it now works

gabrielhdt · 2020-06-10T16:55:58Z

It's not the first time it happens, perhaps we should check the awk version with a awk --version | grep GNU or something of the kind...

fblanqui · 2020-06-10T16:57:56Z

Why not simply calling gawk explicitly instead of awk?

fblanqui · 2020-06-10T16:58:41Z

tools/git_hook_helper.sh could also check that gawk exists

fblanqui · 2020-06-10T17:03:02Z

Fixed in f2c363c

fblanqui · 2022-12-12T20:49:38Z

src/parsing/scope.ml

@@ -478,12 +478,28 @@ let scope =
    a type (defaults to [false]). No {b new} metavariables may appear in
    [t], but metavariables in the image of [mok] may be used. The function
    [mok] defaults to the function constant to [None] *)
-let scope_term : ?typ:bool -> ?mok:(int -> meta option) ->
+let scope_term: ?typ:bool -> ?mok:(int -> meta option) ->


You can remove the diff here.

fblanqui · 2022-12-12T20:50:51Z

src/parsing/scope.ml

  bool -> sig_state -> env -> p_term -> term =
  fun ?(typ=false) ?(mok=fun _ -> None) m_term_prv ss env t ->
  let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in
  Bindlib.unbox (scope ~typ 0 md ss env t)

+let scope_term_w_pats: ?typ:bool -> ?mok:(int -> meta option) ->


Missing explanation of the function.

fblanqui · 2022-12-12T20:51:28Z

src/parsing/scope.mli

@@ -18,6 +18,11 @@ val scope_term :
  ?mok:(int -> meta option) ->
  bool -> sig_state -> env -> p_term -> term

+val scope_term_w_pats :


Missing explanation of the function.

- lp.unif branched, but it works only in the empty context - it does not work at all like the one of Coq: x |- ? x x == R x x is post-poned Thus it is quite useless - it requires most symbols in the encoding (e.s. Decode/code/uncode/...) to be defined as injective, even if maybe they are not so Game over in using that?

gares force-pushed the elpi branch 2 times, most recently from c6ef22f to 88bff84 Compare June 11, 2020 08:35

gares force-pushed the elpi branch from 67ec225 to 0dd874b Compare October 18, 2022 14:11

fblanqui reviewed Dec 12, 2022

View reviewed changes

gares added 3 commits January 27, 2023 14:30

[core] generalize context from term |-> type to term |-> 'a

b4d6b43

[opam] depend on Elpi

0c56e85

[elpi] minimalistic integration

32bb531

gares force-pushed the elpi branch from 2796969 to 32bb531 Compare January 27, 2023 13:40

gares and others added 10 commits January 27, 2023 15:34

xxx

c58aef2

Generate lp files with requires automatically

2f8e741

zip everything

dc51dfe

fix

5d965df

all rewriting rules generate typed abstractions

6f28826

print unfinished goals

f7a1559

existing instance in coq/dk/lp

bc1a626

[ctx] unbind option to keep non dependent entries in ctx

be3dba1

keep all ctx entries

8fe5dbe

run elpi tc on all metas

09de08a

gares and others added 12 commits January 28, 2023 12:19

[open] open "tc" modules; to enable only TC from modules

6a62980

example

27f40ce

no more need for filtering out #directives

ffa5809

Use sequential to make Leq-checking more complete with or rules

a805895

fixup open tc

aadb90b

bind some stuff

67e852a

skip non-tc-instantiation problems

483a789

slightly more interesting example

e884094

use coercions to itnroduce cast from Type[1] to Type[2] in test

b597256

Bugs fixed on meta instantiation + second example working

b03c354

added (but commented) dubious injective symbols for lambdapi unification

37c1730

fblanqui mentioned this pull request Aug 1, 2023

Error: «Introduced symbol cannot be removed.» Feature proposal job: primitive structure/record types to pack multiple arguments #1006

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[POC] run Elpi code in lambdapi #418

[POC] run Elpi code in lambdapi #418

gares commented Jun 9, 2020 •

edited

Loading

fblanqui commented Jun 9, 2020

gares commented Jun 10, 2020

fblanqui commented Jun 10, 2020

gares commented Jun 10, 2020 •

edited

Loading

fblanqui commented Jun 10, 2020

gares commented Jun 10, 2020 •

edited

Loading

gabrielhdt commented Jun 10, 2020

fblanqui commented Jun 10, 2020

fblanqui commented Jun 10, 2020

fblanqui commented Jun 10, 2020

fblanqui Dec 12, 2022

fblanqui Dec 12, 2022

fblanqui Dec 12, 2022

[POC] run Elpi code in lambdapi #418

Are you sure you want to change the base?

[POC] run Elpi code in lambdapi #418

Conversation

gares commented Jun 9, 2020 • edited Loading

fblanqui commented Jun 9, 2020

gares commented Jun 10, 2020

fblanqui commented Jun 10, 2020

gares commented Jun 10, 2020 • edited Loading

fblanqui commented Jun 10, 2020

gares commented Jun 10, 2020 • edited Loading

gabrielhdt commented Jun 10, 2020

fblanqui commented Jun 10, 2020

fblanqui commented Jun 10, 2020

fblanqui commented Jun 10, 2020

fblanqui Dec 12, 2022

Choose a reason for hiding this comment

fblanqui Dec 12, 2022

Choose a reason for hiding this comment

fblanqui Dec 12, 2022

Choose a reason for hiding this comment

gares commented Jun 9, 2020 •

edited

Loading

gares commented Jun 10, 2020 •

edited

Loading

gares commented Jun 10, 2020 •

edited

Loading